lio 0.9.2.2 → 0.10.0.0

raw patch · 39 files changed

+1180/−3252 lines, 39 filesdep −SHAdep −binarydep −directorydep ~bytestringdep ~containersPVP ok

version bump matches the API change (PVP)

Dependencies removed: SHA, binary, directory, filepath, transformers, xattr, zlib

Dependency ranges changed: bytestring, containers

API changes (from Hackage documentation)

Files

• LIO.hs +15/−15
• LIO/Concurrent.hs +95/−141
• LIO/Concurrent/LMVar.hs +50/−55
• LIO/Concurrent/LMVar/TCB.hs +0/−109
• LIO/Concurrent/TCB.hs +0/−31
• LIO/Core.hs +87/−300
• LIO/DCLabel.hs +20/−29
• LIO/DCLabel/Core.hs +80/−37
• LIO/DCLabel/DSL.hs +69/−42
• LIO/DCLabel/Privs.hs +14/−36
• LIO/DCLabel/Privs/TCB.hs +0/−45
• LIO/DCLabel/Serialize.hs +0/−33
• LIO/Exception.hs +99/−0
• LIO/FS/TCB.hs +0/−266
• LIO/Gate.hs +0/−97
• LIO/Handle.hs +0/−549
• LIO/LIORef.hs +38/−35
• LIO/LIORef/TCB.hs +0/−94
• LIO/Label.hs +12/−31
• LIO/Labeled.hs +62/−245
• LIO/Labeled/TCB.hs +0/−52
• LIO/Privs.hs +155/−38
• LIO/Privs/TCB.hs +0/−57
• LIO/Run.hs +47/−0
• LIO/TCB.hs +130/−86
• LIO/TCB/Concurrent.hs +44/−0
• LIO/TCB/DCLabel.hs +22/−0
• LIO/TCB/LObj.hs +117/−0
• examples/LambdaChair/AliceCode.hs +0/−22
• examples/LambdaChair/BobCode.hs +0/−17
• examples/LambdaChair/LambdaChair.hs +0/−15
• examples/LambdaChair/LambdaChair/TCB.hs +0/−445
• examples/LambdaChair/Main.hs +0/−32
• examples/bracket.hs +0/−33
• examples/dclabel.hs +4/−4
• examples/fsExample.hs +0/−206
• examples/gate.hs +4/−4
• examples/waitAndCatch.hs +4/−4
• lio.cabal +12/−47

@@ -4,18 +4,18 @@ This is the main module to be included by code using the Labeled IO (LIO) library. This module exports the core library (documented in "LIO.Core"), with support for labeled values (documented in-"LIO.Labeled"), privileges (documented in "LIO.Privs"), and gates-(documented in "LIO.Gate").+"LIO.Labeled") and privileges (documented in "LIO.Privs"). -Certain symbols in the LIO library supersede variants in the-standard Haskell libraries.  Thus, depending on the modules-imported and functions used, you may wish to import LIO with-commands like these:+Certain symbols in the lio library, particularly those in+"LIO.Exception", use the same names as their 'IO' equivalents in the+system libraries.  Hence main modules that mostly include 'IO' code+and only need to invoke 'LIO' code should import "LIO.Run" (or+"LIO.DCLabel") to avoid polluting their namespaces. +Most code will need to use a particular label format, which needs to+be imported separately.  For instance:+ @- import Control.Exception hiding ( 'onException'-                                 , 'finally'-                                 , 'bracket')  import "LIO"  -- Import your favorite label format:  import "LIO.DCLabel"@@ -30,14 +30,14 @@  module LIO (      module LIO.Label+  , module LIO.Exception   , module LIO.Core   , module LIO.Labeled   , module LIO.Privs-  , module LIO.Gate   ) where -import           LIO.Label-import           LIO.Core-import           LIO.Labeled-import           LIO.Privs-import           LIO.Gate+import LIO.Core+import LIO.Exception+import LIO.Label+import LIO.Labeled+import LIO.Privs

@@ -24,53 +24,40 @@ -} module LIO.Concurrent (     LabeledResult-  , ThreadId, myThreadId   -- * Forking new threads-  , forkLIO, lForkP, lFork+  , lForkP, lFork, forkLIO   -- * Waiting on threads   , lWaitP, lWait   , trylWaitP, trylWait-  , threadDelay-  -- * Forcing computations (EXPERIMENTAL)-  , AsyncException(..)-  , lBracket, lBracketP+  , timedlWaitP, timedlWait+  -- * Labeled MVars+  , module LIO.Concurrent.LMVar   ) where  -import           Control.Monad-import           Control.Concurrent hiding ( myThreadId, threadDelay )-import qualified Control.Concurrent as C-import           Control.Exception ( toException-                                   , Exception-                                   , AsyncException(..))-                 -import           LIO.Label-import           LIO.Core-import           LIO.Labeled-import           LIO.Labeled.TCB-import           LIO.Privs-import           LIO.TCB-                 -import           LIO.Concurrent.TCB-import           LIO.Concurrent.LMVar-import           LIO.Concurrent.LMVar.TCB (tryTakeLMVarTCB, putLMVarTCB)+import qualified Control.Concurrent as IO+import qualified Control.Exception as IO+import Control.Monad+import Data.IORef +import LIO.Concurrent.LMVar+import LIO.Core+import LIO.Exception+import LIO.Label+import LIO.Privs+import LIO.TCB+import LIO.TCB.Concurrent --- | Get the 'ThreadId' of the calling thread.-myThreadId :: MonadLIO l m => m ThreadId-myThreadId = liftLIO $ ioTCB C.myThreadId  -- -- Fork -- --- | Execute an 'LIO' computation in a new lightweight thread. The--- 'ThreadId' of the newly created thread is returned.-forkLIO :: Label l => LIO l () -> LIO l ThreadId-forkLIO act = do+-- | Execute an 'LIO' computation in a new lightweight thread.+forkLIO :: LIO l () -> LIO l ()+forkLIO lio = do   s <- getLIOStateTCB-  ioTCB . forkIO . void $ tryLIO act s-+  ioTCB $ void $ IO.forkIO $ void $ runLIO lio s  -- | Labeled fork. @lFork@ allows one to invoke computations that -- would otherwise raise the current label, but without actually@@ -81,13 +68,13 @@ -- raise the current label. Of couse,  this can be postponed until the -- result is needed. ----- @lFork@ takes a label, which corresponds to the label of the result.--- It is require that this label is above the current label, and below--- the current clearance as enforced by the underlying 'guardAlloc'.--- Moreover, the supplied computation must not read anything more--- sensitive (i.e., with a label above the supplied label) ---  doing so--- will result in an exception (whose label will reflect this--- observation) being thrown. +-- @lFork@ takes a label, which corresponds to the label of the+-- result.  It is required that this label be between the current+-- label and clearance as enforced by a call to 'guardAlloc'.+-- Moreover, the supplied computation must not terminate with its+-- label above the result label; doing so will result in an exception+-- (whose label will reflect this observation) being thrown in the+-- thread reading the result. -- -- If an exception is thrown in the inner computation, the exception -- label will be raised to the join of the result label and original@@ -104,33 +91,30 @@       => l                -- ^ Label of result       -> LIO l a          -- ^ Computation to execute in separate thread       -> LIO l (LabeledResult l a) -- ^ Labeled result-lFork = lForkP NoPrivs+lFork = lForkP noPrivs  -- | Same as 'lFork', but the supplied set of priviliges are accounted -- for when performing label comparisons.-lForkP :: Priv l p-       => p -> l -> LIO l a -> LIO l (LabeledResult l a)-lForkP p l act = do-  -- Upperbound is between current label and clearance, asserted by-  -- 'newEmptyLMVarP', otherwise add: guardAllocP p l-  mv <- newEmptyLMVarP p l-  tid <- forkLIO $ do-    res      <- (Right `liftM` act) `catchTCB` (return . Left . taintError)-    endLabel <- getLabel-    putLMVarTCB mv $! -      let le = endLabel `upperBound` l-          m = "End label does not flow to specified upper bound"-          e = VMonitorFailure { monitorFailure = CanFlowToViolation-                              , monitorMessage = m }-      in if canFlowToP p endLabel l-           then res-           else Left $! LabeledExceptionTCB le (toException e)-  return $ LabeledResultTCB { lresThreadIdTCB = tid, lresResultTCB = mv }-    where -- raise the label of the exception to the join of the-          -- exception label and supplied lForkP upper bound-          taintError (LabeledExceptionTCB le e) =-            LabeledExceptionTCB (le `upperBound` l) e+lForkP :: PrivDesc l p =>+          Priv p -> l -> LIO l a -> LIO l (LabeledResult l a)+lForkP p l lio = do+  guardAllocP p l+  mv <- ioTCB IO.newEmptyMVar+  st <- ioTCB $ newIORef LResEmpty+  s0 <- getLIOStateTCB+  tid <- ioTCB $ IO.mask $ \unmask -> IO.forkIO $ do+    sp <- newIORef s0+    ea <- IO.try $ unmask $ unLIOTCB lio sp+    LIOState lEnd _ <- readIORef sp+    writeIORef st $ case ea of+      _ | not (lEnd `canFlowTo` l) -> LResLabelTooHigh lEnd+      Left e                       -> LResResult $ IO.throw $ makeCatchable e+      Right a                      -> LResResult a+    IO.putMVar mv ()+  return $ LabeledResultTCB tid l mv st ++ -- -- Wait --@@ -145,92 +129,62 @@ -- example if it violates clearance), the exception is rethrown by -- @lWait@. Similarly, if the thread reads values above the result label, -- an exception is thrown in place of the result.-lWait :: MonadLIO l m => LabeledResult l a -> m a-lWait = lWaitP NoPrivs+lWait :: Label l => LabeledResult l a -> LIO l a+lWait = lWaitP noPrivs  -- | Same as 'lWait', but uses priviliges in label checks and raises.-lWaitP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m a-lWaitP p m = do-  v <- readLMVarP p $ lresResultTCB m-  -- kill thread:-  liftLIO . ioTCB . killThread . lresThreadIdTCB $ m-  case v of-    Right x -> return x-    Left e  -> liftLIO $ unlabeledThrowTCB e+lWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l a+lWaitP p (LabeledResultTCB _ l mv st) = taintP p l >> go+  where go = ioTCB (readIORef st) >>= check+        check LResEmpty = ioTCB (IO.readMVar mv) >> go+        check (LResResult a) = return $! a+        check (LResLabelTooHigh lnew) = do+          modifyLIOStateTCB $ \s -> s {+            lioLabel = partDowngradeP p lnew (lioLabel s) }+          throwLIO ResultExceedsLabel + -- | Same as 'lWait', but does not block waiting for result.-trylWait :: MonadLIO l m => LabeledResult l a -> m (Maybe a)-trylWait = trylWaitP NoPrivs+trylWait :: Label l => LabeledResult l a -> LIO l (Maybe a)+trylWait = trylWaitP noPrivs  -- | Same as 'trylWait', but uses priviliges in label checks and raises.-trylWaitP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m (Maybe a)-trylWaitP p m = do-  let mvar = lresResultTCB m-  mv <- tryTakeLMVarP p mvar-  case mv of-    Just v -> do putLMVarP p mvar v-                 -- kill thread:-                 liftLIO . ioTCB . killThread . lresThreadIdTCB $ m-                 case v of-                   Right x -> return $! Just x-                   Left e  -> liftLIO $ unlabeledThrowTCB e-    _ -> return Nothing+trylWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l (Maybe a)+trylWaitP p (LabeledResultTCB _ rl _ st) =+  taintP p rl >> ioTCB (readIORef st) >>= check+  where check LResEmpty = return Nothing+        check (LResResult a) = return . Just $! a+        check (LResLabelTooHigh lnew) = do+          curl <- getLabel+          if canFlowToP p lnew curl+            then throwLIO ResultExceedsLabel+            else return Nothing  --- | Suspend current thread for a given number of microseconds.-threadDelay :: MonadLIO l m => Int -> m ()-threadDelay = liftLIO . ioTCB . C.threadDelay ------ Forcing computations-------- | Though in most cases using a 'LabeledResult' is sufficient, in--- certain scenarios it is desirable to produce a pure 'Labeled' value--- that is the result of other potentially sensitive values. As such, we--- provide @lBracket@.--- --- @lBracket@ is like 'lFork', but rather than returning a--- 'LabeledResult', it returns a 'Labeled' value. The key difference--- between the two is that @lBracket@ takes an additional parameter--- specifying the number of microseconds the inner computation will take.--- As such, @lBracket@ will block for the specified duration and the--- result of the inner computation be /forced/. That is, if the--- computation terminated /cleanly/, i.e., it did not throw an--- exception and it finished in the time specified, then 'Just' the--- result is returned, otherwise 'Nothing' is returned.------ Note that the original LIO (before version 0.9) included a similar--- \"primitive\" called @toLabeled@. We have chosen to call this--- @lBracket@ in part because it is a more descriptive name and to--- avoid confusion with the previous @toLabeled@ where time was not --- considered.-lBracket :: (MonadLIO l m)-          => l                -- ^ Label of result-          -> Int              -- ^ Duration of computation in microseconds-          -> LIO l a          -- ^ Computation to execute in separate thread-          -> m (Labeled l (Maybe a)) -- ^ Labeled result-lBracket = lBracketP NoPrivs+-- | Like 'lWait', with two differences.  First, a timeout is+-- specified and the thread is unconditionally killed after this+-- timeout (if it has not yet returned a value).  Second, if the+-- thread's result exceeds its label @timedWait@ and exceeds what the+-- calling thread can observe, consumes the whole timeout and throws a+-- 'ResultExceedsLabel' exception you can catch (i.e., it never raises+-- the label above the clearance).+timedlWait :: Label l => LabeledResult l a -> Int -> LIO l a+timedlWait = timedlWaitP noPrivs --- | Same as 'lBracket', but uses privileges when forking the new--- thread.-lBracketP :: (MonadLIO l m, Priv l p)-           => p                -- ^ Privileges-           -> l                -- ^ Label of result-           -> Int              -- ^ Duration of computation in microseconds-           -> LIO l a          -- ^ Computation to execute in separate thread-           -> m (Labeled l (Maybe a)) -- ^ Labeled result-lBracketP p l t act = do-  f <- liftLIO $ lForkP p l act-  threadDelay t-  force f-    where force m = do-            let mv = lresResultTCB m-            -- check to see if it wrote to MVar:-            -- kill thread:-            liftLIO . ioTCB . killThread . lresThreadIdTCB $ m-            v <- tryTakeLMVarTCB mv-            return . labelTCB l =<< case v of-              Just (Right x) -> return (Just x)-              _  -> return Nothing+-- | A version of 'timedlWait' that takes privileges.  The privileges+-- are used both to downgrade the result (if necessary), and to try+-- catching any 'ResultExceedsLabel' before the timeout period (if+-- possible).+timedlWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> Int -> LIO l a+timedlWaitP p lr@(LabeledResultTCB t _ mvb _) to = trylWaitP p lr >>= go+  where go (Just a) = return a+        go Nothing = do+          mvk <- ioTCB $ IO.newEmptyMVar+          tk <- ioTCB $ IO.forkIO $ IO.finally (IO.threadDelay to) $ do+            IO.putMVar mvk ()+            IO.throwTo t (UncatchableTCB IO.ThreadKilled)+          ioTCB $ IO.readMVar mvb+          trylWaitP p lr >>= maybe+            (ioTCB (IO.takeMVar mvk) >> throwLIO ResultExceedsLabel)+            (\a -> ioTCB (IO.killThread tk) >> return a)

@@ -40,31 +40,38 @@   , isEmptyLMVar, isEmptyLMVarP   ) where -import           LIO.Label-import           LIO.Core-import           LIO.Privs-import           LIO.Concurrent.LMVar.TCB+import Control.Concurrent.MVar +import LIO.Label+import LIO.Core+import LIO.Privs+import LIO.TCB+import LIO.TCB.LObj+ -- -- Creating labeled 'MVar's -- +-- | An @LMVar@ is a labeled synchronization variable (an 'MVar') that+-- can be used by concurrent threads to communicate.+type LMVar l a = LObj l (MVar a)+ -- | Create a new labeled MVar, in an empty state. Note that the supplied -- label must be above the current label and below the current clearance. -- An exception will be thrown by the underlying 'guardAlloc' if this is -- not the case.-newEmptyLMVar :: MonadLIO l m+newEmptyLMVar :: Label l               => l                -- ^ Label of @LMVar@-              -> m (LMVar l a)    -- ^ New mutable location-newEmptyLMVar = newEmptyLMVarP NoPrivs+              -> LIO l (LMVar l a)    -- ^ New mutable location+newEmptyLMVar l = guardAlloc l >> ioTCB (LObjTCB l `fmap` newEmptyMVar)  -- | Same as 'newEmptyLMVar' except it takes a set of privileges which -- are accounted for in comparing the label of the MVar to the current -- label and clearance.-newEmptyLMVarP :: (MonadLIO l m, Priv l p) => p -> l -> m (LMVar l a)+newEmptyLMVarP :: PrivDesc l p => Priv p -> l -> LIO l (LMVar l a) newEmptyLMVarP p l = do   guardAllocP p l-  newEmptyLMVarTCB l+  ioTCB $ LObjTCB l `fmap` newEmptyMVar  -- | Create a new labeled MVar, in an filled state with the supplied -- value. Note that the supplied label must be above the current label@@ -73,15 +80,15 @@          => l                       -- ^ Label of @LMVar@          -> a                       -- ^ Initial value of @LMVar@          -> LIO l (LMVar l a)       -- ^ New mutable location-newLMVar = newLMVarP NoPrivs+newLMVar l a = guardAlloc l >> ioTCB (LObjTCB l `fmap` newMVar a)  -- | Same as 'newLMVar' except it takes a set of privileges which are -- accounted for in comparing the label of the MVar to the current label -- and clearance.-newLMVarP :: (MonadLIO l m, Priv l p) => p -> l -> a -> m (LMVar l a)+newLMVarP :: PrivDesc l p => Priv p -> l -> a -> LIO l (LMVar l a) newLMVarP p l a = do   guardAllocP p l-  newLMVarTCB l a+  ioTCB $ LObjTCB l `fmap` newMVar a  -- -- Take 'LMVar'@@ -97,28 +104,24 @@ -- 'guardWrite' will throw an exception if any of the IFC checks fail. -- If the Finally, like 'MVars' if the 'LMVar' is empty, @takeLMVar@ -- blocks.-takeLMVar :: MonadLIO l m => LMVar l a -> m a-takeLMVar = takeLMVarP NoPrivs+takeLMVar :: Label l => LMVar l a -> LIO l a+takeLMVar = blessTCB takeMVar  -- | Same as 'takeLMVar' except @takeLMVarP@ takes a privilege object -- which is used when the current label is raised.-takeLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> m a-takeLMVarP p m = do-  guardWriteP p (labelOf m)-  takeLMVarTCB m+takeLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l a+takeLMVarP = blessPTCB takeMVar  -- | Non-blocking version of 'takeLMVar'. It returns @Nothing@ if the -- 'LMVar' is empty, otherwise it returns @Just@ value, emptying the -- 'LMVar'.-tryTakeLMVar :: MonadLIO l m => LMVar l a -> m (Maybe a)-tryTakeLMVar = tryTakeLMVarP NoPrivs+tryTakeLMVar :: Label l => LMVar l a -> LIO l (Maybe a)+tryTakeLMVar = blessTCB tryTakeMVar  -- | Same as 'tryTakeLMVar', but uses priviliges when raising current -- label.-tryTakeLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> m (Maybe a)-tryTakeLMVarP p m = do-  guardWriteP p (labelOf m)-  tryTakeLMVarTCB m+tryTakeLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l (Maybe a)+tryTakeLMVarP = blessPTCB tryTakeMVar  -- -- Put 'LMVar'@@ -137,42 +140,38 @@          => LMVar l a   -- ^ Source 'LMVar'          -> a           -- ^ New value          -> LIO l ()-putLMVar = putLMVarP NoPrivs+putLMVar = blessTCB putMVar  -- | Same as 'putLMVar' except @putLMVarP@ takes a privilege object -- which is used when the current label is raised.-putLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> a -> m ()-putLMVarP p m a = do-  guardWriteP p (labelOf m)-  putLMVarTCB m a+putLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l ()+putLMVarP = blessPTCB putMVar  -- | Non-blocking version of 'putLMVar'. It returns @True@ if the -- 'LMVar' was empty and the put succeeded, otherwise it returns @False@.-tryPutLMVar :: MonadLIO l m => LMVar l a -> a -> m Bool-tryPutLMVar = tryPutLMVarP NoPrivs+tryPutLMVar :: Label l => LMVar l a -> a -> LIO l Bool+tryPutLMVar = blessTCB tryPutMVar  -- | Same as 'tryPutLMVar', but uses privileges when raising current label.-tryPutLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> a -> m Bool-tryPutLMVarP p m x = do-  guardWriteP p (labelOf m)-  tryPutLMVarTCB m x+tryPutLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l Bool+tryPutLMVarP = blessPTCB tryPutMVar  -- -- Read 'LMVar' -- --- | Combination of 'takeLMVar' and 'putLMVar'. Read the value, and just--- put it back. As specified for 'readMVar', this operation is atomic--- iff there is no other thread calling 'putLMVar' for this 'LMVar'.-readLMVar :: MonadLIO l m => LMVar l a -> m a-readLMVar = readLMVarP NoPrivs+-- | Combination of 'takeLMVar' and 'putLMVar'. Read the value, and+-- just put it back. This operation is not atomic, and can can result+-- in unexpected outcomes if another thread is simultaneously calling+-- a function such as 'putLMVar', 'tryTakeLMVarP', or 'isEmptyLMVar'+-- for this 'LMVar'.+readLMVar :: Label l => LMVar l a -> LIO l a+readLMVar = blessTCB readMVar  -- | Same as 'readLMVar' except @readLMVarP@ takes a privilege object -- which is used when the current label is raised.-readLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> m a-readLMVarP p m = do-  guardWriteP p (labelOf m)-  readLMVarTCB m+readLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l a+readLMVarP = blessPTCB readMVar  -- -- Swap 'LMVar'@@ -189,14 +188,12 @@           => LMVar l a          -- ^ Source @LMVar@           -> a                  -- ^ New value           -> LIO l a            -- ^ Taken value-swapLMVar = swapLMVarP NoPrivs+swapLMVar = blessTCB swapMVar  -- | Same as 'swapLMVar' except @swapLMVarP@ takes a privilege object -- which is used when the current label is raised.-swapLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> a -> m a-swapLMVarP p m x = do-  guardWriteP p (labelOf m)-  swapLMVarTCB m x+swapLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l a+swapLMVarP = blessPTCB swapMVar  -- -- Check state of 'LMVar'@@ -208,11 +205,9 @@ -- label and the current label. Note that this function only returns a -- snapshot of the state and does not modify it -- hence the -- underlying guard is 'taint' and not 'guardWrite'.-isEmptyLMVar :: MonadLIO l m => LMVar l a -> m Bool-isEmptyLMVar = isEmptyLMVarP NoPrivs+isEmptyLMVar :: Label l => LMVar l a -> LIO l Bool+isEmptyLMVar = blessTCB isEmptyMVar  -- | Same as 'isEmptyLMVar', but uses privileges when raising current label.-isEmptyLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> m Bool-isEmptyLMVarP p m = do-  taintP p (labelOf m)-  isEmptyLMVarTCB m+isEmptyLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l Bool+isEmptyLMVarP = blessPTCB isEmptyMVar

