lio 0.1.2 → 0.1.3

raw patch · 6 files changed

+549/−102 lines, 6 filesdep +QuickCheckdep +liodep +test-frameworkdep ~basedep ~dclabelPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: QuickCheck, lio, test-framework, test-framework-quickcheck2

Dependency ranges changed: base, dclabel

API changes (from Hackage documentation)

Files

• LIO/DCLabel.hs +16/−5
• LIO/Safe.hs +10/−0
• LIO/TCB.hs +231/−74
• examples/maskExample.hs +0/−19
• lio.cabal +19/−4
• tests/Tests.hs +273/−0

@@ -19,18 +19,16 @@                      -- * Renamed privileges                    , DCPriv, DCPrivTCB                      -- * Useful aliases for the LIO Monad-                   , DCLabeled, DC, evalDC, evalDCWithRoot +                   , DCLabeled, DC, evalDC, evalDCWithRoot, DCGate+                     -- * Public label+                   , lpub                    )where  import LIO.TCB  import LIO.Handle (evalWithRoot) -#if __GLASGOW_HASKELL__ >= 702-import safe Data.Typeable-#else import Data.Typeable-#endif  import DCLabel.Safe hiding ( Priv                            , bottom@@ -94,14 +92,20 @@                                          | pr == DCL.noPriv      = l `lub` g                                          | otherwise             = lr ++instance PrivDesc DCPrivTCB DCPriv where+  privDesc = priv+ -- -- Renaming --  -- | A @DCLabel@ category set. type DCCatSet = DCL.Component+ -- | A @DCLabel@ (untrusted) privilege. type DCPriv = DCL.Priv+ -- | A @DCLabel@ privilege. type DCPrivTCB = DCL.TCBPriv @@ -126,3 +130,10 @@ -- | Same as 'evalDC', but with support for filesystem. evalDCWithRoot ::  FilePath -> Maybe DCLabel -> DC a -> IO (a, DCLabel) evalDCWithRoot path ml act = evalWithRoot path ml act ()++-- | A DC Label gate+type DCGate = Gate DCLabel DCPriv++-- | Label corresponding to public data.+lpub :: DCLabel+lpub = newDC (<>) (<>)

@@ -11,6 +11,7 @@                  , Priv(..), noPrivs                  , getPrivileges, withPrivileges                  , withCombinedPrivs +                 , dropPrivileges                   , LIO, LabelState                  , evalLIO                  , getLabel, setLabelP@@ -19,6 +20,8 @@                  , label, labelP                  , unlabel, unlabelP                  , taintLabeled+                 , untaintLabeled, untaintLabeledP+                 , relabelP                  , toLabeled, toLabeledP, discard, discardP                  , taint, taintP                  , wguard, wguardP, aguard, aguardP@@ -26,12 +29,15 @@                  , LabelFault(..)                  , catchP, handleP, onExceptionP, bracketP                  , evaluate+                 , PrivDesc+                 , Gate, mkGate, mkGateP, callGate                  ) where  import LIO.TCB ( Label(..)                , Priv(..), noPrivs                , getPrivileges, withPrivileges                , withCombinedPrivs +               , dropPrivileges                 , LIO, LabelState                , evalLIO                , getLabel, setLabelP@@ -40,6 +46,8 @@                , label, labelP                , unlabel, unlabelP                , taintLabeled+               , untaintLabeled, untaintLabeledP+               , relabelP                , toLabeled, toLabeledP, discard, discardP                , taint, taintP                , wguard, wguardP, aguard, aguardP@@ -47,4 +55,6 @@                , LabelFault(..)                , catchP, handleP, onExceptionP, bracketP                , evaluate+               , PrivDesc+               , Gate, mkGate, mkGateP, callGate                )

