Changes between Version 55 and Version 56 of SafeHaskell


Ignore:
Timestamp:
Jul 12, 2011 12:31:20 AM (4 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