Changes between Version 30 and Version 31 of SafeHaskell


Ignore:
Timestamp:
Jan 19, 2011 8:22:29 AM (3 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