@@ -1,109 +0,0 @@-{-# LANGUAGE Unsafe #-}-{-|--This module implements the core of labeled 'MVars's in the 'LIO ad.-to "Control.Concurrent.MVar", but the operations take place in the-'LIO' monad.  The types and functions exported by this module are-strictly TCB and do not perform any information flow checks. The-external, safe interface is provided and documented in-"LIO.Concurrent.LMVar".---}-module LIO.Concurrent.LMVar.TCB (-    LMVar(..)-  -- * Creating labeled 'MVar's-  , newEmptyLMVarTCB, newLMVarTCB-  -- * Take 'LMVar'-  , takeLMVarTCB, tryTakeLMVarTCB-  -- * Put 'LMVar'-  , putLMVarTCB, tryPutLMVarTCB-  -- * Read 'LMVar'-  , readLMVarTCB-  -- * Swap 'LMVar'-  , swapLMVarTCB-  -- * Check state of 'LMVar'-  , isEmptyLMVarTCB-  ) where--import           Control.Concurrent.MVar-                 -import           LIO.Label-import           LIO.Core-import           LIO.TCB---- | An @LMVar@ is a labeled synchronization variable (an 'MVar') that--- can be used by concurrent threads to communicate.-data LMVar l a = LMVarTCB { labelOfLMVar :: !l-                            -- ^ Label of MVar.-                          , unlabelLMVarTCB :: MVar a-                            -- ^ Access the underlying 'MVar', ignoring IFC.-                          }--instance LabelOf LMVar where-  labelOf = labelOfLMVar------- Creating labeled 'MVar's------- | Trusted function used to create an empty @LMVar@, ignoring IFC.-newEmptyLMVarTCB :: MonadLIO l m => l -> m (LMVar l a)-newEmptyLMVarTCB l = do-  m <- liftLIO . ioTCB $ newEmptyMVar-  return $ LMVarTCB l m---- | Trusted function used to create an @LMVar@ with the supplied--- value, ignoring IFC.-newLMVarTCB :: MonadLIO l m => l -> a -> m (LMVar l a)-newLMVarTCB l a = do-  m <- liftLIO . ioTCB $ newMVar a-  return $ LMVarTCB l m------- Take 'LMVar'------- | Read the contents of an 'LMVar', ignoring IFC.-takeLMVarTCB :: MonadLIO l m => LMVar l a -> m a-takeLMVarTCB (LMVarTCB _ m) = liftLIO . ioTCB $ takeMVar m---- | Same as 'tryTakeLMVar', but ignorses IFC.-tryTakeLMVarTCB :: MonadLIO l m => LMVar l a -> m (Maybe a)-tryTakeLMVarTCB (LMVarTCB _ m) = liftLIO . ioTCB $ tryTakeMVar m------- Put 'LMVar'------- | Put a value into an 'LMVar', ignoring IFC.-putLMVarTCB :: MonadLIO l m => LMVar l a -> a -> m ()-putLMVarTCB (LMVarTCB _ m) a = liftLIO . ioTCB $ putMVar m a---- | Same as 'tryPutLMVar', but ignorses IFC.-tryPutLMVarTCB :: MonadLIO l m => LMVar l a -> a -> m Bool-tryPutLMVarTCB (LMVarTCB _ m) x = liftLIO . ioTCB $ tryPutMVar m x-------- Read 'LMVar'------- | Trusted function used to read (take and put) an 'LMVar', ignoring IFC.-readLMVarTCB :: MonadLIO l m => LMVar l a -> m a-readLMVarTCB (LMVarTCB _ m) = liftLIO . ioTCB $ readMVar m------- Swap 'LMVar'------- | Trusted function that swaps value of 'LMVar', ignoring IFC.-swapLMVarTCB :: MonadLIO l m => LMVar l a -> a -> m a-swapLMVarTCB (LMVarTCB _ m) x = liftLIO . ioTCB $ swapMVar m x------- Check state of 'LMVar'------- | Same as 'isEmptyLMVar', but ignorses IFC.-isEmptyLMVarTCB :: MonadLIO l m => LMVar l a -> m Bool-isEmptyLMVarTCB (LMVarTCB _ m) = liftLIO . ioTCB $ isEmptyMVar m

@@ -1,31 +0,0 @@-{-# LANGUAGE Unsafe #-}--{- |--This module exports 'LabeledResult's which are effectively thread exit-results protected by a label. See "LIO.Concurrent" for a description-of the concurrency abstractions of LIO.---}--module LIO.Concurrent.TCB (-    LabeledResult(..), ThreadId-  ) where--import LIO.Label-import LIO.Core-import LIO.Concurrent.LMVar-import Control.Concurrent---- | A labeled thread result is simply a wrapper for a 'LMVar'. A thread--- can observe the result of another thread, only after raising its label--- to the label of the result.-data LabeledResult l a = LabeledResultTCB {-    lresThreadIdTCB :: ThreadId -    -- ^ Thread executing the computation-  , lresResultTCB :: LMVar l (Either (LabeledException l) a) -    -- ^ Plecement of computation result-  }--instance LabelOf LabeledResult where-  labelOf = labelOf . lresResultTCB

@@ -1,6 +1,9 @@ {-# LANGUAGE Trustworthy #-}-{-# LANGUAGE ScopedTypeVariables,-             DeriveDataTypeable #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE DeriveDataTypeable #-}  {- |  @@ -24,7 +27,7 @@ will be at least \"top-secret\". The role of the current label is two-fold. First, the current label protects all the data in scope -- it is the label associated with any /unlabeled/ data. For example, the-current label is the label on contants such as @3@ or @\"tis a+current label is the label on constants such as @3@ or @\"tis a string\"@. More interestingly, consider reading a \"secret\" file:  > bs <- readFile "/secret/file.txt"@@ -71,28 +74,13 @@     LIO   , MonadLIO(..)   -- ** Execute LIO actions-  , evalLIO, runLIO, tryLIO, paranoidLIO-  -- ** Internal state-  , LIOState(..)-  -- *** Current label+  , LIOState(..), evalLIO, runLIO+  -- ** Manipulating label state   , getLabel, setLabel, setLabelP-  -- *** Current clerance+  -- ** Manipulating clearance   , getClearance, setClearance, setClearanceP-  , withClearance, withClearanceP-  -- * Exceptions-  -- $exceptions-  , LabeledException-  -- ** Throwing exceptions-  , throwLIO-  -- ** Catching exceptions-  , catchLIO, catchLIOP-  -- ** Utilities-  -- $utils-  , onException, onExceptionP-  , finally, finallyP-  , bracket, bracketP-  , evaluate-  -- ** Exceptions thrown by LIO+  , scopeClearance, withClearance, withClearanceP+  -- * Exceptions thrown by LIO   -- $lioExceptions   , MonitorFailure(..)   , VMonitorFailure(..)@@ -106,105 +94,52 @@   , guardWrite, guardWriteP   ) where -import           Data.Typeable -import           Control.Monad-import           Control.Monad.Trans.State.Strict-import qualified Control.Exception as E-import           Control.Exception hiding ( finally-                                          , onException-                                          , bracket-                                          , evaluate )+import qualified Control.Exception as IO+import Control.Monad+import Data.IORef+import Data.Typeable -import           LIO.TCB-import           LIO.Label-import           LIO.Privs+import LIO.Exception+import LIO.TCB+import LIO.Label+import LIO.Privs+import LIO.Run   ----- Execute LIO actions------- | Given an 'LIO' computation and some initial state, return an--- IO action which when executed will perform the IFC-safe LIO--- computation.------ Because untrusted code cannot execute 'IO' computations, this function--- should only be useful within trusted code.  No harm is done from--- exposing the @evalLIO@ symbol to untrusted code.  (In general,--- untrusted code is free to produce 'IO' computations, but it cannot--- execute them.)-evalLIO :: Label l-        => LIO l a       -        -- ^ LIO computation-        -> LIOState l-        -- ^ Initial state-        -> IO a-evalLIO act s = fst `liftM` runLIO act s---- | Execute an 'LIO' action, returning the final state.--- See 'evalLIO'.-runLIO :: Label l-       => LIO l a-        -- ^ LIO computation that may throw an exception-       -> LIOState l-        -- ^ Initial state-       -> IO (a, LIOState l)-runLIO act s = runStateT (unLIOTCB act) s---- | Similar to 'evalLIO', but catches all exceptions, including--- language level exceptions.-paranoidLIO :: Label l-            => LIO l a-             -- ^ LIO computation that may throw an exception-            -> LIOState l-             -- ^ Initial state-            -> IO (Either SomeException (a, LIOState l))-paranoidLIO act s = (Right `liftM` runLIO act s) `E.catch` (return . Left)---- | Similar to 'evalLIO', but catches all exceptions exceptions--- thrown with 'throwLIO'.-tryLIO :: Label l-       => LIO l a-        -- ^ LIO computation that may throw an exception-       -> LIOState l-        -- ^ Initial state-       -> IO (Either (LabeledException l) a, LIOState l)-tryLIO act = runLIO (Right `liftM` act `catchTCB` (return . Left))---- -- Internal state --  -- | Returns the current value of the thread's label.-getLabel :: MonadLIO l m => m l-getLabel = liftLIO $ lioLabel `liftM` getLIOStateTCB+getLabel :: Label l => LIO l l+getLabel = lioLabel `liftM` getLIOStateTCB   -- | Raise the current label to the provided label, which must be -- between the current label and clearance. See 'taint'.-setLabel :: MonadLIO l m => l -> m ()-setLabel = setLabelP NoPrivs+setLabel :: Label l => l -> LIO l ()+setLabel = setLabelP noPrivs  -- | If the current label is @oldLabel@ and the current clearance is -- @clearance@, this function allows code to raise the current label to -- any value @newLabel@ such that @oldLabel ``canFlowTo`` newLabel && -- newLabel ``canFlowTo`` clearance@.-setLabelP :: (MonadLIO l m, Priv l p) => p -> l -> m ()+setLabelP :: PrivDesc l p => Priv p -> l -> LIO l () setLabelP p l = do-  liftLIO $ guardAllocP p l `catchLIO`+  guardAllocP p l `catch`       \(_ :: MonitorFailure) -> throwLIO InsufficientPrivs-  liftLIO . updateLIOStateTCB $ \s -> s { lioLabel = l }+  modifyLIOStateTCB $ \s -> s { lioLabel = l }  -- | Returns the current value of the thread's clearance.-getClearance :: MonadLIO l m => m l-getClearance = liftLIO $ lioClearance `liftM` getLIOStateTCB+getClearance :: Label l => LIO l l+getClearance = lioClearance `liftM` getLIOStateTCB  -- | Lower the current clearance. The new clerance must be between -- the current label and clerance. One cannot raise the current label -- or create object with labels higher than the current clearance.-setClearance :: MonadLIO l m => l -> m ()-setClearance = setClearanceP NoPrivs+setClearance :: Label l => l -> LIO l ()+setClearance = setClearanceP noPrivs  -- | Raise the current clearance (undoing the effects of -- 'setClearance') by exercising privileges. If the current label is@@ -213,215 +148,53 @@ -- clearance (modulo privileges), i.e., @'canFlowToP' p cnew c@ must -- hold. Additionally, the current label must flow to the new -- clearance, i.e., @l ``canFlowTo`` cnew@ must hold.-setClearanceP :: (MonadLIO l m, Priv l p) => p -> l -> m ()+setClearanceP :: PrivDesc l p => Priv p -> l -> LIO l () setClearanceP p cnew = do-  l <- getLabel-  c <- getClearance+  LIOState l c <- getLIOStateTCB   unless (canFlowToP p cnew c) $! throwLIO InsufficientPrivs   unless (l `canFlowTo` cnew)  $! throwLIO CurrentLabelViolation-  liftLIO . updateLIOStateTCB $ \s -> s { lioClearance = cnew }+  putLIOStateTCB $ LIOState l cnew --- | Lowers the clearance of a computation, then restores the clearance to its--- previous value (actually, to the upper bound of the current label and previous--- value).  Useful to wrap around a computation if you want to be sure you can--- catch exceptions thrown by it. The supplied clearance label must be bounded by--- the current label and clearance as enforced by 'guardAlloc'.+-- | Runs an 'LIO' action and re-sets the current clearance to its+-- previous value once the action returns.  In particular, if the+-- action lowers the current clearance, the clearance will be restored+-- upon return.+--+-- Note that @scopeClearance@ always restores the clearance.  If+-- that causes the clearance to drop below the current label, a+-- 'ClearanceViolation' exception is thrown.  That exception can only+-- be caught outside a second @scopeClearance@ that restores the+-- clearance to higher than the current label.+scopeClearance :: Label l => LIO l a -> LIO l a+scopeClearance lio = LIOTCB $ \sp -> do+  LIOState _ c <- readIORef sp+  ea <- IO.try $ unLIOTCB lio sp+  LIOState l _ <- readIORef sp+  writeIORef sp (LIOState l c)+  if l `canFlowTo` c+    then either (IO.throwIO :: SomeException -> IO a) return ea+    else IO.throwIO ClearanceViolation++-- | Lowers the clearance of a computation, then restores the+-- clearance to its previous value (actually, to the upper bound of+-- the current label and previous value).  Useful to wrap around a+-- computation if you want to be sure you can catch exceptions thrown+-- by it. The supplied clearance label must be bounded by the current+-- label and clearance as enforced by 'guardAlloc'. --  -- Note that if the computation inside @withClearance@ acquires any -- 'Priv's, it may still be able to raise its clearance above the -- supplied argument using 'setClearanceP'. withClearance :: Label l => l -> LIO l a -> LIO l a-withClearance = withClearanceP NoPrivs+withClearance c lio = scopeClearance $ setClearance c >> lio  -- | Same as 'withClearance', but uses privileges when applying -- 'guardAllocP' to the supplied label.-withClearanceP :: Priv l p => p -> l -> LIO l a -> LIO l a-withClearanceP p l act = do-  c <- getClearance-  setClearanceP p l-  act `finally` (updateLIOStateTCB $ \s ->-                   s { lioClearance = c `lub` lioLabel s })------- Exceptions-----{- $exceptions--   We must define 'throwIO'- and 'catch'-like functions to work in-   the 'LIO' monad.  A complication is that exceptions could-   potentially leak information.  For instance, one might examine a-   secret bit, and throw an exception when the bit is 1 but not 0.-   Allowing untrusted code to catch the exception leaks the bit.--   The solution is to wrap exceptions up with a label.  The exception-   may be caught, but only if the label of the exception can flow to-   the label at the point the catch statement began execution.-   Arbitrary code can use 'throwLIO' to throw an exception that will-   be labeled with the current label, while 'catchLIO' can be used to-   catch exceptions (whose label flows to the current clearance).-   Wherever possible, code should use the 'catchLIOP' and-   'onExceptionP' variants that use privileges to downgrade the-   exception. --   If an exception is uncaught in the 'LIO' monad, the 'evalLIO'-   function will re-throw the exception, so that it is okay to throw-   exceptions from within the 'LIO' monad and catch them within the-   'IO' monad.  Of course, code in the 'IO' monad must be careful not-   to let the 'LIO' code exploit it to exfiltrate information.  Hence,-   we recommend the use of 'paranoidLIO' to execute 'LIO' actions as-   to prevent accidental, but unwanted crashes.+withClearanceP :: PrivDesc l p => Priv p -> l -> LIO l a -> LIO l a+withClearanceP p c lio = scopeClearance $ setClearanceP p c >> lio  -   /Note/:  Do not use 'throw' (as opposed to 'throwLIO') within the-   'LIO' monad.  Because 'throw' can be invoked from pure code, it has-   no notion of current label and so cannot assign an appropriate-   label to the exception.  As a result, the exception will not be-   catchable within the 'LIO' monad and will propagate all the way out-   to the executing 'IO' layer.  Similarly, asynchronous exceptions-   (such as divide by zero or undefined values in lazily evaluated-   expressions) cannot be caught within the 'LIO' monad.---}- ----- Throwing exceptions------- | Throw an exception. The label on the exception is the current--- label.-throwLIO :: (Exception e, MonadLIO l m) => e -> m a-throwLIO e = do-  l <- getLabel-  liftLIO . unlabeledThrowTCB $! LabeledExceptionTCB l (toException e)------- Catching exceptions-------- | Same as 'catchLIO' but does not use privileges when raising the--- current label to the join of the current label and exception label.-catchLIOP :: (Exception e, Priv l p)-          => p-          -> LIO l a-          -> (e -> LIO l a)-          -> LIO l a-catchLIOP p act handler = do -  clr <- getClearance-  act `catchTCB` \se@(LabeledExceptionTCB l seInner) -> -    case fromException seInner of-     Just e | l `canFlowTo` clr -> taintP p l >> handler e-     _                          -> unlabeledThrowTCB se---- | Catches an exception, so long as the label at the point where the--- exception was thrown can flow to the clearance at which @catchLIO@ is--- invoked. Note that the handler raises the current label to the join--- ('upperBound') of the current label and exception label.-catchLIO :: (Exception e, Label l)-         => LIO l a-         -> (e -> LIO l a)-         -> LIO l a-catchLIO = catchLIOP NoPrivs ------- Utilities-----{- $utils--Similar to "Control.Exception" we export 'onException', 'finally' and-'bracket' which should be used by programmers to properly acquire and-release resources in the presence of exceptions.  Different from-"Control.Exception" our non-TCB utilities are not implemented in terms-of 'mask', and thus untrusted threads may be killed (and thus garbage-collected) with synchronous exceptions. Of course, only trusted code-may has access to 'throwTo'-like functionality.---}---- | Performs an action only if there was an exception raised by the--- computation. Note that the exception is rethrown after the final--- computation is executed.-onException :: Label l-            => LIO l a -- ^ The computation to run-            -> LIO l b -- ^ Computation to run on exception-            -> LIO l a -- ^ Result if no exception thrown-onException = onExceptionP NoPrivs---- | Privileged version of 'onExceptionP'.  'onException' cannot run its--- handler if the label was raised in the computation that threw the--- exception.  This variant allows privileges to be supplied, so as to--- catch exceptions thrown with a \"higher\" label.-onExceptionP :: Priv l p-             => p       -- ^ Privileges to downgrade exception-             -> LIO l a -- ^ The computation to run-             -> LIO l b -- ^ Computation to run on exception-             -> LIO l a -- ^ Result if no exception thrown-onExceptionP p act1 act2 = -    catchLIOP p act1 (\(e :: SomeException) -> do-                       void act2-                       throwLIO e )---- | Execute a computation and a finalizer, which is executed even if--- an exception is raised in the first computation.-finally :: Label l-        => LIO l a -- ^ The computation to run firstly-        -> LIO l b -- ^ Final computation to run (even if exception is thrown)-        -> LIO l a -- ^ Result of first action-finally = finallyP NoPrivs---- | Version of 'finally' that uses privileges when handling--- exceptions thrown in the first computation.-finallyP :: Priv l p-         => p       -- ^ Privileges to downgrade exception-         -> LIO l a -- ^ The computation to run firstly-         -> LIO l b -- ^ Final computation to run (even if exception is thrown)-         -> LIO l a -- ^ Result of first action-finallyP p act1 act2 = do-  r <- onExceptionP p act1 act2-  void act2-  return r---- | The @bracket@ function is used in patterns where you acquire a--- resource, perform a computation on it, and then release the resource.--- The function releases the resource even if an exception is raised in--- the computation. An example of its use case is file handling:------ >  bracket--- >    (openFile ... {- open file -} )--- >    (\handle -> {- close file -} )--- >    (\handle -> {- computation on handle -})------ Note: @bracket@ does not use 'mask' and thus asynchronous may leave--- the resource unreleased if the thread is killed in during release.--- An interface for arbitrarily killing threads is not provided by LIO.-bracket :: Label l-        => LIO l a           -- ^ Computation to run first-        -> (a -> LIO l c)    -- ^ Computation to run last-        -> (a -> LIO l b)    -- ^ Computation to run in-between-        -> LIO l b-bracket = bracketP NoPrivs---- | Like 'bracket', but uses privileges to downgrade the label of any--- raised exception.-bracketP :: Priv l p-         => p                 -- ^ Priviliges used to downgrade-         -> LIO l a           -- ^ Computation to run first-         -> (a -> LIO l c)    -- ^ Computation to run last-         -> (a -> LIO l b)    -- ^ Computation to run in-between-         -> LIO l b-bracketP p first third second = do-  x <- first-  finallyP p (second x) (third x)---- | Forces its argument to be evaluated to weak head normal form when the--- resultant LIO action is executed. This is simply a wrapper for --- "Control.Exception"'s @evaluate@.-evaluate :: MonadLIO l m => a -> m a-evaluate = liftLIO . rethrowIoTCB . E.evaluate---- -- Exceptions thrown by LIO -- @@ -451,6 +224,7 @@                     | CanFlowToViolation                     -- ^ Generic can-flow-to failure, use with                     -- 'VMonitorFailure'+                    | ResultExceedsLabel                     deriving (Show, Typeable)  instance Exception MonitorFailure@@ -534,13 +308,13 @@ -- If the label does not flow to clearance 'ClearanceViolation' is -- thrown; if the current label does not flow to the argument label -- 'CurrentLabelViolation' is thrown.-guardAlloc :: MonadLIO l m => l -> m ()-guardAlloc = guardAllocP NoPrivs+guardAlloc :: Label l => l -> LIO l ()+guardAlloc = guardAllocP noPrivs  -- | Like 'guardAlloc', but takes privilege argument to be more -- permissive.  Note: privileges are /only/ used when checking that -- the current label can flow to the given label.-guardAllocP :: (MonadLIO l m, Priv l p) => p -> l -> m ()+guardAllocP :: PrivDesc l p => Priv p -> l -> LIO l () guardAllocP p newl = do   c <- getClearance   l <- getLabel@@ -555,20 +329,20 @@ -- @l@.  This will raise the current label to a value @l'@ such that -- @l ``canFlowTo`` l'@, or throw 'ClearanceViolation' if @l'@ would -- have to be higher than the current clearance.-taint :: MonadLIO l m => l -> m ()-taint = taintP NoPrivs+taint :: Label l => l -> LIO l ()+taint = taintP noPrivs  -- | Like 'taint', but use privileges to reduce the amount of taint -- required.  Note that @taintP@ will never lower the current label. -- It simply uses privileges to avoid raising the label as high as -- 'taint' would raise it.-taintP :: (MonadLIO l m, Priv l p) => p -> l -> m ()+taintP :: PrivDesc l p => Priv p -> l -> LIO l () taintP p newl = do   c <- getClearance   l <- getLabel   let l' = partDowngradeP p newl l   unless (l' `canFlowTo` c) $! throwLIO ClearanceViolation-  liftLIO . updateLIOStateTCB $ \s -> s { lioLabel = l' }+  modifyLIOStateTCB $ \s -> s { lioLabel = l' }   -- | Use @guardWrite l@ in any (trusted) code before modifying an@@ -582,12 +356,25 @@ -- This guarantees that @l@ ``canFlowTo`` the current label (and -- clearance), and that the current label ``canFlowTo`` @l@. ---guardWrite :: MonadLIO l m => l -> m ()-guardWrite = guardWriteP NoPrivs+guardWrite :: Label l => l -> LIO l ()+guardWrite = guardWriteP noPrivs  -- | Like 'guardWrite', but takes privilege argument to be more -- permissive.-guardWriteP ::(MonadLIO l m, Priv l p) => p -> l -> m ()+guardWriteP :: PrivDesc l p => Priv p -> l -> LIO l () guardWriteP p newl = do   taintP      p newl   guardAllocP p newl++--+-- Monad base+--++-- | Synonym for monad in which 'LIO' is the base monad.+class (Monad m, Label l) => MonadLIO l m | m -> l where+  -- | Lift an 'LIO' computation.+  liftLIO :: LIO l a -> m a++instance Label l => MonadLIO l (LIO l) where+  liftLIO = id+

@@ -16,14 +16,15 @@  module LIO.DCLabel (   -- ** Principals-    Principal, principalName, principal+    Principal(..), principal   -- ** Clauses   , Clause, clause   -- ** Components   , Component, dcTrue, dcFalse, dcFormula   , isTrue, isFalse   -- ** Labels-  , DCLabel, dcSecrecy, dcIntegrity, dcLabel, dcPub+  , DCLabel, dcSecrecy, dcIntegrity, dcLabel+  , dcPub, dcTop, dcBottom   -- ** Privileges   , module LIO.DCLabel.Privs   -- ** DSL@@ -31,10 +32,8 @@   -- * Synonyms for "LIO"   -- $dcMonad   , DCState, defaultState-  , DC, evalDC, runDC, tryDC, paranoidDC+  , DC, evalDC, runDC, tryDC   , MonadDC-  -- ** Exceptions-  , DCLabeledException   -- ** Labeled values   , DCLabeled   -- ** Labeled references@@ -43,34 +42,26 @@   , DCGate   ) where -import           Control.Exception--import           LIO-import           LIO.LIORef-import           LIO.Labeled.TCB+import qualified Control.Exception as IO -import           LIO.DCLabel.Core-import           LIO.DCLabel.Privs-import           LIO.DCLabel.DSL-import           LIO.DCLabel.Serialize ()+import LIO.Core+import LIO.Labeled+import LIO.Privs+import LIO.LIORef+import LIO.DCLabel.Core+import LIO.DCLabel.Privs+import LIO.DCLabel.DSL  -- -- LIO synonyms --  --- | DC Labeled exceptions.-type DCLabeledException = LabeledException DCLabel- -- | DC 'Labeled' values. type DCLabeled = Labeled DCLabel -instance LabeledFunctor DCLabel where-  lFmap lv f = let l = labelOf lv `upperBound` dcPub-               in label l $ f (unlabelTCB lv)- -- | DC Labeled 'LIORef's.-type DCRef = LIORef DCLabel+type DCRef a = LIORef DCLabel a   -- | DC 'Gate'.@@ -101,7 +92,8 @@ -- | Default, starting state for a 'DC' computation. The current label -- is public (i.e., 'dcPub') and the current clearance is 'top'. defaultState :: DCState-defaultState = LIOState { lioLabel = dcPub, lioClearance = top }+defaultState = LIOState { lioLabel = dcPub+                        , lioClearance = dcTop }  -- | The monad for LIO computations using 'DCLabel' as the label. type DC = LIO DCLabel@@ -117,9 +109,8 @@  -- | Similar to 'evalLIO', but catches any exceptions thrown by -- untrusted code with 'throwLIO'.-tryDC :: DC a -> IO (Either DCLabeledException a, DCState)-tryDC act = tryLIO act defaultState---- | Similar to 'evalLIO', but catches all exceptions.-paranoidDC :: DC a -> IO (Either SomeException (a, DCState))-paranoidDC act = paranoidLIO act defaultState+tryDC :: DC a -> IO (Either IO.SomeException a, DCState)+tryDC act = runDC act >>= tryit+  where tryit (a, s) = do+          ea <- IO.try (IO.evaluate a)+          return (ea, s)

@@ -1,5 +1,6 @@ {-# LANGUAGE Safe #-} {-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE MultiParamTypeClasses #-} {-|  This module implements Disjunction Category Labels (DCLabels).@@ -53,23 +54,22 @@   , dcTrue, dcFalse, dcFormula    , isTrue, isFalse   -- * Labels-  , DCLabel(..), dcLabel, dcLabelNoReduce, dcPub+  , DCLabel(..), dcLabel, dcLabelNoReduce+  , dcPub, dcTop, dcBottom   -- * Internal   , dcReduce, dcImplies   , dcAnd, dcOr   ) where  import qualified Data.ByteString.Char8 as S8-import           Data.Typeable-import           Data.Set (Set)+import Data.List (intercalate)+import Data.Monoid+import Data.Set (Set) import qualified Data.Set as Set--import           Data.List (intercalate)--import           LIO.Label--type S8 = S8.ByteString+import Data.Typeable +import LIO.Label+import LIO.Privs  -- -- Principals@@ -78,16 +78,17 @@ -- | A @Principal@ is a simple string representing a source of -- authority. Any piece of code can create principals, regardless of how -- untrusted it is.-newtype Principal = Principal { principalName :: S8 +newtype Principal = Principal { principalName :: S8.ByteString                                 -- ^ Get the principal name.                               } deriving (Eq, Ord, Typeable)  instance Show Principal where-  show = S8.unpack . principalName+  showsPrec _ = shows . principalName --- | Principal constructor.-principal :: S8 -> Principal-principal = Principal+-- | Generate a principal from a 'String'.  (To create one from a+-- 'S8.ByteString', just use the 'Principal' constructor directly.)+principal :: String -> Principal+principal = Principal . S8.pack  -- -- Category - disjunction clauses@@ -106,9 +107,12 @@       _ -> Set.size c1 < Set.size c2  instance Show Clause where-  show c = let ps = map show . Set.toList $! unClause c-           in parens . intercalate " \\/ " $! ps-    where parens x = "[" ++ x ++ "]"+  show c@(Clause uc)+         | Set.size uc == 1 = show . head . Set.toList $ uc+         | otherwise =+              let ps = map show . Set.toList $! unClause c+              in parens . intercalate " \\/ " $! ps+    where parens x = "(" ++ x ++ ")"  -- | Clause constructor clause :: Set Principal -> Clause@@ -126,12 +130,42 @@   deriving (Eq, Typeable)  instance Show Component where-  show c | isFalse c = "|False"-         | isTrue c  = "|True"+  show c | isFalse c = show False+         | isTrue c  = show True          | otherwise = let cs = map show . Set.toList $! unDCFormula c-                       in parens . intercalate " /\\ " $! cs-    where parens x = "{" ++ x ++ "}"+                       in intercalate " /\\ " $! cs +-- | Privileges can be combined using 'mappend'+instance Monoid Component where+  mempty = dcTrue+  mappend p1 p2 = dcReduce $! p1 `dcAnd` p2++instance PrivDesc DCLabel Component where+  canFlowToPrivDesc pd l1 l2+           | pd == dcTrue = canFlowTo l1 l2+           | otherwise =+    let i1 = dcReduce $ dcIntegrity l1 `dcAnd` pd+        s2 = dcReduce $ dcSecrecy l2   `dcAnd` pd+    in l1 { dcIntegrity = i1 } `canFlowTo` l2 { dcSecrecy = s2 }++  partDowngradePrivDesc pd la lg+               | pd == mempty  = la `lub` lg+               | pd == dcFalse = lg+               | otherwise = +    let sec_a  = dcSecrecy la+        int_a  = dcIntegrity la+        sec_g  = dcSecrecy   lg+        int_g  = dcIntegrity lg+        sec_a' = dcFormula . Set.filter f $ unDCFormula sec_a+        sec_res  = if isFalse sec_a+                then sec_a+                else sec_a' `dcAnd` sec_g+        int_res  = (pd `dcAnd` int_a) `dcOr` int_g+    in dcLabel sec_res int_res+      where f c = not $ pd `dcImplies` (dcFormula . Set.singleton $ c)+++ -- | Logical @True@. dcTrue :: Component dcTrue = DCFormula Set.empty@@ -171,12 +205,13 @@                        } deriving (Eq, Typeable)  instance Show DCLabel where -  show l = let s = dcSecrecy l-               i = dcIntegrity l-           in "< " ++ show s ++ " , " ++ show i ++ " >"+  showsPrec d l = showParen (d > 5) $+    let s = dcSecrecy l+        i = dcIntegrity l+    in showsPrec (d + 1) s . showString " %% " . showsPrec (d + 1) i --- | Label constructor. Note that each component is first reduced to--- CNF.+-- | @dcLabel secrecyComponent integrityComponent@ creates a label,+-- reducing each component to CNF. dcLabel :: Component -> Component -> DCLabel dcLabel c1 c2 = DCLabel (dcReduce c1) (dcReduce c2) @@ -186,6 +221,18 @@   +-- | Element in the DCLabel lattice corresponding to the most secret+-- and least trustworthy data.+-- @dcTop = \< False, True \> @.+dcTop :: DCLabel+dcTop = dcLabel dcFalse dcTrue++-- | Element in the DCLabel lattice corresponding to the least secret+-- and most trustworthy data.+-- @dcTop = \< True, False \> @.+dcBottom :: DCLabel+dcBottom = dcLabel dcTrue dcFalse+ -- | Element in the DCLabel lattice corresponding to public data. -- @dcPub = \< True, True \> @. This corresponds to data that is not -- secret nor trustworthy.@@ -193,20 +240,17 @@ dcPub = DCLabel { dcSecrecy = dcTrue, dcIntegrity = dcTrue }  --+-- Bounded by \< True, False \> and \< False, True \>+--+instance Bounded DCLabel where+  minBound = dcBottom+  maxBound = dcTop++-- -- Lattice operations --  instance Label DCLabel where-  -- | Minimal element of the DCLabel lattice, /bottom/ &#8869;, such-  -- that @&#8869; &#8849; L@ for any label @L@.-  -- Bottom is defined as: @ &#8868; = \< False, True \> @-  bottom = dcLabel dcTrue dcFalse--  -- | Maximum element of the DCLabel lattice, /top/ &#8868;,-  -- such that @L &#8849; &#8868;@ for any label @L@.-  -- Top is defined as: @ &#8868; = \< False, True \> @-  top = DCLabel dcFalse dcTrue-   -- | Partial /can-flow-to/ relation on labels.   canFlowTo l1 l2 = (dcSecrecy l2   `dcImplies` dcSecrecy l1) &&                     (dcIntegrity l1 `dcImplies` dcIntegrity l2)@@ -221,7 +265,6 @@   glb l1 l2 = DCLabel     { dcSecrecy   = dcReduce $ dcSecrecy l1   `dcOr`  dcSecrecy l2     , dcIntegrity = dcReduce $ dcIntegrity l1 `dcAnd` dcIntegrity l2 }-  -- -- Helpers

@@ -1,12 +1,22 @@ {-# LANGUAGE Safe #-}-{-# LANGUAGE TypeSynonymInstances,-             FlexibleInstances #-}+{-# LANGUAGE FlexibleInstances #-}  {-|-  This module implements a ``nano``, very simple, embedded domain-  specific language to create 'Component's and privilage descriptions-  from conjunctions of principal disjunctions.-  +  This module implements a simple, embedded domain specific language+  to create 'Component's, privilage descriptions and labels from+  conjunctions of principal disjunctions.++  A 'DCLabel' consists of a secrecy 'Component' and an integrity+  'Component'.  The '%%' operator allows one to construct a 'DCLabel'+  by joining a secrecy 'Component' (on the left) with an integrity+  'Component' on the right.  This is similar to 'dcLabel', except that+  the arguments can also be instances of 'ToComponent'.  For example,+  the following expresses data that can be exported by the principal+  \"Alice\" and written by anybody:  @\"Alice\" '%%' 'True'@.  (The+  component 'True' or 'dcTrue' indicates a trivially satisfiable label+  component, which in this case means a label with no integrity+  guarantees.)+   A 'Component' or 'DCPrivDesc' is created using the ('\/') and ('/\')   operators.  The disjunction operator ('\/') is used to create a   'Clause' from 'Principal's, ByteStrings, or a disjunctive@@ -42,64 +52,82 @@   Consider the following, example:    @-     l1 = \"Alice\" '\/' \"Bob\" '/\' \"Carla\"-     l2 = \"Alice\" '/\' \"Carla\"-     dc1 = 'dcLabel' l1 l2-     dc2 = 'dcLabel' ('toComponent' \"Djon\") ('toComponent' \"Alice\")-     pr = 'dcPrivTCB' . 'dcPrivDesc' $ \"Alice\" '/\' \"Carla\"+l1 = \"Alice\" '\/' \"Bob\" '/\' \"Carla\"+l2 = \"Alice\" '/\' \"Carla\"+dc1 = 'dcLabel' l1 l2+dc2 = 'dcLabel' ('toComponent' \"Djon\") ('toComponent' \"Alice\")+pr = PrivTCB $ toComponent $ \"Alice\" '/\' \"Carla\"   @ -where--  * @ dc1 = \<{[\"Alice\" &#8897; \"Bob\"] &#8896; [\"Carla\"]} , {[\"Alice\"] &#8896; [\"Carla\"]}\>@-  -  * @ dc2 = \<{[\"Djon\"]} , {[\"Alice\"]}\>@--  * @ 'canFlowTo' dc1 dc2 = False @+  This will result in the following: -  * @ 'canFlowToP' pr dc1 dc2 = True@+>>> dc1+"Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla"+>>> dc2+"Djon" %% "Alice"+>>> canFlowTo dc1 dc2+False+>>> canFlowToP pr dc1 dc2+True  -}  module LIO.DCLabel.DSL (   -- * Operators-    (\/), (/\), ToComponent(..)+    (%%), (\/), (/\), ToComponent(..)   , fromList, toList   -- * Aliases-  , everybody, anybody+  , impossible, unrestricted   ) where -import           LIO.DCLabel.Privs-import           LIO.DCLabel.Core import qualified Data.Set as Set-import qualified Data.ByteString.Char8 as S8 -type S8 = S8.ByteString+import LIO.Privs+import LIO.DCLabel.Core  -- | Convert a type (e.g., 'Clause', 'Principal') to a label component. class ToComponent a where   -- | Convert to 'Component'   toComponent :: a -> Component-  -- | Trivial synonym for 'toComponent'. Convert to a 'DCPrivDesc'.-  dcPrivDesc :: a -> DCPrivDesc-  dcPrivDesc = toComponent +infix 5 %%++-- | Create a `DCLabel` from a secrecy `ToComponent` and integrity+-- `ToComponent`. E.g.:+--+-- @+--   \"secrecy\" %% \"integrity\"+-- @+--+-- @+-- infix 5 %%+-- @+(%%) :: (ToComponent a, ToComponent b) => a -> b -> DCLabel+(%%) sec int = dcLabel (toComponent sec) (toComponent int)+ -- | Identity of 'Component'. instance ToComponent Component where+  {-# INLINE toComponent #-}   toComponent = id+instance ToComponent (Priv Component) where+  {-# INLINE toComponent #-}+  toComponent = privDesc -- | Convert singleton 'Clause' to 'Component'. instance ToComponent Clause    where   toComponent c = DCFormula $! Set.singleton c -- | Convert singleton 'Principal' to 'Component'. instance ToComponent Principal where   toComponent p = toComponent . Clause $! Set.singleton p--- | Convert singleton 'Principal' (in the form of a @ByteString@)to 'Component'.-instance ToComponent S8 where-  toComponent = toComponent . principal+ -- | Convert singleton 'Principal' (in the form of a 'String')to 'Component'. instance ToComponent String where-  toComponent = toComponent . S8.pack+  toComponent = toComponent . principal +instance ToComponent Bool where+  {-# INLINE toComponent #-}+  toComponent True = DCFormula Set.empty+  toComponent False = DCFalse+ infixl 7 \/ infixl 6 /\ @@ -126,25 +154,24 @@ --  -- | Logical falsehood can be thought of as the component containing--- every possible principal:+-- every possible principal, hence impossible to express: ----- > everybody = dcFalse+-- > impossible = dcFalse ---everybody :: Component-everybody = dcFalse+impossible :: Component+impossible = dcFalse  -- | Logical truth can be thought of as the component containing--- no specific principal:+-- no specific principal, hence imposing no restrictions: ----- > anybody = dcTrue+-- > unrestricted = dcTrue ---anybody :: Component-anybody = dcTrue-+unrestricted :: Component+unrestricted = dcTrue  -- | Convert a 'Component' to a list of list of 'Principal's if the -- 'Component' does not have the value 'DCFalse'. In the latter case--- the function returns 'Nothing'.+-- the function returns an exception. toList :: Component -> [[Principal]] toList DCFalse        = error "toList: Invalid use, expected DCFormula" toList (DCFormula cs) = map (Set.toList . unClause) $! Set.toList cs

@@ -1,6 +1,4 @@ {-# LANGUAGE Trustworthy #-}-{-# LANGUAGE MultiParamTypeClasses,-             TypeSynonymInstances #-} {- |  Privileges allow a piece of code to bypass certain information flow@@ -36,42 +34,21 @@   , dcOwns   ) where -import           Data.Monoid import qualified Data.Set as Set -import           LIO-import           LIO.Privs.TCB (mintTCB)-import           LIO.DCLabel.Core-import           LIO.DCLabel.Privs.TCB+import LIO+import LIO.DCLabel.Core+import LIO.TCB --- | Privileges can be combined using 'mappend'-instance Monoid DCPriv where-  mempty = noPriv-  mappend p1 p2 = mintTCB . dcReduce $!-                      privDesc p1 `dcAnd` privDesc p2+-- | A privilege description is simply a conjunction of disjunctions.+-- Unlike (actually minted) privileges (see 'DCPriv'), privilege+-- descriptions may be created by untrusted code.+type DCPrivDesc = Component -instance Priv DCLabel DCPriv where-  canFlowToP p l1 l2 | pd == dcTrue = canFlowTo l1 l2-                     | otherwise =-    let i1 = dcReduce $ dcIntegrity l1 `dcAnd` pd-        s2 = dcReduce $ dcSecrecy l2   `dcAnd` pd-    in l1 { dcIntegrity = i1 } `canFlowTo` l2 { dcSecrecy = s2 }-      where pd = privDesc p-  partDowngradeP p la lg | p == noPriv     = la `upperBound` lg-                         | p == allPrivTCB = lg-                         | otherwise        = -    let sa  = dcSecrecy $ la-        ia  = dcIntegrity la-        sg  = dcSecrecy   lg-        ig  = dcIntegrity lg-        pd  = privDesc    p-        sa' = dcFormula . Set.filter (f pd) $ unDCFormula sa-        sr  = if isFalse sa -                then sa-                else sa' `dcAnd` sg-        ir  = (pd `dcAnd` ia) `dcOr` ig-    in dcLabel sr ir-      where f pd c = not $ pd `dcImplies` (dcFormula . Set.singleton $ c)+-- | A privilege is a minted and protected privilege description+-- ('DCPrivDesc') that may only be created by trusted code or+-- delegated from an existing @DCPriv@.+type DCPriv = Priv DCPrivDesc  -- -- Helpers@@ -80,7 +57,7 @@ -- | The empty privilege, or no privileges, corresponds to logical -- @True@. noPriv :: DCPriv-noPriv = mintTCB dcTrue+noPriv = PrivTCB dcTrue  -- | Given a privilege and a privilege description turn the privilege -- description into a privilege (i.e., mint). Such delegation succeeds@@ -88,7 +65,7 @@ dcDelegatePriv :: DCPriv -> DCPrivDesc -> Maybe DCPriv dcDelegatePriv p pd = let c  = privDesc $! p                       in if c `dcImplies` pd-                           then Just $! mintTCB pd+                           then Just $! PrivTCB pd                            else Nothing  -- | We say a piece of code having a privilege object (of type 'DCPriv')@@ -98,3 +75,4 @@ -- function can be used to make such checks. dcOwns :: DCPrivDesc -> Clause -> Bool dcOwns pd c = pd `dcImplies` dcFormula (Set.singleton c)+

@@ -1,45 +0,0 @@-{-# LANGUAGE Unsafe #-}-{-# LANGUAGE DeriveDataTypeable,-             MultiParamTypeClasses,-             TypeSynonymInstances #-}--{-|--This module implements the trusted compoenet of DCLabel privileges,-documented in "LIO.DCLabel.Privs".-Since privilege objects may be used unsafely, this module is marked-@-XUnsafe@. Untrusted code may access privileges using the interface-provided by "LIO.DCLabel.Privs".---}--module LIO.DCLabel.Privs.TCB (-    DCPrivDesc-  , DCPriv(..)-  , allPrivTCB-  ) where--import           Data.Typeable-import           LIO.DCLabel.Core-import           LIO.Privs-import           LIO.Privs.TCB---- | A privilege description is simply a conjunction of disjunctions.--- Unlike (actually minted) privileges (see 'DCPriv'), privilege--- descriptions may be created by untrusted code.-type DCPrivDesc = Component---- | A privilege is a minted and protected privilege description--- ('DCPrivDesc') that may only be created by trusted code or--- delegated from an existing @DCPriv@.-newtype DCPriv = DCPrivTCB { unDCPriv :: DCPrivDesc }-  deriving (Eq, Show, Typeable)--instance PrivTCB  DCPriv-instance PrivDesc DCPriv DCPrivDesc where privDesc = unDCPriv-instance MintTCB  DCPriv DCPrivDesc where mintTCB = DCPrivTCB---- | The all privilege corresponds to logical @False@-allPrivTCB :: DCPriv-allPrivTCB = mintTCB dcFalse-

@@ -1,33 +0,0 @@-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE StandaloneDeriving,-             GeneralizedNewtypeDeriving #-}-{- |--This module provides instances for binary serialization of-'DCLabel's. Specifically, we provide insgtances for @binary@\'s-@Data.Binary@.---}-module LIO.DCLabel.Serialize () where---import           LIO.DCLabel.Core-import           Data.Binary-import           Control.Monad--deriving instance Binary Principal-deriving instance Binary Clause---- | Serialize components by converting them to maybe's-instance Binary Component where-  put c = put . dcToMaybe $! c-    where dcToMaybe DCFalse       = Nothing-          dcToMaybe (DCFormula f) = Just f-  get = dcFromMaybe `liftM` get-    where dcFromMaybe Nothing  = dcFalse-          dcFromMaybe (Just f) = dcFormula f---- | Serialize labels by converting them to pairs of components.-instance Binary DCLabel where-  put l = put (dcSecrecy l, dcIntegrity l)-  get   = uncurry dcLabelNoReduce `liftM` get

@@ -0,0 +1,99 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ExistentialQuantification #-}++{- |++Exception routines much like the 'IO' ones in "Control.Exception" (we+duplicate the documentation below).  There are two differences,+however.  First, LIO does not allow masking of asynchronous exceptions+(since these are relied upon to kill a misbehaving thread).  Hence,+routines like 'onException' are not guaranteed to run if a thread is+unconditionally killed.  Second, in a few cases (such as 'lWait') it+is possible for the current label to be raised above the current+clearance as an exception is thrown, in which case these functions do+not catch the exception, either, since code cannot run under such+circumstances.++-}+module LIO.Exception (+  Exception(..), SomeException(..), throwLIO, catch, handle, try+  , onException, finally, bracket, evaluate+  ) where++import Control.Exception (Exception(..), SomeException(..))+import qualified Control.Exception as IO+import Control.Monad+import Data.Typeable++import LIO.TCB+import LIO.Label++throwLIO :: Exception e => e -> LIO l a+throwLIO = ioTCB . IO.throwIO++-- | A simple wrapper around IO catch.  The only subtlety is that code+-- is not allowed to run unless the current label can flow to the+-- current clearance.  Hence, if the label exceeds the clearance, the+-- exception is not caught.  (Only a few conditions such as 'lWait' or+-- raising the clearance within 'scopeClearance' can lead to the label+-- exceeding the clarance, and an exception is always thrown at the+-- time this happens.)+catch :: (Label l, Exception e) => LIO l a -> (e -> LIO l a) -> LIO l a+catch io h =+  LIOTCB $ \s -> unLIOTCB io s `IO.catch` \e -> unLIOTCB (safeh e) s+  where uncatchableType = typeOf (undefined :: UncatchableTCB)+        safeh e@(SomeException einner) = do+          when (typeOf einner == uncatchableType) $ throwLIO e+          LIOState l c <- getLIOStateTCB+          unless (l `canFlowTo` c) $ throwLIO e+          maybe (throwLIO e) h $ fromException e++-- | A version of 'catch' with the arguments swapped around.+handle :: (Label l, Exception e) => (e -> LIO l a) -> LIO l a -> LIO l a+handle = flip catch++-- | Like 'finally', but only performs the final action if there was+-- an exception raised by the computation. +onException :: Label l => LIO l a -> LIO l b -> LIO l a+onException io cleanup =+  io `catch` \e -> cleanup >> throwLIO (e :: SomeException)++-- | A variant of 'bracket' where the return value from the first+-- computation is not required. +finally :: Label l => LIO l a -> LIO l b -> LIO l a+finally io cleanup = do+  a <- io `onException` cleanup+  void cleanup+  return a+  +++-- | When you want to acquire a resource, do some work with it, and+-- then release the resource, it is a good idea to use @bracket@,+-- because bracket will install the necessary exception handler to+-- release the resource in the event that an exception is raised+-- during the computation. If an exception is raised, then bracket+-- will re-raise the exception (after performing the release). +bracket :: Label l => LIO l a         -- ^ Computation to run first+                   -> (a -> LIO l c)  -- ^ Computation to run last+                   -> (a -> LIO l b)  -- ^ Computation to run in-between+                   -> LIO l b+bracket before after thing = do+  a <- before+  b <- thing a `onException` after a+  void $ after a+  return b++-- | Forces its argument to be evaluated to weak head normal form when+-- the resultant 'LIO' action is executed.+evaluate :: a -> LIO l a+evaluate = ioTCB . IO.evaluate++-- | Similar to catch, but returns an 'Either' result which is+-- ('Right' @a@) if no exception of type @e@ was raised, or ('Left'+-- @ex@) if an exception of type 'e' was raised and its value is @ex@.+-- If any other type of exception is raised than it will be propogated+-- up to the next enclosing exception handler.+try :: (Label l, Exception a1) => LIO l a -> LIO l (Either a1 a)+try io = fmap Right io `catch` (return . Left)

@@ -1,266 +0,0 @@-{-# LANGUAGE Unsafe #-}-{-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE ScopedTypeVariables #-}-{- |--This module exports the basic interface for creating and using the-labeled file system, implemented as a file store. Trusted code should-use 'initFSTCB' to set the root of the labeled file system. Moreover,-trusted code should implement all the IO functions in terms of-'createFileTCB', 'createDirectoryTCB', and 'getPathLabelTCB' and-'setPathLabelTCB'.---}-module LIO.FS.TCB (-  -- * Initializing labeled filesystem-    initFSTCB, mkFSTCB, setFSTCB-  , getRootDirTCB-  -- * Handling path labels-  , setPathLabelTCB-  , getPathLabelTCB-  -- * Creating labeled objects-  , createFileTCB-  , createDirectoryTCB-  -- * Labeled 'FilePath'-  , LFilePath(..)-  -- * Filesystem errors-  , FSError(..)-  -- * Serializable label constraint-  , SLabel-  , lazyEncodeLabel, encodeLabel, decodeLabel-  ) where--import           Data.Binary-import           Data.Typeable-import           Data.IORef-import qualified Data.ByteString as S-import qualified Data.ByteString.Char8 as S8-import qualified Data.ByteString.Lazy as L-import qualified Data.ByteString.Lazy.Char8 as L8-import qualified Data.Digest.Pure.SHA as SHA--import           Codec.Compression.Zlib hiding (compress)--import           Control.Monad-import           Control.Exception-import qualified Control.Exception as E-                 -import           System.FilePath-import           System.Directory-import           System.IO-import           System.IO.Unsafe-import           System.Xattr--import           LIO.Label-import           LIO.Core-import           LIO.TCB---- | Synonym for strict ByteString-type S8 = S8.ByteString- --- | Synonym for lazy ByteString-type L8 = L8.ByteString---- | Constraintfor serializable labels-type SLabel l = (Label l, Binary l)------- Exception thrown by the file store interface------- | Filesystem errors-data FSError = FSRootCorrupt           -- ^ Root structure is corrupt.-             | FSRootInvalid           -- ^ Root is invalid (must be absolute).-             | FSRootExists            -- ^ Root already exists.-             | FSRootNoExist           -- ^ Root does not exists.-             | FSRootNeedLabel         -- ^ Cannot create root, missing label.-             | FSObjNeedLabel          -- ^ FSobjectcannot be created without a label.-             | FSLabelCorrupt FilePath -- ^ Object label is corrupt.-             | FSIllegalFileName       -- ^ Supplied file name is illegal.-      deriving Typeable--instance Exception FSError--instance Show FSError where-  show FSRootCorrupt      = "Root structure is corrupt."-  show FSRootInvalid      = "Root path is invalid, must be absolute."-  show FSRootExists       = "Root already exists."-  show FSRootNoExist      = "Root directory does not exist."-  show FSRootNeedLabel    = "Root cannot be created without a label."-  show (FSLabelCorrupt f) = "Label of " ++ show f ++ " is corrupt/non-existant."-  show FSObjNeedLabel     = "FS object cannot be created without a label."-  show FSIllegalFileName  = "Supplied file name is illegal."------- Handling root of FS-----magicAttr :: AttrName-magicAttr = "user._lio_magic"---- | Content written to magic key. -magicContent :: AttrValue-magicContent = S.pack  [ 0x7f, 0x45, 0x4c, 0x46, 0x01-                       , 0x01, 0x01, 0x00, 0x00, 0x00-                       , 0x00, 0x00, 0x00, 0x00, 0x00-                       , 0x00, 0xde, 0xad, 0xbe, 0xef]---- | Root of labeled filesystem.-rootDir :: IORef FilePath-{-# NOINLINE rootDir #-}-rootDir = unsafePerformIO $ newIORef (error "LIO Filesystem not initialized.")---- | Get the root directory.-getRootDirTCB :: SLabel l => LIO l FilePath-getRootDirTCB = ioTCB $ readIORef rootDir---- | Create a the file store (i.e., labeled file system) with a given--- label and root file path.  The path must be an absolute path,--- otherwise @initFSTCB@ throws 'FSRootInvalid'.-mkFSTCB :: SLabel l-        => FilePath      -- ^ Path to the filesystem root-        -> l             -- ^ Label of root-        -> LIO l ()-mkFSTCB path l = do-  unless (isAbsolute path) $ ioTCB $ throwIO FSRootInvalid-  -- Create root of filesystem:-  ioTCB $ createDirectory path-  -- Set root label:-  setPathLabelTCB path l-  -- Create magic attribute:-  ioTCB $ lsetxattr path magicAttr magicContent CreateMode-  -- Set the root filesystem:-  ioTCB $ writeIORef rootDir path---- | Set the given file path as the root of the labeled filesystem.  This--- function throws a 'FSLabelCorrupt' if the directory does not contain a--- valid label, and  a 'FSRootCorrupt' if the 'magicAttr' attribute is--- missing.-setFSTCB :: SLabel l => FilePath -> LIO l ()-setFSTCB path = do-  -- Path must be absolute-  unless (isAbsolute path) $ ioTCB $ throwIO FSRootInvalid-  -- Path must be a directory-  checkDirExists-  -- Check magic attribute:-  checkMagic-  -- Check that the label of the root is valid-  void $ getPathLabelTCB path-  -- Set the root directory-  ioTCB $ writeIORef rootDir path-   where checkMagic = ioTCB $ do-           magicOK <-(==magicContent) `liftM` -                      (throwOnFail $ lgetxattr path magicAttr)-           unless magicOK doFail-         checkDirExists = ioTCB $ do-          e <- doesDirectoryExist path-          unless e $ throwIO FSRootNoExist-         doFail = throwIO FSRootCorrupt-         throwOnFail act = act `E.catch` (\(_:: SomeException) -> doFail)---- | Initialize filesystem at the given path. The supplied path must be--- absolute, otherwise @initFSTCB@ throw 'FSRootInvalid'.  If the FS has--- already been created then @initFSTCB@ solely verifies that the root--- directory is not corrupt (see 'setFSTCB'). Otherwise, a new FS is created--- with the supplied label (see 'mkFSTCB').------ This function performs several checks that 'setFSTCB' and 'mkFSTCB' perform,--- so when considering performance they should be called directly.-initFSTCB :: SLabel l => FilePath -> Maybe l -> LIO l ()-initFSTCB path ml = do- unless (isAbsolute path) $ ioTCB $ throwIO FSRootInvalid- exists <- ioTCB $ doesDirectoryExist path- (if exists then setFSTCB else mkFSTCB') path-  where mkFSTCB' p = maybe (ioTCB $ throwIO FSRootNeedLabel) (mkFSTCB p) ml-                    ------- Objects--- ---- | Label attribute name.-labelAttr :: AttrName-labelAttr = "user._lio_label"---- | Hash-of-label attribute name.-labelHashAttr :: AttrName-labelHashAttr = "user._lio_label_sha"---- | Encode a label into an attribute value.-lazyEncodeLabel :: SLabel l => l -> L8-lazyEncodeLabel = compress . encode---- | Encode a label into an attribute value.-encodeLabel :: SLabel l => l -> AttrValue-encodeLabel = strictify . lazyEncodeLabel---- | Descode label from an attribute value.-decodeLabel :: SLabel l => AttrValue -> Either String l-decodeLabel = decode . decompress . lazyfy---- | Set the label of a given path. This function sets the 'labelAttr'--- attribute to the encoded label, and the hash to 'labelHashAttr'.-setPathLabelTCB :: SLabel l => FilePath -> l -> LIO l ()-setPathLabelTCB path l = ioTCB $ do-  lsetxattr path labelAttr     (strictify lEnc) RegularMode-  lsetxattr path labelHashAttr lHsh             RegularMode-    where lEnc = lazyEncodeLabel l-          lHsh = strictify . SHA.bytestringDigest . SHA.sha1 $ lEnc---- | Get the label of a given path. If the object does not have an--- associated label or the hash of the label and stored-hash are not--- equal, this function throws 'FSLabelCorrupt'.-getPathLabelTCB :: SLabel l => FilePath -> LIO l l-getPathLabelTCB path = rethrowIoTCB $ do-  (b, h) <- throwOnFail $ do b <- lgetxattr path labelAttr-                             h <- lgetxattr path labelHashAttr-                             return (b, h)-  let b' = lazyfy b-      h' = strictify . SHA.bytestringDigest . SHA.sha1 $ b'-  case decodeLabel b of-    Right l | h == h' -> return l-    _                 -> doFail-  where doFail = throwIO $ FSLabelCorrupt path-        throwOnFail act = act `E.catch` (\(_:: SomeException) -> doFail)----- | Create a directory object with the given label.-createDirectoryTCB :: (SLabel l) => l -> FilePath -> LIO l ()-createDirectoryTCB l path = do-  rethrowIoTCB $ createDirectory path-  setPathLabelTCB path l---- | Create a file object with the given label and return a handle to--- the new file.-createFileTCB :: (SLabel l) => l -> FilePath -> IOMode -> LIO l Handle-createFileTCB l path mode = do-  h <- rethrowIoTCB $ openFile path mode-  setPathLabelTCB path l-  return h------- Labeled 'FilePath's-----data LFilePath l = LFilePathTCB { labelOfFilePath :: l-                                -- ^ Label of file path-                                , unlabelFilePathTCB :: FilePath-                                -- ^ Unlabel a filepath, ignoring IFC.-                                } ------- Misc helper------- | Convert lazy ByteString to strict ByteString.-strictify :: L8 -> S8-strictify = S8.concat . L.toChunks---- | Convert strict ByteString to lazy ByteString.-lazyfy :: S8 -> L8-lazyfy x = L8.fromChunks [x]---- | Compress with zlib (optimized for speed).-compress :: L8 -> L8-compress = compressWith (defaultCompressParams { compressLevel = bestSpeed })

@@ -1,97 +0,0 @@-{-# LANGUAGE Safe #-}--{- |--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 'gate' to create a gate data type @'Gate' d a@-given a computation of type @d -> a@. Here, @d@ is a privilege-description (type variable for an instance of 'PrivDesc').  Gates are-invoked with 'callGate', and as such the service provider has the-guarantee that the client (the caller) 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 before-performing the \"actual\" computation.  The client and server solely-need to trust the implementation of 'callGate'.---}--module LIO.Gate (-    Gate-  , gate, callGate-  -- * Example-  -- $example-  ) where--import           LIO.Privs---- | A Gate is a lambda abstraction from a privilege description to an--- arbitrary type @a@. Applying the gate is accomplished with 'callGate'--- which takes a privilege argument that is converted to a description--- before invoking the gate computation.-newtype Gate d a = Gate { unGate :: d -> a }---- | Create a gate given a computation from a privilege description.--- Note that because of currying type 'a' may itself be a function--- type and thus gates can take arguments in addition to the privilege--- descriptoin.-gate :: PrivDesc p d-     => (d -> a)  -- ^ Gate computation-     -> Gate d a-gate = Gate---- | Given a gate and privilege, execute the gate computation.  It is--- important to note that @callGate@ invokes the gate computation with--- the privilege description and /NOT/ the privilege itself.------ Note that, in general, code should /not/ provide privileges to--- functions other than @callGate@ when wishing to call a gate. This--- function is provided by LIO since it can be easily inspected by--- both the gate creator and caller to be doing the \"right\" thing:--- provide the privilege description corresponding to the supplied--- privilege as \"proof\" without explicitly passing in the privilege.--- -callGate :: PrivDesc p d-         => Gate d a -- ^ Gate-         -> p        -- ^ Privilege used as proof-of-ownership-         -> a-callGate g = unGate g . privDesc--{- $example--This example uses "LIO.DCLabel" to demonstrate the use of gates.  The-service provider provides @addGate@ which adds two integers if the-gate is called by a piece of code that owns the \"Alice\" or \"Bob\"-principals. Otherwise, it simply returns @Nothing@.--> import LIO-> import LIO.DCLabel-> -> import LIO.Privs.TCB (mintTCB)-> -> -> -- | Add two numbers if the computation is invoked by Alice or Bob.-> addGate :: DCGate (Int -> Int -> Maybe Int)-> addGate = gate $ \pd a b ->->   if pd `elem` (dcPrivDesc `map` ["Alice", "Bob"])->     then Just $ a + b->     else Nothing-> -> -> alice, bob, clark :: DCPriv-> alice = mintTCB . dcPrivDesc $ "Alice"-> bob   = mintTCB . dcPrivDesc $ "Bob"-> clark = mintTCB . dcPrivDesc $ "Clark"-> -> main = putStrLn . show $ ->   [ callGate addGate alice 1 2 -- Just 3->   , callGate addGate bob   3 4 -- Just 7->   , callGate addGate clark 5 6 -- Nothing->   ]----}

@@ -1,549 +0,0 @@-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE ConstraintKinds,-             FlexibleInstances,-             FlexibleContexts,-             TypeSynonymInstances,-             MultiParamTypeClasses #-}-{- | --This module abstracts the basic file 'Handle' methods provided by the-system library, and provides a 'LabeledHandle' type that can be-manipulated from within the 'LIO' Monad. A 'LabeledHandle' is imply a-file 'Handle' with an associated label that is used to track and-control the information flowing from and to the file. The API exposed-by this module is analogous to "System.IO", and the functions mainly-differ in taking an additional label and enforcing IFC.--The actual storage of labeled files is handled by the "LIO.FS" module.-The filesystem is implemented as a file store in which labels are-associated with files and directories (using extended attributes).--/IMPORTANT:/ To use the labeled filesystem you must use-'evalWithRootFS' (or other initializers from "LIO.FS.TCB"), otherwise-any actions built using the combinators of this module will crash.--An example use case shown below: -->->  main = dcEvalWithRoot "/tmp/lioFS" $ do->    createDirectoryP p lsecrets "secrets"->    writeFileP p ("secrets" </> "alice" ) "I like Bob!"->      where p = ...->            lsecrets = ....->--The file store for the labeled filesystem (see "LIO.FS") will-be created in @\/tmp\/lioFS@, but this is transparent and the user-can think of the filesystem as having root @/@. Note that for this to-work the filesystem must be mounted with the @user_xattr@ option.-For example, on GNU/Linux:--> mount -o rw,noauto,user,sync,noexec,user_xattr /dev/sdb1 /tmp/lioFS--In the current version of the filesystem, there is no notion of-changeable current working directory in the 'LIO' Monad, nor symbolic-links.--}-module LIO.Handle ( evalWithRootFS-                  , SLabel-                  , SMonadLIO-                    -- * LIO Handle-                  , LabeledHandle, Handle-                  , IOMode(..)-                  , BufferMode(..)-                    -- * File operations-                  , openFile, openFileP-                  , hClose, hCloseP-                  , hFlush, hFlushP-                  , HandleOps(..)-                  , hGetP-                  , hGetNonBlockingP-                  , hGetContentsP-                  , hGetLineP-                  , hPutP-                  , hPutStrP-                  , hPutStrLnP-                  -- ** Special cases-                  , readFile, readFileP-                  , writeFile, writeFileP-                  -- * Directory operations-                  , getDirectoryContents, getDirectoryContentsP-                  , createDirectory, createDirectoryP-                  -- * Setting/getting handle status/settings-                  , hSetBuffering, hSetBufferingP-                  , hGetBuffering, hGetBufferingP-                  , hSetBinaryMode, hSetBinaryModeP-                  , hIsEOF, hIsEOFP-                  , hIsOpen, hIsOpenP-                  , hIsClosed, hIsClosedP-                  , hIsReadable, hIsReadableP-                  , hIsWritable, hIsWritableP-                  ) where--import Prelude hiding (readFile, writeFile)--import           Data.Binary-import qualified Data.ByteString.Char8 as S8-import qualified Data.ByteString.Lazy.Char8 as L8--import           Control.Monad-import           Control.Exception (throwIO)---import           System.IO (IOMode(..), BufferMode(..), Handle)-import qualified System.IO as IO-import qualified System.Directory as IO-import           System.FilePath--import           LIO-import           LIO.Labeled.TCB-import           LIO.TCB-import           LIO.FS.TCB------- LIO related------- | Serialize 'MonadLIO'-type SMonadLIO l m = (SLabel l, MonadLIO l m)----- | Same as 'evalLIO', but takes two additional parameters--- corresponding to the path of the labeled filesystem store and the--- label of the root. If the labeled filesystem store does not exist,--- it is created at the specified path with the root having the--- supplied label.--- If the filesystem does exist, the supplied label is ignored and thus--- unnecessary. However, if the root label is not provided and the--- filesystem has not been initialized, a 'FSRootNeedLabel' exception--- will be thrown.-evalWithRootFS :: SLabel l-               => FilePath   -- ^ Filesystem root-               -> Maybe l    -- ^ Label of root-               -> LIO l a    -- ^ LIO action-               -> LIOState l -- ^ Initial state-               -> IO a-evalWithRootFS path ml act = evalLIO (initFSTCB path ml >> act)------- LIO Handle Operations------- | Get the contents of a directory. The current label is raised to the--- join of the current label and that of all the directories traversed to--- the leaf directory. Note that, unlike the standard Haskell--- 'getDirectoryContents', we first normalise the path by collapsing all--- the @..@'s. The function uses 'unlabelFilePath' when raising the--- current label and thus may throw an exception if the clearance is--- too low.--- /Note:/ The current LIO filesystem does not support links.-getDirectoryContents :: SMonadLIO l m => FilePath -> m [FilePath]-getDirectoryContents = getDirectoryContentsP NoPrivs---- | Same as 'getDirectoryContents', but uses privileges when raising--- the current label.-getDirectoryContentsP :: (SMonadLIO l m, Priv l p)-                      => p              -- ^ Privilege-                      -> FilePath       -- ^ Directory-                      -> m [FilePath]-getDirectoryContentsP p dir = do-  path <- taintObjPathP p dir-  liftLIO . rethrowIoTCB $ IO.getDirectoryContents path---- | Create a directory at the supplied path with the given label.  The--- given label must be bounded by the the current label and clearance, as--- checked by 'guardAlloc'.  The current label (after traversing the--- filesystem to the directory path) must flow to the supplied label,--- which must, in turn, flow to the current label as required by--- 'guardWrite'.-createDirectory :: SMonadLIO l m => l -> FilePath -> m ()-createDirectory = createDirectoryP NoPrivs---- | Same as 'createDirectory', but uses privileges when raising the--- current label and checking IFC restrictions.-createDirectoryP :: (SMonadLIO l m, Priv l p)-                 => p           -- ^ Privilege-                 -> l           -- ^ Label of new directory-                 -> FilePath    -- ^ Path of directory-                 -> m ()-createDirectoryP p l dir0 = do-  -- Check that the label is bounded by the current label and clearance:-  guardAllocP p l-  -- Clean up directory:-  dir  <- cleanUpPath dir0-  let (containingDir, dName) = breakDir dir-  -- Taint up to containing dir:-  path <- taintObjPathP p containingDir-  -- Get label of containing dir:-  ldir <- liftLIO $ getPathLabelTCB path-  -- Can write to containing dir:-  guardWriteP p ldir-  -- Can still create dir:-  guardAllocP p l-  -- Create actual directory:-  liftLIO $ createDirectoryTCB l $ path </> dName-    where breakDir dir = let ds  = splitDirectories dir-                             cd' = joinPath $ init ds-                             cd  = if null cd' then [pathSeparator] else cd'-                         in (cd, last ds)------- Files------- Synonym for a labeled handle.-type LabeledHandle l = Labeled l Handle---- | Given a set of privileges, a (maybe) new label of a file, a--- filepath, and the IO mode, open (and possibly create) the file. If the--- file exists, the supplied label is not necessary; otherwise it must be--- supplied.  The current label is raised to reflect all the traversed--- directories.  Additionally the label of the file (new or existing)--- must be between the current label and clearance, as imposed by--- 'guardAlloc'. If the file is created, it is further required that the--- current computation be able to write to the containing directory, as--- imposed by 'guardWrite'.-openFile :: SMonadLIO l m-         => Maybe l    -- ^ Label of file if created-         -> FilePath   -- ^ File to open-         -> IOMode     -- ^ Mode-         -> m (LabeledHandle l)-openFile = openFileP NoPrivs---- | Same as 'openFile', but uses privileges when traversing--- directories and performing IFC checks.-openFileP :: (SMonadLIO l m, Priv l p)-          => p          -- ^ Privileges-          -> Maybe l    -- ^ Label of file if created-          -> FilePath   -- ^ File to open-          -> IOMode     -- ^ Mode-          -> m (LabeledHandle l)-openFileP p ml file' mode = do-  file <- cleanUpPath file'-  let containingDir = takeDirectory file-      fileName      = takeFileName  file-  -- Check that the supplied label is bounded by current label and clearance:-  maybe (return ()) (guardAllocP p) ml-  -- Taint up to containing dir:-  path <- taintObjPathP p containingDir-  --Get label of containing dir:-  ldir <- liftLIO $ getPathLabelTCB path-  -- Create actual file path:-  let objPath = path </> fileName-  -- Check if file exists:-  exists <- liftLIO . rethrowIoTCB $ IO.doesFileExist objPath-  if exists-     then do-       -- Get label of file:-       l <- liftLIO $ getPathLabelTCB objPath-       -- Make sure we can create labeled handle:-       guardAllocP p l-       -- NOTE: if mode == ReadMode, we might want to instead do-       -- guardAllocp p (l `lub` currentLabel) to allow opening     -       -- a handle for an object whose label is below the current-       -- label. Some Unix systems still update a file's atime-       -- when performing a read and so, for now, a read always-       -- implies a write.-       h <- liftLIO . rethrowIoTCB $ IO.openFile objPath mode-       return $ labelTCB l h-     else case ml of-           Nothing -> throwLIO FSObjNeedLabel-           Just l -> do-             -- Can write to containing dir:-             guardWriteP p ldir-             -- Can still create file with this label:-             guardAllocP p l-             h <- liftLIO $ createFileTCB l objPath mode-             return $ labelTCB l h---- | Close a file handle. Must be able to write to the the labeled--- handle, as checkd by 'guardWrite'.-hClose :: SMonadLIO l m => LabeledHandle l -> m ()-hClose = hCloseP NoPrivs---- | Close a labeled file handle.-hCloseP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m ()-hCloseP p lh = do-  guardWriteP p (labelOf lh)-  liftLIO . rethrowIoTCB . IO.hClose $ unlabelTCB lh----- | Flush a file handle. Must be able to write to the the labeled--- handle, as checkd by 'guardWrite'.-hFlush :: SMonadLIO l m => LabeledHandle l -> m ()-hFlush = hFlushP NoPrivs---- | Flush a labeled file handle.-hFlushP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m ()-hFlushP p lh = do-  guardWriteP p (labelOf lh)-  liftLIO . rethrowIoTCB . IO.hFlush $ unlabelTCB lh----- | Class used to abstract reading and writing from and to handles,--- respectively.-class Monad m => HandleOps h b m where-  hGet            :: h -> Int -> m b-  hGetNonBlocking :: h -> Int -> m b-  hGetContents    :: h -> m b-  hGetLine        :: h -> m b-  hPut            :: h -> b -> m ()-  hPutStr         :: h -> b -> m ()-  hPutStr         = hPut-  hPutStrLn       :: h -> b -> m ()--instance HandleOps IO.Handle L8.ByteString IO where-  hGet            = L8.hGet-  hGetNonBlocking = L8.hGetNonBlocking-  hGetContents    = L8.hGetContents-  hGetLine  h     = (L8.fromChunks . (:[])) `liftM` S8.hGetLine h-  hPut            = L8.hPut-  hPutStrLn       = L8.hPutStrLn--instance HandleOps IO.Handle S8.ByteString IO where-  hGet            = S8.hGet-  hGetNonBlocking = S8.hGetNonBlocking-  hGetContents    = S8.hGetContents-  hGetLine        = S8.hGetLine-  hPut            = S8.hPut-  hPutStrLn       = S8.hPutStrLn--instance (SLabel l, HandleOps IO.Handle b IO) =>-         HandleOps (LabeledHandle l) b (LIO l) where-  hGet            = hGetP NoPrivs-  hGetNonBlocking = hGetNonBlockingP NoPrivs-  hGetContents    = hGetContentsP NoPrivs-  hGetLine        = hGetLineP NoPrivs-  hPut            = hPutP NoPrivs-  hPutStrLn       = hPutStrLnP NoPrivs---- | Read @n@ bytes from the labeled handle, using privileges when--- performing label comparisons and tainting.-hGetP :: (Priv l p, Binary l, HandleOps IO.Handle b IO)-      => p               -- ^ Privileges-      -> LabeledHandle l -- ^ Labeled handle-      -> Int             -- ^ Number of bytes to read-      -> LIO l b-hGetP p lh n = do- guardWriteP p (labelOf lh)- liftLIO . rethrowIoTCB $ hGet (unlabelTCB lh) n---- | Same as 'hGetP', but will not block waiting for data to become--- available. Instead, it returns whatever data is available.--- Privileges are used in the label comparisons and when raising--- the current label.-hGetNonBlockingP :: (Priv l p, Binary l, HandleOps IO.Handle b IO)-                 => p -> LabeledHandle l -> Int -> LIO l b-hGetNonBlockingP p lh n = do- guardWriteP p (labelOf lh)- liftLIO . rethrowIoTCB $ hGetNonBlocking (unlabelTCB lh) n---- | Read the entire labeled handle contents and close handle upon--- reading @EOF@.  Privileges are used in the label comparisons--- and when raising the current label.-hGetContentsP :: (Priv l p, Binary l, HandleOps IO.Handle b IO)-              => p -> LabeledHandle l -> LIO l b-hGetContentsP p lh = do- guardWriteP p (labelOf lh)- liftLIO . rethrowIoTCB $ hGetContents (unlabelTCB lh)---- | Read the a line from a labeled handle.-hGetLineP :: (Priv l p, Binary l, HandleOps IO.Handle b IO)-          => p -> LabeledHandle l -> LIO l b-hGetLineP p lh = do- guardWriteP p (labelOf lh)- liftLIO . rethrowIoTCB $ hGetLine (unlabelTCB lh)---- | Output the given (Byte)String to the specified labeled handle.--- Privileges are used in the label comparisons and when raising--- the current label.-hPutP :: (Priv l p, Binary l, HandleOps IO.Handle b IO)-      => p -> LabeledHandle l -> b -> LIO l ()-hPutP p lh s = do- guardWriteP p (labelOf lh)- liftLIO . rethrowIoTCB $ hPut (unlabelTCB lh) s---- | Synonym for 'hPutP'.-hPutStrP :: (Priv l p, Binary l, HandleOps IO.Handle b IO)-          => p -> LabeledHandle l -> b -> LIO l ()-hPutStrP = hPutP---- | Output the given (Byte)String with an appended newline to the--- specified labeled handle. Privileges are used in the label--- comparisons and when raising the current label.-hPutStrLnP :: (Priv l p, Binary l, HandleOps IO.Handle b IO)-            => p -> LabeledHandle l -> b -> LIO l ()-hPutStrLnP p lh s = do- guardWriteP p (labelOf lh)- liftLIO . rethrowIoTCB $ hPutStrLn (unlabelTCB lh) s------- Special cases------- | Reads a file and returns the contents of the file as a ByteString.-readFile :: (HandleOps Handle b IO, SLabel l)-         => FilePath -> LIO l b-readFile = readFileP NoPrivs---- | Same as 'readFile' but uses privilege in opening the file.-readFileP :: (HandleOps Handle b IO, Priv l p, Binary l)-          => p -> FilePath -> LIO l b-readFileP p file = openFileP p Nothing file ReadMode >>= hGetContentsP p---- | Write a ByteString to the given filepath with the supplied label.-writeFile :: (HandleOps Handle b IO, SLabel l)-          => l -> FilePath -> b -> LIO l ()-writeFile = writeFileP NoPrivs---- | Same as 'writeFile' but uses privilege when opening, writing and--- closing the file.-writeFileP  :: (HandleOps Handle b IO, Priv l p, Binary l)-            => p -> l -> FilePath -> b -> LIO l ()-writeFileP p l file contents = do-  bracket (openFileP p (Just l) file WriteMode) (hCloseP p)-          (flip (hPutP p) contents)------- Setting/getting handle status/setting------- | Set the buffering mode-hSetBuffering :: SMonadLIO l m => LabeledHandle l -> BufferMode -> m ()-hSetBuffering = hSetBufferingP NoPrivs---- | Set the buffering mode-hSetBufferingP :: (SMonadLIO l m, Priv l p)-               => p -> LabeledHandle l -> BufferMode -> m ()-hSetBufferingP p lh m = do-  guardWriteP p (labelOf lh)-  liftLIO . rethrowIoTCB $ IO.hSetBuffering (unlabelTCB lh) m---- | Get the buffering mode-hGetBuffering :: SMonadLIO l m => LabeledHandle l -> m BufferMode-hGetBuffering = hGetBufferingP NoPrivs---- | Get the buffering mode-hGetBufferingP :: (SMonadLIO l m, Priv l p)-               => p -> LabeledHandle l -> m BufferMode-hGetBufferingP p lh = do-  taintP p (labelOf lh)-  liftLIO . rethrowIoTCB $ IO.hGetBuffering (unlabelTCB lh)---- | Select binary mode ('True') or text mode ('False')-hSetBinaryMode :: SMonadLIO l m => LabeledHandle l -> Bool -> m ()-hSetBinaryMode = hSetBinaryModeP NoPrivs---- | Select binary mode ('True') or text mode ('False')-hSetBinaryModeP :: (SMonadLIO l m, Priv l p)-                => p -> LabeledHandle l -> Bool -> m ()-hSetBinaryModeP p lh m = do-  guardWriteP p (labelOf lh)-  liftLIO . rethrowIoTCB $ IO.hSetBinaryMode (unlabelTCB lh) m---- | End of file.-hIsEOF :: SMonadLIO l m => LabeledHandle l -> m Bool-hIsEOF = hIsEOFP NoPrivs---- | End of file.-hIsEOFP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool-hIsEOFP p lh = do-  taintP p (labelOf lh)-  liftLIO . rethrowIoTCB $ IO.hIsEOF (unlabelTCB lh)-                                                                          --- | Is handle open.                                                      -hIsOpen :: SMonadLIO l m => LabeledHandle l -> m Bool      -hIsOpen = hIsOpenP NoPrivs---- | Is handle open.                                                      -hIsOpenP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool      -hIsOpenP p lh = do-  taintP p (labelOf lh)-  liftLIO . rethrowIoTCB $ IO.hIsOpen (unlabelTCB lh)-                                                                          --- | Is handle closed.                                                    -hIsClosed :: SMonadLIO l m => LabeledHandle l -> m Bool      -hIsClosed = hIsClosedP NoPrivs---- | Is handle closed.                                                    -hIsClosedP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool-hIsClosedP p lh = do-  taintP p (labelOf lh)-  liftLIO . rethrowIoTCB $ IO.hIsClosed (unlabelTCB lh)-                                                                          --- | Is handle readable.                                                  -hIsReadable :: SMonadLIO l m => LabeledHandle l -> m Bool      -hIsReadable = hIsReadableP NoPrivs---- | Is handle readable.                                                  -hIsReadableP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool-hIsReadableP p lh = do-  taintP p (labelOf lh)-  liftLIO . rethrowIoTCB $ IO.hIsReadable (unlabelTCB lh)-                                                                          --- | Is handle writable.                                                  -hIsWritable :: SMonadLIO l m => LabeledHandle l -> m Bool-hIsWritable = hIsWritableP NoPrivs---- | Is handle writable.                                                  -hIsWritableP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool-hIsWritableP p lh = do-  taintP p (labelOf lh)-  liftLIO . rethrowIoTCB $ IO.hIsWritable (unlabelTCB lh)------- Internal helpers------- | Given a pathname to a labeled filesystem object, traverse all the--- directories up to the object, while correspondingly raising the--- current label. Note that if the object or a parent-directory does not--- exist, an exception will be thrown; the label of the exception will be--- the join of all the directory labels up to the lookup failure.------ /Note:/ this function cleans up the path before doing the--- lookup, so e.g., path @/foo/bar/..@ will first be rewritten to @/foo@--- and thus no traversal to @bar@.  Note that this is a more permissive--- behavior than forcing the read of @..@ from @bar@.--- @taintObjPath@ returns this cleaned up path.-taintObjPathP :: (SMonadLIO l m, Priv l p)-              => p         -- ^ Privilege -              -> FilePath  -- ^ Path to object-              -> m FilePath-taintObjPathP p path0 = do-  -- Clean up supplied path:-  path <- cleanUpPath path0-  -- Get root directory:-  root <- liftLIO $ getRootDirTCB-  let dirs = splitDirectories . stripSlash $ path-  -- "Traverse" all directories up to object:-  forM_ ("" : allSubDirs dirs) $ \dir -> do-    l <- liftLIO $ getPathLabelTCB (root </> dir)-    taintP p l-  return $ root </> joinPath dirs---- | Take a list of directories (e.g., @[\"a\",\"b\",\"c\"]@) and return--- all the subtrees up to the node (@[\"a\",\"a/b\",\"a/b/c\"]@).-allSubDirs :: [FilePath] -> [FilePath]-allSubDirs dirs = reverse $ allSubDirs' dirs "" []-  where allSubDirs' []       _    acc = acc-        allSubDirs' (dir:[]) pfix acc = (pfix </> dir) : acc-        allSubDirs' (dir:ds) pfix acc = let ndir = pfix </> dir-                                        in allSubDirs' ds ndir (ndir : acc)---- | Remove any 'pathSeparator's from the front of a file path.-stripSlash :: FilePath -> FilePath -stripSlash [] = []-stripSlash xx@(x:xs) | x == pathSeparator = stripSlash xs-                     | otherwise          = xx---- | Cleanup a file path, if it starts out with a @..@, we consider this--- invalid as it can be used explore parts of the filesystem that should--- otherwise be unaccessible. Similarly, we remove any @.@ from the path.-cleanUpPath :: MonadLIO l m => FilePath -> m FilePath -cleanUpPath = liftLIO . rethrowIoTCB . doit . splitDirectories . normalise . stripSlash-  where doit []          = return []-        doit ("..":_)    = throwIO FSIllegalFileName-        doit (_:"..":xs) = doit xs-        doit (".":xs)    = doit xs-        doit (x:xs)      = (x </>) `liftM` doit xs

@@ -7,7 +7,7 @@ Mutable reference in the 'LIO' monad. As with other objects in LIO, mutable references have an associated label that is used to impose restrictions on its operations. In fact, labeled references-('LIORef's) are solely labeled 'IORef's with read and write access+('LIORef's) are simply labeled 'IORef's with read and write access restricted according to the label. This module is analogous to "Data.IORef", but the operations take place in the 'LIO' monad. @@ -28,30 +28,40 @@   , atomicModifyLIORef, atomicModifyLIORefP   ) where -import           LIO-import           LIO.LIORef.TCB+import Data.IORef+import LIO.Core+import LIO.Label+import LIO.Privs+import LIO.TCB+import LIO.TCB.LObj  -- -- Create labeled 'IORef's -- +-- | An @LIORef@ is an @IORef@ with an associated, fixed label.  The+-- restriction to an immutable label come from the fact that it is+-- possible to leak information through the label itself, if we wish to+-- allow @LIORef@ to be an instance of 'LabelOf'.  Of course, you can+-- create an @LIORef@ of 'Labeled' to get a limited form of+-- flow-sensitivity.+type LIORef l a = LObj l (IORef a)+ -- | To create a new reference the label of the reference must be -- below the thread's current clearance and above the current label. -- If this is the case, the reference is built. Otherwise an exception -- will be thrown by the underlying 'guardAlloc' guard.-newLIORef :: MonadLIO l m+newLIORef :: Label l           => l                  -- ^ Label of reference           -> a                  -- ^ Initial value-          -> m (LIORef l a) -- ^ Mutable reference-newLIORef = newLIORefP NoPrivs+          -> LIO l (LIORef l a) -- ^ Mutable reference+newLIORef = newLIORefP noPrivs  -- | Same as 'newLIORef' except @newLIORefP@ takes a set of -- privileges which are accounted for in comparing the label of -- the reference to the current label and clearance.-newLIORefP :: (MonadLIO l m, Priv l p) => p -> l -> a -> m (LIORef l a)-newLIORefP p l a = do-  guardAllocP p l-  newLIORefTCB l a+newLIORefP :: PrivDesc l p => Priv p -> l -> a -> LIO l (LIORef l a)+newLIORefP p l a = guardAllocP p l >> ioTCB (LObjTCB l `fmap` newIORef a)  -- -- Read 'LIORef's@@ -62,15 +72,13 @@ -- the current label is raised to the join of the current label and -- the reference label. To avoid failures (introduced by the 'taint' ---guard) use 'labelOf' to check that a read will succeed.-readLIORef :: MonadLIO l m => LIORef l a -> m a-readLIORef = readLIORefP NoPrivs+readLIORef :: Label l => LIORef l a -> LIO l a+readLIORef (LObjTCB l r) = taint l >> ioTCB (readIORef r)  -- | Same as 'readLIORef' except @readLIORefP@ takes a privilege object -- which is used when the current label is raised.-readLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> m a-readLIORefP p lr = do-  taintP p $! labelOf lr-  readLIORefTCB lr+readLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> LIO l a+readLIORefP p (LObjTCB l r) = taintP p l >> ioTCB (readIORef r)  -- -- Write 'LIORef's@@ -80,16 +88,14 @@ -- the current label can-flow-to the label of the reference, and the -- label of the reference can-flow-to the current clearance. Otherwise, -- an exception is raised by the underlying 'guardAlloc' guard.-writeLIORef :: MonadLIO l m => LIORef l a -> a -> m ()-writeLIORef = writeLIORefP NoPrivs+writeLIORef :: Label l => LIORef l a -> a -> LIO l ()+writeLIORef (LObjTCB l r) a = guardAlloc l >> ioTCB (writeIORef r a)  -- | Same as 'writeLIORef' except @writeLIORefP@ takes a set of -- privileges which are accounted for in comparing the label of -- the reference to the current label and clearance.-writeLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> a -> m ()-writeLIORefP p lr a = do-  guardAllocP p $! labelOf lr -  writeLIORefTCB lr a+writeLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> a -> LIO l ()+writeLIORefP p (LObjTCB l r) a = guardAllocP p l >> ioTCB (writeIORef r a)  -- -- Modify 'LIORef's@@ -107,16 +113,14 @@              =>  LIORef l a            -- ^ Labeled reference              -> (a -> a)               -- ^ Modifier              -> LIO l ()-modifyLIORef = modifyLIORefP NoPrivs+modifyLIORef (LObjTCB l r) f = guardAlloc l >> ioTCB (modifyIORef r f)  -- | Same as 'modifyLIORef' except @modifyLIORefP@ takes a set of -- privileges which are accounted for in comparing the label of -- the reference to the current label and clearance.-modifyLIORefP :: (MonadLIO l m, Priv l p)-              =>  p -> LIORef l a -> (a -> a) -> m ()-modifyLIORefP p lr f = do-  guardAllocP p $! labelOf lr -  modifyLIORefTCB lr f+modifyLIORefP :: PrivDesc l p+              =>  Priv p -> LIORef l a -> (a -> a) -> LIO l ()+modifyLIORefP p (LObjTCB l r) f = guardAllocP p l >> ioTCB (modifyIORef r f)  -- | Atomically modifies the contents of an 'LIORef'. It is required -- that the label of the reference be above the current label, but@@ -127,13 +131,12 @@ -- labels). These checks and label raise are done by 'guardWrite', -- which will raise an exception if any of the IFC conditions cannot -- be satisfied.-atomicModifyLIORef :: MonadLIO l m => LIORef l a -> (a -> (a, b)) -> m b-atomicModifyLIORef = atomicModifyLIORefP NoPrivs+atomicModifyLIORef :: Label l => LIORef l a -> (a -> (a, b)) -> LIO l b+atomicModifyLIORef = blessTCB atomicModifyIORef  -- | Same as 'atomicModifyLIORef' except @atomicModifyLIORefP@ takes -- a set of privileges which are accounted for in label comparisons.-atomicModifyLIORefP :: (MonadLIO l m, Priv l p)-                    => p -> LIORef l a -> (a -> (a, b)) -> m b-atomicModifyLIORefP p lr f = do-  guardWriteP p $! labelOf lr -  atomicModifyLIORefTCB lr f+atomicModifyLIORefP :: PrivDesc l p+                    => Priv p -> LIORef l a -> (a -> (a, b)) -> LIO l b+atomicModifyLIORefP = blessPTCB atomicModifyIORef+

@@ -1,94 +0,0 @@-{-# LANGUAGE Unsafe #-}-{- |--This module implements the core of labeled 'IORef's in the 'LIO ad.-to "Data.IORef", but the operations take place in the 'LIO' monad.  The-types and functions exported by this module are strictly TCB and do-not perform any information flow checks. The external, safe interface-is provided and documented in "LIO.LIORef".---Different from many labeled objects (e.g., files or MVars), references-are uni-directional. This means that reading from a reference can be-done without being able to write to it; and writing to a refernece can-be done without raising the current label, as if also performing a read.---}-module LIO.LIORef.TCB (-  LIORef(..)-  -- * Basic Functions-  -- ** Create labeled 'IORef's-  , newLIORefTCB-  -- ** Read 'LIORef's-  , readLIORefTCB-  -- ** Write 'LIORef's-  , writeLIORefTCB-  -- ** Modify 'LIORef's-  , modifyLIORefTCB, atomicModifyLIORefTCB-  ) where--import           LIO-import           LIO.TCB-import           Data.IORef----- | An @LIORef@ is an @IORef@ with an associated, fixed label.  The--- restriction to an immutable label come from the fact that it is--- possible to leak information through the label itself, if we wish to--- allow @LIORef@ to be an instance of 'LabelOf'.  Of course, you can--- create an @LIORef@ of 'Labeled' to get a limited form of--- flow-sensitivity.-data LIORef l a = LIORefTCB { labelOfLIORef :: !l-                            -- ^ Label of the labeled 'IORef'.-                            , unlabelLIORefTCB :: (IORef a)-                            -- ^ Access the underlying 'IORef', ignoring IFC.-                            }---- | Get the label of an 'LIORef'.-instance LabelOf LIORef where-  labelOf = labelOfLIORef------- Create labeled 'IORef's------- | Trusted constructor that creates labeled references with the--- given label without any IFC checks.-newLIORefTCB :: MonadLIO l m => l -> a -> m (LIORef l a)-newLIORefTCB l a = do-  ior <- liftLIO . ioTCB $! newIORef a-  return $! LIORefTCB l ior------- Write 'LIORef's------- | Trusted function used to read the value of a reference without--- raising the current label.-readLIORefTCB :: MonadLIO l m => LIORef l a -> m a-readLIORefTCB = liftLIO . ioTCB . readIORef . unlabelLIORefTCB------- Write 'LIORef's------- | Trusted function used to write a new value into a labeled--- reference, ignoring IFC.-writeLIORefTCB :: MonadLIO l m => LIORef l a -> a -> m ()-writeLIORefTCB lr a = liftLIO . ioTCB $! writeIORef (unlabelLIORefTCB lr) a------- Modify 'LIORef's------- | Trusted function that mutates the contents on an 'LIORef',--- ignoring IFC.-modifyLIORefTCB :: MonadLIO l m =>  LIORef l a -> (a -> a) -> m ()-modifyLIORefTCB lr f = liftLIO . ioTCB $! modifyIORef (unlabelLIORefTCB lr) f---- | Trusted function used to atomically modify the contents of a--- labeled reference, ignoring IFC.-atomicModifyLIORefTCB :: MonadLIO l m => LIORef l a -> (a -> (a, b)) -> m b-atomicModifyLIORefTCB lr f =-  liftLIO . ioTCB $! atomicModifyIORef (unlabelLIORefTCB lr) f-

@@ -26,7 +26,7 @@ /clearance/ (accessible via the @getClearance@ function), that represents the highest value the current thread can raise its label to. The purpose of clearance is to enforce discretionary access-control: you can set the clearance to a label @L_clear@ as to prevent+control: you can set the clearance to a label @L_clear@ so as to prevent a piece of LIO code from accessing anything above @L_clear@.  Conversely, it is only permissible to modify data labeled @L_w@ when@@ -69,12 +69,11 @@  module LIO.Label (   -- * Labels-    Label(..), upperBound, lowerBound+    Label(..)   -- * Accessing label of labeled values  , LabelOf(..)   ) where -import Data.Typeable  -- | This class defines a label format, corresponding to a bounded -- lattice (see <https://en.wikipedia.org/wiki/Bounded_lattice>).@@ -85,15 +84,9 @@ -- 'glb' (in literature, written as &#8851;), and of course the -- can-flow-to partial-order 'canFlowTo' (in literature, written as -- &#8849;).-class (Eq l, Show l, Typeable l) => Label l where-  -- | Bottom, or minimum, element. It must be that for any label @L@, -  -- @'bottom' ``canFlowTo`` L@.-  bottom :: l-  -- | Top, or maximum, element. It must be that for any label @L@, -  -- @L ``canFlowTo`` 'top'@.-  top :: l+class (Eq l, Show l) => Label l where   -- | /Least/ upper bound, or join, of two labels. For any two labels-  -- @L_1@ and @L_2@, such that @L_3 = L_1 ``lub`` L_2@, it must be that:+  -- @L_1@ and @L_2@, if @L_3 = L_1 \`lub` L_2@, it must be that:   --   -- * @L_1 ``canFlowTo`` L_3@,   --@@ -105,7 +98,7 @@   --   such element.   lub :: l -> l -> l   -- | /Greatest/ lower bound, or meet, of two labels. For any two labels-  -- @L_1@ and @L_2@, such that @L_3 = L_1 ``glb`` L_2@, it must be that:+  -- @L_1@ and @L_2@, if @L_3 = L_1 \`glb` L_2@, it must be that:   --   -- * @L_3 ``canFlowTo`` L_1@,   --@@ -117,31 +110,20 @@   --   such element.   glb :: l -> l -> l   -- | Can-flow-to relation. An entity labeled @L_1@ should be allowed-  -- to affect an entity @L_2@ only if @L_1 ``canFlowTo`` L_2@. This+  -- to affect an entity @L_2@ only if @L_1 \`canFlowTo` L_2@. This   -- relation on labels is at least a partial order (see   -- <https://en.wikipedia.org/wiki/Partially_ordered_set>), and must   -- satisfy the following rules:   ---  -- * Reflexivity: @L_1 ``canFlowTo`` L_1@ for any @L_1@.+  -- * Reflexivity: @L_1 \`canFlowTo` L_1@ for any @L_1@.   ---  -- * Antisymmetry: If @L_1 ``canFlowTo`` L_2@ and-  --   @L_2 ``canFlowTo`` L_1@ then @L_1 = L_2@.+  -- * Antisymmetry: If @L_1 \`canFlowTo` L_2@ and+  --   @L_2 \`canFlowTo` L_1@ then @L_1 = L_2@.   ---  -- * Transitivity: If @L_1 ``canFlowTo`` L_2@ and-  --   @L_2 ``canFlowTo`` L_3@ then @L_1 ``canFlowTo`` L_3@.+  -- * Transitivity: If @L_1 \`canFlowTo` L_2@ and+  --   @L_2 \`canFlowTo` L_3@ then @L_1 \`canFlowTo` L_3@.   canFlowTo :: l -> l -> Bool --- | A more meaningful name for 'lub'. Note that since the name--- does not imply /least/ upper bound it is not a method of 'Label'.-upperBound :: Label l => l -> l -> l-upperBound = lub---- | A more meaningful name for 'glb'. Note that since the name--- does not imply /greatest/ lower bound it is not a method of--- 'Label'.-lowerBound :: Label l => l -> l -> l-lowerBound = glb- -- | Generic class used to get the type of labeled objects. For, -- instance, if you wish to associate a label with a pure value (as in -- "LIO.Labeled"), you may create a data type:@@ -156,5 +138,4 @@ -- >   labelOf (LValTCB lv) = fst lv class LabelOf t where   -- | Get the label of a type kinded @* -> *@-  labelOf :: Label l => t l a -> l-  +  labelOf :: t l a -> l

@@ -34,32 +34,17 @@   , unlabel, unlabelP   -- * Relabel values   , relabelLabeledP-  , taintLabeled, taintLabeledP , untaintLabeled, untaintLabeledP-  -- * Labeled functor-  -- $functor-  , LabeledFunctor(..)-#ifdef TO_LABELED-  -- * Executing sensitive computation-  -- $toLabeled-  , toLabeled, toLabeledP-  , discard, discardP-#endif+  , taintLabeled, taintLabeledP , untaintLabeledP+  , lFmap, lAp   ) where -import           LIO.TCB-import           LIO.Label-import           LIO.Core-import           LIO.Privs-import           LIO.Labeled.TCB-import           Control.Monad--#ifdef TO_LABELED-import qualified Control.Exception as E-#endif+import Control.Monad --- | Returns label of a 'Labeled' type.-instance LabelOf Labeled where-  labelOf = labelOfLabeled+import LIO.Exception+import LIO.TCB+import LIO.Label+import LIO.Core+import LIO.Privs  -- -- Label values@@ -70,8 +55,8 @@ -- @ccurrent@, then the label @l@ specified must satisfy @lcurrent -- ``canFlowTo`` l && l ``canFlowTo`` ccurrent@. Otherwise an -- exception is thrown (see 'guardAlloc').-label :: MonadLIO l m => l -> a -> m (Labeled l a)-label = labelP NoPrivs+label :: Label l => l -> a -> LIO l (Labeled l a)+label = labelP noPrivs  -- | Constructs a 'Labeled' using privilege to allow the `Labeled`'s -- label to be below the current label.  If the current label is@@ -81,10 +66,10 @@ -- the clearance.  You must use 'setClearanceP' to raise the clearance -- first if you wish to create an 'Labeled' at a higher label than the -- current clearance.-labelP :: (MonadLIO l m, Priv l p) => p -> l -> a -> m (Labeled l a)+labelP :: PrivDesc l p => Priv p -> l -> a -> LIO l (Labeled l a) labelP p l a = do   guardAllocP p l-  return $! labelTCB l a+  return $ LabeledTCB l a  -- -- Unlabel values@@ -101,40 +86,36 @@ -- current clearance, then @unlabel@ throws 'ClearanceViolation'. -- However, you can use 'labelOf' to check if 'unlabel' will succeed -- without throwing an exception.-unlabel :: MonadLIO l m => Labeled l a -> m a-unlabel = unlabelP NoPrivs+unlabel :: Label l => Labeled l a -> LIO l a+unlabel = unlabelP noPrivs  -- | Extracts the value of an 'Labeled' just like 'unlabel', but takes a -- privilege argument to minimize the amount the current label must be -- raised.  Function will throw 'ClearanceViolation' under the same -- circumstances as 'unlabel'.-unlabelP :: (MonadLIO l m, Priv l p) => p -> Labeled l a -> m a-unlabelP p lv = do-  taintP p $! labelOf lv-  return $! unlabelTCB lv+unlabelP :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a+unlabelP p (LabeledTCB l v) = taintP p l >> return v  -- -- Relabel values --  -- | Relabels a 'Labeled' value to the supplied label if the given--- privilege privileges permits it. It must be that the original--- label and new label are equal, modulo the supplied privileges. In--- other words the label remains in the same congruence class.+-- privilege privileges permits it.  An exception is thrown unless the+-- following two conditions hold: ----- Consequently @relabelP p l lv@ throws an 'InsufficientPrivs'--- exception if+--   1. The new label must be between the current label and clearance+--      (modulo privileges), as enforced by 'guardAllocP'. ----- @'canFlowToP' p l ('labelOf' lv) && 'canFlowToP' p ('labelOf' lv) l@+--   2. The old label must flow to the new label (again modulo+--      privileges), as enforced by 'canFlowToP'. ----- does not hold.-relabelLabeledP :: (MonadLIO l m, Priv l p)-                => p -> l -> Labeled l a -> m (Labeled l a)-relabelLabeledP p newl lv = do-  let origl = labelOf lv-  unless (canFlowToP p newl origl &&-          canFlowToP p origl newl) $ throwLIO InsufficientPrivs-  return . labelTCB newl $! unlabelTCB lv+relabelLabeledP :: PrivDesc l p+                => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)+relabelLabeledP p newl (LabeledTCB oldl v) = do+  guardAllocP p newl+  unless (canFlowToP p oldl newl) $ throwLIO InsufficientPrivs+  return $ LabeledTCB newl v  -- | Raises the label of a 'Labeled' to the 'upperBound' of it's current -- label and the value supplied.  The label supplied must be bounded by@@ -142,28 +123,23 @@ -- if the 'Labeled' is already above the current thread's clearance. If -- the supplied label is not bounded then @taintLabeled@ will throw an -- exception (see 'guardAlloc').-taintLabeled :: MonadLIO l m => l -> Labeled l a -> m (Labeled l a)-taintLabeled = taintLabeledP NoPrivs+taintLabeled :: Label l => l -> Labeled l a -> LIO l (Labeled l a)+taintLabeled = taintLabeledP noPrivs  -- | Same as 'taintLabeled', but uses privileges when comparing the -- current label to the supplied label. In other words, this function -- can be used to lower the label of the labeled value by leveraging -- the supplied privileges.-taintLabeledP :: (MonadLIO l m, Priv l p)-              => p -> l -> Labeled l a -> m (Labeled l a)-taintLabeledP p l lv = do-  guardAllocP p l-  return . labelTCB (l `upperBound` labelOf lv) $! unlabelTCB lv---- | Downgrades the label of a 'Labeled' as much as possible given the--- current privilege.-untaintLabeled :: MonadLIO l m => l -> Labeled l a -> m (Labeled l a)-untaintLabeled = untaintLabeledP NoPrivs+taintLabeledP :: PrivDesc l p+              => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)+taintLabeledP p l (LabeledTCB lold v) = do+  let lnew = lold `lub` l+  guardAllocP p lnew+  return $ LabeledTCB lnew v --- | Same as 'untaintLabeled' but uses the supplied privileges when--- downgrading the label of the labeled value.-untaintLabeledP :: (MonadLIO l m, Priv l p)-                => p -> l -> Labeled l a -> m (Labeled l a)+-- | Downgrades a label.+untaintLabeledP :: PrivDesc l p+                => Priv p -> l -> Labeled l a -> LIO l (Labeled l a) untaintLabeledP p target lv =   relabelLabeledP p (partDowngradeP p (labelOf lv) target) lv @@ -178,194 +154,35 @@ 2. 'LIO' is polymorphic in the label type and thus 'fmap' would is    susceptible to /refinement attacks/. Superficially if the label type    contains an integrity component (see for example "LIO.DCLabel")-   then @fmap (\ -> 3) lv@ would produce a high-integrity labeled @3@+   then @fmap (const 3) lv@ would produce a high-integrity labeled @3@    if @lv@ is a high-integrity labeled value without any any authority    or /endorsement/. -As a result, we provide a class 'LabeledFunctor' that export 'lFmap'-(labeled 'lFmap') that addressed the above issues. Firstly, each newly-created value is in the 'LIO' monad and secondly each label format-implementation must produce their own definition of 'lFmap' such that-the end label protects the computation result accordingly.---}---- | IFC-aware functor instance. Since certain label formats may contain--- integrity information, this is provided as a class rather than a--- function. Such label formats will likely wish to drop endorsements in--- the new labeled valued.-class Label l => LabeledFunctor l where-  -- | 'fmap'-like funciton that is aware of the current label and-  -- clearance.-  lFmap :: MonadLIO l m => Labeled l a -> (a -> b) -> m (Labeled l b)--#ifdef TO_LABELED--{- $toLabeled--LIO provides a means for executing a sensitive computation without-raising the current label. This is done with the function 'toLabeled'.-The semantics of the function is as follows:--1. Execute whatever action is supplied. This action may raise the-current label or lower the current clearance.--2. Take the result of the computation and wrap it in a 'Labeled'-value. The label of the value is provided as an argument to-'toLabeled'. Hence, the computation should not observe anything more-sensitive than this.--3. Restore the current label and clearance to that of step 1. Return-the 'Labeled' value created in step 2, if the end current label is not-above the value's label. Otherwise raise an exception to indicate that-the computation read data more sensitive than the set bound.--Note that if the executed computation raises an exception, 'toLabeled'-hides the exception -- this exception is only propagated when the-'Labeled' value is 'unlabel'ed.+Similarly, defining an instance of 'Applicative' is an issue. -NOTE:-As indicated by the warnings, 'toLabeled' is not safe with respect to-/termination sensitive non-interference/. This means that a malicious-computation can carry out an attack that leaks information by not-terminating in a 'toLabeled' block. Similarly an attacker can leverage-timing to do the same.  Your version of LIO has been compiled with the-@toLabeled@ flag, and thus susceptible to such attacks. If this was-not by choice, recompile the package (by default, 'toLabeled' is not-included) and use the primitives in "LIO.Concurrent" to implement a-similarly-behaving program.+Instead, we provide 'lFmap' (labeled 'fmap') and 'lAp' that address+the above issues.  -} --- | @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--- computation is packaged into a 'Labeled' with a supplied--- label. (Of couse, the computation executed by @toLabeled@ must--- most observe any data whose label exceeds the supplied label.)------ To get at the result of the computation one will have to call--- 'unlabel' and raise the label, but this can be postponed, or--- done inside some other call to 'toLabeled'.  This suggests that--- the provided label must be above the current label and below--- the current clearance.  ----- Note that @toLabeled@ always restores the clearance to whatever--- it was when it was invoked, regardless of what occurred in the--- computation producing the value of the 'Labeled'.  This highlights--- one main use of clearance: to ensure that a @Labeled@ computed--- does not exceed a particular label.------ If an exception is thrown within a @toLabeled@ block, such that--- the outer context is withing a 'catchLIO', which is further 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.)------  > main = evalDC' $ do---  >   lRef <- newLIORef bottom ""---  >   hRef <- newLIORef top "secret"---  >   -- brute force:---  >   forM_ ["fun", "secret"] $ \guess -> do---  >     stash <- readLIORef lRef---  >     writeLIORef lRef $ stash ++ "\n" ++ guess ++ ":"---  >     discard top $ do---  >       catchLIO ( discard top $ do---  >                    secret <- readLIORef hRef---  >                    when (secret == guess) $ throwIO . userError $ "got it!"---  >                ) (\(e :: IOError) -> return ())---  >       l <- getLabel---  >       when (l == bottom) $ do stash <- readLIORef lRef---  >                             writeLIORef lRef $ stash ++ "no!"---  >   readLIORef lRef---  >     where evalDC' act = do (r,l) <- runDC 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 'bottom' (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 'catchLIO' 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'.----toLabeled :: Label l-          => l       -- ^ Label of result and upper bound on-                     --  inner-computations' observation-          -> LIO l a -- ^ Inner computation-          -> LIO l (Labeled l a)-toLabeled = toLabeledP NoPrivs-{-# WARNING 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.----toLabeledP :: Priv l p-           => p -> l -> LIO l a -> LIO l (Labeled l a)-toLabeledP p l act = do-  -- Check that the supplied upper bound is bounded-  guardAllocP p l-  -- Get current state:-  save_s <- getLIOStateTCB-  -- Execute action, catching any exceptions:-  res <- (liftM Right act) `catchTCB` (return . Left . lubErr l)-  -- Get the new state:-  s   <- getLIOStateTCB-  let lastL = lioLabel s-  -- Restore state-  putLIOStateTCB save_s-  return . labelTCB l $-    if canFlowToP p lastL l-           -- If the result was an exception, rethrow it when unlabel-           -- otherwise just return the result-      then either E.throw id res-           -- Violated the upper bound:-      else let l1  = lastL `upperBound` l-               -- Join of exception label (if any) and l1-               l2 = either (upperBound l1 . getErrLabel) (const l1) res-               -- Throw pure exception with label l1-           in E.throw $ LabeledExceptionTCB l2 $ E.toException $ -                  VMonitorFailure { monitorFailure = CanFlowToViolation-                                  , monitorMessage = errMsg }-    where lubErr lnew (LabeledExceptionTCB le e) =-                  LabeledExceptionTCB (le `lub` lnew) e-          ---          getErrLabel (LabeledExceptionTCB le _) = le-          ---          errMsg = "Computation read data more sensitive than bound."-{-# WARNING toLabeledP "toLabeledP is susceptible to termination attacks" #-}+-- | Similar to 'fmap', apply function to the 'Labeled' value. The+-- label of the returned value is the least upper bound of the current+-- label and label of the supplied labeled value.+lFmap :: Label l => Labeled l a -> (a -> b) -> LIO l (Labeled l b)+lFmap (LabeledTCB lold v) f = do+  l <- getLabel+  -- Result label is joined with current label+  let lnew = lold `lub` l+  -- `label` checks for clearance violation then labels+  label lnew $ f v  --- | 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--- instance, if @log_handle@ is an 'LHandle' with a high label, one--- can execute------ @---   discard top $ 'hputStrLn' log_handle \"Log message\"--- @------ to create a log message without affecting the current label.----discard :: Label l => l -> LIO l a -> LIO l ()-discard = discardP NoPrivs-{-# WARNING discard "discard is susceptible to termination attacks" #-}---- | Same as 'discard', but uses privileges when comparing initial and--- final label of the computation.-discardP :: Priv l p => p -> l -> LIO l a -> LIO l ()-discardP p l act = void $ toLabeledP p l act-{-# WARNING discardP "discardP is susceptible to termination attacks" #-}-#endif+-- | Similar to 'ap', apply function (wrapped by 'Labeled') to the+-- labeld value. The label of the returned value is the least upper+-- bound of the current label, label of the supplied labeled value,+-- and label of the supplied function.+lAp :: Label l => Labeled l (a -> b) -> Labeled l a -> LIO l (Labeled l b)+lAp (LabeledTCB lf f) (LabeledTCB la a) = do+  l <- getLabel+  let lnew = l `lub` lf `lub` la+  label lnew $ f a

@@ -1,52 +0,0 @@-{-# LANGUAGE Unsafe #-}-{-# LANGUAGE DeriveDataTypeable #-}--{- |--This is the TCB-restricted version of "LIO.Labeled", which documents-the implementation of 'Labeled' values and their use. It provides-functions for labeling ('labelTCB') and unlabeling ('unlabelTCB')-labeled values without imposing any information flow restrictions.---}--module LIO.Labeled.TCB (-    Labeled(..)-  , labelTCB-  ) where--import           Data.Typeable-import           LIO.Label-import           LIO.TCB---- | @Labeled l a@ is a value that associates a label of type @l@ with--- a value of type @a@. Labeled values allow users to label data with--- a label other than the current label. In an embedded setting this--- is akin to having first class labeled values. Note that 'Labeled'--- is an instance of 'LabelOf', which effectively means that the label--- of a 'Labeled' value is usually just protected by the current--- label. (Of course if you have a nested labeled value then the label--- on the inner labeled value's label is the outer label.)-data Labeled l t = LabeledTCB { labelOfLabeled :: !l-                              -- ^ Label of 'Labeled' valued-                              , unlabelTCB     :: !t -                              -- ^ Extracts the value from an-                              -- 'Labeled', discarding the label and any-                              -- protection.-                              } deriving Typeable---- | Trusted constructor that creates labeled values.-labelTCB :: Label l => l -> a -> Labeled l a-labelTCB = LabeledTCB---- | Trusted 'Show' instance.-instance (Label l, Show a) => ShowTCB (Labeled l a) where-    showTCB (LabeledTCB l t) = show t ++ " {" ++ show l ++ "}"---- | Trusted 'Read' instance.-instance (Label l, Read l, Read a) => ReadTCB (Labeled l a) where-  readsPrecTCB _ str = do (val, str1) <- reads str-                          ("{", str2) <- lex str1-                          (lab, str3) <- reads str2-                          ("}", rest) <- lex str3-                          return (labelTCB lab val, rest)

@@ -1,46 +1,65 @@ {-# LANGUAGE Trustworthy #-}-{-# LANGUAGE MultiParamTypeClasses,-             FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+ {- |  -Privileges are instances of the class called 'Priv'. They represent-the ability to bypass the protection of certain labels.  Specifically,-privilege allows you to behave as if @L_1 ``canFlowTo`` L_2@ even when-that is not the case.  The process of making data labeled @L_1@ affect-data labeled @L_2@ when @not (L_1 ``canFlowTo`` L_2)@ is called-/downgrading/.+Privileges are objects the possesion of which allows code to bypass+some label protections.  An in instance of class 'PrivDesc' describes+a pre-order among labels in which certain unequal labels become+equivalent.  When wrapped in a 'Priv' type (whose constructor is+private) a 'PrivDesc' allows code to treat those labels as equivalent. -The basic method of the 'Priv' class is 'canFlowToP', which performs a-more permissive can-flow-to check by exercising particular privileges-(in literature this relation is a pre-order, commonly written as-⊑ₚ).  Almost all 'LIO' operations have variants ending-@...P@ that take a privilege argument to act in a more permissive way. +Put another way, privileges represent the ability to bypass the+protection of certain labels.  Specifically, privilege allows you to+behave as if @L_1 ``canFlowTo`` L_2@ even when that is not the case.+The process of making data labeled @L_1@ affect data labeled @L_2@+when @not (L_1 ``canFlowTo`` L_2)@ is called /downgrading/. -All 'Priv' types are 'Monoid's, and so privileges can be combined with-'mappend'.  The creation of 'Priv' values is specific to the-particular label type in use;  the method used is 'mintTCB', but the-arguments depend on the particular label type. +The basic method of the 'PrivDesc' class is 'canFlowToP', which+performs a more permissive can-flow-to check by exercising particular+privileges (in literature this relation is a pre-order, commonly+written as ⊑ₚ).  Almost all 'LIO' operations have variants+ending @...P@ that take a privilege argument to act in a more+permissive way. +By convention, all 'PrivDesc' instances are also be instances of+'Monoid', allowing privileges to be combined with 'mappend'.  The+creation of 'PrivDesc' values is specific to the particular label type+in use; the method used is 'mintTCB', but the arguments depend on the+particular label type.+ -}  module LIO.Privs (   -- * Privilege descriptions-    PrivDesc(..)+    PrivDesc(..), canFlowToP, partDowngradeP   -- * Privileges-  , Priv(..)-  , NoPrivs(..)+  , Priv, privDesc+  , NoPrivs, noPrivs+  -- * Gates+  -- $gateIntro+  , Gate, gate, callGate+  -- ** Gate example+  -- $gateExample   ) where  import Data.Monoid- import LIO.Label-import LIO.Privs.TCB+import LIO.TCB +--+-- No privileges+--++privDesc :: Priv a -> a+privDesc (PrivTCB a) = a+ -- | This class defines privileges and the more-permissive relation -- ('canFlowToP') on labels using privileges. Additionally, it defines -- 'partDowngradeP' which is used to downgrage a label up to a limit, -- given a set of privilege.-class (Label l, PrivTCB p, Monoid p) => Priv l p where+class (Label l) => PrivDesc l p where     -- | The \"can-flow-to given privileges\" pre-order used to compare     -- two labels in the presence of privileges.  If @'canFlowToP' p L_1     -- L_2@ holds, then privileges @p@ are sufficient to downgrade data@@ -48,13 +67,13 @@     -- @'canFlowToP' p L_1 L_2@ for all @p@, but for some labels and     -- privileges, 'canFlowToP' will hold even where 'canFlowTo' does     -- not.-    canFlowToP :: p -> l -> l -> Bool-    canFlowToP p a b = partDowngradeP p a b `canFlowTo` b+    canFlowToPrivDesc :: p -> l -> l -> Bool+    canFlowToPrivDesc p a b = partDowngradePrivDesc p a b `canFlowTo` b      -- | Roughly speaking, @L_r = partDowngradeP p L L_g@ computes how-    -- close one can come to downgrading data labeled @L@ to the goal label-    -- @L_g@, given privileges @p@.  When @p == 'NoPrivs'@, the resulting-    -- label @L_r == L ``upperBound`` L_g@.  If @p@ contains /all/+    -- close one can come to downgrading data labeled @L@ to the goal+    -- label @L_g@, given privileges @p@.  When @p == 'NoPrivs'@, the+    -- resulting label @L_r == L ``lub`` L_g@.  If @p@ contains /all/     -- possible privileges, then @L_r == L_g@.     --     -- More specifically, @L_r@ is the greatest lower bound of the@@ -70,27 +89,125 @@     -- goal is to use privileges @p@ to avoid changing the label at all),     -- and then compute @L_r@ based on the label of data the code is     -- about to observe. -    partDowngradeP :: p  -- ^ Privileges+    partDowngradePrivDesc :: p  -- ^ Privileges                    -> l  -- ^ Label from which data must flow                    -> l  -- ^ Goal label                    -> l  -- ^ Result ------ No privileges---+-- | TODO(dm): document+canFlowToP :: PrivDesc l p => Priv p -> l -> l -> Bool+canFlowToP priv = canFlowToPrivDesc (privDesc priv) +-- | TODO(dm): document+partDowngradeP :: PrivDesc l p => Priv p -> l -> l -> l+partDowngradeP priv = partDowngradePrivDesc (privDesc priv)++ -- | Generic privilege type used to denote the lack of privileges. data NoPrivs = NoPrivs deriving (Show, Read) -instance PrivTCB NoPrivs-instance PrivDesc NoPrivs NoPrivs where privDesc = id-instance MintTCB  NoPrivs NoPrivs where mintTCB  = id+noPrivs :: Priv NoPrivs+noPrivs = PrivTCB NoPrivs+ instance Monoid NoPrivs where   mempty      = NoPrivs   mappend _ _ = NoPrivs  -- | With lack of privileges, 'canFlowToP' is simply 'canFlowTo', and -- 'partDowngradeP' is the least 'upperBound'.-instance Label l => Priv l NoPrivs where-  canFlowToP _ l1 l2    = l1 `canFlowTo` l2-  partDowngradeP _ l lg = l `upperBound` lg+instance Label l => PrivDesc l NoPrivs where+  canFlowToPrivDesc _ l1 l2    = l1 `canFlowTo` l2+  partDowngradePrivDesc _ l lg = l `lub` lg+++{- $gateIntro++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 'gate' to create a gate data type @'Gate' d a@+given a computation of type @d -> a@. Here, @d@ is a privilege+description (type variable for an instance of 'PrivDesc').  Gates are+invoked with 'callGate', and as such the service provider has the+guarantee that the client (the caller) 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 before+performing the \"actual\" computation.  The client and server solely+need to trust the implementation of 'callGate'.++-}+++-- | A Gate is a lambda abstraction from a privilege description to an+-- arbitrary type @a@. Applying the gate is accomplished with 'callGate'+-- which takes a privilege argument that is converted to a description+-- before invoking the gate computation.+newtype Gate d a = GateTCB (d -> a)+-- Note GateTCB is trusted by convention.  Anyone with access to the+-- symbol can call any gate while claiming arbitrary privileges.  In+-- the absence of gates, however, GateTCB doesn't provide any+-- particular privileges.++-- | Create a gate given a computation from a privilege description.+-- Note that because of currying type 'a' may itself be a function+-- type and thus gates can take arguments in addition to the privilege+-- descriptoin.+gate :: (d -> a)  -- ^ Gate computation+     -> Gate d a+{-# INLINE gate #-}+gate = GateTCB++-- | Given a gate and privilege, execute the gate computation.  It is+-- important to note that @callGate@ invokes the gate computation with+-- the privilege description and /NOT/ the privilege itself.+--+-- Note that, in general, code should /not/ provide privileges to+-- functions other than @callGate@ when wishing to call a gate. This+-- function is provided by LIO since it can be easily inspected by+-- both the gate creator and caller to be doing the \"right\" thing:+-- provide the privilege description corresponding to the supplied+-- privilege as \"proof\" without explicitly passing in the privilege.+-- +callGate :: Gate p a -- ^ Gate+         -> Priv p   -- ^ Privilege used as proof-of-ownership+         -> a+{-# INLINE callGate #-}+callGate (GateTCB g) = g . privDesc++{- $gateExample++This example uses "LIO.DCLabel" to demonstrate the use of gates.  The+service provider provides @addGate@ which adds two integers if the+gate is called by a piece of code that owns the \"Alice\" or \"Bob\"+principals. Otherwise, it simply returns @Nothing@.++> import LIO+> import LIO.DCLabel+> +> import LIO.Privs.TCB (mintTCB)+> +> +> -- | Add two numbers if the computation is invoked by Alice or Bob.+> addGate :: DCGate (Int -> Int -> Maybe Int)+> addGate = gate $ \pd a b ->+>   if pd `elem` (dcPrivDesc `map` ["Alice", "Bob"])+>     then Just $ a + b+>     else Nothing+> +> +> alice, bob, clark :: DCPriv+> alice = PrivTCB . dcPrivDesc $ "Alice"+> bob   = PrivTCB . dcPrivDesc $ "Bob"+> clark = PrivTCB . dcPrivDesc $ "Clark"+> +> main = putStrLn . show $ +>   [ callGate addGate alice 1 2 -- Just 3+>   , callGate addGate bob   3 4 -- Just 7+>   , callGate addGate clark 5 6 -- Nothing+>   ]+++-}

@@ -1,57 +0,0 @@-{-# LANGUAGE Unsafe #-}-{-# LANGUAGE MultiParamTypeClasses,-             FunctionalDependencies #-}--{- | --This module exports the class 'PrivTCB' which all privilege types must-be an instance of. This class is in the TCB since privileges can be-used to bypass label restrictions and untrusted code should not be-allowed to do do arbitrarily. See "LIO.Privs" for an additional-description of privileges and their role within "LIO".--In addition to 'PrivTCB' this module exports the class 'PrivDesc'-which provides a function from privileges to /privilege descriptions/.-A privilege description is a meaningful and safe interpretation of a-coresponding privilege (note that the function must be one-to-on).-Privilege descriptions are used in "LIO.Gate" as \"proof\" of-privilege ownership.  Additionally, privilege descriptions can be used-by TCB code to mint new privileges using the 'MintTCB' class.---}--module LIO.Privs.TCB ( -    PrivTCB-  , PrivDesc(..)-  , MintTCB(..)-  ) where---- | Zero-method class that imposes a restriction on what code--- (namely trusted) can make a \"privilege type\".-class PrivTCB p---- | Class used to convert a privilege to a privilege description.  This--- is particularly useful when one piece of code wishes to prove--- ownership of certain privileges without granting the privilege.--- NOTE: it (almost) always a security violation if the privilege is--- also the privilege description.------ Although this class is not part of the TCB there are some security--- implications that should be considered when making a type an--- instance of this class. Specifically, if the value constructor for--- the privilege description type @d@ is exported then some--- trusted code must be used when \"proving\" ownership of a certain--- privilege. This is generally a good idea even if the constructor is--- not made available, since code can (usually) cache such privilege --- descriptions. An alternative is to use phantom types to enforce a--- linear-type-like behavior.-class (PrivTCB p, Show d) => PrivDesc p d | p -> d, d -> p where-  -- | Retrive privilege description from a privilege.-  privDesc :: p -> d---- | The dual of 'PrivDesc'. This class provides @mintTCB@ which may--- be used to convert, or /mint/, a privilege descriptions into a--- privilege.  Of course, @mintTCB@ must be restricted to the TCB.-class (PrivDesc p d) => MintTCB p d where-  -- | Mint a new privilege values given a privilege description.-  mintTCB :: d -> p

@@ -0,0 +1,47 @@+{-# LANGUAGE Trustworthy #-}++-- | This module contains functions to launch 'LIO' computations from+-- within the 'IO' monad.  These functions are not useful from within+-- 'LIO' code (but not harmful either, since their types are in the+-- 'IO' monad).+--+-- This module is intended to be imported into your Main module, for+-- use in invoking 'LIO' code.  The functions are also available via+-- "LIO" and "LIO.Core", but those modules will clutter your namespace+-- with symbols you don't need in the 'IO' monad.+module LIO.Run (LIOState(..), runLIO, evalLIO) where++import Control.Exception+import Data.IORef+import LIO.TCB++-- | Execute an 'LIO' action, returning its result and the final label+-- state as a pair.  Note that it returns a pair whether or not the+-- 'LIO' action throws an exception.  Forcing the result value will+-- re-throw the exception, but the label state will always be valid.+--+-- See also 'evalLIO'.+runLIO :: LIO l a -> LIOState l -> IO (a, LIOState l)+runLIO (LIOTCB m) s0 = do+  sp <- newIORef s0+  a <- m sp `catch` \e -> return $ throw $ makeCatchable e+  s1 <- readIORef sp+  return (a, s1)++-- | Given an 'LIO' computation and some initial state, return an IO+-- action which when executed will perform the IFC-safe LIO+-- computation.+--+-- Because untrusted code cannot execute 'IO' computations, this function+-- should only be useful within trusted code.  No harm is done from+-- exposing the @evalLIO@ symbol to untrusted code.  (In general,+-- untrusted code is free to produce 'IO' computations, but it cannot+-- execute them.)+--+-- Unlike 'runLIO', this function throws an exception if the+-- underlying 'LIO' action terminates with an exception.+evalLIO :: LIO l a -> LIOState l -> IO a+evalLIO lio s = do+  (a, _) <- runLIO lio s+  return $! a+

@@ -1,9 +1,6 @@ {-# LANGUAGE Unsafe #-}-{-# LANGUAGE GeneralizedNewtypeDeriving,-             MultiParamTypeClasses,-             FunctionalDependencies,-             FlexibleInstances,-             DeriveDataTypeable #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ExistentialQuantification #-}  {- |  @@ -12,11 +9,14 @@ * The definition of the 'LIO' monad and relevant trusted state   access/modifying functions. -* Labeled exceptions that are use throughout 'LIO' and low-level,-  /unsafe/, throw and catch primitives.+* Various other types whose constructors are privileged and must be+  hidden from untrusted code. -* Combinators for executing 'IO' actions.+* Uncatchable exceptions used to pop threads out of the 'LIO' monad+  unconditionally. +* Combinators for executing 'IO' actions within the 'LIO' monad.+ The documentation and external, safe 'LIO' interface is provided in "LIO.Core". @@ -24,33 +24,28 @@  module LIO.TCB (   -- * LIO monad-    LIO(..), MonadLIO(..)-  -- ** Internal state-  , LIOState(..)-  , getLIOStateTCB, putLIOStateTCB, updateLIOStateTCB -  -- * Exceptions-  , LabeledException(..)-  -- ** Throw and catch-  , unlabeledThrowTCB, catchTCB+    LIOState(..), LIO(..)+  -- ** Accessing internal state+  , getLIOStateTCB, putLIOStateTCB, modifyLIOStateTCB, updateLIOStateTCB    -- * Executing IO actions-  , ioTCB, rethrowIoTCB+  , ioTCB+  -- * Privileged constructors+  , Priv(..), Labeled(..)+  -- * Uncatchable exception type+  , UncatchableTCB(..), makeCatchable   -- * Trusted 'Show' and 'Read'   , ShowTCB(..), ReadTCB(..)   ) where -import           Data.Typeable--import           Control.Applicative-import           Control.Monad-import           Control.Monad.Trans.State.Strict-import           Control.Monad.Trans.Class (lift)-import           Control.Monad.IO.Class (liftIO)-import           Control.Exception (Exception, SomeException)-import qualified Control.Exception as E--import           Text.Read (minPrec)+import Control.Applicative+import Control.Exception (Exception(..), SomeException(..))+import Control.Monad+import Data.Monoid+import Data.IORef+import Data.Typeable+import Text.Read (minPrec) -import           LIO.Label+import LIO.Label  -- -- LIO Monad@@ -70,20 +65,28 @@ -- we need a way to prevent certain computations from reading overly -- sensitive data. This is the role of the current clearance: it imposes -- an upper bound on the current label.-newtype LIO l a = LIOTCB { unLIOTCB :: StateT (LIOState l) IO a }-  deriving (Functor, Applicative, Monad)+newtype LIO l a = LIOTCB {+    unLIOTCB :: IORef (LIOState l) -> IO a+  } deriving (Typeable) ------ Monad base---+instance Monad (LIO l) where+  {-# INLINE return #-}+  return = LIOTCB . const . return+  {-# INLINE (>>=) #-}+  m >>= k = LIOTCB $ \s -> do+    a <- unLIOTCB m s+    unLIOTCB (k a) s+  fail = LIOTCB . const . fail --- | Synonym for monad in which 'LIO' is the base monad.-class (Monad m, Label l) => MonadLIO l m | m -> l where-  -- | Lift an 'LIO' computation.-  liftLIO :: LIO l a -> m a+instance Functor (LIO l) where+  {-# INLINE fmap #-}+  fmap f ma = LIOTCB $ \s -> unLIOTCB ma s >>= return . f -instance Label l => MonadLIO l (LIO l) where-  liftLIO = id+instance Applicative (LIO l) where+  {-# INLINE pure #-}+  pure = return+  {-# INLINE (<*>) #-}+  (<*>) = ap  -- -- Internal state@@ -92,71 +95,112 @@ -- | Get internal state. This function is not actually unsafe, but -- to avoid future security bugs we leave all direct access to the -- internal state to trusted code.-getLIOStateTCB :: Label l => LIO l (LIOState l)-getLIOStateTCB = LIOTCB . StateT $! \s -> return (s, s)+getLIOStateTCB :: LIO l (LIOState l)+{-# INLINE getLIOStateTCB #-}+getLIOStateTCB = LIOTCB readIORef  -- | Set internal state.-putLIOStateTCB :: Label l => LIOState l -> LIO l ()-putLIOStateTCB s = LIOTCB . StateT $! \_ -> return ((), s)+putLIOStateTCB :: LIOState l -> LIO l ()+{-# INLINE putLIOStateTCB #-}+putLIOStateTCB s = LIOTCB $ \sp -> writeIORef sp $! s  -- | Update the internal state given some function.-updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()-updateLIOStateTCB f = do+modifyLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()+{-# INLINE modifyLIOStateTCB #-}+modifyLIOStateTCB f = do   s <- getLIOStateTCB-  putLIOStateTCB $! f s+  putLIOStateTCB (f s) +{-# DEPRECATED updateLIOStateTCB "Use modifyLIOStateTCB instead" #-}+updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()+updateLIOStateTCB = modifyLIOStateTCB  ----- Exceptions+-- Executing IO actions -- --- | A labeled exception is simply an exception associated with a label.-data LabeledException l = LabeledExceptionTCB !l SomeException-  deriving (Show, Typeable)+-- | Lifts an 'IO' computation into the 'LIO' monad.  Note that+-- exceptions thrown within the 'IO' computation cannot directly be+-- caught within the 'LIO' computation.  Thus, you will generally want to+-- use 'rethrowIoTCB'.+ioTCB :: IO a -> LIO l a+{-# INLINE ioTCB #-}+ioTCB = LIOTCB . const -instance Label l => Exception (LabeledException l)+--+-- Exception handling+-- --- | Throw an arbitrary exception. Note that the exception being--- thrown is not labeled.-unlabeledThrowTCB :: (Exception e, Label l) => e -> LIO l a-unlabeledThrowTCB = LIOTCB . liftIO . E.throwIO+-- | An uncatchable exception hierarchy use to terminate an untrusted+-- thread.  Wrap the uncatchable exception in 'UncatchableTCB' before+-- throwing it to the thread.  'runLIO' will subsequently unwrap the+-- 'UncatchableTCB' constructor.+--+-- Note this can be circumvented by 'IO.mapException', which should be+-- made unsafe.+data UncatchableTCB = forall e. (Exception e) =>+                      UncatchableTCB e deriving (Typeable) --- | Catch an exception. Note that all exceptions thrown by LIO are--- labeled and thus this trusted function can be used to handle any--- exception. Note that the label of the exception must be considered--- in the handler (i.e., handler must raise the current label) to--- preserve security.-catchTCB :: Label l-         => LIO l a-         -> (LabeledException l -> LIO l a)-         -> LIO l a-catchTCB act handler = do-  s0 <- getLIOStateTCB-  (res, s1) <- ioTCB $! toIO act s0 `E.catch` ioHandler s0-  putLIOStateTCB s1-  return res-    where toIO io = runStateT (unLIOTCB io)-          ioHandler s e = toIO (handler e) s+instance Show UncatchableTCB where+  showsPrec p (UncatchableTCB e) = showsPrec p e +instance Exception UncatchableTCB where+  toException = SomeException+  fromException (SomeException e) = cast e++-- | Simple utility function that strips 'UncatchableTCB' from around an+-- exception.+makeCatchable :: SomeException -> SomeException+makeCatchable e@(SomeException einner) =+  case cast einner of Just (UncatchableTCB enew) -> SomeException enew+                      Nothing                    -> e+ ----- Executing IO actions+-- Privileges -- --- | Lifts an 'IO' computation into the 'LIO' monad.  Note that--- exceptions thrown within the 'IO' computation cannot directly be--- caught within the 'LIO' computation.  Thus, you will generally want to--- use 'rtioTCB' exported by "LIO.Exception.TCB" instead of 'ioTCB'.-ioTCB :: Label l => IO a -> LIO l a-ioTCB = LIOTCB . lift+-- | A newtype wrapper that can be used by trusted code to bless+-- privileges.  Privilege-related functions are defined in+-- "LIO.Privs", but the constructor, 'PrivTCB', allows one to mint+-- arbitrary privileges and hence must be located in this file.+newtype Priv a = PrivTCB a deriving (Show, Eq, Typeable) --- | Lifts an 'IO' computation into the 'LIO' monad.  If the 'IO'--- computation throws an exception, it labels the exception with the--- current label so that the exception can be caught with 'catchLIO'.-rethrowIoTCB :: Label l => IO a -> LIO l a-rethrowIoTCB io = do-  l <- lioLabel `liftM` getLIOStateTCB-  ioTCB $ io `E.catch` (E.throwIO . LabeledExceptionTCB l)+instance Monoid p => Monoid (Priv p) where+  mempty = PrivTCB mempty+  {-# INLINE mappend #-}+  mappend (PrivTCB m1) (PrivTCB m2) = PrivTCB $ m1 `mappend` m2+  {-# INLINE mconcat #-}+  mconcat ps = PrivTCB $ mconcat $ map (\(PrivTCB p) -> p) ps +--+-- Pure labeled values+--++-- | @Labeled l a@ is a value that associates a label of type @l@ with+-- a value of type @a@. Labeled values allow users to label data with+-- a label other than the current label. In an embedded setting this+-- is akin to having first class labeled values. Note that 'Labeled'+-- is an instance of 'LabelOf', which effectively means that the label+-- of a 'Labeled' value is usually just protected by the current+-- label. (Of course if you have a nested labeled value then the label+-- on the inner labeled value's label is the outer label.)+data Labeled l t = LabeledTCB !l t deriving Typeable+-- Note: t cannot be strict if we want things like lFmap.++instance LabelOf Labeled where+  labelOf (LabeledTCB l _) = l++-- | Trusted 'Show' instance.+instance (Label l, Show a) => ShowTCB (Labeled l a) where+    showTCB (LabeledTCB l t) = show t ++ " {" ++ show l ++ "}"++-- | Trusted 'Read' instance.+instance (Label l, Read l, Read a) => ReadTCB (Labeled l a) where+  readsPrecTCB _ str = do (val, str1) <- reads str+                          ("{", str2) <- lex str1+                          (lab, str3) <- reads str2+                          ("}", rest) <- lex str3+                          return (LabeledTCB lab val, rest)  -- -- Trusted 'Show' and 'Read'

@@ -0,0 +1,44 @@+{-# LANGUAGE Unsafe #-}++{- |++This module exports 'LabeledResult's which are effectively thread exit+results protected by a label. See "LIO.Concurrent" for a description+of the concurrency abstractions of LIO.++-}++module LIO.TCB.Concurrent (+    LabeledResult(..), LResStatus(..)+  ) where++import qualified Control.Concurrent as IO+import Data.IORef++import LIO.Label++data LResStatus l a = LResEmpty+                    | LResLabelTooHigh !l+                    | LResResult a+                      deriving (Show)++-- | A LabeledResult encapsulates a future result from a computation running+-- in a thread. It holds the 'ThreadId' and an 'LMVar' where the result is+-- stored. The thread referenced in 'lresThreadIdTCB' should fill in+-- 'lresResultTCB' (either with a value or exception), so waiting on the thread+-- should ensure that a result is ready.+data LabeledResult l a = LabeledResultTCB {+    lresThreadIdTCB :: !IO.ThreadId+    -- ^ Thread executing the computation+  , lresLabelTCB :: !l+    -- ^ Label of the tresult+  , lresBlockTCB :: !(IO.MVar ())+  , lresStatusTCB :: !(IORef (LResStatus l a))+    -- ^ Result (when it is ready), or the label at which the thread+    -- terminated, if that label could not flow to 'lresLabelTCB'.+  }++instance LabelOf LabeledResult where+  labelOf = lresLabelTCB++

@@ -0,0 +1,22 @@+{-# LANGUAGE Unsafe #-}++{-|++This module implements the trusted compoenet of DCLabel privileges,+documented in "LIO.DCLabel.Privs".+Since privilege objects may be used unsafely, this module is marked+@-XUnsafe@. Untrusted code may access privileges using the interface+provided by "LIO.DCLabel.Privs".++-}++module LIO.TCB.DCLabel (allPrivTCB) where++import LIO.DCLabel.Core+import LIO.DCLabel.Privs+import LIO.TCB++-- | The all privilege corresponds to logical @False@+allPrivTCB :: DCPriv+allPrivTCB = PrivTCB dcFalse+

@@ -0,0 +1,117 @@+{-# LANGUAGE Unsafe #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE CPP #-}++-- | This module provides routines for safely exposing IO functions in+-- the 'LIO' monad.  At a high level, certain IO objects such as+-- handles can be associated with a label via 'LObj', while certain+-- operations can then be blessed (via 'blessTCB') to operate on such+-- 'LObj' objects.+--+-- For example, trusted code might define the following:+--+-- > import qualified System.IO as IO+-- > +-- > type Handle = LObj DCLabel IO.Handle+-- > +-- > hPutStrLn :: LObj DCLabel IO.Handle -> String -> LIO DCLabel ()+-- > hPutStrLn h = blessTCB IO.hPutStrLn noPrivs h+-- > +-- > hGetLine :: LObj DCLabel IO.Handle -> LIO DCLabel String+-- > hGetLine h = blessTCB IO.hGetLine noPrivs h+--+-- Then application-specific trusted code can wrap a specific label+-- around each 'Handle' using the 'LObjTCB' constructor.+module LIO.TCB.LObj (LObj(..), blessTCB, blessPTCB, GuardIO(..)) where++import Data.Typeable++import safe LIO.Core+import safe LIO.Label+import safe LIO.Privs+import LIO.TCB++-- | A "@LObj label object@" is a wrapper around an IO abstraction of+-- type @object@ (such as a file handle or socket) on which it is safe+-- to do @IO@ operations in the 'LIO' monad when the caller can read+-- and write a particular label.  It is the job of the trusted code+-- constructing such a @LObj@ object to ensure both that the same IO+-- object is only ever blessed with one label, and that the+-- abstraction combined with its blessed IO operations (see+-- 'blessTCB') cannot be used to communicate with code running at+-- different labels.+data LObj label object = LObjTCB !label !object deriving (Typeable)++instance LabelOf LObj where+  labelOf (LObjTCB l _) = l++instance (Label l, Show t) => ShowTCB (LObj l t) where+  showTCB (LObjTCB l t) = show t ++ " {" ++ show l ++ "}"++#if 0+genTypesVals :: Int -> IO ()+genTypesVals n0 =+  putStrLn $ "#define TypesVals(macro) \\\n" ++ concatMap doit [1..n0]+  where doit n = "  macro(" ++ intercalate " -> " (as n) ++ ", \\\n" +++                 "        " ++ intercalate " " (as n) ++ ")" +++                 (if n < n0 then "; \\\n" else "\n")+        as n = map (\i -> "a" ++ show i) [1..n]+#endif++#define TypesVals(macro) \+  macro(a1, \+        a1); \+  macro(a1 -> a2, \+        a1 a2); \+  macro(a1 -> a2 -> a3, \+        a1 a2 a3); \+  macro(a1 -> a2 -> a3 -> a4, \+        a1 a2 a3 a4); \+  macro(a1 -> a2 -> a3 -> a4 -> a5, \+        a1 a2 a3 a4 a5); \+  macro(a1 -> a2 -> a3 -> a4 -> a5 -> a6, \+        a1 a2 a3 a4 a5 a6); \+  macro(a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7, \+        a1 a2 a3 a4 a5 a6 a7); \+  macro(a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8, \+        a1 a2 a3 a4 a5 a6 a7 a8); \+  macro(a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9, \+        a1 a2 a3 a4 a5 a6 a7 a8 a9); \+  macro(a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10, \+        a1 a2 a3 a4 a5 a6 a7 a8 a9 a10)++class GuardIO l io lio | l io -> lio where+  -- | Lifts an 'IO' action in the 'LIO' monad, executing a guard+  -- before calling the function.+  guardIOTCB :: (LIO l ()) -> io -> lio+instance GuardIO l (IO r) (LIO l r) where+  {-# INLINE guardIOTCB #-}+  guardIOTCB guard io = guard >> ioTCB io+#define GUARDIO(types, vals) \+instance GuardIO l (types -> IO r) (types -> LIO l r) where { \+  {-# INLINE guardIOTCB #-}; \+  guardIOTCB guard io vals = guard >> ioTCB (io vals); \+}+TypesVals (GUARDIO)++-- | This function can be used to turn an 'IO' function into an 'LIO'+-- one.  The 'LIO' version expects a 'LObj' argument, and before+-- performing any IO uses 'guardWrite' to check that the current label+-- can write the label in the 'LObj' object.+--+-- Note that @io@ and @lio@ are function types (of up to nine+-- arguments), which must be the same in all types except the monad.+-- For example, if @io@ is @Int -> String -> IO ()@, then @lio@ must+-- be @Int -> String -> LIO l ()@.+blessTCB :: (GuardIO l io lio, Label l) => (a -> io) -> (LObj l a) -> lio+{-# INLINE blessTCB #-}+blessTCB io (LObjTCB l a) = guardIOTCB (guardWrite l) (io a)++-- | A variant of 'blessTCB' that takes a privilege argument.+blessPTCB :: (GuardIO l io lio, PrivDesc l p) =>+             (a -> io) -> Priv p -> (LObj l a) -> lio+{-# INLINE blessPTCB #-}+blessPTCB io p (LObjTCB l a) = guardIOTCB (guardWriteP p l) (io a)

@@ -1,22 +0,0 @@-{-# LANGUAGE Safe #-}-module AliceCode ( mainReview ) where--import LambdaChair--findPaper' s = do-  ep <- findPaper s-  case ep of-    Left e -> error $ "Failed with" ++ e-    Right p -> return p--mainReview = do-  p1 <- findPaper' "Flexible Dynamic"-  p2 <- findPaper' "A Static"--  readPaper p1--  appendToReview p1 "Interesting work!"--  readPaper p2-  readReview p2-  appendToReview p2 "What about adding new users?"

@@ -1,17 +0,0 @@-{-# LANGUAGE Safe #-}-module BobCode ( mainReview ) where--import LambdaChair--findPaper' s = do-  ep <- findPaper s-  case ep of-    Left e -> error $ "Failed with" ++ e-    Right p -> return p--mainReview = do-  p1 <- findPaper' "Flexible Dynamic..."-  p2 <- findPaper' "A Static..."-  appendToReview p2 "Hmm, IFC.."-  readReview p2-  readReview p1

@@ -1,15 +0,0 @@-{-# LANGUAGE Trustworthy #-}-{- | --Safe version of "LambdaChair.TCB".---}--module LambdaChair ( -    findPaper-  , retrievePaper, readPaper-  , retrieveReview, readReview-  , appendToReview-  , reviewDCPutStrLn-  ) where-import LambdaChair.TCB

@@ -1,445 +0,0 @@-{-# LANGUAGE Unsafe #-}-{-# LANGUAGE OverloadedStrings,-             MultiParamTypeClasses,-             GeneralizedNewtypeDeriving,-             ScopedTypeVariables #-}--{- | --Basic review system API.--Must compile LIO with @--flags="toLabeled"@.--This is a prototype/toy implementation.  A more serious implementation-will be implemented using the Hails framework.---}--module LambdaChair.TCB (-  --- * Admin actions-    runReviewDC-  , emptyReviewState-  , addUser-  , addPaper-  , addConflict-  , addAssignment-  , asUser-  --- * User actions-  , findPaper-  , retrievePaper, readPaper-  , retrieveReview, readReview-  , appendToReview-  , reviewDCPutStrLn -  -- TCB-  , printUsersTCB-  , printReviewsTCB-  , reviewDCPutStrLnTCB -  , dcPutStrLnTCB -  ) where--import Prelude hiding (catch)-import Control.Monad-import Control.Exception (SomeException, ErrorCall(..))-import Control.Monad.Trans.Class-import Control.Monad.Trans.State-import Data.Maybe-import Data.List--import LIO-import LIO.TCB-import LIO.Privs.TCB-import LIO.LIORef-import LIO.LIORef.TCB (readLIORefTCB)-import LIO.DCLabel-import LIO.DCLabel.Privs.TCB--import qualified Data.ByteString.Char8 as C---type ErrorStr  = String---- | Class with sideffectful show-class DCShowTCB s where-  dcShowTCB :: s -> DC String---- | Print to standard output-dcPutStrLnTCB :: String -> DC ()-dcPutStrLnTCB = ioTCB . putStrLn---- | Read from standard input-dcGetLineTCB :: DC String-dcGetLineTCB = ioTCB getLine---- | A name-type Name      = String--- | A password-type Password  = String--- | Paper/Rewview content-type Content   = String--- | A review log-type ReviewLog = String---- | Paper id-type Id     = Int--- | A paper is just a wrapper for its contents-data Paper  = Paper  Content--- | A review is just a wrapper for its contents-data Review = Review ReviewLog---- | A user contains a name, password a list of conflicting papers and--- list of papers to review (i.e., assignments).-data User = User { name :: Name-                 , password :: Password-                 , conflicts :: [Id]-                 , assignments :: [Id] }--instance Eq User where-  u1 == u2 = name u1 == name u2--instance DCShowTCB User where-  dcShowTCB u = do-    return $  "Name: " ++ (name u) ++ "\n"-           ++ "Password: " ++ (password u) ++ "\n"-           ++ "Conflicts: " ++ (show . conflicts $ u) ++ "\n"-           ++ "Assignments: " ++ (show . assignments $ u)---- | Areview entry contains the paper id, paper contents and review--- log.-data ReviewEnt =  ReviewEnt { paperId :: Id-                            , paper   :: DCRef Paper-                            , review  :: DCRef Review }--instance Eq ReviewEnt where-  r1 == r2 = paperId r1 == paperId r2--instance DCShowTCB ReviewEnt where-  dcShowTCB r = do-    (Paper pap)  <- readLIORefTCB (paper r)-    (Review rev) <- readLIORefTCB (review r)-    return $  "ID:" ++ (show . paperId $ r)-           ++ "\nPaper:" ++ pap-           ++ "\nReviews:" ++ rev----- Internal state of the 'ReviewDC' monad.-data ReviewState = ReviewState { users :: [User]-                               , reviewEntries :: [ReviewEnt]-                               , curUser :: Maybe Name }---- | Emtpy state.-emptyReviewState :: ReviewState-emptyReviewState = ReviewState [] [] Nothing---- | Monad in which all review actions are executed.-newtype ReviewDC a = ReviewDC (StateT ReviewState DC a)-  deriving (Monad)---- | Lift a 'DC' into thew 'ReviewDC' monad.-instance MonadLIO DCLabel ReviewDC where-  liftLIO = ReviewDC . lift---- | Get internal state-get' :: ReviewDC ReviewState-get' = ReviewDC . StateT $ \s -> return (s,s)---- | Update internal state-put' :: ReviewState -> ReviewDC ()-put' s = ReviewDC . StateT $ \_ -> return ((),s)---- | Execute a review action-runReviewDC :: ReviewDC a -> ReviewState -> DC (a, ReviewState)-runReviewDC (ReviewDC m) s = runStateT m s-------- | Get all users-getUsers :: ReviewDC [User]-getUsers = users `liftM` get'---- | Get all review entries-getReviews :: ReviewDC [ReviewEnt]-getReviews = reviewEntries `liftM` get'---- | Get priviliges-getCurUserName :: ReviewDC (Maybe Name)-getCurUserName = curUser `liftM` get'---- | Get current user name-getCurUser :: ReviewDC (Maybe User)-getCurUser = do-  n <- getCurUserName-  maybe (return Nothing) findUser n---- | Get priviliges of the user executing the action-getPrivs :: ReviewDC DCPriv-getPrivs = do -  u <- getCurUser-  return $ maybe noPriv (mintTCB . dcPrivDesc . name) u---- | Updat users-putUsers :: [User] -> ReviewDC ()-putUsers us = do-  rs <- getReviews-  u <- getCurUserName-  put' $ ReviewState us rs u---- | Update reviews-putReviews :: [ReviewEnt] -> ReviewDC ()-putReviews rs = do-  us <- getUsers-  u <- getCurUserName-  put' $ ReviewState us rs u---- | Set current user-putCurUserName :: Name -> ReviewDC ()-putCurUserName u = do-  us <- getUsers-  rs <- getReviews-  put' $ ReviewState us rs (Just u)---- | Remove current user-clearCurUserName :: ReviewDC ()-clearCurUserName = do-  us <- getUsers-  rs <- getReviews-  put' $ ReviewState us rs Nothing---- | Find review entry by id-findReview :: Id -> ReviewDC (Maybe ReviewEnt)-findReview pId = do-  reviews <- getReviews-  return $ find (\e -> paperId e == pId) reviews---- | Find user by name-findUser :: Name -> ReviewDC (Maybe User)-findUser n = do-  us <- getUsers-  return $ find (\u -> name u == n) us---- | Add new (fresh) user-addUser :: Name -> Password -> ReviewDC ()-addUser n p = do-  u <- findUser n-  unless (isJust u) $ do-    let newUser = User { name = n-                       , password = p-                       , conflicts = []-                       , assignments = [] }-    us <- getUsers-    putUsers (newUser:us)---- | Add conflicting paper to user-addConflict :: Name -> Id -> ReviewDC ()-addConflict n i = do-  usr <- findUser n-  pap <- findReview i-  case (usr, pap) of-    (Just u, Just _) -> -      if i `elem` (assignments u)-        then return ()-        else do let u' = u { conflicts = i : (conflicts u)}-                usrs <- getUsers-                putUsers $ u' : (filter (/= u) usrs)-    _ -> return ()---- | Assign a paper for the user to review-addAssignment :: Name -> Id -> ReviewDC ()-addAssignment n i = do-  usr <- findUser n-  pap <- findReview i-  case (usr, pap) of-    (Just u, Just _) -> -      if i `elem` (conflicts u)-        then return ()-        else do let u' = u { assignments = i : (assignments u)}-                usrs <- getUsers-                putUsers $ u' : (filter (/= u) usrs)-    _ -> return ()---- | Print users-printUsersTCB :: ReviewDC ()-printUsersTCB = do- us <- getUsers- mapM (liftLIO . dcShowTCB) us >>=-   reviewDCPutStrLnTCB . (intercalate "\n--\n")---- ^ Print papers and reviews-printReviewsTCB :: ReviewDC ()-printReviewsTCB = do- reviews <- getReviews- mapM (liftLIO . dcShowTCB) reviews >>=-   reviewDCPutStrLnTCB . (intercalate "\n--\n")---- ^ Create new paper given id and content-newReviewEnt :: Id -> Content -> ReviewDC ReviewEnt-newReviewEnt pId content = do-  let p1 = toComponent $ "Paper" ++ (show pId)-      r1 = toComponent $ "Review" ++ (show pId)-      pLabel = dcLabel dcTrue p1 -      rLabel = dcLabel r1 r1 -      privs = mintTCB $ dcPrivDesc (p1 /\ r1)-  liftLIO $ do-    rPaper  <- newLIORefP privs pLabel (Paper content)-    rReview <- newLIORefP privs rLabel (Review "")-    return $ ReviewEnt pId rPaper rReview---- ^ Adda new paper to be reviewed-addPaper :: Content -> ReviewDC Id-addPaper content = do-  reviews <- getReviews-  let pId = 1 + (length reviews)-  ent <- newReviewEnt pId content-  putReviews (ent:reviews)-  return pId----- ^ Given a paper number return the paper-retrievePaper :: Id -> ReviewDC (Either ErrorStr Content)-retrievePaper pId = do-  mu <- getCurUser-  case mu of-    Nothing -> return $ Left "Need to be logged in"-    Just u -> do-      mRev <- findReview pId -      case mRev of -        Nothing -> return $ Left "Invalid Id"-        Just rev -> let as = assignments u-                        priv = mintTCB . fromList $ map id2cat as-                    in  doReadPaper priv rev-       where doReadPaper priv rev = liftLIO $ do-                 (Paper lPaper) <- readLIORefP priv (paper rev)-                 return (Right lPaper)-             id2cat i = [principal . C.pack $ "Review"++(show i)]---- ^ Given a paper number print the paper--- NOTE: in the paper, the functionality of @readPaper@ corresponds to--- that of @retrievePaper@; here, we print out the content.-readPaper :: Id -> ReviewDC ()-readPaper i = retrievePaper i >>= \r -> reviewDCPutStrLn $ show r----- ^ Given a paper/review number return the review, if the entry exists-retrieveReview :: Id -> ReviewDC (Either ErrorStr Content)-retrieveReview pId = do-  mRev <- findReview pId -  case mRev of -    Nothing -> return $ Left "Invalid Id"-    Just rev -> do mu <- getCurUser-                   case mu of-                    Nothing -> return $ Left "Must login first"-                    Just _ -> doReadReview rev-   where doReadReview rev = liftLIO $ do-             (Review r) <- readLIORef (review rev)-             return (Right r)---- ^ Given a paper/review number print the review, if the entry exists-readReview :: Id -> ReviewDC ()-readReview i = retrieveReview i >>= \r -> reviewDCPutStrLn $ show r---- ^ Computer the label of the output' channel-getOutputChLbl :: ReviewDC (DCLabel) -getOutputChLbl = do-  mu <- getCurUser-  case mu of-    Nothing -> liftLIO $ throwLIO (ErrorCall "No user is logged in.")-    Just u -> do-      as <- getReviews >>= return . map paperId -- all reviews-      let cs = conflicts u -- conflicting reviews-          c_cat = map id2conf_cat (cs) -- conflicting categories-          nc_cat = map id2cat (as \\ cs) -- noconflicting categories-      return $ dcLabel (fromList $ c_cat ++ nc_cat) dcTrue-        where id2cat i = [ principal . C.pack $ "Review"++(show i)]-              id2conf_cat i = [ principal . C.pack $ "Review" ++ (show i)-                              , principal $ "CONFLICT" ]-          --- ^ Print if the current label flows to the output channel label, i.e.,--- there is no conflict of interest.-dcPutStrLn :: DCLabel -> Content -> DC ()-dcPutStrLn lo cont = do-  l <- getLabel-  if l `canFlowTo` lo-    then dcPutStrLnTCB cont-    else throwLIO . ErrorCall $ "Trying to print conflicting review:\n" ++-                               (show l) ++ " [/= " ++ (show lo)---- ^ Main printing function. Print to a labeled output channel.-reviewDCPutStrLn :: String -> ReviewDC ()-reviewDCPutStrLn s = do -  l <- getOutputChLbl-  liftLIO $ dcPutStrLn l $ "-> "++ s---- | Print line to standard output-reviewDCPutStrLnTCB :: String -> ReviewDC ()-reviewDCPutStrLnTCB = liftLIO . dcPutStrLnTCB---- ^ Given a paper number and review content append to the current review.-appendToReview :: Id -> Content -> ReviewDC (Either ErrorStr ())-appendToReview pId content = do-  mRev <- findReview pId -  case mRev of -    Nothing -> return $ Left "Invalid Id"-    Just rev -> do privs <- getPrivs-                   _ <- doWriteReview privs rev-                   return $ Right ()-   where doWriteReview privs rev = liftLIO $ do-           toLabeledP privs top $ do-             (Review rs) <- readLIORef (review rev)-             -- restrict writes: -             writeLIORef (review rev) (Review (rs++content))---- ^ Set the current label to the assignments-assign2curLabel :: [Id] -> ReviewDC() -assign2curLabel as = liftLIO $ do-  let l = dcLabel dcTrue (fromList $ map id2cat as)-  setLabelP allPrivTCB l-        where id2cat i = [principal . C.pack $ "Review"++(show i)]-  --- ^ Safely execute untrusted code-safeExecTCB :: ReviewDC () -> ReviewDC ()-safeExecTCB m = do-  s <- get'-  s' <- liftLIO $ do-    cc <- getClearance-    cl <- getLabel-    (_, s') <- (runReviewDC m s) `catchLIO` -                  (\(_::SomeException) -> do-                        dcPutStrLnTCB "-> ERROR: IFC violated\n"-                        return ((), s))-    setClearanceP allPrivTCB cc-    setLabelP allPrivTCB cl-    return s'-  put' s'---- ^ Execute on behalf of user-asUser :: Name -> ReviewDC a -> ReviewDC ()-asUser n m = do-  putCurUserName n-  mu <- getCurUser-  case mu of-    Nothing -> return ()-    Just u -> do-      reviewDCPutStrLnTCB $ "| Hi, "++ (name u)++".\n| Password>"-      p <- liftLIO dcGetLineTCB-      if p /= (password u)-        then reviewDCPutStrLnTCB "| Failed, try again" >> asUser n m-        else do-          reviewDCPutStrLnTCB $ "| Executing on behalf of "++(name u)++"...\n"-          safeExecTCB $ assign2curLabel (assignments u) >> m >> return ()-          clearCurUserName---- | Given a paper prefix return either an error string, if the paper cannot be--- found or the paper id.-findPaper :: String -> ReviewDC (Either ErrorStr Id)-findPaper s = do-  revs <- getReviews-  res <- mapM (simpleMatch s) revs >>= return . find isJust-  case res of-    Nothing -> return . Left $ "Could not find paper"-    Just i -> return . Right $ fromJust i-      -- ^ Fing paper by checking for prefix-    where simpleMatch :: String -> ReviewEnt -> ReviewDC (Maybe Id)-          simpleMatch m ent = do-            (Paper pap)  <- liftLIO $ readLIORefTCB (paper ent)-            if m `isPrefixOf` pap-              then return . Just $ paperId ent-              else return Nothing

@@ -1,32 +0,0 @@-{-# LANGUAGE Unsafe #-}--module Main (main) where--import LIO.DCLabel-import LambdaChair.TCB--import safe AliceCode as Alice-import safe BobCode as Bob---main :: IO ()-main = printL . runReviewDC' $ do-  addUser "Alice" "password"-  -  p1 <- addPaper "Flexible Dynamic..."-  p2 <- addPaper "A Static..."-  -  addAssignment "Alice" p1-  addAssignment "Alice" p2-  -  asUser "Alice" $ Alice.mainReview-  -  addUser "Bob" "password"-  -  addAssignment "Bob" p2-  addConflict "Bob" p1--  asUser "Bob" $ Bob.mainReview-    where printL m = m >>= (putStrLn . show . snd)-          runReviewDC' act = -            runDC $ runReviewDC act (emptyReviewState)

@@ -1,33 +0,0 @@--module Main where -- (main) where--import Control.Monad--import LIO-import LIO.Concurrent-import LIO.DCLabel--import System.Clock--cmp :: DCLabeled Int-        -> DCLabeled Int-        -> DC (DCLabeled (Maybe Bool))-cmp la lb = lBracket (lub (labelOf la) (labelOf lb)) (500) $ do-  a <- unlabel la-  b <- unlabel lb-  when (a == b) $ forever (return ())-  return (a == b)--exec :: Int -> Int -> IO ()-exec x y = runDC' $ do-  a <- label (dcLabel (toComponent "alice") dcTrue) x-  b <- label (dcLabel (toComponent "bob") dcTrue) y-  c <- cmp a b-  unlabel c-    where runDC' act = do-            t0 <- getTime Monotonic-            res <- runDC act-            t1 <- getTime Monotonic-            let micro t = (sec t * 1000000) + (nsec t `div` 1000)-            putStrLn $ "Result   = " ++ show res-                    ++ "Duration = " ++ show (micro t1 - micro t0)

@@ -1,7 +1,7 @@ module Main where   import LIO-import LIO.Privs.TCB (mintTCB)+import LIO.TCB import LIO.DCLabel  -- | Simple secrecy component example@@ -22,13 +22,13 @@  -- | Creating privilege using constructor from TCB p :: DCPriv-p = mintTCB  $ "Alice" /\ "Carla"+p = PrivTCB  $ "Alice" /\ "Carla"  main = do   putStrLn $ "Label 1: " ++ show l1   putStrLn $ "Label 2: " ++ show l2-  putStrLn $ "Join of labels: " ++ show (l1 `upperBound` l2)-  putStrLn $ "Meet of labels: " ++ show (l1 `lowerBound` l2)+  putStrLn $ "Join of labels: " ++ show (l1 `lub` l2)+  putStrLn $ "Meet of labels: " ++ show (l1 `glb` l2)   putStrLn $ "Privileges: " ++ show p   putStrLn $ "Label 1 flows to Label 2? " ++ (show $ canFlowTo l1 l2)   putStrLn $ "Label 1 flows to Label 2 given privileges? " ++

@@ -1,206 +0,0 @@-{-# LANGUAGE ScopedTypeVariables #-}--import Prelude hiding (catch)--import qualified Data.ByteString.Lazy as L-import qualified Data.ByteString.Lazy.Char8 as LC--import           Control.Monad-import           Control.Exception (SomeException)--import           System.FilePath--import           LIO-import           LIO.DCLabel-import           LIO.Concurrent-import           LIO.Handle-import           LIO.TCB (ioTCB, updateLIOStateTCB)-import           LIO.Privs.TCB (mintTCB)---dcEvalWithRoot :: FilePath -> DC a ->  IO a-dcEvalWithRoot path act = evalWithRootFS path (Just dcPub) act defaultState----- Enable malicious code:-malicious :: Bool-malicious = False---- Execute alice first?-execAliceFirst :: Bool-execAliceFirst = True------- Labels and privileges-----lalice, lbob, lbobOralice :: DCLabel-lalice      = dcLabel (toComponent "alice")   (toComponent "alice")-lbob        = dcLabel (toComponent "bob")     (toComponent "bob")-lclarice    = dcLabel (toComponent "clarice") (toComponent "clarice")-lbobOralice = dcLabel ("bob" \/ "alice")      ("bob" \/ "alice")--palice, pbob, pclarice :: DCPriv-pbob     = mintTCB $ dcPrivDesc "bob"-palice   = mintTCB $ dcPrivDesc "alice"-pclarice = mintTCB $ dcPrivDesc "clarice"---main = dcEvalWithRoot "/tmp/lio_fs/root" $ do-  putStrLnTCB $ "malicious = " ++ show malicious-  putStrLnTCB $ "execAliceFirst = " ++ show execAliceFirst-  let execA = exec alicesCode palice (dcLabel (toComponent "alice") dcTrue) "alice"-      execB = exec bobsCode pbob (dcLabel (toComponent "bob") dcTrue) "bob"-  if execAliceFirst -    then execA >> execB-    else execB >> execA-  exec claricesCode pclarice (dcLabel (toComponent "clarice") dcTrue) "clarice"-    where exec act p l s = do putStrLnTCB $ ">Executing for " ++ s ++ ":"-                              catchLIO (withClearance l $ setLabelTCB dcPub >> act p)-                                       (\(e::SomeException) ->-                                        putStrLnTCB "IFC violation attempt!")-                              printCurLabel $ ">" ++ s-                              putStrLnTCB "\n"-          setLabelTCB l = updateLIOStateTCB $ \s -> s { lioLabel = l }---printCurLabel s = do l <- getLabel -                     c <- getClearance-                     ioTCB . putStrLn $ s ++ " : " ++ show l ++ " : " ++ show c------- Bob's code:-----bobsCode :: DCPriv -> DC ()-bobsCode p = do-  discard_ $ createDirectoryP p lbobOralice "bobOralice"-  discard_ $ createDirectoryP p lbob ("bobOralice" </> "bob")-  -- Write alice a message:-  h <- openFileP p (Just lbobOralice) ("bobOralice" </> "messages") AppendMode-  hPutStrLnP p h (LC.pack "Hi Alice!")-  hCloseP p h-  -- Write secret:-  writeFileP p lbob ("bobOralice" </> "bob" </> "secret")-                    (LC.pack "I am Chuck Norris!")-------- Alice's code:--- --alicesCode :: DCPriv -> DC ()-alicesCode p = do-  when malicious malCode -  discard_ $ createDirectoryP p lbobOralice "bobOralice"-  discard_ $ createDirectoryP p lalice ("bobOralice" </> "alice")-  files <- getDirectoryContentsP p "bobOralice"-  if "messages" `elem` files-    then do msg <- readFileP p ("bobOralice" </> "messages")-            putStrLnTCB $ "Message log:\n" ++ (LC.unpack msg)-    else writeFileP p lbobOralice ("bobOralice" </> "messages")-                                   (LC.pack "Hello Bob!")-    where malCode = do-            msg <- readFileP p ("bobOralice" </> "bob" </> "secret")-            putStrLnTCB $ "Bob's secret:\n" ++ (LC.unpack msg)-            -------- Clarice's malicious code:-----claricesCode :: DCPriv -> DC ()-claricesCode p = do-  discard_ $ createDirectoryP p lclarice "clarice"-  when malicious $ do-    files <- getDirectoryContentsP p "bobOralice"-    forM_ files $ \f -> putStrLnTCB f-------- Misc helper functions--- --discard_ :: DC a -> DC ()-discard_ act = do-  forkLIO $ void act-  threadDelay 100---putStrLnTCB :: String -> DC ()-putStrLnTCB s = ioTCB $ putStrLn s----{- OUTPUT:-*Main> main-malicious = False-execAliceFirst = False->Executing for bob:->bob : < |True , |True > : < |False , |True >--->Executing for alice:-Message log:-Hi Alice!-->alice : < |True , |True > : < |False , |True >--->Executing for clarice:->clarice : < |True , |True > : < |False , |True >--- rm -rf /tmp/lio_fs/root --------------------------------------------*Main> main-malicious = True-execAliceFirst = False->Executing for bob:->bob : < |True , |True > : < |False , |True >--->Executing for alice:-IFC violation attempt!->alice : < |True , |True > : < |False , |True >--->Executing for clarice:-IFC violation attempt!->clarice : < |True , |True > : < |False , |True >--- rm -rf /tmp/lio_fs/root --------------------------------------------*Main> main-malicious = False-execAliceFirst = True->Executing for alice:->alice : < |True , |True > : < |False , |True >--->Executing for bob:->bob : < |True , |True > : < |False , |True >--->Executing for clarice:->clarice : < |True , |True > : < |False , |True >---- rm -rf /tmp/lio_fs/root --------------------------------------------*Main> main-malicious = True-execAliceFirst = True->Executing for alice:-IFC violation attempt!->alice : < |True , |True > : < |False , |True >--->Executing for bob:->bob : < |True , |True > : < |False , |True >--->Executing for clarice:-IFC violation attempt!->clarice : < |True , |True > : < |False , |True >----}-

@@ -1,7 +1,7 @@ import LIO import LIO.DCLabel -import LIO.Privs.TCB (mintTCB)+import LIO.TCB   -- | Add two numbers if the computation is invoked by Alice or Bob.@@ -13,9 +13,9 @@   alice, bob, clark :: DCPriv-alice = mintTCB . dcPrivDesc $ "Alice"-bob   = mintTCB . dcPrivDesc $ "Bob"-clark = mintTCB . dcPrivDesc $ "Clark"+alice = PrivTCB . dcPrivDesc $ "Alice"+bob   = PrivTCB . dcPrivDesc $ "Bob"+clark = PrivTCB . dcPrivDesc $ "Clark"  main = putStrLn . show $    [ callGate addGate alice 1 2 -- Just 3

@@ -16,13 +16,13 @@ h = dcLabel ("A" /\ "B")      dcTrue  main =  do-  (_,lr) <- runDC $ do+  lr <- evalDC $ do     lb <- label m (6 :: Int)     f <- lFork (if doFail then l else m) $ do       v <- unlabel lb       return (3+v)-    catchLIO (do r <- lWait f-                 ioTCB . putStrLn $ "No exception: " ++ show r -             ) (\(_::SomeException) -> ioTCB . putStrLn $ "Exception")+    catch (do r <- lWait f+              ioTCB . putStrLn $ "No exception: " ++ show r +          ) (\(_::SomeException) -> ioTCB . putStrLn $ "Exception")   print lr     where doFail = not True

@@ -1,5 +1,5 @@ Name:           lio-Version:        0.9.2.2+Version:        0.10.0.0 Cabal-Version:  >= 1.8 Build-type:     Simple License:        GPL@@ -40,85 +40,50 @@   should have type 'LIO', which trusted code can safely execute with   'evalLIO'. See "LIO" for a description of the core library API. -  . -  The paper that describes the core of LIO, including motivation and-  formal modeling/proofs, is available here:-  <http://arxiv.org/abs/1207.1457>-- Extra-source-files:   examples/dclabel.hs   examples/gate.hs   examples/waitAndCatch.hs-  examples/bracket.hs-  examples/fsExample.hs-  examples/LambdaChair/LambdaChair.hs-  examples/LambdaChair/LambdaChair/TCB.hs-  examples/LambdaChair/AliceCode.hs-  examples/LambdaChair/BobCode.hs-  examples/LambdaChair/Main.hs   Source-repository head   Type:     git-  Location: ssh://anonymous@gitstar.com/scs/lio.git--Flag toLabeled-  Description:-    Enable toLabeled primitive. This is NOT-    termination-sensitive non-interferant so use with care.-  Default: False+  Location: git://github.com/scslab/lio.git  Library   Build-Depends:-    base         >= 4.5     && < 5.0-   ,binary       >= 0.5.0.0-   ,transformers >= 0.2.2-   ,containers   >= 0.4.2-   ,bytestring   >= 0.9-   ,filepath     >= 1.3.0.0-   ,directory    >= 1.1.0.2-   ,xattr        >= 0.6.1-   ,zlib         >= 0.5.3.1-   ,SHA          >= 1.5.0.0+    base          >= 4.5     && < 5.0+   ,containers+   ,bytestring    GHC-options: -Wall -fno-warn-orphans -  if flag(toLabeled)-    CPP-options: -DTO_LABELED-   Exposed-modules:     -- * Top-level exporter     LIO+    LIO.Run     -- * Label definition     LIO.Label     -- * Core library     LIO.Core-    LIO.TCB+    LIO.Exception     -- * Labeled values     LIO.Labeled-    LIO.Labeled.TCB     -- * Labeled IORefs     LIO.LIORef-    LIO.LIORef.TCB-    -- * Gates-    LIO.Gate     -- * LIO privileges     LIO.Privs-    LIO.Privs.TCB     -- * Concurrency     LIO.Concurrent-    LIO.Concurrent.TCB     LIO.Concurrent.LMVar-    LIO.Concurrent.LMVar.TCB     -- * DCLabels     LIO.DCLabel     LIO.DCLabel.Core     LIO.DCLabel.Privs-    LIO.DCLabel.Privs.TCB-    LIO.DCLabel.Serialize     LIO.DCLabel.DSL-    -- * File system-    LIO.Handle-    LIO.FS.TCB+    -- * Privileged internals+    LIO.TCB+    LIO.TCB.LObj+    LIO.TCB.Concurrent+    LIO.TCB.DCLabel