| 27 | | The Safe dialect is intended to be of use for both normal (trusted) and untrusted code. Authors of trusted modules may wish to include `{-# LANGUAGE Safe #-}` pragmas to ensure they do not accidentally invoke unsafe actions (directly or indirectly), or to allow other Safe code to import their modules. |
| 28 | | |
| 29 | | |
| 30 | | == Language extension == |
| 31 | | |
| 32 | | There are two parts to the proposed extension: |
| 33 | | |
| 34 | | 1. Two new GHC LANGUAGE options, `-XSafe` and `-XTrustworthy`. Intuitively |
| 35 | | * `-XSafe` enables a "Safe" dialect of Haskell in which GHC rejects any source code that might produce unsafe effects or otherwise subvert the type system. |
| 36 | | * `-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. (There is a corresponding `-XUntrustworthy` option to enable the language extension but negate `-XTrustworthy`. '''SLPJ: don't understand''') |
| 37 | | |
| 38 | | 2. A small extension to the syntax of import statements (enabled by `-XSafe` or `-XTrustworhty`), adding a `safe` keyword: |
| 39 | | |
| 40 | | impdecl -> `import` [`safe`] [`qualified`] modid [`as` modid] [impspec] |
| 41 | | |
| 42 | | The LANGUAGE extensions have the following effect. When a client C compiles a module M: |
| 43 | | * Under `-XSafe` several potentially-unsafe language features, listed under "Threats" below, are disabled. |
| 44 | | * Under `-XSafe`, all M's `imports` must be trusted by C |
| 45 | | * Under `-XTrustworthy` or `-XUntrustworthy` (but not `-XSafe`) all M's `safe imports` must be trusted by C |
| 46 | | |
| 47 | | What does it mean for a module to be "trusted by C"? Here is the definition: |
| | 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. |
| | 39 | |
| | 40 | The 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. |
| | 41 | |
| | 42 | |
| | 43 | == Safe Imports == |
| | 44 | |
| | 45 | A small extension to the syntax of import statements, adding a `safe` keyword: |
| | 46 | |
| | 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. |
| | 50 | |
| | 51 | |
| | 52 | == Trust == |
| | 53 | |
| | 54 | Trust can be thought of simply as a boolean property that applies both to packages and to modules, it is defined as: |
| 51 | | * A '''package P is trusted by a client C''' iff one of these conditions holds |
| 52 | | * C's package database records that P is trusted (and command-line arguments do not override the database) |
| 53 | | * C's command-line flags say to trust it regardless of the database (see `-trust`, `-distrust` below)[[BR]] |
| 54 | | It is up to C to decide what packages to trust; it is not a property of P. |
| 55 | | |
| 56 | | * A '''module M from package P is trusted by a client C''' iff |
| 57 | | * Both of these hold: |
| 58 | | * The module was compiled with `-XSafe` and without `-XUntrustworthy` |
| 59 | | * All of M's direct `imports` are trusted by C |
| 60 | | * OR all of these hold: |
| 61 | | * The module was compiled with `-XTrustworthy` |
| 62 | | * All of M's direct `safe imports` are trusted by C |
| 63 | | * Package P is trusted by C |
| 64 | | |
| 65 | | |
| 66 | | |
| 67 | | The intuition is this. The '''author''' of a package undertakes the following obligations: |
| 68 | | * 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. |
| 69 | | * 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. |
| 70 | | |
| 71 | | When 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. |
| 72 | | |
| 73 | | For example, suppose we have this setup: |
| 74 | | {{{ |
| 75 | | Package Wuggle: |
| 76 | | {-# LANGUAGE Safe #-} |
| 77 | | module Buggle where |
| 78 | | import Prelude |
| 79 | | f x = ...blah... |
| 80 | | |
| 81 | | Package P: |
| 82 | | {-# LANGUAGE Trustworthy #-} |
| 83 | | module M where |
| 84 | | import System.IO.Unsafe |
| 85 | | import safe Buggle |
| 86 | | }}} |
| 87 | | Suppose client C decides to trust package P. Then does C trust module M? To decide, C must check M's imports: |
| 88 | | * 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. |
| 89 | | * 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`. |
| 90 | | |
| 91 | | Notice 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. |
| 92 | | |
| 93 | | === Command line options === |
| | 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`. |
| | 62 | * (This is done by using the safe language extension for M without any compromises). |
| | 63 | * All of M's direct dependencies must be trusted (all imports are safe imports). |
| | 64 | * M can reside in any package P, regardless of if P is trusted or not. |
| | 65 | 2. '''OR''': M is specified by the client C to be `safe`. |
| | 66 | * M can use all of Haskell. |
| | 67 | * Only M's direct dependencies imported with the safe keyword need to be trusted. |
| | 68 | * M must reside in a trusted package P |
| | 69 | |
| | 70 | 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 client C. 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). |
| | 71 | |
| | 72 | |
| | 73 | == User Interface for Safe Haskell == |
| | 74 | |
| | 75 | Now that the high level goals and definitions have been established we discuss how these are exposed to the Haskell user. |
| | 76 | |
| | 77 | |
| | 78 | === Safe Language & Imports (Module Trust) === |
| | 79 | |
| | 80 | We propose two new GHC Options that can be set in the usual way either as a `{-# LANGUAGE #-}` pragma or on the command line. |
| | 81 | |
| | 82 | * `-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. |
| | 83 | * `-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. |
| | 84 | |
| | 85 | We also want to be able to enable the safe dialect and safe import extensions without any corresponding trust assertion for the code: |
| | 86 | |
| | 87 | * `-XSafeImports` ('''previously''' `-XUntrustworthy`) enables the safe import extension. Module M is left untrusted though. |
| | 88 | * `-XSafeLanguage` ('''previously''' `-XUntrustworthy` `-XSafe`) enables the safe language (and therefore safe imports). Module M is left untrusted though. |
| | 89 | |
| | 90 | 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: |
| | 91 | |
| | 92 | * `-XSafeLanguage` implies `-XSafeImports`. |
| | 93 | * `-XTrustworthy` implies `-XSafeImports` and establishes Trust guaranteed by client C. |
| | 94 | * `-XSafe` implies `-XSafeLanguage` and establishes Trust guaranteed by GHC. |
| | 95 | |
| | 96 | |
| | 97 | === Specifying Package Trust === |
| 107 | | Safety-critical options must not be specified or overwritten by `LANGUAGE` and `OPTIONS_GHC` pragmas in the Safe dialect. To avoid such surprises, certain options and pragmas are '''restricted''', meaning they can only be supplied before the safe dialect is enabled. 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. Thus, the `-XSafe` command-line option disallows all restricted pragmas, but, in the absence of `-XSafe` on the command line, `{-# LANGUAGE Safe #-}` may appear below restricted pragmas in the source, just not above them. |
| 108 | | |
| 109 | | At least the following options (and their pragma equivalents) are restricted: |
| 110 | | |
| 111 | | - `-XTrustworthy` - Rationale: Trusted packages may wish to include untrusted code compiled with `-XSafe`. Yet once `-XSafe` is applied, the module must not be able to prune its trust dependency set, which it could with `{-# Trustworthy #-}`. |
| 112 | | - `-XUntrustworthy` - Rationale: Unless -XUntrustworthy is applied first, if compilation does not fail, then `-XSafe` should produce code that can be trusted with the specified set of trusted packages. |
| 113 | | - `-XForeignFunctionInterface` - Rationale: Trustworthy code in the Safe dialect may wish to have foreign import declarations, but modules from untrusted sources do not need this feature. Thus, `-XSafe` on the command line should disable `{-# ForeignFunctionInterface #-}` pragmas. |
| 114 | | - `-trust` - it is not safe to increase the set of trusted packages. |
| 115 | | - `-package`, `-package-id`, `-package-conf`, `-no-user-package-conf` - untrusted code should not have access to explicitly hidden packages. |
| 116 | | - `-package-name` - package name should be set only by trusted user |
| 117 | | - `-F`, `-cpp`, `-XCPP` - these options allow access to the local file system. |
| 118 | | - All of the linking options should be restricted (`-main-is`, `-l`__lib__, `-L`__dir__, `-framework`, etc.) |
| 119 | | - Several other options discussed below: `-XTemplateHaskell`, `-XStandaloneDeriving`, `-XGeneralizedNewtypeDeriving`. |
| 120 | | - The `RULES` and `SPECIALIZE` pragmas are also restricted and cannot appear below `{-# LANGUAGE Safe #-}` or when the `-XSafe` option has been specified on the command line. |
| 121 | | |
| 122 | | Note that `-ultrasafe` only enables Safe mode at the end of the command-line. Thus, one can supply one or more `-trust` options after `-ultrasafe` to allow ultrasafe code to do I/O. |
| 123 | | |
| 124 | | == Threats == |
| | 112 | 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. |
| | 113 | |
| | 114 | * '''`-XSafe`''' disables some options and extensions completely while for others it restricts them to appearing before `-XSafe` does. ('''Note:''' Incomplete) |
| | 115 | * '''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` |
| | 116 | * '''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), ` |
| | 117 | * '''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` |
| | 118 | * '''Not Sure''': `-D''symbol''`, `-U''symbol''`, `-I''dir''`, |
| | 119 | |
| | 120 | * '''`-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. |
| | 121 | * If `-XSafeImports` appears nothing changes since `-XTrustworthy` implies `-XSafeImports`. |
| | 122 | * 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. |
| | 123 | |
| | 124 | * '''`-XSafeImports`''' has no special interactions. `-XSafe`, `-XTrustworthy` and `-XSafeLanguage` are all compatible with it as they all imply `-XSafeImports` anyway. |
| | 125 | |
| | 126 | * '''`-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. |
| | 127 | |
| | 128 | |
| | 129 | == Safe Language Threats == |
| 287 | | * when I compile untrusted module `Ba`d 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 |
| 288 | | |
| 289 | | 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 to those restricted IO actions. And now we are back to something RIO like. |
| 290 | | |
| 291 | | 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 contructed by a bad guy. |
| | 303 | * 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 |
| | 304 | |
| | 305 | 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. |
| | 306 | |
| | 307 | 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. |