Changes between Version 58 and Version 59 of SafeHaskell


Ignore:
Timestamp:
Sep 14, 2011 12:03:52 AM (3 years ago)
Author:
dterei
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • SafeHaskell

    v58 v59  
    3535== Safe Language Overview == 
    3636 
    37 As long as no module compiled with -XTrustworthy contains a vulnerability, the goal of the Safe dialect (used through `-XSafe`) is to guarantee the following properties: 
    38  
    39  * '''Referential transparency.'''  Functions in the Safe dialect must be deterministic. Moreover, evaluating them should have no side effects, and should not halt the program (except by throwing uncaught exceptions or looping forever). 
    40  
    41  * '''Constructor access control.'''  Safe code must not be able to examine or synthesize data values using data constructors the module cannot import. 
    42  
    43  * '''Semantic consistency.'''  Any expression that compiles both with and without the import of a Safe module must have the same meaning in both cases. (E.g., {{{1 + 1 == 3}}} must remain `False` when you add the import of a Safe module.) Safe Haskell reduces the scope of compilable Haskell code but it shouldn't change its meaning. 
     37As long as no module compiled with `-XTrustworthy` contains a vulnerability, the goal of the Safe dialect (used through `-XSafe`) is to guarantee the following properties: 
     38 
     39 * '''Referential transparency.''' Functions in the Safe dialect must be deterministic. Moreover, evaluating them should have no side effects, and should not halt the program (except by throwing uncaught exceptions or looping forever). 
     40 
     41 * '''Constructor access control.''' Safe code must not be able to examine or synthesize data values using data constructors the module cannot import. 
     42 
     43 * '''Semantic consistency.''' Any expression that compiles both with and without the import of a Safe module must have the same meaning in both cases. (E.g., {{{1 + 1 == 3}}} must remain `False` when you add the import of a Safe module.) Safe Haskell reduces the scope of compilable Haskell code but it shouldn't change its meaning. 
    4444 
    4545The Safe dialect is intended to be used on untrusted code to allow that code to be trusted. Please keep in mind though that the issue of trust is at a higher level than the safe dialect. Using the safe dialect doesn't automatically imply trust, trust is defined separately below. 
     
    5454    `impdecl -> `import` [`safe`] [`qualified`] modid [`as` modid] [impspec]` 
    5555 
    56 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`, `-XUnsafe` or `-XSafeImports`. 
     56When enabled, a module imported with the safe keyword must be a trusted module, otherwise a compilation error will result. Safe imports are enabled through either `-XSafe`, `-XTrustworthy` or `-XUnsafe`. 
    5757 
    5858 
     
    6262  * `-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. 
    6363  * `-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. 
     64  * `-XUnsafe`: means that GHC should always regard this module as untrusted. This is needed as without any flags GHC will try to [wiki:SafeHaskell#SafetyInference infer safety]. 
    6565 
    6666A '''client''' (C) is someone compiling a source module with GHC. 
     
    8282When required we will differentiate between `-XSafe` and `-XTrustworthy` using '''safe''' and '''trustworthy''' respectively. 
    8383 
    84 The 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: 
     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 `-fpackage-trust` 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: 
    8585 
    8686A '''package P is trusted by a client C''' iff one of these conditions holds 
     
    9090It is up to C to decide what packages to trust; it is not a property of P. 
    9191 
    92 When the `-XPackageTrust` flag is used a '''module M from package P is trusted by a client C''' iff 
     92When the `-fpackage-trust` flag is used a '''module M from package P is trusted by a client C''' iff 
    9393  * Both of these hold: 
    9494    * The module was compiled with `-XSafe` 
     
    9999    * Package P is trusted by C 
    100100 
    101 While 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  
    103 Previously 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. 
     101While the mechanism to check if a `-XSafe` compiled module appears to be the same both when `-fpackage-trust` is and isn't used this is not strictly the case. The definition of trust is transitive, so when `-fpackage-trust` 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 `-fpackage-trust` 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. 
    104104 
    105105 
     
    147147 
    148148 
    149 === Imports Without Trust === 
    150  
    151 We also want to be able to enable the safe import extensions without any corresponding trust assertion for the code: 
    152  
    153  * `-XSafeImports` enables the safe import extension. Module M is left untrusted though. (See [#UsecasesforSafeImports use cases]) 
    154  
    155 We see these being used for more flexibility during development of trusted code. We have this relation between the flags: 
    156  
    157  * `-XSafe` implies `-XSafeImports`, enables the Safe dialect and establishes Trust guaranteed by GHC. 
    158  * `-XTrustworthy` implies `-XSafeImports` and establishes Trust guaranteed by client C. 
    159  * `-XUnsafe` implies `-XSafeImports` and marks a module as Untrusted. 
    160  
    161 In Summary we have the following LANGUAGE options and affects: 
     149=== Safe Haskell Language Flag Summary === 
     150 
     151We have this relation between the flags: 
     152 
     153 * `-XSafe` enables safe imports and enables the safe dialect and establishes Trust guaranteed by GHC. 
     154 * `-XTrustworthy` enables safe imports and establishes Trust guaranteed by client C. 
     155 * `-XUnsafe` enables safe imports and marks a module as Untrusted. 
     156 
     157In summary we have the following LANGUAGE options and effects: 
     158 
    162159  * '''`-XSafe`''': 
    163160     To be trusted, all of the module's direct imports must be 
     
    176173     provided by the module's author. A client of this module then 
    177174     specifies that they trust the module author by specifying they 
    178      trust the package containing the module. '-XTrustworthy' has 
     175     trust the package containing the module. `-XTrustworthy` has 
    179176     no effect on the accepted range of Haskell programs or their 
    180177     semantics. 
     
    186183  * '''`-XUnsafe`''': 
    187184     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. 
     185          record it as safe. 
    189186 
    190187     '''Module Trusted''': No [[BR]] 
     
    192189     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
    193190 
    194   * '''`-XSafeImport`''': 
    195      Enable the Safe Import extension so that a module can require 
    196      a dependency to be trusted without asserting any trust about itself. 
    197  
    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  
    202 All of the above flags can also be combined with the `-XPackageTrust` flag, resulting in: [[BR]] 
    203  
    204   * '''`-XPackageTrust -XSafe`'''' 
     191All of the above flags can also be combined with the `-fpackage-trust` flag, resulting in: [[BR]] 
     192 
     193  * '''`-fpackage-trust -XSafe`'''' 
    205194    Enable package trust checking plus restrictions normally enabled by `-XSafe` on its own. 
    206195 
     
    209198     '''Imported Modules''': All forced to be safe imports, all must be trusted [[BR]] 
    210199 
    211   * '''`-XPackageTrust -XTrustworthy`''' 
     200  * '''`-fpackage-trust -XTrustworthy`''' 
    212201    Enable package trust checking and marks a module as trustworthy. 
    213202 
     
    216205     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
    217206 
    218   * '''`-XPackageTrust -XUnsafe`''' 
     207  * '''`-fpackage-trust -XUnsafe`''' 
    219208    Enable package trust checking and mark the module as unsafe. 
    220209 
     
    223212     '''Imported Modules''': Under control of module author which ones must be trusted [[BR]] 
    224213 
    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]] 
    231  
     214While it seems that `-fpackage-trust -XSafe` has the same effect as just `-XSafe`, it doesn't. As trust checking is a transitive operation, turning on package trust may require some package that a depdencies resides in needs to now be trusted. 
    232215 
    233216=== Specifying Package Trust  === 
     
    241224 * `-distrust-all-packages` - considers all packages untrusted unless they are explicitly trusted by subsequent command-line options.  (This option does not change the exposed/hidden status of packages, so is not equivalent to applying `-distrust` to all packages on the system.) 
    242225 
    243  * A convenience option `-ultrasafe` which is equivalent to specifying {{{-distrust-all-packages -XNoForeignFunctionInterface -XNoImplicitPrelude}}} at the point of the `-ultrasafe` option, and `-XSafe` at the end of the command line. 
    244  
    245226 
    246227=== Interaction of Options === 
    247228 
    248 The `-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. 
     229The `-XSafe`, `-XTrustworthy`, `-XUnsafe`, and `-fpackage-trust` GHC LANGUAGE options are all order independent. When they are used they disable certain other GHC LANGUAGE and OPTIONS_GHC options. 
    249230 
    250231  * '''`-XSafe`''': 
     
    256237  * '''`-XUnsafe`''' has no special interactions except that it can't be used when `-XSafe` or `-XTrustworthy` is used. 
    257238 
    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`. 
     239  * '''`-fpackage-trust`''' turns on package trust checking. Has no special interactions, can be used with `-XSafe`, `-XTrustworthy`, and `-XUnsafe`. 
    264240 
    265241 
     
    437413 
    438414 
    439 === Restricted `IO` imports === 
    440  
    441 An alternate approach to sandboxing possibly malicious plugins is to allow the code to execute `IO` actions, but to limit the primitive `IO` actions such code can import.  In this case, the plugin module `Danger` must be compiled with `-ultrasafe`.  Moreover, it will import a module such as the following: 
    442  
    443 {{{ 
    444 {-# LANGUAGE Trustworthy #-} 
    445  
    446 module SafeIO (rioReadFile, rioWriteFile 
    447               , module RestrictedPrelude) where 
    448  
    449 import RestrictedPrelude -- Subset of Prelude without IO actions 
    450  
    451 -- Returns True iff access is allowed to file name 
    452 pathOK :: FilePath -> IO Bool 
    453 pathOK file = {- Implement some policy based on file name -} 
    454  
    455 rioReadFile :: FilePath -> IO String 
    456 rioReadFile file = do 
    457   ok <- pathOK file 
    458   if ok then readFile file else return "" 
    459  
    460 rioWriteFile :: FilePath -> String -> IO () 
    461 rioWriteFile file contents = do 
    462   ok <- pathOK file 
    463   if ok then writeFile file contents else return () 
    464 }}} 
    465  
    466 In 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  
    468  
    469 == Use cases for `SafeImports` == 
    470  
    471 Say I'm in module Main or some other unsafe place, and I want to 
    472 import a module from an untrusted author.  I'd like to say: 
    473  
    474 {{{ 
    475    import safe Untrusted.Module 
    476 }}}  
    477  
    478 Unfortunately, safe is not a Haskell98 keyword, so this fails.  There 
    479 are several other ways of enabling the safe keyword, namely the 
    480 `LANGUAGE Safe`, and `Trustworthy` pragmas, but these all do 
    481 more than just enable the safe keyword--they restrict the language 
    482 and/or mark the module as trusted.  I don't want any of these things. 
    483 I just want to make module Main fail to compile should 
    484 Untrusted.Module be importing trustworthy modules from untrusted 
    485 packages, nothing more. 
    486  
    487  
    488415== Ultra-safety == 
    489416 
    490417'''Note'''. This section concerns a possible extension/variant.   
    491418 
    492 The safe dialect does not prevent use of the symbol `IO`. Nor does it prevent use of `foreign import`.  So this module is OK: 
     419The safe dialect does not prevent use of the symbol `IO`. Nor does it prevent use of `foreign import`. So this module is OK: 
    493420 
    494421{{{ 
     
    498425}}} 
    499426 
    500 Hence, while an application A importing a safe but possibly malicious module M may safely invoke pure functions from M, it must avoid executing `IO` actions construted inside M unless some other mechanism ensures those actions conform to A's security goal.  Such actions may be hidden inside data structures: 
     427Hence, while an application A importing a safe but possibly malicious module M may safely invoke pure functions from M, it must avoid executing `IO` actions construted inside M unless some other mechanism ensures those actions conform to A's security goal. Such actions may be hidden inside data structures: 
    501428 
    502429{{{ 
     
    509436}}} 
    510437 
    511 The flag (and LANGUAGE pragma) `UltraSafe` is just like `Safe` except that it also disables `foreign import`.  This strengthens the safety guarantee, by ensuring that an `UltraSafe` module can construct IO actions only by composing together IO actions that it imports from trusted modules. Note that `UltraSafe` does not disable the use of IO itself. For example this is fine: 
     438The flag (and LANGUAGE pragma) `UltraSafe` is just like `Safe` except that it also disables `foreign import`. This strengthens the safety guarantee, by ensuring that an `UltraSafe` module can construct IO actions only by composing together IO actions that it imports from trusted modules. Note that `UltraSafe` does not disable the use of IO itself. For example this is fine: 
    512439 
    513440{{{ 
     
    519446}}} 
    520447 
    521 Do we really want ultra-safety.  As shown above, we can get some of the benefit by sandboxing with a RIO-like mechanism. But there is no machine check that you've done it right. What I'd like is a machine check: 
     448Do we really want ultra-safety. As shown above, we can get some of the benefit by sandboxing with a RIO-like mechanism. But there is no machine check that you've done it right. What I'd like is a machine check: 
    522449 * when I compile untrusted module `Bad` with `-XUltraSafe` I get the guarantee that any I/O actions accessible through U's exports are obtained by composing I/O actions from modules that I trust 
    523450 
    524 I think that's a valuable guarantee.  Simon M points out that if I want to freely call I/O actions exported by an untrusted `-XUltraSafe` module, then I must be careful to trust only packages whose I/O actions are pretty restricted. In practice, I'll make a sandbox library, and trust only that; now the untrusted module can only call to those restricted IO actions. And now we are back to something RIO like.   
    525  
    526 Well, yes, but I want a stronger static guarantee.  As things stand the untrusted module U might export `removeFiles`, and I might accidentally call it. (After all, I have to call some IO actions!) I want a static check that I'm not calling IO actions constructed by a bad guy. 
    527  
    528 An alternative way to achieve this would be to have a machine check that none of `Bad`'s exports mention IO, even hidden inside a data type, but I don't really know how to do that.  For example, if the RIO sandbox accidentally exposed the IO-to-RIO constructor, we'd be dead, and that's nothing to do with U's exports. 
     451I think that's a valuable guarantee. Simon M points out that if I want to freely call I/O actions exported by an untrusted `-XUltraSafe` module, then I must be careful to trust only packages whose I/O actions are pretty restricted. In practice, I'll make a sandbox library, and trust only that; now the untrusted module can only call to those restricted IO actions. And now we are back to something RIO like.   
     452 
     453Well, yes, but I want a stronger static guarantee. As things stand the untrusted module U might export `removeFiles`, and I might accidentally call it. (After all, I have to call some IO actions!) I want a static check that I'm not calling IO actions constructed by a bad guy. 
     454 
     455An alternative way to achieve this would be to have a machine check that none of `Bad`'s exports mention IO, even hidden inside a data type, but I don't really know how to do that. For example, if the RIO sandbox accidentally exposed the IO-to-RIO constructor, we'd be dead, and that's nothing to do with U's exports. 
    529456 
    530457In short, I still think there is a useful extra static guarantee that we could get, but at the cost of some additional complexity (an extra flag, and its consequences).