@@ -1,7 +1,4 @@ {-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ < 704-{-# LANGUAGE SafeImports #-}-#endif #if __GLASGOW_HASKELL__ >= 704 {-# LANGUAGE Unsafe #-} #endif@@ -56,8 +53,11 @@                 -- * Basic Privilige Functions                 -- $privs                , Priv(..), noPrivs-               , getPrivileges, withPrivileges-               , withCombinedPrivs +               , getPrivileges+               , setPrivileges+               , withPrivileges+               , withCombinedPrivs+               , dropPrivileges                 -- * Labeled IO Monad (LIO)                -- $LIO                , LIO(..), LabelState@@ -72,6 +72,8 @@                , label, labelP                , unlabel, unlabelP                , taintLabeled+               , untaintLabeled, untaintLabeledP+               , relabelP                , toLabeled, toLabeledP, discard, discardP                -- ** LIO Guards                -- $guards@@ -89,6 +91,12 @@                , catchP, handleP                , onExceptionP, bracketP                , evaluate+               -- * Gates+               -- $gates+               , PrivDesc(..)+               , Gate(..)+               , mkGate, mkGateP+               , callGate                -- * Unsafe (TCB) Operations                -- ** Basic Label Functions                , PrivTCB, MintTCB(..)@@ -103,29 +111,22 @@                -- ** Labeled Exceptions                , catchTCB, OnExceptionTCB(..)                , ioTCB, rtioTCB+               -- ** Gates+               , mkGateTCB, callGateTCB                ) where -#if __GLASGOW_HASKELL__ >= 702-import safe Prelude hiding (catch)-import safe Control.Exception hiding (catch, handle, throw, throwIO,-                                 onException, block, unblock, evaluate)-import safe qualified Control.Exception as E-import safe Data.Monoid-import safe Data.Typeable-import safe Data.Functor-import safe Control.Applicative-import safe Text.Read (minPrec)-import safe LIO.MonadCatch-#else import Prelude hiding (catch)+import Control.Exception hiding (catch, handle, throw, throwIO,+                                 onException, block, unblock,+                                 evaluate, finally, mask) import qualified Control.Exception as E import Data.Monoid import Data.Typeable import Data.Functor+import Data.IORef import Control.Applicative import Text.Read (minPrec) import LIO.MonadCatch-#endif  import Control.Monad.Error import Control.Monad.State.Lazy hiding (put, get)@@ -437,13 +438,31 @@ -- @withPrivileges@ block. withPrivileges :: (LabelState l p s) => p -> LIO l p s a -> LIO l p s a withPrivileges p m = do-  s <- getTCB   p0 <- getPrivileges-  putTCB s { lioP = p `mappend` p0 }-  a <- m-  putTCB s { lioP = p0 }-  return a+  setPrivileges p+  -- restore privileges even if an exception is thrown+  m `finallyTCB` setPrivileges p0 +-- | Execute an 'LIO' action with the combination of the supplied+-- privileges (usually passed to @...P@ functions) and current+-- privileges.+withCombinedPrivs :: LabelState l p s => p -> (p -> LIO l p s a) -> LIO l p s a+withCombinedPrivs p0 io = do+  p1 <- getPrivileges+  io (p0 `mappend` p1)++-- | Set the underlying privileges. Although this function is not+-- unsafe, it is not exported by "LIO.Safe" as it provides a higher security+-- risk. Users are encouraged to use 'withPrivileges'.+setPrivileges :: (LabelState l p s) => p -> LIO l p s ()+setPrivileges p = do s <- getTCB+                     putTCB $ s { lioP = p }++-- | Drop all privileges. It is useful to remove all privileges when+-- executing some untrusted code withing a 'withPrivileges' block.+dropPrivileges :: (LabelState l p s) => LIO l p s ()+dropPrivileges = setPrivileges noPrivs+ -- | If the current label is @oldLabel@ and the current clearance is -- @clearance@, this function allows code to raise the label to -- any value @newLabel@ such that@@ -525,7 +544,7 @@ rtioTCB :: (LabelState l p s) => IO a -> LIO l p s a rtioTCB io = do   l <- getLabel-  ioTCB $ io `catch` (throwIO . (LabeledExceptionTCB l))+  ioTCB $ io `catch` (throwIO . LabeledExceptionTCB l)  --------------------------------------------------------------------- -- Labeled value ----------------------------------------------------@@ -562,7 +581,7 @@  -- | Trusted constructor that creates labeled values. labelTCB :: Label l => l -> a -> Labeled l a-labelTCB l a = LabeledTCB l a+labelTCB = LabeledTCB  -- | Within the 'LIO' monad, this function takes a 'Labeled' and returns -- the value.  Thus, in the 'LIO' monad one can say:@@ -602,6 +621,28 @@   return $ LabeledTCB (lub l la) a  +-- | Downgrades the label of a 'Labeled' as much as possible given the+-- current privilege.+untaintLabeled :: (LabelState l p s)+               => l -> Labeled l a -> LIO l p s (Labeled l a)+untaintLabeled = untaintLabeledP noPrivs++-- | Same as 'untaintLabeled' but combines the current privilege with the+-- supplied privilege when downgrading the label.+untaintLabeledP :: (LabelState l p s)+                => p -> l -> Labeled l a -> LIO l p s (Labeled l a)+untaintLabeledP p target lbld =+  relabelP p (lostar p (labelOf lbld) target) lbld++-- | Relabeles a @Labeled@ value if the given privilege combined+-- with the current privileges permits it.+relabelP :: (LabelState l p s)+        => p -> l -> Labeled l a -> LIO l p s (Labeled l a)+relabelP p' lbl (LabeledTCB la a) = withCombinedPrivs p' $ \p ->+   if leqp p lbl la && leqp p la lbl+     then return $ LabeledTCB lbl a+     else throwIO LerrPriv+ -- | @toLabeled@ is the dual of 'unlabel'.  It allows one to invoke -- computations that would raise the current label, but without -- actually raising the label.  Instead, the result of the@@ -621,47 +662,87 @@ -- one main use of clearance: to ensure that a @Labeled@ computed -- does not exceed a particular label. ----- If an exception is thrown a a @toLabeled@ block, the join of--- the exception label and supplied label will be used as the new--- label.  If the current label of the inner computation is above--- the supplied label, an exception (whose label will reflect this--- observatoin) is throw by @toLabeled@.+-- If an exception is thrown within a @toLabeled@ block, such that+-- the outer context is withing a 'catch', which is futher within+-- a @toLabeled@ block, infromation can be leaked. Consider the+-- following program that uses 'DCLabel's. (Note that 'discard' is+-- simply @toLabeled@ that throws throws the result away.) ----- WARNING: @toLabeled@ is susceptible to termination attacks.+--  > main = evalDC' $ do+--  >   lRef <- newLIORef lbot ""+--  >   hRef <- newLIORef ltop "secret" +--  >   -- brute force:+--  >   forM_ ["fun", "secret"] $ \guess -> do+--  >     stash <- readLIORef lRef+--  >     writeLIORef lRef $ stash ++ "\n" ++ guess ++ ":"+--  >     discard ltop $ do +--  >       catch ( discard ltop $ do+--  >                 secret <- readLIORef hRef+--  >                 when (secret == guess) $ throwIO . userError $ "got it!"+--  >             ) (\(e :: IOError) -> return ())+--  >       l <- getLabel+--  >       when (l == lbot) $ do stash <- readLIORef lRef+--  >                             writeLIORef lRef $ stash ++ "no!"+--  >   readLIORef lRef+--  >     where evalDC' act = do (r,l) <- evalDC act+--  >                            putStrLn r+--  >                            putStrLn $ "label = " ++ prettyShow l --+--  The output of the program is:+--+--  > $ ./new+--  > +--  > fun:no!+--  > secret:+--  > label = <True , False>+--+-- Note that the current label is 'lbot' (which in DCLabels is+-- @<True , False>@), and the secret is leaked. The fundamental issue+-- is that the outer 'discard' allows for the current label to remain+-- low even though the 'catch' raised the current label when the+-- secret was found (and thus exception was throw). As a consequence,+-- 'toLabeled' catches all exceptions, and returns a 'Labeled'+-- value that may have a labeled exception as wrapped by @throw@.+-- All exceptions within the outer computation, including+-- IFC violation attempts, are essentially rethrown when performing+-- an 'unlabel'.+--+-- DEPRECATED: @toLabeled@ is susceptible to termination attacks.+-- toLabeled :: (LabelState l p s)           => l -- ^ Label of result and upper bound on                --  inner-computations' observation           -> LIO l p s a -- ^ Inner computation           -> LIO l p s (Labeled l a) toLabeled = toLabeledP noPrivs-{-# WARNING toLabeled "toLabeled is susceptible to termination attacks" #-}+{-# DEPRECATED toLabeled "toLabeled is susceptible to termination attacks" #-}  -- | Same as 'toLabeled' but allows one to supply a privilege object -- when comparing the initial and final label of the computation. ----- WARNING: @toLabeledP@ is susceptible to termination attacks.+-- DEPRECATED: @toLabeledP@ is susceptible to termination attacks. -- toLabeledP :: (LabelState l p s)            => p -> l -> LIO l p s a -> LIO l p s (Labeled l a) toLabeledP p' l m = withCombinedPrivs p' $ \p -> do   aguardP p l   save_s <- getTCB-  ---  res <- (Right <$> m) `catchTCB` (return . Left .  (lubErr l))+  res <- (Right <$> m) `catchTCB` (return . Left . lubErr l)   s <- getTCB   let lastL = lioL s   putTCB s { lioL = lioL save_s, lioC = lioC save_s, lioP = lioP save_s }-  if leqp p lastL l-    then either (ioTCB . throwIO) (return . LabeledTCB l) res-    else let l' = lub lastL l-         in ioTCB . throwIO . mkErr . (lub l') $ either getELabel (const l') res+  return . labelTCB l $+    if leqp p lastL l+      then either E.throw id res+      else let l' = lub lastL l+           in E.throw . mkErr . lub l' $ either getELabel (const l') res     where mkErr le = LabeledExceptionTCB le $ toException LerrLow           lubErr lnew (LabeledExceptionTCB le e) =                   LabeledExceptionTCB (le `lub` lnew) e           getELabel (LabeledExceptionTCB le _) = le-{-# WARNING toLabeledP "toLabeledP is susceptible to termination attacks" #-}+{-# DEPRECATED toLabeledP "toLabeledP is susceptible to termination attacks" #-} + -- | Executes a computation that would raise the current label, but -- discards the result so as to keep the label the same.  Used when -- one only cares about the side effects of a computation.  For@@ -672,22 +753,19 @@ --   discard ltop $ 'hputStrLn' log_handle \"Log message\" -- @ ----- to create a log message without affecting the current label.  (Of--- course, if @log_handle@ is closed and this throws an exception, it--- may not be possible to catch the exception within the 'LIO' monad--- without sufficient privileges--see 'catchP'.)+-- to create a log message without affecting the current label.  ----- WARNING: discard is susceptible to termination attacks.+-- DEPRECATED: discard is susceptible to termination attacks. -- discard :: (LabelState l p s) =>  l -> LIO l p s a -> LIO l p s () discard = discardP noPrivs-{-# WARNING discard "discard is susceptible to termination attacks" #-}+{-# DEPRECATED discard "discard is susceptible to termination attacks" #-}  -- | Same as 'discard', but uses privileges when comparing initial and -- final label of the computation. discardP :: (LabelState l p s) => p -> l -> LIO l p s a -> LIO l p s ()-discardP p l m = toLabeledP p l m >> return ()-{-# WARNING discardP "discardP is susceptible to termination attacks" #-}+discardP p l m = void $ toLabeledP p l m+{-# DEPRECATED discardP "discardP is susceptible to termination attacks" #-}   @@ -919,8 +997,19 @@                 => ((forall a. LIO l p s a -> LIO l p s a) -> LIO l p s b)                 -> LIOstate l p s                 -> (forall a. IO a -> IO a) -> IO (b, LIOstate l p s)-            -- this is a little bit like magic to make types work:-            fun f s = \g -> unLIO (f (\x -> rtioTCB $ g (fst <$> unLIO x s))) s+            -- a little bit of magic:+            fun lioMask s = \ioRestore ->+              unLIO' s $ lioMask $ \lioRestore -> do+                            s'  <- getTCB+                            ref <- ioTCB $ newIORef s'+                            res <- ioTCB $ ioRestore $ do+                              (a,s'') <- unLIO lioRestore s'+                              writeIORef ref s''+                              return a+                            s'' <- ioTCB $ readIORef ref+                            putTCB s''+                            return res+            unLIO' s act = unLIO act s     -- | It is not possible to catch pure exceptions from within the 'LIO'     -- monad, but @throwIO@ wraps up an exception with the current label,     -- so that it can be caught with 'catch' or 'catchP'..@@ -935,29 +1024,22 @@     --     catch = catchP noPrivs - -- | Catches an exception, so long as the label at the point where the -- exception was thrown can flow to the label at which @catchP@ is -- invoked, modulo the privileges specified.  Note that the handler--- receives an extra first argument (before the exception), which--- is the label when the exception was thrown.+-- raises the current label to the joint of the current label and +-- exception label. catchP :: (Exception e, LabelState l p s)        => p   -- ^ Privileges with which to downgrade exception        -> LIO l p s a        -- ^ Computation to run        -> (e -> LIO l p s a) -- ^ Exception handler        -> LIO l p s a        -- ^ Result of computation or handler catchP p' io handler = withCombinedPrivs p' $ \p -> do-  s <- getTCB   clr <- getClearance-  (a, s') <- ioTCB $ do-    (unLIO io s) `catch` (\e@(LabeledExceptionTCB le se) ->+  io `catchTCB` (\e@(LabeledExceptionTCB le se) ->       case fromException se of-        Nothing -> throwIO e-        Just e' -> if le `leq` clr-                     then unLIO (taintP p le >> handler e') s-                     else throwIO e)-  putTCB s'-  return a+        Just e' | le `leq` clr -> taintP p le >> handler e'+        _                      -> throwIO e)  -- | Trusted catch functin. catchTCB :: (LabelState l p s)@@ -1015,6 +1097,11 @@ -- of these methods. class (MonadCatch m) => OnExceptionTCB m where     onExceptionTCB :: m a -> m b -> m a+    finallyTCB     :: m a -> m b -> m a+    finallyTCB a b = mask $ \restore -> do+                       r <- restore a `onExceptionTCB` b+                       _ <-  b+                       return r     bracketTCB     :: m a -> (a -> m c) -> (a -> m b) -> m b     bracketTCB     = genericBracket onExceptionTCB @@ -1023,22 +1110,92 @@     bracketTCB     = E.bracket  instance (LabelState l p s) => OnExceptionTCB (LIO l p s) where-    onExceptionTCB m cleanup = mkLIO $ \s ->-      unLIO m s `catch` (\e -> unLIO cleanup s >> throwIO (e :: SomeException))+    onExceptionTCB io cleanup = io `catchTCB` (\e -> do void cleanup +                                                        ioTCB $ E.throwIO e)  instance (LabelState l p s) => MonadError IOException (LIO l p s) where     throwError = throwIO     catchError = catch +---------------------------------------------------------------------+-- Gates ------------------------------------------------------------+--------------------------------------------------------------------- ------ Misc helper---+{- $gates --- | Execute an 'LIO' action with the combination of the supplied--- privileges (usually passed to @...P@ functions) and current--- privileges.-withCombinedPrivs :: LabelState l p s => p -> (p -> LIO l p s a) -> LIO l p s a-withCombinedPrivs p0 io = do-  p1 <- getPrivileges-  io (p0 `mappend` p1)+LIO provides a basic implementation of /gates/, useful in providing+controlled RPC-like services where the client and service provider are+in mutual distrust. ++A service provider uses 'mkGate' to create a gate data type 'Gate l d+a'.  The type parameter @l@ indicates the 'Label' type used to protect+the gate computation; the label value @ is bounded by the current+label and clearance at the time of creation.  The gate computation+itself is of type @d -> a@, where @d@, an instance of 'PrivDesc'.+Since gates are invoked with 'callGate', the service provider has the+guarantee that the client (the callee) owns the privileges+corresponding to the privilege description @d@. In effect, this allows+a client to \"prove\" to the service provider that they own certain+privileges without entrusting the service with its privileges.+The gate computation can analyze this privilege description when+determining the result.++A client invokes a gate with 'callGate', which unlabels the gate+computation and applies the gate computation to the description of the+supplied privilege.++-}++-- | Class used to describe privileges in a meaningful manner.+class (PrivTCB p, Show d) => PrivDesc p d | p -> d where+  -- | Get privilege description+  privDesc :: p -> d++-- | A Gate is a wrapper for a 'Labeled' type.+newtype Gate l d a = Gate (Labeled l (d -> a))+  deriving (Typeable)++-- | Create a gate given a gate label and computation.+-- The label of the gate must be bounded by the current label and+-- clearance.+mkGate :: (LabelState l p s, PrivDesc p d)+       => l                   -- ^ Label of gate+       -> (d -> a)            -- ^ Gate omputation+       -> LIO l p s (Gate l d a)+mkGate = mkGateP noPrivs++-- | Same as 'mkGate', but uses privileges when making the gate.+mkGateP :: (LabelState l p s, PrivDesc p d)+        => p                   -- ^ Privileges+        -> l                   -- ^ Label of gate+        -> (d -> a)            -- ^ Gate computation+        -> LIO l p s (Gate l d a)+mkGateP p l f = Gate <$> labelP p l f++-- | Same as 'mkGate', but ignores IFC.+mkGateTCB :: (LabelState l p s, PrivDesc p d)+          => l            -- ^ Label of gate+          -> (d -> a)     -- ^ Gate action+          -> Gate l d a+mkGateTCB l f = Gate (labelTCB l f)++-- | Given a labeled gate and privilege, execute the gate computation.+-- The current label is raised to the join of the gate and current+-- label, clearance permitting. It is important to note that+-- @callGate@ invokes the gate computation with the privilege+-- description and /not/ the actual privilege.+callGate :: (LabelState l p s, PrivDesc p d)+         => Gate l d a   -- ^ Gate+         -> p            -- ^ Privilege used to unlabel gate action+         -> LIO l p s a+callGate (Gate lf) p = withCombinedPrivs p $ \pAmp -> do+  f <- unlabelP pAmp lf+  return $ f (privDesc p)++-- | Same as 'callGate', but does not raise label in accessing the+-- gate computation.+callGateTCB :: (LabelState l p s, PrivDesc p d)+            => Gate l d a   -- ^ Gate+            -> p            -- ^ Privilege used to unlabel gate action+            -> a+callGateTCB (Gate lf) p = unlabelTCB lf $ privDesc p

@@ -1,19 +0,0 @@-import LIO.TCB-import LIO.DCLabel-import DCLabel.Safe-import Control.Concurrent-import Control.Monad---main = do-  tid <- forkIO $ do-    _ <- evalDC $ -      mask $ \restore -> do-        forM_ [1..10000] (ioTCB . print)-        ioTCB . putStrLn  $ "bye!"-        restore (return ())-        ioTCB . putStrLn  $ "DONE!"-    return ()-  threadDelay 100000-  throwTo tid (userError "WOO")-  

@@ -1,5 +1,5 @@ Name:           lio-Version:        0.1.2+Version:        0.1.3 build-type:     Simple License:        GPL License-File:   LICENSE@@ -27,7 +27,7 @@         The library depends on the @DCLabel@ module. You can read more on         DC Labels here:         <http://www.scs.stanford.edu/~deian/dclabels/>.-Cabal-Version:  >= 1.6+Cabal-Version:  >= 1.8  Build-Type:     Configure Extra-source-files:@@ -37,7 +37,6 @@     examples/LambdaChair/Main.hs     examples/LambdaChair/Safe.hs     examples/fsExample.hs-    examples/maskExample.hs     examples/waitAndCatch.hs     configure.ac     configure@@ -47,7 +46,7 @@  Source-repository head   Type:     git-  Location: http://www.scs.stanford.edu/~deian/lio.git+  Location: http://www.github.com/scslab/lio.git   Library@@ -96,3 +95,19 @@     Includes: HsTmp.h     Install-Includes: HsTmp.h HsTmpConfig.h     C-Sources:	cbits/HsTmp.c++test-suite tests+  type: exitcode-stdio-1.0+  hs-source-dirs: tests+  main-is: Tests.hs++  ghc-options:+    -Wall -threaded -rtsopts++  build-depends:+    QuickCheck,+    base,+    dclabel,+    lio,+    test-framework,+    test-framework-quickcheck2

@@ -0,0 +1,273 @@+{-# LANGUAGE OverloadedStrings #-}+{-# OPTIONS_GHC -fno-warn-orphans #-}+module Main (main) where++import Prelude hiding (catch)+import Test.Framework (Test, defaultMain, testGroup)+import Test.Framework.Providers.QuickCheck2 (testProperty)++import Test.QuickCheck hiding (label)+import Test.QuickCheck.Monadic++import Data.List (tails)+import Data.Functor ((<$>))+import Data.IORef++import LIO.TCB+import LIO.DCLabel+import DCLabel.TCB+import DCLabel.PrettyShow++import Control.Monad (liftM, void, forM_)+import Control.Exception (SomeException(..))+import Control.Concurrent++import System.IO.Unsafe++instance Arbitrary Principal where +     arbitrary = do p <- oneof $ map return ["A", "B", "C", "D"]+                    return $ principal (p :: String)+++instance Arbitrary Disj where +     arbitrary = sized disjunction +                 where disjunction 0 = return $ MkDisj { disj = [] }+                       disjunction n = do a  <- arbitrary+                                          m  <- choose (0, n-1) +                                          djs <- disjunction m+                                          return $ MkDisj $ a:(disj djs)     +++instance Arbitrary Conj where +     arbitrary = sized conjunction +                 where conjunction 0 = oneof +                        [ return $ MkConj { conj = [] }+                        , return $ MkConj { conj = [MkDisj []] }+                        , return $ MkConj { conj = [MkDisj [], MkDisj []] }+                        ] +                       conjunction n = do a  <- arbitrary+                                          m  <- choose (0, n-1) +                                          cjs <- conjunction m+                                          return $ MkConj $ a:(conj cjs)     +     shrink (MkConj ls) = [MkConj ll | l <- tails ls, ll <- shrink l]++instance Arbitrary Component where+  arbitrary = do m <- choose (0, 1) :: Gen Int+                 if m==0 then mkArbLbl arbitrary+			 else return MkComponentAll+    where mkArbLbl :: Gen Conj -> Gen Component+          mkArbLbl = liftM MkComponent++instance Arbitrary DCLabel where+  arbitrary = do s <- arbitrary+                 i <- arbitrary +                 return $ MkDCLabel { secrecy = s, integrity = i }++instance Arbitrary TCBPriv where+  arbitrary = do p <- arbitrary+                 return $ MkTCBPriv p++--+--+--++main :: IO ()+main = defaultMain tests++--+--+--++monadicDC :: PropertyM DC a -> Property+monadicDC (MkPropertyM m) =+ property $ unsafePerformIO <$> dorun <$> m (const (return (return (property True))))+  where dorun x =fst <$> evalDC x++-- Helper function+printLIOState :: String -> DC ()+printLIOState m = do+  s <- getTCB+  ioTCB . putStrLn $ "\n" ++ m ++ ":\nLabel = " ++ (prettyShow $ lioL s ) +                          ++ "\nClear = " ++ (prettyShow $ lioC s ) +                          ++ "\nPrivs = " ++ (prettyShow $ lioP s ) ++--+--+--++tests :: [Test]+tests = [+    testGroup "label" [+      testProperty+        "unlabel raises current label"+        prop_label_unlabel+    ]+  , testGroup "withPrivileges" [+      testProperty+        "restores privileges: nop" $+        prop_withPrivileges_restores_privs (return ())+    , testProperty+        "restores privileges: exception" $+        prop_withPrivileges_restores_privs (throwIO . userError $ "ex")+    , testProperty+        "restores privileges: IFC violation" $+        prop_withPrivileges_restores_privs (do taint ltop+                                               void $ label lbot '1')+    , testProperty+        "does not escallate privileges"+        prop_withPrivileges_no_escalate +    ]+  , testGroup "catch" [+      testProperty+        "does not untaint computation: id" $+        prop_catch_preserves_taint (const id)+    , testProperty+        "does not untaint computation: withPrivileges" $+        prop_catch_preserves_taint withPrivileges+    , testProperty+        "does not untaint computation: toLabeled" $+        prop_catch_preserves_taint withPrivileges+    ]+  , testGroup "onException" [+      testProperty+        "does not untaint computation: id" $+        prop_onException_preserves_taint (const id)+    , testProperty+        "does not untaint computation: withPrivileges" $+        prop_onException_preserves_taint withPrivileges+    , testProperty+        "does not untaint computation: toLabeled" $+        prop_onException_preserves_taint withPrivileges+    ]+  , testGroup "mask" [+      testProperty+        "does not untaint computation: id" $+        prop_mask_preserves_taint (const id)+    , testProperty+        "does not untaint computation: withPrivileges" $+        prop_mask_preserves_taint withPrivileges+    , testProperty+        "does not untaint computation: toLabeled" $+        prop_mask_preserves_taint withPrivileges+    , testProperty+        "restore allows throwTo exceptions" $+        prop_mask_correct  True+    , testProperty+        "mask without restore ignores throwTo exceptions" $+        prop_mask_correct  False+    ]+  ]++--+-- label/unlabe related+-- ++-- NOTE: we assume that the initial label is bottom and initial+-- clearance is top++-- | Check that the current label is raised when unlabeling a labeled value+prop_label_unlabel :: Property+prop_label_unlabel = monadicDC $ do+  l    <- pick (arbitrary :: Gen DCLabel)+  x    <- pick (arbitrary :: Gen Int)+  lx   <- run $ label l x+  x'   <- run $ unlabel lx+  lbl1 <- run $ getLabel+  assert $ lbl1 == l && x' == x+  +--+-- withPrivileges related+-- ++-- | Makesure that the privileges after a withPrivileges are restored+-- correctly+prop_withPrivileges_restores_privs :: DC () -> Property +prop_withPrivileges_restores_privs act = monadicDC $ do+  p0 <- pick (arbitrary :: Gen TCBPriv)+  p1 <- pick (arbitrary :: Gen TCBPriv)+  pre $ p0 /= p1+  run $ setPrivileges p0+  run $ (withPrivileges p1 act) `catchTCB` (\_ -> return ())+  p0' <- run $ getPrivileges+  assert $ p0 == p0'+++-- | Assert that the privileges in a withPrivileged block are only+-- what is provided.+prop_withPrivileges_no_escalate :: Property +prop_withPrivileges_no_escalate = monadicDC $ do+  p0 <- pick (arbitrary :: Gen TCBPriv)+  p1 <- pick (arbitrary :: Gen TCBPriv)+  pre $ p0 /= p1+  run $ setPrivileges p0+  p1' <- run $ withPrivileges p1 getPrivileges+  assert $ p1 == p1'++--+-- catch related+-- ++-- | Taint within catch does not get ignored+prop_catch_preserves_taint :: (TCBPriv -> DC DCLabel -> DC DCLabel) -> Property +prop_catch_preserves_taint wrapper = monadicDC $ do+  p <- pick (arbitrary :: Gen TCBPriv)+  l  <- pick (arbitrary :: Gen DCLabel)+  l' <- run $ catch (wrapper p $ do taint l+                                    _ <- throwIO (userError "u")+                                    getLabel+                    ) (\(SomeException _) -> getLabel)+  l'' <- run $ getLabel+  assert $ l == l' && l == l''++--+-- onException related+-- ++-- | onException does not ignore taint+prop_onException_preserves_taint :: (TCBPriv -> DC DCLabel -> DC DCLabel)+                                 -> Property +prop_onException_preserves_taint wrapper = monadicDC $ do+  p <- pick (arbitrary :: Gen TCBPriv)+  l  <- pick (arbitrary :: Gen DCLabel)+  l' <- run $ catch ((wrapper p $ do taint l+                                     _ <- throwIO (userError "u")+                                     getLabel+                     ) `onException`+                         (return ())) (\(SomeException _) -> getLabel)+  l'' <- run $ getLabel+  assert $ l == l' && l == l''++--+-- mask related+-- ++-- | onException does not ignore taint+prop_mask_preserves_taint :: (TCBPriv -> DC DCLabel -> DC DCLabel) -> Property +prop_mask_preserves_taint wrapper = monadicDC $ do+  p  <- pick (arbitrary :: Gen TCBPriv)+  l  <- pick (arbitrary :: Gen DCLabel)+  doRestore <- pick (arbitrary :: Gen Bool)+  l' <- run $ catch (mask $ \restore -> (if doRestore then restore else id) $+                       wrapper p $ do taint l+                                      _ <- throwIO (userError "u")+                                      getLabel+                    ) (\(SomeException _) -> getLabel)+  l'' <- run $ getLabel+  assert $ l == l' && l == l''+++-- | Check that if restore is used then a throwTo is not ignored.+-- Conversely, if restore is not used then a throwTo should not affect+-- the count.+prop_mask_correct :: Bool -> Property+prop_mask_correct doRestore = monadicIO $ do+  let count = 1000000+  ref <- run $ newIORef 1+  run $ do+    tid <- forkIO $ (\(SomeException _) -> return ()) `handle` (void $ evalDC $ +        mask $ \restore -> (if doRestore then restore else id) $ do+          forM_ [1..count] (ioTCB . writeIORef ref))+    threadDelay 10+    throwTo tid (userError "kill")+  res <- run $ readIORef ref+  assert $ if doRestore then res < count else res == count