Changes between Version 55 and Version 56 of SafeHaskell


Ignore:
Timestamp:
Jul 12, 2011 12:31:20 AM (3 years ago)
Author:
dterei
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • SafeHaskell

    v55 v56  
    2626The design of Safe Haskell involves the following aspects: 
    2727 
    28  * A safe language dialect of Haskell (as an extension) that provides certain guarantees about the code. Mainly it allows the types to be trusted. 
     28 * A safe language dialect of Haskell that provides certain guarantees about the code. Mainly it allows the types to be trusted. 
    2929 * A new "safe import" extension to Haskell that specifies the module being imported must be trusted. 
    3030 * A definition of "trust" and how it operates, as well as ways of defining and changing the trust of modules and packages. 
     
    3333== Safe Language Overview == 
    3434 
    35 As 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: 
     35As 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: 
    3636 
    3737 * '''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). 
     
    4141 * '''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. 
    4242 
    43 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 (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. 
     43The 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. 
    4444 
    4545The 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. 
     
    5252    `impdecl -> `import` [`safe`] [`qualified`] modid [`as` modid] [impspec]` 
    5353 
    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`, `-XSafeLanguage`, `-XTrustworthy`or `-XSafeImports`. 
     54When 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`. 
    5555 
    5656 
     
    116116 
    117117 
    118 === Safe Language & Imports Without Trust === 
    119  
    120 We also want to be able to enable the safe dialect and safe import extensions without any corresponding trust assertion for the code: 
     118=== Imports Without Trust === 
     119 
     120We also want to be able to enable the safe import extensions without any corresponding trust assertion for the code: 
    121121 
    122122 * `-XSafeImports` enables the safe import extension. Module M is left untrusted though. (See [#UsecasesforSafeImports use cases]) 
    123  * `-XSafeLanguage` enables the safe language (and therefore safe imports). Module M is left untrusted though. (See [#UsecasesforSafeLanguage use cases]) 
    124  
    125 We see these being used both for good coding style and more flexibility during development of trusted code. We have this relation between the flags: 
    126  
    127  * `-XSafeLanguage` implies `-XSafeImports`. 
     123 
     124We see these being used for more flexibility during development of trusted code. We have this relation between the flags: 
     125 
    128126 * `-XTrustworthy` implies `-XSafeImports` and establishes Trust guaranteed by client C. 
    129  * `-XSafe` implies `-XSafeLanguage` and establishes Trust guaranteed by GHC. 
     127 * `-XSafe` implies `-XSafeImports`, enables the Safe dialect and establishes Trust guaranteed by GHC. 
    130128 
    131129In Summary we have the following LANGUAGE options and affects: 
     
    142140     '''Imported Modules''': All forced to be safe imports, all must be trusted. [[BR]] 
    143141 
    144   * '''`-XSafeLanguage`''': 
    145      The module is never trusted, because the author does not claim 
    146      it is trustworthy.  As long as the module compiles both ways, 
    147      the result is identical whether or not the `-XSafeLanguage` flag 
    148      is supplied.  As with `-XSafe`, the "safe" import keyword is 
    149      allowed but meaningless--all imports must be safe. 
    150  
    151      '''Module Trusted''': No [[BR]] 
    152      '''Haskell Language''': Restricted to Safe Language [[BR]] 
    153      '''Imported Modules''': All forced to be safe imports, all must be trusted. [[BR]] 
    154  
    155142  * '''`-XTrustworthy`''': 
    156143     This establishes that the module is trusted, but the guarantee is 
     
    165152     '''Imported Modules''': Under control of module author which ones must be trusted. [[BR]] 
    166153 
    167   * '''`-XSafeLanguage -XTrustworthy`''': 
    168      For the trust property this has the same effect as '-XTrustworthy' 
    169      by itself. However unlike `-XTrustworthy` it also restricts the 
    170      range of acceptable Haskell programs to the Safe language. The 
    171      difference from this and using `-XSafe` is the different trust 
    172      type and that not all imports are forced to be safe imports, they 
    173      are instead optionally specified by the module author. 
    174  
    175      '''Module Trusted''': Yes but only if Package the module resides in is also trusted. [[BR]] 
    176      '''Haskell Language''': Restricted to Safe Language [[BR]] 
    177      '''Imported Modules''': Under control of module author which ones must be trusted. [[BR]] 
    178  
    179154  * '''`-XSafeImport`''': 
    180155     Enable the Safe Import extension so that a module can require 
     
    201176=== Interaction of Options === 
    202177 
    203 The `-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. 
     178The `-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. 
    204179 
    205180 
     
    207182    * 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. 
    208183 
    209   * '''`-XTrustworthy`''' has no special interactions, except for 
    210     * If `-XSafeLanguage`: See summary of !SafeHaskell options at bottom of [#SafeLanguageImportsWithoutTrust Safe Language & Imports (Without Trust)] 
    211  
    212   * '''`-XSafeLanguage`''' has the exact same restrictions as `-XSafe`. `-XSafe` and `-XSafeLanguage` can't be used together though simply as it is most likely a mistake by the module author of client if they do. 
    213  
    214   * '''`-XSafeImports`''' has no special interactions. `-XSafe`, `-XTrustworthy` and `-XSafeLanguage` are all compatible with it as they all imply `-XSafeImports` anyway. 
     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. 
    215187 
    216188 
    217189== Safe Language == 
    218190 
    219 The Safe Language restricts things in two different ways: 
     191The Safe Language (enabled through `-XSafe`) restricts things in two different ways: 
    220192 
    221193  1. Certain GHC LANGUAGE extensions are disallowed completely. 
     
    224196Below is precisely what flags and extensions fall into each category: 
    225197 
    226     * '''Disallowed completely''': `GeneralizedNewtypeDeriving`, `TemplateHaskell`, `-XSafeLanguage` 
     198    * '''Disallowed completely''': `GeneralizedNewtypeDeriving`, `TemplateHaskell` 
    227199    * '''Restricted functionality''': `OverlappingInstances`, `ForeignFunctionInterface`, {{{RULES}}} 
    228200      * See [#RestrictedandDisabledGHCHaskellFeatures Restricted Features below] 
     
    235207 * {{{ForeignFunctionInterface}}}: This is mostly safe, but {{{foreign import}}} declarations that import a function with a non-`IO` type are be disallowed. All FFI imports must reside in the IO Monad. 
    236208 
    237  * {{{RULES}}}: As they can change the behaviour of trusted code in unanticipated ways, violating semantic consistency they are restricted in function. Specifically any {{{RULES}}} defined in a module M compiled with `-XSafe` or `-XSafeLanguage` are dropped. {{{RULES}}} defined in trustworthy modules that M imports are still valid and will fire as usual. 
    238  
    239  * {{{OverlappingInstances}}}: This extension can be used to violate semantic consistency, because malicious code could redefine a type instance (by containing a more specific instance definition) in a way that changes the behaviour of code importing the untrusted module. The extension is not disabled for a module M compiled with `-XSafe` or `-XSafeLanguage` but restricted. While M can defined overlapping instance declarations, they can only be used in M. If in a module N that imports M, at a call site that uses a type-class function there is a choice of which instance to use (i.e overlapping) and the most specific choice is from M (or any other Safe compiled module), then compilation will fail. It is irrelevant if module N is considered Safe, or Trustworthy or neither. 
     209 * {{{RULES}}}: As they can change the behaviour of trusted code in unanticipated ways, violating semantic consistency they are restricted in function. Specifically any {{{RULES}}} defined in a module M compiled with `-XSafe` are dropped. {{{RULES}}} defined in trustworthy modules that M imports are still valid and will fire as usual. 
     210 
     211 * {{{OverlappingInstances}}}: This extension can be used to violate semantic consistency, because malicious code could redefine a type instance (by containing a more specific instance definition) in a way that changes the behaviour of code importing the untrusted module. The extension is not disabled for a module M compiled with `-XSafe` but restricted. While M can defined overlapping instance declarations, they can only be used in M. If in a module N that imports M, at a call site that uses a type-class function there is a choice of which instance to use (i.e overlapping) and the most specific choice is from M (or any other Safe compiled module), then compilation will fail. It is irrelevant if module N is considered Safe, or Trustworthy or neither. 
    240212 
    241213In the Safe language dialect we disable completely the following Haskell language features: 
     
    424396Unfortunately, safe is not a Haskell98 keyword, so this fails.  There 
    425397are several other ways of enabling the safe keyword, namely the 
    426 `LANGUAGE Safe`, `SafeLanguage`, and `Trustworthy` pragmas, but these all do 
     398`LANGUAGE Safe`, and `Trustworthy` pragmas, but these all do 
    427399more than just enable the safe keyword--they restrict the language 
    428400and/or mark the module as trusted.  I don't want any of these things. 
     
    430402Untrusted.Module be importing trustworthy modules from untrusted 
    431403packages, nothing more. 
    432  
    433 == Use cases for `SafeLanguage` == 
    434  
    435 Here again the idea is that I want to create an untrusted module that 
    436 exports unsafe constructors, but I want to use the Safe dialect, 
    437 because it enforces good programming style.  An example would be the 
    438 `RIO` module, if it wanted to export `UnsafeRIO`.  There's no reason RIO 
    439 itself can't be implemented in the Safe dialect, we just need to make 
    440 sure that only Trustworthy modules can import `RIO`. 
    441404 
    442405