Changes between Version 19 and Version 20 of SafeHaskell


Ignore:
Timestamp:
Jan 14, 2011 11:43:16 AM (5 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • SafeHaskell

    v19 v20  
    1717More specifically, there are two parts to the proposed extension:
    1818
    19  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.
     19 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.
    2020
    2121 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:
     
    2727== Safety Goal ==
    2828
    29 As long as no module compiled with `-XTrustworthy` contains a vulnerability, the Safe dialect's goal is to guarantee the following properties:
     29As 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:
    3030
    3131 * '''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).
     
    3737The 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.
    3838
    39 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.)
     39== Ultra-safety ==
     40
     41The safe dialect does not prevent use of the symbol `IO`. Nor does it prevent use of `foreign import`.  So this module is OK:
     42{{{
     43{-# LANGUAGE Safe #-}
     44module Bad( deleteAllFiles ) where
     45  foreign import "deleteAllFiles" :: IO ()
     46}}}
     47Hence, 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:
     48{{{
     49{-# LANGUAGE Safe #-}
     50module Bad( RM(..), rm ) where
     51  foreign import "deleteAllFiles" :: IO ()
     52  data RM = RM (IO ())
     53  rm :: RM
     54  rm = RM deleteAllFiles
     55}}}
     56 (See `-ultrasafe` below for one such mechanism.)
    4057
    4158== Module trust ==