Changes between Version 19 and Version 20 of SafeHaskell

Timestamp:

01/14/11 03:43:16 (2 years ago)

Author:

simonpj

Comment:

--

SafeHaskell

@@ -17 +17 @@
 More specifically, there are two parts to the proposed extension:
 
- 1. A new GHC option (`-XSafe`) enabling a "Safe" dialect of Haskell in which GHC rejects any source code that might produce unsafe effects or otherwise subvert the type system.
+ 1. A new GHC option (`-XSafe`) enabling a "Safe" dialect of Haskell  in which GHC rejects any source code that might produce unsafe effects or otherwise subvert the type system.
 
  2. Another new GHC option (`-XTrustworthy`) indicating that, though a module may invoke unsafe functions internally, the set of exported symbols cannot be used in an unsafe way.  The `-XTrustworthy` option makes a small extension to the syntax of import statements, adding a `safe` keyword:
@@ -27 +27 @@
 == Safety Goal ==
 
-As long as no module compiled with `-XTrustworthy` contains a vulnerability, the Safe dialect's goal is to guarantee the following properties:
+As long as no module compiled with `-XTrustworthy` contains a vulnerability, the goal of the Safe dialect (ie code compiled with `-XSafe`) is to guarantee the following properties:
 
  * '''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).
@@ -37 +37 @@
 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.
 
-The safe dialect does not prevent use of the symbol `IO`. If an untrusted module exports an `IO` action, that action may have arbitrary side effects, regardless of the `-XSafe` option.  Hence, while an application A importing a safe but possibly malicious module M may safely invoke pure functions from M, it must avoid executing `IO` actions exported by M unless some other mechanism ensures those actions conform to A's security goal. (See `-ultrasafe` below for one such mechanism.)
+== Ultra-safety ==
+
+The safe dialect does not prevent use of the symbol `IO`. Nor does it prevent use of `foreign import`.  So this module is OK:
+{{{
+{-# LANGUAGE Safe #-}
+module Bad( deleteAllFiles ) where
+  foreign import "deleteAllFiles" :: IO ()
+}}}
+Hence, while an application A importing a safe but possibly malicious module M may safely invoke pure functions from M, it must avoid executing `IO` actions construted inside M unless some other mechanism ensures those actions conform to A's security goal.  Such actions may be hidden inside data structures:
+{{{
+{-# LANGUAGE Safe #-}
+module Bad( RM(..), rm ) where
+  foreign import "deleteAllFiles" :: IO ()
+  data RM = RM (IO ())
+  rm :: RM
+  rm = RM deleteAllFiles
+}}}
+ (See `-ultrasafe` below for one such mechanism.)
 
 == Module trust ==