Changes between Version 58 and Version 59 of SafeHaskell


Ignore:
Timestamp:
Sep 14, 2011 12:03:52 AM (4 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).