Changes between Version 57 and Version 58 of SafeHaskell


Ignore:
Timestamp:
Sep 9, 2011 6:33:28 PM (3 years ago)
Author:
dterei
Comment:

update for -XPackageTrust and safe inference

Legend:

Unmodified
Added
Removed
Modified
  • SafeHaskell

    v57 v58  
    22 
    33This is a proposal for a Haskell extension through which people can safely execute untrusted Haskell code, much the way web browsers currently run untrusted Java and !JavaScript, or the way the Spin and Singularity operating systems ran untrusted Modula-3 and C#/Sing#. 
     4 
    45 
    56== Outline == 
     
    89 * See this [wiki:SafeHaskell/BasePackage page] the safety status of the '''Base package'''. 
    910 * See this [wiki:SafeHaskell/SafeCompilation page] for the '''Safe Compilation''' extension. 
     11 
    1012 
    1113== Setup == 
     
    5254    `impdecl -> `import` [`safe`] [`qualified`] modid [`as` modid] [impspec]` 
    5355 
    54 When enabled, a module imported with the safe keyword must be a trusted module, otherwise a compilation error will result. Safe imports can be enabled by themselves but are automatically enabled as part of the safe language dialect where all imports are considered safe imports. Safe imports are enabled through either `-XSafe`, `-XTrustworthy`or `-XSafeImports`. 
     56When enabled, a module imported with the safe keyword must be a trusted module, otherwise a compilation error will result. Safe imports can be enabled by themselves but are automatically enabled as part of the safe language dialect where all imports are considered safe imports. Safe imports are enabled through either `-XSafe`, `-XTrustworthy`, `-XUnsafe` or `-XSafeImports`. 
    5557 
    5658 
    5759== Trust == 
    5860 
    59 The !SafeHaskell project will introduce two new GHC LANGUAGE options. Intuitively: 
     61The !SafeHaskell project will introduce three new GHC LANGUAGE options. Intuitively: 
    6062  * `-XSafe`: enables the Safe Language dialect of Haskell in which GHC rejects any module that might produce unsafe effects or otherwise subvert the type system. 
    6163  * `-XTrustworthy`: means that, though a module may invoke unsafe functions internally, the module's author claims that the exported API cannot be used in an unsafe way. 
     64  * `-XUnsafe`: means that GHC should always regard this module as untrusted. This is needed as without any flags GHC will try to infer safety. 
    6265 
    6366A '''client''' (C) is someone compiling a source module with GHC. 
     
    6770  * Under `-XSafe`, all M's imports must be trusted by C (defined below), or the module will be rejected 
    6871  * Under `-XTrustworthy` all M's `safe` imports must be trusted by C, or the module will be rejected 
    69  
    70 A '''package P is trusted by a client C''' iff one of these conditions holds 
    71   * C's package database records that P is trusted (and command-line arguments do not override the database) 
    72   * C's command-line flags say to trust it regardless of the database (see -trust, -distrust below) 
    73  
    74 It is up to C to decide what packages to trust; it is not a property of P. 
     72  * Under `-XUnsafe` all M's `safe` imports must be trusted by C, or the module will be rejected 
    7573 
    7674A '''module M from package P is trusted by a client C''' iff 
     
    7876    * The module was compiled with `-XSafe` 
    7977    * All of M's direct imports are trusted by C 
    80   * OR all of these hold: 
     78  * OR both of these hold: 
     79    * The module was compiled with `-XTrustworthy` 
     80    * All of M's direct safe imports are trusted by C 
     81 
     82When required we will differentiate between `-XSafe` and `-XTrustworthy` using '''safe''' and '''trustworthy''' respectively. 
     83 
     84The above definition of trust has an issue though. Any module can be compiled with `-XTrustworthy` and it will be trusted regardless of what it does. To control this there is an additional definition of '''package trust''' (enabled with the `-XPackageTrust` flag). The point of package trusts is to require that the client C explicitly say which packages are allowed to contain trustworthy modules. That is, C establishes that it trusts a package P and its author and so trust the modules in P that use `-XTrustworthy`. When package trust is enabled, any modules that are considered trustworthy but reside in a package that isn't trusted are '''not''' considered trusted. In a more formal definition we have: 
     85 
     86A '''package P is trusted by a client C''' iff one of these conditions holds 
     87  * C's package database records that P is trusted (and command-line arguments do not override the database) 
     88  * C's command-line flags say to trust it regardless of the database (see -trust, -distrust below) 
     89 
     90It is up to C to decide what packages to trust; it is not a property of P. 
     91 
     92When the `-XPackageTrust` flag is used a '''module M from package P is trusted by a client C''' iff 
     93  * Both of these hold: 
     94    * The module was compiled with `-XSafe` 
     95    * All of M's direct imports are trusted by C 
     96  * OR both of these hold: 
    8197    * The module was compiled with `-XTrustworthy` 
    8298    * All of M's direct safe imports are trusted by C 
    8399    * Package P is trusted by C 
    84100 
    85 When required we will differentiate between `-XSafe` and `-XTrustworthy` using '''safe''' and '''trustworthy''' respectively. 
     101While the mechanism to check if a `-XSafe` compiled module appears to be the same both when `-XPackageTrust` is and isn't used this is not strictly the case. The definition of trust is transitive, so when `-XPackageTrust` is in use importing a safe compiled module can still impose a requirement that a certain package P be trusted if there is a module M in the transitive closure of dependent modules, where M is trustworthy and resides in P. 
     102 
     103Previously the design of Safe Haskell didn't have the `-XPackageTrust` flag. Instead package trust checking was always done. This check was moved into an optional flag as otherwise it causes Safe Haskell to affect users of Haskell who have no interest in Safe Haskell and makes doing safety inference a more complicated story. Please see below for information on Safe Haskell inference. 
    86104 
    87105 
     
    89107 
    90108The intuition is this. The '''author''' of a package undertakes the following obligations: 
    91   * When the author of code compiles it with -XSafe, he asks the compiler to check that it is indeed safe. He takes on no responsibility himself. Although he must trust imported packages in order to compile his package, he takes not responsibility for them. 
    92   * When the author of code compiles it with -XTrustworthy he takes on responsibility for the safety of that code, under the assumption that safe imports are indeed safe. 
     109  * When the author of code compiles it with `-XSafe`, he asks the compiler to check that it is indeed safe. He takes on no responsibility himself. Although he must trust imported packages in order to compile his package, he takes no responsibility for them. 
     110  * When the author of code compiles it with `-XTrustworthy` he takes on responsibility for the safety of that code, under the assumption that safe imports are indeed safe. 
     111  * When the author of code compiles it with `-XUnsafe` he explicitly declares the module untrusted. 
    93112 
    94113When a '''client''' C trusts package P, he expresses trust in the author of that code. But since the author makes no guarantees about safe imports, C may need to chase dependencies to decide which modules in P should be trusted by C.  
     
    116135 
    117136 
     137=== Safety Inference === 
     138 
     139In the case where a module is compiled without one of `-XSafe`, `-XTrustworthy` or `-XUnsafe` being used, GHC will try to figure out itself if the module can be considered safe or not. This safety inference will never mark a module as trustworthy, only as either unsafe or as safe. GHC uses a simply method to determine this for a module M: 
     140 
     141 * If M would compile without error under the `-XSafe` flag, then the module is marked as safe. 
     142 * If M would fail to compile under the `-XSafe` flag, then the module is marked as unsafe. 
     143 
     144When should you use Safe Haskell inference and when should you use an explicit `-XSafe` flag? The later case should be used when you have a hard requirement that the module be safe. That is, the use cases outlined on this page and the purpose for which Safe Haskell is intended: compiling untrusted code. Safe inference is meant to be used by ordinary Haskell programmers. Users who probably don't care about Safe Haskell. 
     145 
     146Say you are writing a Haskell library. Then you probably just want to use Safe inference. Assuming you avoid any unsafe features of the language then your modules will be marked safe. This is a benefit as now a user of your library who may want to use it as part of an API exposed to untrusted code can use the library without any changes. If there wasn't safety inference then either the writer of the library would have to explicitly use Safe Haskell, which is an unreasonable expectation of the whole Haskell community. Or the user of the library would have to wrap it in a shim that simply re-exported your API through a trustworthy module, an annoying practice. 
     147 
     148 
    118149=== Imports Without Trust === 
    119150 
     
    124155We see these being used for more flexibility during development of trusted code. We have this relation between the flags: 
    125156 
     157 * `-XSafe` implies `-XSafeImports`, enables the Safe dialect and establishes Trust guaranteed by GHC. 
    126158 * `-XTrustworthy` implies `-XSafeImports` and establishes Trust guaranteed by client C. 
    127  * `-XSafe` implies `-XSafeImports`, enables the Safe dialect and establishes Trust guaranteed by GHC. 
     159 * `-XUnsafe` implies `-XSafeImports` and marks a module as Untrusted. 
    128160 
    129161In Summary we have the following LANGUAGE options and affects: 
     
    138170     '''Module Trusted''': Yes [[BR]] 
    139171     '''Haskell Language''': Restricted to Safe Language [[BR]] 
    140      '''Imported Modules''': All forced to be safe imports, all must be trusted. [[BR]] 
     172     '''Imported Modules''': All forced to be safe imports, all must be trusted [[BR]] 
    141173 
    142174  * '''`-XTrustworthy`''': 
     
    148180     semantics. 
    149181 
    150      '''Module Trusted''': Yes but only if Package the module resides in is also trusted. [[BR]] 
     182     '''Module Trusted''': Yes [[BR]] 
    151183     '''Haskell Language''': Unrestricted [[BR]] 
    152      '''Imported Modules''': Under control of module author which ones must be trusted. [[BR]] 
     184     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
     185 
     186  * '''`-XUnsafe`''': 
     187     Explicitly mark the module as unsafe. Don't allow the Safe Haskell inference mechanism to 
     188          record it as safe. This flag implies `-XSafeImports`, so safe imports can be used. 
     189 
     190     '''Module Trusted''': No [[BR]] 
     191     '''Haskell Language''': Unrestricted [[BR]] 
     192     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
    153193 
    154194  * '''`-XSafeImport`''': 
     
    156196     a dependency to be trusted without asserting any trust about itself. 
    157197 
     198     '''Module Trusted''': Determined by GHC [[BR]] 
     199     '''Haskell Language''': Unrestricted [[BR]] 
     200     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
     201 
     202All of the above flags can also be combined with the `-XPackageTrust` flag, resulting in: [[BR]] 
     203 
     204  * '''`-XPackageTrust -XSafe`'''' 
     205    Enable package trust checking plus restrictions normally enabled by `-XSafe` on its own. 
     206 
     207     '''Module Trusted''': Yes [[BR]] 
     208     '''Haskell Language''': Restricted to Safe Language [[BR]] 
     209     '''Imported Modules''': All forced to be safe imports, all must be trusted [[BR]] 
     210 
     211  * '''`-XPackageTrust -XTrustworthy`''' 
     212    Enable package trust checking and marks a module as trustworthy. 
     213 
     214     '''Module Trusted''': Yes if the package it resides in is trusted [[BR]] 
     215     '''Haskell Language''': Unrestricted [[BR]] 
     216     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
     217 
     218  * '''`-XPackageTrust -XUnsafe`''' 
     219    Enable package trust checking and mark the module as unsafe. 
     220 
    158221     '''Module Trusted''': No [[BR]] 
    159222     '''Haskell Language''': Unrestricted [[BR]] 
    160      '''Imported Modules''': Under control of module author which ones must be trusted. [[BR]] 
     223     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
     224 
     225  * '''`-XPackageTrust -XSafeImport`''' 
     226    Enable package trust checking and safe imports. 
     227 
     228     '''Module Trusted''': Determined by GHC. [[BR]] 
     229     '''Haskell Language''': Unrestricted [[BR]] 
     230     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
    161231 
    162232 
     
    176246=== Interaction of Options === 
    177247 
    178 The `-XSafe`, `-XTrustworthy`, and `-XSafeImport` GHC LANGUAGE options are all order independent. When they are used they disable certain other GHC LANGUAGE and OPTIONS_GHC options. 
    179  
     248The `-XSafe`, `-XTrustworthy`, `-XUnsafe`, `-XPackageTrust` and `-XSafeImport` GHC LANGUAGE options are all order independent. When they are used they disable certain other GHC LANGUAGE and OPTIONS_GHC options. 
    180249 
    181250  * '''`-XSafe`''': 
    182251    * Enables the Safe Language dialect which disallows the use of some LANGUAGE and OPTIONS, as well as restricting how certain Haskell language features operate. See [#SafeLanguage] below for details. 
    183  
    184   * '''`-XTrustworthy`''' has no special interactions. 
    185  
    186   * '''`-XSafeImports`''' has no special interactions. `-XSafe`, `-XTrustworthy` are both compatible with it as they all imply `-XSafeImports` anyway. 
     252         * Can't be used when `-XTrustworthy` or `-XUnsafe` is used. 
     253 
     254  * '''`-XTrustworthy`''' has no special interactions except that it can't be used when `-XSafe` or `-XUnsafe` is used. 
     255 
     256  * '''`-XUnsafe`''' has no special interactions except that it can't be used when `-XSafe` or `-XTrustworthy` is used. 
     257 
     258  * '''`-XPackageTrust`''' turns on package trust checking. Has no special interactions, can be used with `-XSafe`, `-XTrustworthy`, `-XUnsafe` and `-XSafeImports`. 
     259 
     260  * '''`-XSafeImports`''': 
     261    * Has no special interactions. 
     262         * `-XSafe`, `-XTrustworthy` are both compatible with it as they all imply `-XSafeImports` anyway. 
     263         * Compatible with `-XUnsafe` and with `-XPackageTrust`. 
    187264 
    188265 
     
    252329 * Would be worthwhile modifying Hackage and Haddock to display Safe Haskell information. 
    253330 
     331 
    254332== Symbol Level Safety == 
    255333 
     
    305383For the moment we are sticking with the module level design. Symbol level is a forward compatible extension to the module level design so we can revisit in the future. 
    306384 
     385 
    307386== Intended uses == 
    308387 
     
    386465 
    387466In this case, the type of `Danger.runMe` will be `IO ()`.  However, because `-ultrasafe` implies `-distrust-all-packages`, the only modules `Danger` can import are trustable modules whose entire trust dependency set lies in the current package.  Let's say that `SafeIO` and `Danger` are the only two such modules.  We then know that the only IO actions `Danger.runMe` can directly execute are `rioReadFile` and `rioWriteFile`. 
     467 
    388468 
    389469== Use cases for `SafeImports` == 
     
    465545 
    466546If pointers, peek, and poke are allowed you can craft something that modifies existing heap data and, say, change constructors in existing heap data. 
     547