Changes between Version 30 and Version 31 of SafeHaskell


Ignore:
Timestamp:
Jan 19, 2011 8:22:29 AM (5 years ago)
Author:
simonpj
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • SafeHaskell

    v30 v31  
    2626
    2727The 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 == Ultra-safety ==
    30 
    31 '''SLPJ note'''. This entire subsection is new. See if you agree with it.  If you do, there'd be some knock-on effects.  Notably an ultra-safe module should have only ultrasafe imports.  And some of the later stuff about RIO would need adjusting.  '''End of SLPJ note'''.
    32 
    33 The safe dialect does not prevent use of the symbol `IO`. Nor does it prevent use of `foreign import`.  So this module is OK:
    34 {{{
    35 {-# LANGUAGE Safe #-}
    36 module Bad( deleteAllFiles ) where
    37   foreign import "deleteAllFiles" :: IO ()
    38 }}}
    39 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:
    40 {{{
    41 {-# LANGUAGE Safe #-}
    42 module Bad( RM(..), rm ) where
    43   foreign import "deleteAllFiles" :: IO ()
    44   data RM = RM (IO ())
    45   rm :: RM
    46   rm = RM deleteAllFiles
    47 }}}
    48 The flag (and LANGUAGE pragma) `UltraSafe` is just like `Safe` except that it also disables `foreign import`.  This strengtens the safety guarantee, by esuring that an `UltraSafe` module can construct IO actions only by composing together IO actions that it imports from trusted modules.  Note that `UltraSafe` does not disable the use of IO itself. For example this is fine:
    49 {{{
    50 {-# LANGUAGE UltraSafe #-}
    51 module OK( print2 ) where
    52   import IO( print )
    53   print2 :: Int -> IO ()
    54   print2 x = do { print x; print x }
    55 }}}
    5628
    5729
     
    284256In this case, the type of `Danger.runMe` will be `IO ()`.  However, because `-ultrasafe` implies `-distrust-all-packages`, the only modules `Danger` can import are trustable modules whose entire trust dependency set lies in the current package.  Let's say that `SafeIO` and `Danger` are the only two such modules.  We then know that the only IO actions `Danger.runMe` can directly execute are `rioReadFile` and `rioWriteFile`.
    285257
     258== Ultra-safety ==
     259
     260'''Note'''. This section concerns a possible extension/variant. 
     261
     262The safe dialect does not prevent use of the symbol `IO`. Nor does it prevent use of `foreign import`.  So this module is OK:
     263{{{
     264{-# LANGUAGE Safe #-}
     265module Bad( deleteAllFiles ) where
     266  foreign import "deleteAllFiles" :: IO ()
     267}}}
     268Hence, 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:
     269{{{
     270{-# LANGUAGE Safe #-}
     271module Bad( RM(..), rm ) where
     272  foreign import "deleteAllFiles" :: IO ()
     273  data RM = RM (IO ())
     274  rm :: RM
     275  rm = RM deleteAllFiles
     276}}}
     277The flag (and LANGUAGE pragma) `UltraSafe` is just like `Safe` except that it also disables `foreign import`.  This strengtens the safety guarantee, by esuring that an `UltraSafe` module can construct IO actions only by composing together IO actions that it imports from trusted modules.  Note that `UltraSafe` does not disable the use of IO itself. For example this is fine:
     278{{{
     279{-# LANGUAGE UltraSafe #-}
     280module OK( print2 ) where
     281  import IO( print )
     282  print2 :: Int -> IO ()
     283  print2 x = do { print x; print x }
     284}}}
     285
     286
    286287== References ==
    287288