diff --git a/LIO/DCLabel.hs b/LIO/DCLabel.hs --- a/LIO/DCLabel.hs +++ b/LIO/DCLabel.hs @@ -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 (<>) (<>) diff --git a/LIO/Safe.hs b/LIO/Safe.hs --- a/LIO/Safe.hs +++ b/LIO/Safe.hs @@ -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 ) diff --git a/LIO/TCB.hs b/LIO/TCB.hs --- a/LIO/TCB.hs +++ b/LIO/TCB.hs @@ -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 = +-- +-- Note that the current label is 'lbot' (which in DCLabels is +-- @@), 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 diff --git a/examples/maskExample.hs b/examples/maskExample.hs deleted file mode 100644 --- a/examples/maskExample.hs +++ /dev/null @@ -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") - diff --git a/lio.cabal b/lio.cabal --- a/lio.cabal +++ b/lio.cabal @@ -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: . -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 diff --git a/tests/Tests.hs b/tests/Tests.hs new file mode 100644 --- /dev/null +++ b/tests/Tests.hs @@ -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