Changes between Version 36 and Version 37 of SafeHaskell

Show
Ignore:
Timestamp:
01/24/11 12:25:10 (2 years ago)
Author:
dterei
Comment:

take on board Simon PJ, Simon M and David M's comments.

Legend:

Unmodified
Added
Removed
Modified

  • SafeHaskell

    v36 v37  
    2828== Safe Language == 
    2929 
    30 The goal of the Safe dialect is to guarantee the following properties: 
     30As long as no module compiled with -XTrustworthy contains a vulnerability, the goal of the Safe dialect (used through either `-XSafe` or `-XSafeLanguage`) is to guarantee the following properties: 
    3131 
    3232 * '''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). 
    … …  
    3636 * '''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.) 
    3737 
    38 The Safe dialect is intended to be of use for both trusted and untrusted code. It can be used for trusted code as a way to enforce good programming style. It is also useful 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. 
     38The Safe dialect is intended to be of use for both trusted and untrusted code. It can be used for trusted code as a way to enforce good programming style (through `-XSafeLanguage`). It is also useful on untrusted code to allow that code to be trusted (through `-XSafe`). 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. 
    3939 
    4040The safe dialect basically disallows some dangerous features in Haskell to guarantee the above property, as well as checking that the direct dependencies of a module are trusted. 
    … …  
    4545A small extension to the syntax of import statements, adding a `safe` keyword: 
    4646 
    47 impdecl -> `import` [`safe`] [`qualified`] modid [`as` modid] [impspec] 
    48  
    49 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. 
     47    `impdecl -> `import` [`safe`] [`qualified`] modid [`as` modid] [impspec]` 
     48 
     49When 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`, `-XSafeLanguage`, `-XTrustworthy`or `-XSafeImports`. 
    5050 
    5151 
    5252== Trust == 
    5353 
    54 Trust can be thought of simply as a boolean property that applies both to packages and to modules, it is defined as: 
    55  
    56  * A '''client''' is someone running GHC, typically the person compiling the application. 
    57  
    58  * A '''package P is trusted by the client C''' if decided so by the C. 
    59  
    60  * A '''module M is trusted by the client C''' if either: 
    61    1. M is guaranteed by the compiler (ghc) to be `safe`, and all of M's direct imports are trusted by C ('''AND''') 
    62       * (This is done by using the safe language extension for M without any compromises). 
    63       * M can reside in any package P, regardless of if P is trusted or not. 
    64    2. '''OR''': M's author asserts M to be `safe`. ('''AND''') 
    65       * M can use all of Haskell. 
    66       * Only M's direct dependencies imported with the safe keyword need to be trusted. 
    67       * M must reside in a trusted package P 
    68  
    69 The difference is basically for trust type 1, the trust is provided by ghc while for trust type 2 the trust is provided by the modules author, which the client must trust. Trust 1 should be used for code that C doesn't trust (e.g provided by unknown 3rd party) while type 2 should only be used for code C does trust (his/her own code or code provided by known, trusted 3rd party). 
    70  
    71  
    72 == User Interface for Safe Haskell == 
    73  
    74 Now that the high level goals and definitions have been established we discuss how these are exposed to the Haskell user. 
    75  
    76  
    77 === Safe Language & Imports (Module Trust) === 
    78  
    79 We propose two new GHC Options that can be set in the usual way either as a `{-# LANGUAGE #-}` pragma or on the command line. 
    80  
    81  * `-XSafe` enables the safe dialect of Haskell and ask ghc to guarantee safety. If a module M using `-XSafe` compiles successfully then it is trustable. This corresponds to trust type 1. 
    82  * `-XTrustworthy` enables only the safe import extension and requires the client C guarantee safety. If a module using '-XTrustworthy' compiles successfully then it is trustable. This corresponds to trust type 2. 
     54The !SafeHaskell project will introduce two new GHC LANGUAGE options. Intuitively: 
     55  * `-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. Also sets the module to be trusted. 
     56  * `-XTrustworthy`: means that, though a module may invoke unsafe functions internally, the module's author claims that the set of exported symbols cannot be used in an unsafe way. Also sets the module to trusted. 
     57 
     58The LANGUAGE extensions have the following effect. When a client C compiles a module M:  
     59  * Under `-XSafe` the Safe Language dialect is enabled where several potentially-unsafe language features, listed under "Threats" below, are disabled.  
     60  * Under `-XSafe`, all M's imports must be trusted by C  
     61  * Under `-XTrustworthy` all M's safe imports must be trusted by C 
     62 
     63What does it mean for a module to be "trusted by C"? Here is the definition: 
     64  
     65  * A '''client''' is someone running GHC, typically the person compiling the application. 
     66   
     67  * A '''package P is trusted by a client C''' iff one of these conditions holds 
     68    * C's package database records that P is trusted (and command-line arguments do not override the database) 
     69    * C's command-line flags say to trust it regardless of the database (see -trust, -distrust below) 
     70  * It is up to C to decide what packages to trust; it is not a property of P. 
     71   
     72  * A '''module M from package P is trusted by a client C''' iff 
     73    * Both of these hold: 
     74      * The module was compiled with `-XSafe` 
     75      * All of M's direct imports are trusted by C 
     76    * OR all of these hold: 
     77      * The module was compiled with `-XTrustworthy` 
     78      * All of M's direct safe imports are trusted by C 
     79      * Package P is trusted by C 
     80 
     81The intuition is this. The '''author''' of a package undertakes the following obligations: 
     82  * 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. 
     83  * When the author of code compiles it with -XTrustworthy he takes on responsibility for the stafety of that code, under the assumption that safe imports are indeed safe. 
     84 
     85We will refer to a module M compiled successfully with either `-XSafe` or `-XTrustworthy` as '''trusted'''. When required we will differentiate between `-XSafe` and `-XTrustworthy` using '''safe''' and '''trustworthy''' respectively. 
     86 
     87When 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.  
     88 
     89For example, suppose we have this setup:  
     90{{{ 
     91Package Wuggle: 
     92   {-# LANGUAGE Safe #-} 
     93   module Buggle where 
     94     import Prelude 
     95     f x = ...blah... 
     96      
     97Package P: 
     98   {-# LANGUAGE Trustworthy #-} 
     99   module M where 
     100     import System.IO.Unsafe 
     101     import safe Buggle 
     102}}} 
     103 
     104Suppose client C decides to trust package P. Then does C trust module M? To decide, C must check M's imports: 
     105  * M imports System.IO.Unsafe. M was compiled with `-XTrustworthy`, so P's author takes responsibility for that import. C trusts P's author, so C trusts M.  
     106  * M has a safe import of Buggle, so P's author takes no responsibility for the safety or otherwise of Buggle. So C must check whether Buggle is trusted by C. Is it? Well, it is compiled with `-XSafe`, so the code in Buggle itself is machine-checked to be OK, but again under the assumption that Buggle's imports are trusted by C. Ah, but Prelude comes from base, which C trusts, and is (let's say) compiled with `-XTrustworthy`.  
     107 
     108Notice that C didn't need to trust package Wuggle; the machine checking is enough. C only needs to trust packages that have `-XTrustworthy` modules in them. 
     109 
     110 
     111=== Safe Language & Imports (Without Trust) === 
    83112 
    84113We also want to be able to enable the safe dialect and safe import extensions without any corresponding trust assertion for the code: 
    … …  
    93122 * `-XSafe` implies `-XSafeLanguage` and establishes Trust guaranteed by GHC. 
    94123 
     124In Summary we have the following LANGUAGE options and affects: 
     125  * `-XSafe`: 
     126     To be trusted, all of the module's direct imports must be 
     127     trusted, but the module itself need not reside in a trusted 
     128     package, because the compiler vouches for its trustworthiness. 
     129     The "safe" keyword is allowed but meaningless in import 
     130     statements--conceptually every import is safe whether or not so 
     131     tagged. 
     132 
     133  * `-XSafeLanguage`: 
     134     The module is never trusted, because the author does not claim 
     135     it is trustworthy.  As long as the module compiles both ways, 
     136     the result is identical whether or not the `-XSafeLanguage` flag 
     137     is supplied.  As with `-XSafe`, "safe" is allowed but 
     138     meaningless--all imports must be safe. 
     139 
     140  * `-XSafeLanguage -XTrustworthy`: 
     141     To be trusted, the module itself must reside in a trusted 
     142     package.  However, not all of its imports need be trusted, only 
     143     those flagged safe.  Thus, the "safe" keyword has no effect on 
     144     whether or not compilation succeeds, but it has an effect on 
     145     when the resulting file may be trusted. 
     146 
     147  * `-XTrustworthy`: 
     148     The effect is identical to `-XSafeLanguage -XTrustworthy`, except 
     149     that the compiler accepts a wider range of programs.  In 
     150     particular, you can import System.IO.Unsafe, do foreign imports 
     151     without IO, and write any code that would ordinarily compile. 
     152 
     153  * `-XSafeImport`: 
     154     Enable the Safe Import extension so that a module can require 
     155     a dependency to be trusted without asserting any trust about itself. 
    95156 
    96157=== Specifying Package Trust  === 
    … …  
    107168 
    108169 
    109 === Order of options === 
    110  
    111 We must decide on if and how the order of various `LANGUAGE` and `OPTIONS_GHC` pragmas interact with `-XSafe`, `-XTrustworthy`, `-XSafeImports` and `-XSafeLanguage`. The order of options is considered to be:  first, all command-line options in the order they appear on the command line, second, all `LANGUAGE` and `OPTIONS_GHC` pragmas, in the order they appear in the module source. We are only really concerned with dynamic options here as static options are under the complete control of the client C. 
    112  
    113  * '''`-XSafe`''' disables some options and extensions completely while for others it restricts them to appearing before `-XSafe` does. ('''Note:''' Incomplete) 
    114    * '''Must appear before''': `TemplateHaskell`, `-cpp`, `-pgm{L,P,lo,lc,m,s,a,l,dll,F,windres}`, `-opt{L,P,lo,lc,m,s,a,l,dll,F,windres}`, `-F`, `-l''lib''`, `-framework`, `-L''dir''`, `-framework-path''dir''`, `-main-is`, `-package-name` 
    115    * '''Can't appear''': `StandaloneDeriving`, `GeneralizedNewtypeDeriving`, {{{RULES}}}, {{{SPECIALIZE}}}, `-fglasgow-exts` (or should we allow but just not have it enabled restricted options?), `OverlappingInstances` (restricted anyway, see threats below), `-XSafeLanguage` 
    116    * '''Doesn't matter''': `-v`, `-vn`, `-fasm`, `-fllvm`, `-fvia-C`, `-fno-code`, `-fobject-code`, `-fbyte-code`, `-c`, `-split-objs`, `-shared`, `-hcsuf`, `-hidir`, `-o`, `-odir`, `-ohi`, `-osuf`, `-stubdir`, `-outputdir`, `-keep-*`, `-tmpdir`, `-ddump-*`, `-fforce-recomp`, `-no-auto-link-packages` 
    117    * '''Not Sure''': `-D''symbol''`, `-U''symbol''`, `-I''dir''`,  
    118  
    119  * '''`-XTrustworthy`''' is incompatible with `-XSafe` since both are about different trust types. If both appear then it is considered an error. Otherwise `-XTrustworthy` has no special interactions. 
    120    * If `-XSafeImports` appears nothing changes since `-XTrustworthy` implies `-XSafeImports`. 
    121    * If `-XSafeLanguage` appears then the module is restricted to the safe language dialect but trust is still guaranteed by the client C and all imports aren't required to be safe. 
    122  
    123  * '''`-XSafeImports`''' has no special interactions. `-XSafe`, `-XTrustworthy` and `-XSafeLanguage` are all compatible with it as they all imply `-XSafeImports` anyway. 
    124  
    125  * '''`-XSafeLanguage`''' not sure yet. Do we want `-XSafeLanguage` to be as restrictive as `-XSafe` or should it allow {{{RULES}}} and `StandaloneDeriving`? I would lean towards it being as restrictive as `-XSafe` to limit the complexity of the overall !SafeHaskell proposal. 
     170=== Interaction of Options === 
     171 
     172'''Note:''' Incomplete 
     173 
     174The `-XSafe`, `-XTrustworthy`, `-XSafeLanguage` and `-XSafeImport` GHC LANGUAGE options are all order independent. When they are used they disable certain other GHC LANGUAGE and OPTIONS_GHC options. There are some options though that while disabled for source file pragmas are allowed when used on the command line. The idea behind this is that in source pragmas are generally specified by the module author, who is untrusted, while command line options are specified by the client since they are compiling the module, who has to be trusted. Below follow the new !SafeHaskell options and what they disallow: 
     175 
     176  * '''`-XSafe`''': 
     177    * '''Disallowed completely''': `StandaloneDeriving`, `GeneralizedNewtypeDeriving`, {{{RULES}}}, {{{SPECIALIZE}}}, `-fglasgow-exts`, `-XSafeLanguage` 
     178    * '''Only allowed on command line''': `TemplateHaskell`, `-cpp`, `-pgm{L,P,lo,lc,m,s,a,l,dll,F,windres}`, `-opt{L,P,lo,lc,m,s,a,l,dll,F,windres}`, `-F`, `-l''lib''`, `-framework`, `-L''dir''`, `-framework-path''dir''`, `-main-is`, `-package-name`, `-D''symbol''`, `-U''symbol''`, `-I''dir''` 
     179    * '''Restricted functionality''': `OverlappingInstances` (requires that Overlapping instance declarations must either all reside in modules compiled without -XSafe, or else all reside in the same module.) 
     180    * '''Doesn't Matter''': `-v`, `-vn`, `-fasm`, `-fllvm`, `-fvia-C`, `-fno-code`, `-fobject-code`, `-fbyte-code`, `-c`, `-split-objs`, `-shared`, `-hcsuf`, `-hidir`, `-o`, `-odir`, `-ohi`, `-osuf`, `-stubdir`, `-outputdir`, `-keep-*`, `-tmpdir`, `-ddump-*`, `-fforce-recomp`, `-no-auto-link-packages`, `-XSafeImports` 
     181 
     182 
     183  * '''`-XTrustworthy`''' mostly has no special interactions, except for 
     184    * If `-XSafeLanguage`: See summary of !SafeHaskell options at bottom of [#SafeLanguage&Imports(WithoutTrust) Safe Language & Imports (Without Trust)] 
     185 
     186  * '''`-XSafeImports`''' has no special interactions. `-XSafe`, `-XTrustworthy` and `-XSafeLanguage` are all compatible with it as they all imply `-XSafeImports` anyway. 
     187   
     188  * '''`-XSafeLanguage`''' has the exact same restrictions as `-XSafe`. 
    126189 
    127190 
    … …  
    166229   * If a module M is Trustworthy then we handle it differently when linking than compiling: 
    167230     * At both link time and compile time M itself must be in a trusted package. 
    168      * At compile time we check each of M's safe imports are indeed safe or trustworthy and that all trustworthy imports reside in the current set of trusted packages. 
    169      * At link time we don't check that M's safe imports are still considered safe or trustworthy. The reasoning behind this is that at compile time we had a guarantee that any modules marked Trustworthy did indeed reside in a package P that was trusted. If at link time some of M's safe imports that are marked Trustworthy now reside in a package marked untrusted this is because the client C changed the package trust. Since C is the one guaranteeing trustworthy modules we believe its fine to not fail. 
     231     * At compile time we check each of M's safe imports are trusted and that all trustworthy imports reside in the current set of trusted packages. 
     232     * At link time we don't check that M's safe imports are still considered trusted. The reasoning behind this is that at compile time we had a guarantee that any modules marked Trustworthy did indeed reside in a package P that was trusted. If at link time some of M's safe imports that are marked Trustworthy now reside in a package marked untrusted this is because the client C changed the package trust. Since C is the one guaranteeing trustworthy modules we believe its fine to not fail. 
    170233     * Guaranteeing trustworthy at link time wouldn't be too hard, it would just require we also record in the interface file format for modules marked as trustworthy, which of their dependencies were safe imports. 
    171234