Changes between Version 57 and Version 58 of SafeHaskell


Ignore:
Timestamp:
Sep 9, 2011 6:33:28 PM (4 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