lio 0.1.3 → 0.9.0.0

raw patch · 48 files changed

+3951/−7804 lines, 48 filesdep +transformersdep +xattrdep +zlibdep −QuickCheckdep −arraydep −base64-bytestringdep ~SHAdep ~basedep ~bytestringPVP ok

version bump matches the API change (PVP)

Dependencies added: transformers, xattr, zlib

Dependencies removed: QuickCheck, array, base64-bytestring, dclabel, lio, mtl, old-time, test-framework, test-framework-quickcheck2, unix

Dependency ranges changed: SHA, base, bytestring, cereal, containers, directory, filepath, time

API changes (from Hackage documentation)

Files

• LIO.hs +35/−59
• LIO/Concurrent.hs +190/−79
• LIO/Concurrent/LMVar.hs +217/−13
• LIO/Concurrent/LMVar/Safe.hs +0/−22
• LIO/Concurrent/LMVar/TCB.hs +73/−234
• LIO/Concurrent/TCB.hs +31/−0
• LIO/Core.hs +595/−0
• LIO/DCLabel.hs +94/−108
• LIO/DCLabel/Core.hs +275/−0
• LIO/DCLabel/DSL.hs +155/−0
• LIO/DCLabel/Privs.hs +100/−0
• LIO/DCLabel/Privs/TCB.hs +45/−0
• LIO/DCLabel/Serialize.hs +31/−0
• LIO/Data/Time.hs +37/−0
• LIO/FS.hs +0/−652
• LIO/FS/TCB.hs +267/−0
• LIO/Gate.hs +97/−0
• LIO/Handle.hs +469/−262
• LIO/LIORef.hs +138/−12
• LIO/LIORef/Safe.hs +0/−19
• LIO/LIORef/TCB.hs +67/−135
• LIO/Label.hs +160/−0
• LIO/Labeled.hs +187/−0
• LIO/Labeled/TCB.hs +52/−0
• LIO/MonadCatch.hs +0/−88
• LIO/MonadLIO.hs +0/−31
• LIO/Privs.hs +96/−0
• LIO/Privs/TCB.hs +57/−0
• LIO/Safe.hs +0/−60
• LIO/TCB.hs +185/−1201
• System/Posix/Tmp.hsc +0/−112
• cbits/HsTmp.c +0/−19
• configure +0/−3666
• configure.ac +0/−13
• examples/LambdaChair/AliceCode.hs +0/−25
• examples/LambdaChair/BobCode.hs +0/−20
• examples/LambdaChair/LambdaChair.hs +0/−419
• examples/LambdaChair/Main.hs +0/−38
• examples/LambdaChair/Safe.hs +0/−10
• examples/dclabel.hs +47/−0
• examples/fsExample.hs +126/−49
• examples/gate.hs +24/−0
• examples/waitAndCatch.hs +11/−11
• include/HsTmp.h +0/−22
• include/HsTmpConfig.h +0/−29
• include/HsTmpConfig.h.in +0/−28
• lio.cabal +90/−95
• tests/Tests.hs +0/−273

@@ -1,67 +1,43 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Safe #-}-#endif--{- | This is the main module to be included by code using the Labeled-   IO (LIO) library.  The core of the library is documented in the-   "LIO.TCB" module.  Note, however, that unprivileged code must not-   be allowed to import "LIO.TCB"--instead, a module "LIO.Safe"-   exports just the safe symbols from "LIO.TCB".  This module,-   "LIO", re-exports "LIO.Safe" as well as a few other handy-   modules.  For many modules it should be the only import necessary.--   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:--   @-    import Prelude hiding ('catch')-    import Control.Exception hiding ('throwIO', 'catch', 'handle', 'onException'-                                    , 'bracket', 'block', 'unblock')-    import LIO-   @--   The LIO variants of the system functions hidden in the above import-   commands are designed to work in both the IO and LIO monads, making-   it easier to have both types of code in the same module.---        Warning:  For security, at a minimum untrusted code must not be-        allowed to do any of the following:--          * Import "LIO.TCB",--          * Use any symbols with names ending @...TCB@,--          * Use the @foreign@ keyword,+{- | -          * Use functions such as 'unsafePerformIO', 'unsafeInterleaveIO',-            'inlinePerformIO',+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"). -          * Use language extensions such as Generalized Newtype-            Deriving and Stand-alone Deriving to extend LIO types-            (such as by deriving an instance of @'Show'@ for 'Lref',-            or deriving an instance of the @'MonadTrans'@ class for-            'LIO', which would allow untrusted code to bypass all-            security with 'lift'),+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: -          * Manually define @typeOf@ methods (as this would cause the-            supposedly safe 'cast' method to make usafe casts); automatically-            deriving @Typeable@ should be safe.+@+ import Control.Exception hiding ( 'onException'+                                 , 'finally'+                                 , 'bracket')+ import "LIO"+ -- Import your favorite label format:+ import "LIO.DCLabel"+@ -          * Define new 'Ix' instances (which could produce out of bounds-            array references).+WARNING:  For security, untrusted code must always be compiled with+the @-XSafe@ and @-fpackage-trust@ /SafeHaskell/ flags. See+<http://hackage.haskell.org/trac/ghc/wiki/SafeHaskell> for more+details on the guarantees provided by SafeHaskell. -        In general, pragmas and imports should be highly scrutinized.-        For example, most of the "Foreign" class of modules are probably-        dangerous. With GHC 7.2, we use the SafeHaskell extension to enforce-        these restrictions. -}-module LIO ( module LIO.Safe-           , module LIO.MonadLIO-           ) where -import safe LIO.Safe-import safe LIO.MonadLIO+module LIO ( +    module LIO.Label+  , 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

@@ -1,102 +1,213 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Trustworthy #-}-#endif--- |This module exposes the concurrent interface to LIO. Specifically,--- it implements labeled /fork/ ('lFork') and /wait/ ('lWait'). We--- strongly suggest these primitives over 'toLabeled' as they are--- termination-senstivie.-module LIO.Concurrent ( lForkP, lFork-                      , lWaitP, lWait-                      ) where+{- | -import LIO.TCB-import LIO.Concurrent.LMVar.TCB-import Control.Concurrent-import Control.Exception (toException)-import Data.Functor+This module exposes useful concurrency abstrations for 'LIO'. This+module is, in part, analogous to "Control.Concurrent". Specifically,+LIO provides a means for spawning 'LIO' computations in a new thread+with 'forkLIO'.  LIO relies on the lightweight threads managed by+Haskell's runtime system; we do not provide a way to fork OS-level+threads. --- | An LIO fork.-forkLIO :: (LabelState l p s) => LIO l p s () -> LIO l p s ThreadId-forkLIO m = do-  s <- getTCB-  ioTCB . forkIO $ runLIO m s >> return ()+In addition to this, LIO also provides 'lFork' and 'lWait' which allow+forking of a computation that is restricted from reading data more+sensitive than a given upper bound. This limit is different from+clearance in that it allows the computation to spawn additional+threads with an upper bound above said upper bound label, but below+the clearance. The 'lFork' function should be used whenever an LIO+computation wishes to execute a sub-computation that may raise the+current label (up to the supplied upper bound).  To this end, the+current label only needs to be raised when the computation is+interested in reading the result of the sub-computation. The role of+'lWait' is precisely this: raise the current label and return the+result of such a sub-computation. +-}+module LIO.Concurrent (+    LabeledResult+  , ThreadId, myThreadId+  -- * Forking new threads+  , forkLIO, lForkP, lFork+  -- * Waiting on threads+  , lWaitP, lWait+  , trylWaitP, trylWait+  , threadDelay+  -- * Forcing computations (EXPERIMENTAL)+  , AsyncException(..)+  , lForce, lForceP+  ) where --- | Same as 'lFork', but the supplied set of priviliges are accounted--- for when performing label comparisons.-lForkP :: (LabelState l p s)-       => p -> l -> LIO l p s a -> LIO l p s (LRes l a)-lForkP p' l m = withCombinedPrivs p' $ \p -> do-  mv <- newEmptyLMVarP p l-  _ <- forkLIO $ do-         res <- (Right <$> m) `catchTCB` (return . Left . (lubErr l))-         lastL <- getLabel-         putLMVarTCB mv (if leqp p lastL l-                           then res-                           else let l' = lub lastL l-                                in Left . mkErr . (lub l') $-                                      either getELabel (const l') res-                        ) -  return $ LRes mv-    where mkErr le = LabeledExceptionTCB le $ toException LerrLow-          lubErr lnew (LabeledExceptionTCB le e) =-                  LabeledExceptionTCB (le `lub` lnew) e-          getELabel (LabeledExceptionTCB le _) = le+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 (putLMVarTCB) --- | Labeled fork. @lFork@ allows one to invoke computations taht++-- | 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+  s <- getLIOStateTCB+  ioTCB . forkIO . void $ tryLIO act s+++-- | Labeled fork. @lFork@ allows one to invoke computations that -- would otherwise raise the current label, but without actually -- raising the label. The computation is executed in a separate thread -- and writes its result into a labeled result (whose label is -- supplied). To observe the result of the computation, or if the -- computation has terminated, one will have to call 'lWait' and--- raise the current label. Of couse, as in 'toLabeled', this can be--- postponed until the result is needed.+-- 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. 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 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.  -- -- If an exception is thrown in the inner computation, the exception -- label will be raised to the join of the result label and original -- exception label. -- --- Not that, compared to 'toLabeled', @lFork@ immediately returns a--- labeled result of type 'LRes', which is essentially a \"future\",--- or \"promise\". Moreover, to guarantee that the computation has--- completed, it is important that some thread actually touch the--- future, i.e., perform an 'lWait'.-lFork :: (LabelState l p s)-      => l                    -- ^ Label of result-      -> LIO l p s a          -- ^ Computation to execute in separate thread-      -> LIO l p s (LRes l a) -- ^ Labeled result-lFork = lForkP noPrivs+-- Note that @lFork@ immediately returns a 'LabeledResult', which is+-- essentially a \"future\", or \"promise\". This prevents+-- timing/termination attacks in which the duration of the forked+-- computation affects the duration of the @lFork@.+-- +-- To guarantee that the computation has completed, it is important that+-- some thread actually touch the future, i.e., perform an 'lWait'.+lFork :: Label l+      => l                -- ^ Label of result+      -> LIO l a          -- ^ Computation to execute in separate thread+      -> LIO l (LabeledResult l a) -- ^ Labeled result+lFork = lForkP NoPrivs --- | A labeled thread result is simply a wrapper for a labeled MVar. A--- thread can observe the result of another thread, only after raising--- its label to the label of the result.-data LRes l a = LRes (LMVar l (Either (LabeledException l) a))+-- | 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 --- | Same as 'lWait', but uses priviliges in label checks and raises.-lWaitP :: (LabelState l p s) => p -> LRes l a -> LIO l p s a-lWaitP p' (LRes mv) = withCombinedPrivs p' $ \p -> do-  ea <- takeLMVarP p mv-  case ea of-    Right x -> return x-    Left e -> ioTCB $ throwIO e+--+-- Wait+-- --- | Given a labeled result (a future), @lWait@ returns the unwrapped+-- | Given a 'LabeledResult' (a future), @lWait@ returns the unwrapped -- result (blocks, if necessary). For @lWait@ to succeed, the label of -- the result must be above the current label and below the current--- clearnce. Moreover, before block-reading, @lWait@ raises the current--- label to the join of the current label and label of result.--- If the thread @lWait@ is terminates with an exception (for example--- if it violates clearance), the exceptin is rethrown. Similarly, if --- the thread reads values above the result label, an exception is--- thrown in place of the result.-lWait :: (LabelState l p s) => LRes l a -> LIO l p s a-lWait = lWaitP noPrivs+-- clearance. Moreover, before block-reading, @lWait@ raises the current+-- label to the join of the current label and label of result.  An+-- exception is thrown by the underlying 'guardWrite' if this is not the+-- case.  Additionally, if the thread terminates with an exception (for+-- 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++-- | 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+  case v of+    Right x -> return x+    Left e  -> liftLIO $ unlabeledThrowTCB e++-- | Same as 'lWait', but does not block waiting for result.+trylWait :: MonadLIO l m => LabeledResult l a -> m (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+                 case v of+                   Right x -> return $! Just x+                   Left e  -> liftLIO $ unlabeledThrowTCB e+    _ -> return Nothing+++-- | Suspend current thread for a given number of microseconds.+threadDelay :: MonadLIO l m => Int -> m ()+threadDelay = liftLIO . ioTCB . C.threadDelay++--+-- Forcing computations+--++-- | Force execution of a thread spawned with 'lFork' or 'lForkP'.+-- If the computation completed without raising an exception, then the+-- result is wrapped in a 'Just', otherwise this function returns+-- 'Nothing'. Note that the current computation must be able to read+-- and write at the security level of the labeled result.+lForce :: MonadLIO l m => LabeledResult l a -> m (Labeled l (Maybe a))+lForce = lForceP NoPrivs++-- | Same as 'lForce', but uses privileges when raising current label+-- to the join of the current label and result label.+lForceP :: (MonadLIO l m, Priv l p)+        => p -> LabeledResult l a -> m (Labeled l (Maybe a))+lForceP p m = do+  let l = labelOf m+      mv = lresResultTCB m+  guardWriteP p l+  -- kill thread:+  liftLIO . ioTCB . killThread . lresThreadIdTCB $ m+  -- check to see if it wrote to MVar:+  v <- tryTakeLMVarP p mv+  return . labelTCB l =<< case v of+    Nothing -> do+      let e = toException ThreadKilled+      putLMVarTCB mv $ Left (LabeledExceptionTCB l e)+      return Nothing+    Just v' -> do+      putLMVarTCB mv v'+      case v' of+        Left _  -> return Nothing+        Right x -> return (Just x)

@@ -1,14 +1,218 @@-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)-{-# LANGUAGE Safe #-}-#endif--- |This module implements labeled @MVar@s.  The interface is analogous--- to "Control.Concurrent.MVar", but the operations take place in--- the LIO monad.  Moreover, taking and putting @MVars@ calls a write--- guard @wguard@ as every read implies a write and vice versa. This--- module exports only the safe subset (non-TCB) of the @LMVar@ module--- trusted code can import "LIO.Concurrent.LMVar.TCB".--- The interface is documented in "LIO.Concurrent.LMVar.TCB".-module LIO.Concurrent.LMVar ( module LIO.Concurrent.LMVar.Safe ) where+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE ConstraintKinds,+             FlexibleContexts #-}+{- | -import LIO.Concurrent.LMVar.Safe+This module implements labeled 'MVar's.  The interface is analogous to+"Control.Concurrent.MVar", but the operations take place in the 'LIO'+monad.  A labeled MVar, of type @'LMVar' l a@, is a mutable location+that can be in of of two states; an 'LMVar' can be empty, or it can be+full (with a value of tye @a@). The location is protected by a label+of type 'l'.  As in the case of @LIORef@s (see "LIO.LIORef"), this+label is fixed and does not change according to the content placed+into the location.  Different from @LIORef@s, taking and putting+'LMVars' calls the write guard 'guardWrite' to enforce sound+information flow control.++'LMVar's can be used to build synchronization primitives and+communication channels ('LMVar's themselves are single-place+channels).  We refer to "Control.Concurrent.MVar" for the full+documentation on MVars.++-}++module LIO.Concurrent.LMVar (+    LMVar+  -- * Creating labeled 'MVar's+  , newEmptyLMVar, newEmptyLMVarP+  , newLMVar, newLMVarP+  -- * Take 'LMVar'+  , takeLMVar, takeLMVarP+  , tryTakeLMVar, tryTakeLMVarP+  -- * Put 'LMVar'+  , putLMVar, putLMVarP+  -- * Read 'LMVar'+  , tryPutLMVar, tryPutLMVarP+  , readLMVar, readLMVarP+  -- * Swap 'LMVar'+  , swapLMVar, swapLMVarP+  -- * Check state of 'LMVar'+  , isEmptyLMVar, isEmptyLMVarP+  ) where++import           LIO.Label+import           LIO.Core+import           LIO.Privs+import           LIO.Concurrent.LMVar.TCB++--+-- Creating labeled 'MVar's+--++-- | 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+              => l                -- ^ Label of @LMVar@+              -> m (LMVar l a)    -- ^ New mutable location+newEmptyLMVar = newEmptyLMVarP NoPrivs++-- | 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 p l = do+  guardAllocP p l+  newEmptyLMVarTCB l++-- | Create a new labeled MVar, in an filled state with the supplied+-- value. Note that the supplied label must be above the current label+-- and below the current clearance.+newLMVar :: Label l+         => l                       -- ^ Label of @LMVar@+         -> a                       -- ^ Initial value of @LMVar@+         -> LIO l (LMVar l a)       -- ^ New mutable location+newLMVar = newLMVarP NoPrivs++-- | 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 p l a = do+  guardAllocP p l+  newLMVarTCB l a++--+-- Take 'LMVar'+--++-- | Return contents of the 'LMVar'. Note that a take consists of a read+-- and a write, since it observes whether or not the 'LMVar' is full, and+-- thus the current label must be the same as that of the 'LMVar' (of+-- course, this is not the case when using privileges).  Hence, if the+-- label of the 'LMVar' is below the current clearance, we raise the+-- current label to the join of the current label and the label of the+-- MVar and read the contents of the @MVar@. The underlying guard+-- '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++-- | 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++-- | 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++-- | 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++--+-- Put 'LMVar'+--++-- | Puts a value into an 'LMVar'. Note that a put consists of a read and+-- a write, since it observes whether or not the 'LMVar' is empty, and so+-- the current label must be the same as that of the 'LMVar' (of course,+-- this is not the case when using privileges). As in the 'takeLMVar'+-- case, if the label of the 'LMVar' is below the current clearance, we+-- raise the current label to the join of the current label and the label+-- of the MVar and put the value into the @MVar@.  Moreover if these IFC+-- restrictions fail, the underlying 'guardWrite' throws an exception.+-- If the 'LMVar' is full, @putLMVar@ blocks.+putLMVar :: Label l+         => LMVar l a   -- ^ Source 'LMVar'+         -> a           -- ^ New value+         -> LIO l ()+putLMVar = putLMVarP NoPrivs++-- | 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++-- | 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++-- | 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++--+-- 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++-- | 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++--+-- Swap 'LMVar'+--++-- | Takes a value from an 'LMVar', puts a new value into the 'LMvar',+-- and returns the taken value.  Like the other 'LMVar' operations it is+-- required that the label of the 'LMVar' be above the current label and+-- below the current clearance. Moreover, the current label is raised to+-- accommodate for the observation. The underlying 'guardWrite' throws an+-- exception if this cannot be accomplished. This operation is atomic iff+-- there is no other thread calling 'putLMVar' for this 'LMVar'.+swapLMVar :: Label l+          => LMVar l a          -- ^ Source @LMVar@+          -> a                  -- ^ New value+          -> LIO l a            -- ^ Taken value+swapLMVar = swapLMVarP NoPrivs++-- | 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++--+-- Check state of 'LMVar'+--++-- | Check the status of an 'LMVar', i.e., whether it is empty. The+-- function succeeds if the label of the 'LMVar' is below the current+-- clearance -- the current label is raised to the join of the 'LMVar'+-- 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++-- | 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

@@ -1,22 +0,0 @@-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)-{-# LANGUAGE Trustworthy #-}-#endif---- | This module exports a safe subset of the labeled MVar interface.--- See "LIO.Concurrent.LMVar.TCB" for the documentation.-module LIO.Concurrent.LMVar.Safe ( module LIO.Concurrent.LMVar.TCB ) where--import LIO.Concurrent.LMVar.TCB ( LMVar-                               , labelOfLMVar-                               , newEmptyLMVar, newEmptyLMVarP-                               , newLMVar, newLMVarP-                               , takeLMVar, takeLMVarP-                               , putLMVar, putLMVarP-                               , readLMVar, readLMVarP-                               , swapLMVar, swapLMVarP-                               , tryTakeLMVar, tryTakeLMVarP-                               , tryPutLMVar, tryPutLMVarP-                               , isEmptyLMVar, isEmptyLMVarP-                               , withLMVar, withLMVarP -                               ) 

@@ -1,270 +1,109 @@-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) && (__GLASGOW_HASKELL__ < 704)-{-# LANGUAGE SafeImports #-}-#endif-#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 704) {-# LANGUAGE Unsafe #-}-#endif {-|-This module provides an implementation for labeled MVars.  A labeled-MVar, of type @'LMVar' l a@, is a mutable location that can be in-of of two states; an 'LMVar' can be empty, or it can be full (with-a value of tye @a@). The location is protected by a label of type-'l'.  As in the case of @LIORef@s (see "LIO.LIORef"), this label-is static and does not change according to the content placed into-the location. -'LMVar's can be used to build synchronization primitives and-communication channels ('LMVar's themselves are single-place-channels).  We refer to "Control.Concurrent.MVar" for the full-documentation on MVars.+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 ( -- * Basic Functions-                                 LMVar-                               , labelOfLMVar-                               , newEmptyLMVar, newEmptyLMVarP-                               , newLMVar, newLMVarP-                               , takeLMVar, takeLMVarP-                               , putLMVar, putLMVarP-                               , readLMVar, readLMVarP-                               , swapLMVar, swapLMVarP-                               , tryTakeLMVar, tryTakeLMVarP-                               , tryPutLMVar, tryPutLMVarP-                               , isEmptyLMVar, isEmptyLMVarP-                               , withLMVar, withLMVarP -                               -- * Unsafe (TCB) Functions-                               , newEmptyLMVarTCB-                               , newLMVarTCB-                               , takeLMVarTCB-                               , putLMVarTCB-                               , readLMVarTCB-                               , swapLMVarTCB-                               , tryTakeLMVarTCB-                               , tryPutLMVarTCB-                               , isEmptyLMVarTCB-                               , withLMVarTCB-                               ) where+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.TCB+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 l (MVar a)---- | This function returns the label of a labeled MVar.-labelOfLMVar :: Label l => LMVar l a -> l-labelOfLMVar (LMVarTCB l _) = l+data LMVar l a = LMVarTCB { labelOfLMVar :: !l+                            -- ^ Label of MVar.+                          , unlabelLMVarTCB :: MVar a+                            -- ^ Access the underlying 'MVar', ignoring IFC.+                          } --- | 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 :: (LabelState l p s) => p -> l -> LIO l p s (LMVar l a)-newEmptyLMVarP p' l = withCombinedPrivs p' $ \p -> do-  aguardP p l-  iom <- ioTCB $ newEmptyMVar-  return $ LMVarTCB l iom+instance LabelOf LMVar where+  labelOf = labelOfLMVar --- | 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.-newEmptyLMVar :: (LabelState l p s)-              => l                        -- ^ Label of @LMVar@-              -> LIO l p s (LMVar l a)    -- ^ New mutable location-newEmptyLMVar l = getPrivileges >>= \p -> newEmptyLMVarP p l+--+-- Creating labeled 'MVar's+--  -- | Trusted function used to create an empty @LMVar@, ignoring IFC.-newEmptyLMVarTCB :: (LabelState l p s) => l -> LIO l p s (LMVar l a)+newEmptyLMVarTCB :: MonadLIO l m => l -> m (LMVar l a) newEmptyLMVarTCB l = do-  iom <- ioTCB $ newEmptyMVar-  return $ LMVarTCB l iom---- | 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 :: (LabelState l p s) => p -> l -> a -> LIO l p s (LMVar l a)-newLMVarP p' l a = withCombinedPrivs p' $ \p -> do-  aguardP p l-  m <- ioTCB $ newMVar a+  m <- liftLIO . ioTCB $ newEmptyMVar   return $ LMVarTCB l m --- | Create a new labeled MVar, in an filled state with the supplied--- value. Note that the supplied label must be above the current label--- and below the current clearance.-newLMVar :: (LabelState l p s)-         => l                           -- ^ Label of @LMVar@-         -> a                           -- ^ Initial value of @LMVar@-         -> LIO l p s (LMVar l a)       -- ^ New mutable location-newLMVar l a = getPrivileges >>= \p -> newLMVarP p l a- -- | Trusted function used to create an @LMVar@ with the supplied -- value, ignoring IFC.-newLMVarTCB :: (LabelState l p s) => l -> a -> LIO l p s (LMVar l a)+newLMVarTCB :: MonadLIO l m => l -> a -> m (LMVar l a) newLMVarTCB l a = do-  m <- ioTCB $ newMVar a+  m <- liftLIO . ioTCB $ newMVar a   return $ LMVarTCB l m --- | Same as 'takeLMVar' except @takeLMVarP@ takes a privilege object--- which is used when the current label is raised.-takeLMVarP :: (LabelState l p s) => p -> LMVar l a -> LIO l p s a-takeLMVarP p' (LMVarTCB l m) = withCombinedPrivs p' $ \p -> do-  wguardP p l-  ioTCB $ takeMVar m---- | Return contents of the 'LMVar'. Note that a take consists of a read--- and a write, since it observes whether or not the 'LMVar' is full,--- and thus the current label must be the same as that of the--- 'LMVar' (of course, this is not the case when using privileges).--- Hence, if the label of the 'LMVar' is below the current clearance,--- we raise the current label to the join of the current label and the--- label of the MVar and read the contents of the @MVar@. If the--- 'LMVar' is empty, @takeLMVar@ blocks.-takeLMVar :: (LabelState l p s) => LMVar l a -> LIO l p s a-takeLMVar x = getPrivileges >>= \p -> takeLMVarP p x+--+-- Take 'LMVar'+--  -- | Read the contents of an 'LMVar', ignoring IFC.-takeLMVarTCB :: (LabelState l p s) => LMVar l a -> LIO l p s a-takeLMVarTCB (LMVarTCB _ m) = ioTCB $ takeMVar m+takeLMVarTCB :: MonadLIO l m => LMVar l a -> m a+takeLMVarTCB (LMVarTCB _ m) = liftLIO . ioTCB $ takeMVar m --- | Same as 'putLMVar' except @putLMVarP@ takes a privilege object--- which is used when the current label is raised.-putLMVarP :: (LabelState l p s) => p -> LMVar l a -> a -> LIO l p s ()-putLMVarP p' (LMVarTCB l m) a = withCombinedPrivs p' $ \p -> do-  wguardP p l-  val <- ioTCB $ putMVar m a-  return val+-- | Same as 'tryTakeLMVar', but ignorses IFC.+tryTakeLMVarTCB :: MonadLIO l m => LMVar l a -> m (Maybe a)+tryTakeLMVarTCB (LMVarTCB _ m) = liftLIO . ioTCB $ tryTakeMVar m --- | Puts a value into an 'LMVar'. Note that a put consists of a read--- and a write, since it observes whether or not the 'LMVar' is empty,--- and so the current label must be the same as that of the 'LMVar'--- (of course, this is not the case when using privileges). As in the--- 'takeLMVar' case, if the label of the 'LMVar' is below the current--- clearance, we raise the current label to the join of the current--- label and the label of the MVar and put the value into the @MVar@.--- If the 'LMVar' is full, @putLMVar@ blocks.-putLMVar :: (LabelState l p s)-         => LMVar l a   -- ^ Source 'LMVar'-         -> a           -- ^ New value-         -> LIO l p s ()-putLMVar x a = getPrivileges >>= \p -> putLMVarP p x a+--+-- Put 'LMVar'+--  -- | Put a value into an 'LMVar', ignoring IFC.-putLMVarTCB :: (LabelState l p s) => LMVar l a -> a -> LIO l p s ()-putLMVarTCB (LMVarTCB _ m) a = ioTCB $ putMVar m a+putLMVarTCB :: MonadLIO l m => LMVar l a -> a -> m ()+putLMVarTCB (LMVarTCB _ m) a = liftLIO . ioTCB $ putMVar m a --- | Same as 'readLMVar' except @readLMVarP@ takes a privilege object--- which is used when the current label is raised.-readLMVarP :: (LabelState l p s) => p -> LMVar l a -> LIO l p s a-readLMVarP p' (LMVarTCB l m) = withCombinedPrivs p' $ \p -> do-  wguardP p l-  ioTCB $ readMVar m +-- | 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 --- | 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 :: (LabelState l p s) => LMVar l a -> LIO l p s a-readLMVar x = getPrivileges >>= \p -> readLMVarP p x --- | Trusted function used to read (take and put) an 'LMVar', ignoring IFC.-readLMVarTCB :: (LabelState l p s) => LMVar l a -> LIO l p s a-readLMVarTCB (LMVarTCB _ m) = ioTCB $ readMVar m+--+-- Read 'LMVar'+-- --- | Same as 'swapLMVar' except @swapLMVarP@ takes a privilege object--- which is used when the current label is raised.-swapLMVarP :: (LabelState l p s) => p -> LMVar l a -> a -> LIO l p s a-swapLMVarP p' (LMVarTCB l m) x = withCombinedPrivs p' $ \p -> do-  wguardP p l-  ioTCB $ swapMVar m x+-- | 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 --- | Takes a value from an 'LMVar', puts a new value into the 'LMvar',--- and returns the taken value.  Like the other 'LMVar' operations it--- is required that the label of the 'LMVar' be above the current label--- and below the current clearance. Moreover, the current label is raised--- to accommodate for the observation. This operation is atomic iff--- there is no other thread calling 'putLMVar' for this 'LMVar'.-swapLMVar :: LabelState l p s -          => LMVar l a          -- ^ Source @LMVar@-          -> a                  -- ^ New value-          -> LIO l p s a        -- ^ Taken value-swapLMVar x a = getPrivileges >>= \p -> swapLMVarP p x a+--+-- Swap 'LMVar'+--  -- | Trusted function that swaps value of 'LMVar', ignoring IFC.-swapLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s a-swapLMVarTCB (LMVarTCB _ m) x = ioTCB $ swapMVar m x---- | Same as 'tryTakeLMVar', but uses priviliges when raising current label.-tryTakeLMVarP :: (LabelState l p s)-              => p -> LMVar l a -> LIO l p s (Maybe a)-tryTakeLMVarP p' (LMVarTCB l m) = withCombinedPrivs p' $ \p -> do-  wguardP p l-  ioTCB $ tryTakeMVar m---- | Non-blocking version of 'takeLMVar'. It returns @Nothing@ if the--- 'LMVar' is empty, otherwise it returns @Just@ value, emptying the 'LMVar'.-tryTakeLMVar :: LabelState l p s => LMVar l a -> LIO l p s (Maybe a)-tryTakeLMVar x = getPrivileges >>= \p -> tryTakeLMVarP p x---- | Same as 'tryTakeLMVar', but ignorses IFC.-tryTakeLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s (Maybe a)-tryTakeLMVarTCB (LMVarTCB _ m) = ioTCB $ tryTakeMVar m---- | Same as 'tryPutLMVar', but uses privileges when raising current label.-tryPutLMVarP :: (LabelState l p s)-              => p -> LMVar l a -> a -> LIO l p s Bool-tryPutLMVarP p' (LMVarTCB l m) x = withCombinedPrivs p' $ \p -> do-  wguardP p l-  ioTCB $ tryPutMVar m x---- | Non-blocking version of 'putLMVar'. It returns @True@ if the--- 'LMVar' was empty and the put succeeded, otherwise it returns @False@.-tryPutLMVar :: LabelState l p s => LMVar l a -> a -> LIO l p s Bool-tryPutLMVar x a = getPrivileges >>= \p -> tryPutLMVarP p x a---- | Same as 'tryPutLMVar', but ignorses IFC.-tryPutLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s Bool-tryPutLMVarTCB (LMVarTCB _ m) x = ioTCB $ tryPutMVar m x----- | Same as 'isEmptyLMVar', but uses privileges when raising current label.-isEmptyLMVarP :: (LabelState l p s) => p -> LMVar l a -> LIO l p s Bool-isEmptyLMVarP p' (LMVarTCB l m) = withCombinedPrivs p' $ \p -> do-  taintP p l-  ioTCB $ isEmptyMVar m+swapLMVarTCB :: MonadLIO l m => LMVar l a -> a -> m a+swapLMVarTCB (LMVarTCB _ m) x = liftLIO . ioTCB $ swapMVar m x --- | Check the status of an 'LMVar', i.e., whether it is empty. The--- function succeeds if the label of the 'LMVar' is below the current--- clearance -- the current label is raised to the join of the 'LMVar'--- label and the current label. Note that this function only returns a--- snapshot of the state.-isEmptyLMVar :: LabelState l p s => LMVar l a -> LIO l p s Bool-isEmptyLMVar x = getPrivileges >>= \p -> isEmptyLMVarP p x+--+-- Check state of 'LMVar'+--  -- | Same as 'isEmptyLMVar', but ignorses IFC.-isEmptyLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s Bool-isEmptyLMVarTCB (LMVarTCB _ m) = ioTCB $ isEmptyMVar m---- | Same as 'withLMVar', but uses privileges when performing label--- comparisons/raises.-withLMVarP :: (LabelState l p s)-          => p -> LMVar l a -> (a -> LIO l p s b) -> LIO l p s b-withLMVarP p' m@(LMVarTCB l _) io = withCombinedPrivs p' $ \p -> do-  wguardP p l-  withLMVarTCB m io---- | Exception-safe wrapper for working with an 'LMVar'. The original--- contents of the 'LMVar' will be restored if the supplied action throws--- an exception. The function is atomic only if there is no other--- thread that performs a 'putLMVar'.-withLMVar :: LabelState l p s-          => LMVar l a -> (a -> LIO l p s b) -> LIO l p s b-withLMVar m io = getPrivileges >>= \p -> withLMVarP p m io---- | Same as 'withLMVar', but ignores IFC.-withLMVarTCB :: LabelState l p s-             => LMVar l a -> (a -> LIO l p s b) -> LIO l p s b-withLMVarTCB m io =-  mask $ \restore -> do-    a <- takeLMVarTCB m-    b <- restore (io a) `onExceptionTCB` putLMVarTCB m a-    putLMVarTCB m a-    return b+isEmptyLMVarTCB :: MonadLIO l m => LMVar l a -> m Bool+isEmptyLMVarTCB (LMVarTCB _ m) = liftLIO . ioTCB $ isEmptyMVar m

@@ -0,0 +1,31 @@+{-# 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

@@ -0,0 +1,595 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE ScopedTypeVariables,+             DeriveDataTypeable #-}++{- | ++This module implements the core of the Labeled IO (LIO) library for+information flow control (IFC) in Haskell.  It provides a monad,+'LIO', that is intended to be used as a replacement for the 'IO' monad+in untrusted code.  The idea is for untrusted code to provide a+computation in the 'LIO' monad, which trusted code can then safely+execute through using 'evalLIO'-like functions. Though, usually a+wrapper function is employed depending on the type of /labels/ used by+an application.  For example, with "LIO.DCLabel" trusted code would+'evalDC' to execute an untrusted computation.++Labels are a way of describing who can observe and modify data. (A+detailed consideration of labels is given in "LIO.Label".) LIO+associates a /current label/ with every 'LIO' computation. The current+label effectively tracks the sensitivity of all the data that the+computation has observed.  For example, if the computation has read a+\"secret\" mutable refernce (see "LIO.LIORef") and then the result of+a \"top-secret\" thread (see "LIO.Concurrent") then the current label+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+string\"@. More interestingly, consider reading a \"secret\" file:++> bs <- readFile "/secret/file.txt"++Though the label in the file store may be \"secret\", @bs@ has type+@ByteString@, which is not explicitly labeled. Hence, to protect the+contents (@bs@) the current label must be at least \"secret\" before+executing @readFile@.  More generally, if the current label is+@L_cur@, then it is only permissible to read data labeled @L_r@ if+@L_r ``canFlowTo`` L_cur@.  Note that, rather than throw an exception,+reading data will often just increase the current label to ensure that+@L_r ``canFlowTo`` L_cur@ using 'taint'.++Second, the current label prevents inforation leaks into public+channels. Specifically, it is only permissible to modify, or write+to, data labeled @L_w@ when @L_cur``canFlowTo`` L_w@. Thus, it the+following attempt to leak the secret @bs@ would fail:++> writeFile "/public/file.txt" bs++In addition to the current label, the LIO monad keeps a second label,+the current /clearance/ (accessible via the 'getClearance' function).+The clearance can be used to enforce a \"need-to-know\" policy since+it represents the highest value the current label can be raised to.+In other words, if the current clearance is @L_clear@ then the+computation cannot create, read or write to objects labeled @L@ such+that @L ``canFlowTo`` L_clear@ does not hold.++This module exports the 'LIO' monad, functions to access the internal+state (e.g., 'getLabel' and 'getClearance'), functions for raising and+catching exceptions, and IFC guards.  Exceptions are core to LIO since+they provide a way to deal with potentially-misbehaving untrusted+code. Specifically, when a computation is about to violate IFC (as+@writeFile@ above), an exception is raised. Guards provide a useful+abstraction for dealing with labeled objects; they should be used+before performing a read-only, write-only, or read-write operation on+a labeled object. The remaining core, but not all, abstractions are+exported by "LIO".++-}++module LIO.Core (+  -- * LIO monad+    LIO+  , MonadLIO(..)+  -- ** Execute LIO actions+  , evalLIO, runLIO, tryLIO, paranoidLIO+  -- ** Internal state+  , LIOState(..)+  -- *** Current label+  , getLabel, setLabel, setLabelP+  -- *** Current clerance+  , 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+  -- $lioExceptions+  , MonitorFailure(..)+  , VMonitorFailure(..)+  -- * Guards+  -- $guards+  -- ** Allocate/write-only+  , guardAlloc, guardAllocP+  -- ** Read-only+  , taint, taintP+  -- ** Write+  , guardWrite, guardWriteP+  ) where++import           Prelude hiding (catch)+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           LIO.TCB+import           LIO.Label+import           LIO.Privs+++--+-- 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) `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+++-- | 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++-- | 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 p l = do+  liftLIO $ guardAllocP p l `catchLIO`+      \(_ :: MonitorFailure) -> throwLIO InsufficientPrivs+  liftLIO . updateLIOStateTCB $ \s -> s { lioLabel = l }++-- | Returns the current value of the thread's clearance.+getClearance :: MonadLIO l m => m l+getClearance = liftLIO $ 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++-- | Raise the current clearance (undoing the effects of+-- 'setClearance') by exercising privileges. If the current label is+-- @l@ and current clearance is @c@, then @setClearanceP p cnew@+-- succeeds only if the new clearance is can flow to the current+-- 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 p cnew = do+  l <- getLabel+  c <- getClearance+  unless (canFlowToP p cnew c) $! throwLIO InsufficientPrivs+  unless (l `canFlowTo` cnew)  $! throwLIO CurrentLabelViolation+  liftLIO . updateLIOStateTCB $ \s -> s { lioClearance = 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'.+-- +-- 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++-- | 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+  guardAllocP p l+  c <- getClearance+  liftLIO . updateLIOStateTCB $ \s -> s { lioClearance = 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.+++   /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+--++{- $lioExceptions++Library functions throw an exceptions before an IFC violation can take+place. 'MonitorFailure' should be used when the reason for failure is+sufficiently described by the type. Otherwise, 'VMonitorFailure'+(i.e., \"Verbose\"-'MonitorFailure') should be used to further+describe the error.++-}++-- | Exceptions thrown when some IFC restriction is about to be+-- violated.+data MonitorFailure = ClearanceViolation+                    -- ^ Current label would exceed clearance, or+                    -- object label is above clearance.+                    | CurrentLabelViolation+                    -- ^ Clearance would be below current label, or+                    -- object label is not above current label.+                    | InsufficientPrivs+                    -- ^ Insufficient privileges. Thrown when lowering+                    -- the current label or raising the clearance+                    -- cannot be accomplished with the supplied+                    -- privileges.+                    | CanFlowToViolation+                    -- ^ Generic can-flow-to failure, use with+                    -- 'VMonitorFailure'+                    deriving (Show, Typeable)++instance Exception MonitorFailure++-- | Verbose version of 'MonitorFailure' also carrying around a+-- detailed message.+data VMonitorFailure = VMonitorFailure { monitorFailure :: MonitorFailure+                                       -- ^ Generic monitor failure.+                                       , monitorMessage :: String+                                       -- ^ Detailed message of failure.+                                       }+                    deriving Typeable++instance Show VMonitorFailure where+  show m = (show $ monitorFailure m) ++ ": " ++ (monitorMessage m)++instance Exception VMonitorFailure+++--+-- Guards+--++{- $guards++   Guards are used by (usually privileged) code to check that the+   invoking, unprivileged code has access to particular data.  If the+   current label is @lcurrent@ and the current clearance is+   @ccurrent@, then the following checks should be performed when+   accessing data labeled @ldata@:++   * When /reading/ an object labeled @ldata@, it must be the case+     that @ldata ``canFlowTo`` lcurrent@.  This check is performed by+     the 'taint' function, so named because it \"taints\" the current+     'LIO' context by raising @lcurrent@ until @ldata ``canFlowTo``+     lcurrent@.  (Specifically, it does this by computing the+     least 'upperBound' of the two labels.) However, this is done+     only if the new @lcurrent ``canFlowTo`` ccurrent@.++   * When /creating/ or /allocating/ objects, it is permissible for+     them to be higher than the current label, so long as they are+     below the current clearance.  In other words, it must be the+     case that @lcurrent ``canFlowTo`` ldata && ldata ``canFlowTo``+     ccurrent@.  This is ensured by the 'guardAlloc' function.++   * When /writing/ an object, it should be the case that+     @lcurrent ``canFlowTo`` ldata && ldata ``canFlowTo`` lcurrent@.+     (As stated, this is the same as saying @ldata == lcurrent@, but+     the two are different when using 'canFlowToP' instead of+     'canFlowTo'.) This is ensured by the 'guardWrite' function, which+     does the equivalent of 'taint' to ensure the target label @ldata@+     can flow to the current label, then throws an exception if+     @lcurrent@ cannot flow back to the target label.++     Note that in this case a write /always/ implies a read. Hence,+     when writing to an object for which you can observe the result,+     you must use 'guardWrite'. However, when performing a write for+     which there is no observable side-effects to the writer, i.e.,+     you cannot observe the success or failure of the write, then it+     is safe to solely use 'guardAlloc'.+++The 'taintP', 'guardAllocP',  and 'guardWriteP' functions are variants+of the above that take privilege to be more permissive and raise the+current label less. ++-}++--+-- Allocation+--++-- | Ensures the label argument is between the current IO label and+-- current IO clearance.  Use this function in code that allocates+-- objects--untrusted code shouldn't be able to create an object+-- labeled @l@ unless @guardAlloc l@ does not throw an exception.+-- Similarly use this guard in any code that writes to an+-- object labeled @l@ for which the write has no observable+-- side-effects.+--+-- 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++-- | 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 p newl = do+  c <- getClearance+  l <- getLabel+  unless (canFlowToP p l newl) $! throwLIO CurrentLabelViolation+  unless (newl `canFlowTo` c)  $! throwLIO ClearanceViolation++--+-- Read+--++-- | Use @taint l@ in trusted code before observing an object labeled+-- @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++-- | 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 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' }+++-- | Use @guardWrite l@ in any (trusted) code before modifying an+-- object labeled @l@, for which a the modification can be observed,+-- i.e., the write implies a read.+--+-- The implementation of @guardWrite@ is straight forward:+--+-- > guardWrite l = taint l >> guardAlloc l+--+-- 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++-- | Like 'guardWrite', but takes privilege argument to be more+-- permissive.+guardWriteP ::(MonadLIO l m, Priv l p) => p -> l -> m ()+guardWriteP p newl = do+  taintP      p newl+  guardAllocP p newl

@@ -1,139 +1,125 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Trustworthy #-}-#endif+{-# LANGUAGE MultiParamTypeClasses,+             ConstraintKinds,+             TypeSynonymInstances #-} -{-| This module provides bindings for the @DCLabel@ module, with some -renaming to resolve name clashes. The delegation of privilege and -other trusted code is not exported by this module and code wishing to-use this should import @DCLabel.TCB@.--}+{-| -{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE DeriveDataTypeable #-}-module LIO.DCLabel ( -- * DCLabel export-  		     module DCLabel.Safe-                   , DCCatSet-                     -- * Renamed privileges-                   , DCPriv, DCPrivTCB-                     -- * Useful aliases for the LIO Monad-                   , DCLabeled, DC, evalDC, evalDCWithRoot, DCGate-                     -- * Public label-                   , lpub-                   )where+/Disjunction Category Labels/ ('DCLabel's) are a label format that+encode secrecy and integrity using propositional logic.  This exports+label operators and instances for the "LIO". The label format is+documented in "LIO.DCLabel.Core", privileges are described in+"LIO.DCLabel.Privs", and a domain specific language for constructing+labels is presented in "LIO.DCLabel.DSL". -import LIO.TCB+-} -import LIO.Handle (evalWithRoot)+module LIO.DCLabel (+  -- ** Principals+    Principal, principal+  -- ** Clauses+  , Clause, clause+  -- ** Components+  , Component, dcTrue, dcFalse, dcFormula+  , isTrue, isFalse+  -- ** Labels+  , DCLabel, dcSecrecy, dcIntegrity, dcLabel, dcPub+  -- ** Privileges+  , module LIO.DCLabel.Privs+  -- ** DSL+  , module LIO.DCLabel.DSL+  -- * Synonyms for "LIO"+  -- $dcMonad+  , DCState, defaultState+  , DC, evalDC, runDC, tryDC, paranoidDC+  , MonadDC+  -- ** Exceptions+  , DCLabeledException+  -- ** Labeled values+  , DCLabeled+  -- ** Labeled references+  , DCRef+  -- ** Gates+  , DCGate+  ) where -import Data.Typeable+import           Control.Exception -import DCLabel.Safe hiding ( Priv-                           , bottom-                           , top-                           , join-                           , meet)-import qualified DCLabel.Core as DCL+import           LIO+import           LIO.LIORef+import           LIO.Labeled.TCB +import           LIO.DCLabel.Core+import           LIO.DCLabel.Privs+import           LIO.DCLabel.DSL+import           LIO.DCLabel.Serialize () -deriving instance Typeable DCL.Disj-deriving instance Typeable DCL.Conj-deriving instance Typeable DCL.Component-deriving instance Typeable DCL.DCLabel+--+-- LIO synonyms+--  -instance Label DCLabel where-	lbot = DCL.bottom-	ltop = DCL.top-	lub  = DCL.join-	glb  = DCL.meet-	leq  = DCL.canflowto--instance PrivTCB DCL.TCBPriv+-- | DC Labeled exceptions.+type DCLabeledException = LabeledException DCLabel -instance MintTCB DCL.TCBPriv DCL.Priv where-	mintTCB = DCL.createPrivTCB+-- | DC 'Labeled' values.+type DCLabeled = Labeled DCLabel -instance MintTCB DCL.TCBPriv DCL.Principal where-	mintTCB p = DCL.createPrivTCB (newPriv p)+instance LabeledFunctor DCLabel where+  lFmap lv f = let l = labelOf lv `upperBound` dcPub+               in label l $ f (unlabelTCB lv) -instance Priv DCLabel DCL.TCBPriv where-  	leqp = DCL.canflowto_p-        {--        The implementation of lostar deserves an explanation. Firstly note-        that the properties, for @r = lostar p l g@ that must be satisfied-        are [the suffix \'s\' (\'i\')is used for seecrecy (resp. integrity):-        1.) @leq g r    : (rs => gs)      and  (gi => ri)@-        2.) @leqp p l r : (rs /\ p => ls) and  (li /\ p => ri)@-        Finding the integrity component of @r@ is trivial: it's-        simply the least upper bound of @gi@ and @li /\ p@.-        Finding the secrecy component is a bit trickier. To do so, we first-        find all the categories of @ls@ that are not implied by @p@ (this-        gives us @rs'@), such that @rs' /\ p => ls@. Then, we need to find-        the remaining categories in @gs@ that are not implied by @rs'@ (this-        gives us @rs''@). Directly, @rs = rs' /\ rs''@.-        -}-        lostar p l g = -          let (ls, li) = (DCL.toLNF . secrecy $ l, DCL.toLNF . integrity $ l)-              (gs, gi) = (DCL.toLNF . secrecy $ g, DCL.toLNF . integrity $ g)-              lp       = DCL.toLNF . DCL.priv $ p-              rs'      = c2l [c | c <- getCats ls-                                , not (lp `DCL.implies` (c2l [c]))]-              rs''     = c2l [c | c <- getCats gs-                                , not (rs' `DCL.implies` (c2l [c]))]-              rs       = rs' `DCL.and_component` rs''-              ri       = (li `DCL.and_component` lp) `DCL.or_component` gi-         in DCL.toLNF $ simpleNewLabel p (newDC rs ri)-              where getCats = DCL.conj . DCL.component-                    c2l = DCL.MkComponent . DCL.MkConj-                    simpleNewLabel pr lr | pr == DCL.rootPrivTCB = g   -                                         | pr == DCL.noPriv      = l `lub` g-                                         | otherwise             = lr+-- | DC Labeled 'LIORef's.+type DCRef = LIORef DCLabel  -instance PrivDesc DCPrivTCB DCPriv where-  privDesc = priv+-- | DC 'Gate'.+type DCGate = Gate DCPrivDesc  ----- Renaming+-- DC monad -- --- | A @DCLabel@ category set.-type DCCatSet = DCL.Component---- | A @DCLabel@ (untrusted) privilege.-type DCPriv = DCL.Priv+{- $dcMonad --- | A @DCLabel@ privilege.-type DCPrivTCB = DCL.TCBPriv+The 'DC' monad is 'LIO' with using 'DCLabel's as the label format.+Most application should be written in terms of this monad, while most+libraries should remain polymorphic in the label type. It is important+that any *real* application set the initial current label and+clearance to values other than 'bottom' and 'top' as set by+'defaultState', respectively. In most cases the initial current label+should be public, i.e., 'dcPub'. +-} ------ LIO aliases---+-- | Type synonym for 'MonadLIO'.+type MonadDC m = MonadLIO DCLabel m -instance LabelState DCLabel DCPrivTCB () where+-- | 'LIOState' with underlying label being 'DCLabel'+type DCState = LIOState DCLabel --- | The type for 'Labeled' values uinsg 'DCLabel' as the label.-type DCLabeled a = Labeled DCLabel a+-- | 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 }  -- | The monad for LIO computations using 'DCLabel' as the label.-type DC = LIO DCLabel DCPrivTCB ()+type DC = LIO DCLabel --- | Runs a computation in the LIO Monad, returning both the--- computation's result and the label of the result.-evalDC :: DC a -> IO (a, DCLabel)-evalDC m = evalLIO m () --- | Same as 'evalDC', but with support for filesystem.-evalDCWithRoot ::  FilePath -> Maybe DCLabel -> DC a -> IO (a, DCLabel)-evalDCWithRoot path ml act = evalWithRoot path ml act ()+-- | Evaluate computation in the 'DC' monad.+evalDC :: DC a -> IO a+evalDC act = evalLIO act defaultState --- | A DC Label gate-type DCGate = Gate DCLabel DCPriv+-- | Evaluate computation in the 'DC' monad.+runDC :: DC a -> IO (a, DCState)+runDC act = runLIO act defaultState --- | Label corresponding to public data.-lpub :: DCLabel-lpub = newDC (<>) (<>)+-- | 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

@@ -0,0 +1,275 @@+{-# LANGUAGE Safe #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-|++This module implements Disjunction Category Labels (DCLabels).+DCLabels is a label format for information flow control (IFC) systems.+This library exports relevant data types and operations that may be+used by dynamic IFC systems such as the "LIO" library.++A 'DCLabel' is a pair of /secrecy/ and /integrity/ 'Component's+(sometimes called category sets).  Each 'Component' (or formula) is a+conjunction (implemented in terms of 'Set's) of 'Clause's (or+category) in propositional logic (without negation) specifying a+restriction on the flow of information labeled as such. Alternatively,+a 'Component' can take on the value 'DCFalse' corresponding to+falsehood.  Each 'Clause', in turn, is a disjunction of 'Principal's,+, where a 'Principal' is a source of authority of type 'ByteString',+whose meaning is application-specific (e.g., a 'Principal' can be a+user name, a URL, etc.).++A clause imposes an information flow restriction. In the case of+secrecy, a clause restricts who can read, receive, or propagate the+information, while in the case of integrity it restricts who can+modify a piece of data. The principals composing a clause are said to+/own/ the clause or category.++For information to flow from a source labeled @L_1@ to a sink @L_2@, the+restrictions imposed by the clauses of @L_2@ must at least as restrictive as+all the restrictions imposed by the clauses of @L_1@ (hence the conjunction)+in the case of secrecy, and at least as permissive in the case of integrity.+More specifically, for information to flow from @L_1@ to @L_2@, the labels+must satisfy the \"can-flow-to\" relation: @L_1 &#8849; L_2@.  The &#8849;+label check is implemented by the 'canFlowTo' function.  For labels+@L_1=\<S_1, I_1\>@, @L_2=\<S_2, I_2\>@ the can-flow-to relation is satisfied+if the secrecy component @S_2@ /implies/ @S_1@ and @I_1@ /implies/ @I_2@+(recall that a category set is a conjunction of disjunctions of principals).+For example, @\<P_1 &#8897; P_2, True\> &#8849; \<P_1, True\>@ because data+that can be read by @P_1@ is more restricting than that readable by @P_1@+or @P_2@. Conversely, @\<True,P_1\> &#8849; \<True,P_1 &#8897; P_2\>@+because data vouched for by @P_1@ or @P_2@ is more permissive than just @P_1@+(note the same principle holds when writing to sinks with such labeling).++-}++module LIO.DCLabel.Core ( +  -- * Principals+    Principal(..), principal+  -- * Clauses+  , Clause(..), clause+  -- * Components+  -- $component+  , Component(..)+  , dcTrue, dcFalse, dcFormula +  , isTrue, isFalse+  -- * Labels+  , DCLabel(..), dcLabel, dcLabelNoReduce, dcPub+  -- * Internal+  , dcReduce, dcImplies+  , dcAnd, dcOr+  ) where++import qualified Data.ByteString.Char8 as S8+import           Data.Typeable+import           Data.Set (Set)+import qualified Data.Set as Set++import           Data.List (intercalate)++import           LIO.Label++type S8 = S8.ByteString+++--+-- Principals+--++-- | 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 +                                -- ^ Get the principal name.+                              } deriving (Eq, Ord, Typeable)++instance Show Principal where+  show = S8.unpack . principalName++-- | Principal constructor.+principal :: S8 -> Principal+principal = Principal++--+-- Category - disjunction clauses+--++-- | A clause or disjunction category is a set of 'Principal's.+-- Logically the set corresponds to a disjunction of the principals.+newtype Clause = Clause { unClause :: Set Principal+                          -- ^ Get underlying principal-set.+                        } deriving (Eq, Typeable)++instance Ord Clause where+  (Clause c1) <= (Clause c2) =+    case () of+      _ | Set.size c1 == Set.size c2 -> c1 <= c2+      _ -> 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 ++ "]"++-- | Clause constructor+clause :: Set Principal -> Clause+clause = Clause++-- | A component is a set of clauses, i.e., a formula (conjunction of+-- disjunction of 'Principal's). @DCFalse@ corresponds to logical+-- @False@, while @DCFormula Set.empty@ corresponds to logical @True@.+data Component = DCFalse+                 -- ^ Logical @False@+               | DCFormula { unDCFormula :: !(Set Clause) +                              -- ^ Get underlying clause-set.+                           }+                 -- ^ Conjunction of disjunction categories+  deriving (Eq, Typeable)++instance Show Component where+  show c | isFalse c = "|False"+         | isTrue c  = "|True"+         | otherwise = let cs = map show . Set.toList $! unDCFormula c+                       in parens . intercalate " /\\ " $! cs+    where parens x = "{" ++ x ++ "}"++-- | Logical @True@.+dcTrue :: Component+dcTrue = DCFormula Set.empty++-- | Logical @False@.+dcFalse :: Component+dcFalse = DCFalse++-- | Arbitrary formula from a clause.+dcFormula :: Set Clause -> Component+dcFormula = DCFormula++-- | Is the component @True@.+isTrue :: Component -> Bool+isTrue = (== dcTrue)++-- | Is the component @False@.+isFalse :: Component -> Bool+isFalse = (== dcFalse)++--+-- Labels+--++{- $component+   A 'Component' is a conjunction of disjunctions of 'Principal's. A+   'DCLabel' is simply a pair of such 'Component's. Hence, we define+   almost all operations in terms of this construct, from which the+   'DCLabel' implementation follows almost trivially.+-}++-- | A @DCLabel@ is a pair of secrecy and integrity 'Component's.+data DCLabel = DCLabel { dcSecrecy   :: !Component+                         -- ^ Extract secrecy component of a label+                       , dcIntegrity :: !Component+                         -- ^ Extract integrity component of a label+                       } deriving (Eq, Typeable)++instance Show DCLabel where +  show l = let s = dcSecrecy l+               i = dcIntegrity l+           in "< " ++ show s ++ " , " ++ show i ++ " >"++-- | Label constructor. Note that each component is first reduced to+-- CNF.+dcLabel :: Component -> Component -> DCLabel+dcLabel c1 c2 = DCLabel (dcReduce c1) (dcReduce c2)++-- | Label contstructor. Note: the components should already be reduced.+dcLabelNoReduce :: Component -> Component -> DCLabel+dcLabelNoReduce = DCLabel++++-- | Element in the DCLabel lattice corresponding to public data.+-- @dcPub = \< True, True \> @. This corresponds to data that is not+-- secret nor trustworthy.+dcPub :: DCLabel+dcPub = DCLabel { dcSecrecy = dcTrue, dcIntegrity = dcTrue }++--+-- 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)+++  -- | The least upper bound of two labels, i.e., the join.+  lub l1 l2 = DCLabel+    { dcSecrecy   = dcReduce $ dcSecrecy l1   `dcAnd` dcSecrecy l2+    , dcIntegrity = dcReduce $ dcIntegrity l1 `dcOr`  dcIntegrity l2 }++  -- | The greatest lower bound of two labels, i.e., the meet.+  glb l1 l2 = DCLabel+    { dcSecrecy   = dcReduce $ dcSecrecy l1   `dcOr`  dcSecrecy l2+    , dcIntegrity = dcReduce $ dcIntegrity l1 `dcAnd` dcIntegrity l2 }+++--+-- Helpers+--++-- | Logical implication.+dcImplies :: Component -> Component -> Bool+dcImplies DCFalse _ = True+dcImplies _ DCFalse = False+dcImplies f1@(DCFormula cs1) f2@(DCFormula cs2)+   | isTrue f2 = True+   | isTrue f1 = False+   | otherwise = Set.foldl' dcImpliesDisj True cs2+  where dcImpliesDisj :: Bool -> Clause -> Bool+        dcImpliesDisj False _ = False+        dcImpliesDisj _ (Clause c2) = Set.foldl' f False cs1+          where f True _  = True+                f _     c1 = unClause c1 `Set.isSubsetOf` c2 ++-- | Logical conjunction+dcAnd :: Component -> Component -> Component +dcAnd x y | isFalse x || isFalse y = dcFalse+          | otherwise = DCFormula $! unDCFormula x `Set.union` unDCFormula y++-- | Logical disjunction+dcOr :: Component -> Component -> Component +dcOr x y | isTrue x || isTrue y = dcTrue+dcOr x y | isFalse x = y+         | isFalse y = x+         | otherwise = let cs1 = unDCFormula x+                           cs2 = unDCFormula y+                       in DCFormula $! doOr cs1 cs2+  where -- | Perform disjunction of two components.+        doOr :: Set Clause -> Set Clause -> Set Clause+        doOr cs1 cs2 = Set.foldl' disjFunc Set.empty cs2+          where disjFunc acc c = acc `Set.union` singleOr c cs1+        -- | Given a clause and a formula, perform logical or of+        -- clause with every clause in formula.+        singleOr :: Clause -> Set Clause -> Set Clause+        singleOr (Clause c1) = Set.map (Clause . Set.union c1 . unClause)++-- | Reduce component to conjunction normal form by removing clauses+-- implied by other.+dcReduce :: Component -> Component+dcReduce f | isFalse f || isTrue f = f+           | otherwise = DCFormula . doReduce . unDCFormula $ f+  where doReduce cs | Set.null cs = cs+        doReduce cs =+          let (x@(Clause x'), xs) = Set.deleteFindMin cs +              ys = doReduce $ Set.filter (not . Set.isSubsetOf x' . unClause) xs+          in Set.singleton x `Set.union` ys

@@ -0,0 +1,155 @@+{-# LANGUAGE Safe #-}+{-# LANGUAGE TypeSynonymInstances,+             FlexibleInstances #-}++{-|+  This module implements a ``nano``, very simple, embedded domain+  specific language to create 'Component's and privilage descriptions+  from conjunctions of principal disjunctions.+  +  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+  sub-expression. For example:++  @+     p1 = 'principal' \"p1\"+     p2 = 'principal' \"p2\"+     p3 = 'principal' \"p3\"+     e1 = p1 '\/' p2+     e2 = e1 '\/' \"p4\"+  @++  Similarly, the conjunction operator ('/\') is used to create category-sets+  from 'Principal's, ByteStrings, and conjunctive or disjunctive sub-expressions.+  For example:++  @+     e3 = p1 '\/' p2+     e4 = e1 '/\' \"p4\" '/\' p3+  @++  /Note/ that because a clause consists of a disjunction of principals, and a+  component is composed of the conjunction of categories, ('\/') binds+  more tightly than ('/\').++  Given two 'Component's, one for secrecy and one for integrity, you+  can create a 'DCLabel' with 'dcLabel'.  Given a 'DCPriv' and+  'DCPrivDesc' you can create a new minted privilege with+  'dcDelegatePriv'.+  +  +  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\"+  @++where++  * @ dc1 = \<{[\"Alice\" &#8897; \"Bob\"] &#8896; [\"Carla\"]} , {[\"Alice\"] &#8896; [\"Carla\"]}\>@+  +  * @ dc2 = \<{[\"Djon\"]} , {[\"Alice\"]}\>@++  * @ 'canFlowTo' dc1 dc2 = False @++  * @ 'canFlowToP' pr dc1 dc2 = True@++-}++module LIO.DCLabel.DSL (+  -- * Operators+    (\/), (/\), ToComponent(..)+  , fromList, toList+  -- * Aliases+  , everybody, anybody+  ) 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++-- | 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++-- | Identity of 'Component'.+instance ToComponent Component where+  toComponent = id+-- | 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++infixl 7 \/+infixl 6 /\++-- | Conjunction of two 'Principal'-based elements.+-- +-- @+-- infixl 6 /&#92;+-- @+--+(/\) :: (ToComponent a, ToComponent b) => a -> b -> Component+a /\ b = dcReduce $! toComponent a `dcAnd` toComponent b++-- | Disjunction of two 'Principal'-based elements.+-- +-- @+-- infixl 7 \\/+-- @+--+(\/) :: (ToComponent a, ToComponent b) => a -> b -> Component+a \/ b = dcReduce $! toComponent a `dcOr` toComponent b++--+-- Aliases+--++-- | Logical falsehood can be thought of as the component containing+-- every possible principal:+--+-- > everybody = dcFalse+--+everybody :: Component+everybody = dcFalse++-- | Logical truth can be thought of as the component containing+-- no specific principal:+--+-- > anybody = dcTrue+--+anybody :: Component+anybody = 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'.+toList :: Component -> [[Principal]]+toList DCFalse        = error "toList: Invalid use, expected DCFormula"+toList (DCFormula cs) = map (Set.toList . unClause) $! Set.toList cs++-- | Convert a list of list of 'Principal's to a 'Component'. Each+-- inner list is considered to correspond to a 'Clause'.+fromList :: [[Principal]] -> Component+fromList ps = DCFormula . Set.fromList $! map (Clause . Set.fromList) ps

@@ -0,0 +1,100 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE MultiParamTypeClasses,+             TypeSynonymInstances #-}+{- |++Privileges allow a piece of code to bypass certain information flow+restrictions imposed by labels.  A privilege is simply a conjunction+of disjunctions of 'Principal's, i.e., a 'Component'. We say that a+piece of code containing a singleton 'Clause' owns the 'Principal'+composing the 'Clause'.  However, we allow for the more general notion+of ownership of a clause, or category, as to create a+privilege-hierarchy. Specifically, a piece of code exercising a+privilege @P@ can always exercise privilege @P'@ (instead), if @P' => P@.+(This is similar to the DLM notion of \"can act for\".) Hence, if a+piece of code with certain privileges implies a clause, then it is+said to own the clause. Consequently it can bypass the restrictions of+the clause in any label.++Note that the privileges form a partial order over logicla implication+(@=>@), such that @'allPrivTCB' => P@ and @P => 'noPriv'@ for any+privilege @P@.  Hence, a privilege hierarchy which can be concretely+built through delegation, with 'allPrivTCB' corresponding to the+/root/, or all, privileges from which all others may be created. More+specifically, given a privilege @P'@ of type 'DCPriv', and a privilege+description @P@ of type 'DCPrivDesc', any piece of code can use+'delegatePriv' to \"mint\" @P@, assuming @P' => P@.++-}++module LIO.DCLabel.Privs (+    DCPrivDesc+  , DCPriv+  -- ** Helpers+  , noPriv+  , dcDelegatePriv+  , 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++-- | Privileges can be combined using 'mappend'+instance Monoid DCPriv where+  mempty = noPriv+  mappend p1 p2 = mintTCB . dcReduce $!+                      privDesc p1 `dcAnd` privDesc p2++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)++--+-- Helpers+--++-- | The empty privilege, or no privileges, corresponds to logical+-- @True@.+noPriv :: DCPriv+noPriv = mintTCB dcTrue++-- | Given a privilege and a privilege description turn the privilege+-- description into a privilege (i.e., mint). Such delegation succeeds+-- only if the supplied privilege implies the privilege description.+dcDelegatePriv :: DCPriv -> DCPrivDesc -> Maybe DCPriv+dcDelegatePriv p pd = let c  = privDesc $! p+                      in if c `dcImplies` pd+                           then Just $! mintTCB pd+                           else Nothing++-- | We say a piece of code having a privilege object (of type 'DCPriv')+-- owns a clause when the privileges allow code to bypass restrictions+-- imposed by the clause. This is the case if and only if the 'DCPriv'+-- object contains one of the 'Principal's in the 'Clause'.  This+-- function can be used to make such checks.+dcOwns :: DCPrivDesc -> Clause -> Bool+dcOwns pd c = pd `dcImplies` dcFormula (Set.singleton c)

@@ -0,0 +1,45 @@+{-# 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+

@@ -0,0 +1,31 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE StandaloneDeriving,+             GeneralizedNewtypeDeriving #-}++{- | This module provides instances for binary serialization of+'DCLabel's. Specifically, we provide insgtances for @cereal@\'s+@Data.Serialize@.  -}++module LIO.DCLabel.Serialize () where+++import           LIO.DCLabel.Core+import           Data.Serialize+import           Control.Monad++deriving instance Serialize Principal+deriving instance Serialize Clause++-- | Serialize components by converting them to maybe's+instance Serialize 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 Serialize DCLabel where+  put l = put (dcSecrecy l, dcIntegrity l)+  get   = uncurry dcLabelNoReduce `liftM` get

@@ -0,0 +1,37 @@+{-# LANGUAGE Trustworthy #-}+{- |++This module re-exports "Data.Time" wrapped in 'LIO'.++WARNING: The time functions can be used to carry out+/external-timing attacks/ with less effort than using threads and+synchronization. It is therefore advised that computations that+operate on sensitive data take the same amount of time regardless of+the input.++-}+module LIO.Data.Time (+    module Data.Time+  , getCurrentTime+  , getZonedTime+  , utcToLocalZonedTime+  ) where++import qualified Data.Time as T+import           Data.Time hiding ( getCurrentTime+                                  , getZonedTime+                                  , utcToLocalZonedTime)+import           LIO+import           LIO.TCB++-- | Get the current UTC time from the system clock.+getCurrentTime :: MonadLIO l m => m UTCTime+getCurrentTime = liftLIO $ rethrowIoTCB T.getCurrentTime++-- | Get the local time together with a TimeZone.+getZonedTime :: MonadLIO l m => m ZonedTime+getZonedTime = liftLIO $ rethrowIoTCB T.getZonedTime++-- | Convert UTC time to local time with TimeZone.+utcToLocalZonedTime :: MonadLIO l m => UTCTime -> m ZonedTime+utcToLocalZonedTime = liftLIO . rethrowIoTCB . T.utcToLocalZonedTime

@@ -1,652 +0,0 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702 && __GLASGOW_HASKELL__ < 704-{-# LANGUAGE SafeImports #-}-#endif-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE ScopedTypeVariables #-}--{- | This module implements a labeled filesystem as a file store in-   which a label is associated with every file and directory. The-   module "LIO.Handle" provides an interface for working with labeled-   directories and files -- this module provides the underlying-   low-level (mostly trusted) interface.--   The file store contains 3 components:--   * @.magic@ file containing a sequence of pre-defined bytes. The-     existence of this file and correct contents indicates that-     the file store and root of the labeled filesystem were created-     before any system crash.--   * @.obj@ directory containing all the objects (files and-     directories) in the filesystem, organized according to the-     object's label.--   * @ROOT@ symbolic link pointing to a directory object in @.obj@,-     representing the root of the filesystem.--   As the details of @.magic@ and @ROOT@ are straight forward, we-   now focus on the details of @.obj@.--   Each object is stored in @.obj@ in a directory corresponding-   to the label of the file. For example, an object protected by-   @bob@'s label will exist as:--   > .obj/oTAUzOt5YoQAyThw89eSgWuig-0=/obj012345--   where @oTAUzOt5YoQAyThw89eSgWuig-0=@ is the base64url encoding of-   the (SHA-224 hash of) label @bob@, and @obj012345@ is the object's-   name. Each label directory also contains a @.label@ file whose-   contents correspond to the serialization of the label. Hence, for-   example,--   > .obj/oTAUzOt5YoQAyThw89eSgWuig-0=/.label--   would have @bob@'s label.-   -   Every object in a label directory is either a file or a directory.-   If the object is a directory, its contents will strictly have-   symbolic links to objects in the file store. This is more easily-   understood using an example.--   Consider the following familiar filesystem layout, containing 4-   directories and 2 files:--   >-   > /-   > |-- bobOralice      (type: directory, label: bob \/ alice)-   > |   |-- alice       (type: directory, label: alice)-   > |   |-- bob         (type: directory, label: bob)-   > |   |   '-- secret  (type: file     , label: bob)-   > |   '-- messages    (type: file     , label: bob \/ alice)-   > '-- clarice         (type: directory, label: clarice)-   >--   Suppose we take @/lioFS@ as the location of the file store for our-   labeled filesystem. The above files and directories will have the-   same layout in our file system, but each file/directory points to-   an object in the object store (@.obj@), as shown below. --   >-   > /lioFS/ROOT-   > |-- bobOralice -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objXIBabq-   > |   |-- alice -> ../../12to8q3vDp7ApyKEQk2LQ_2nrvs=/objqZeR5w-   > |   |-- bob -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objtsePnc-   > |   |   '-- secret -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objFIQCIm-   > |   '-- messages -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objQaiwuA-   > '-- clarice -> ../../wordEFmBzWc7Q6qP-TetDgZaG8A=/objOMh0mj-   >--   Note that, to a user, the interface (see "LIO.Handle") is-   unchanged and they do not need to handle or understand the-   underlying file store. We refer to this view as \"friendly\". The-   file store for the above layout is:--   >-   > /lioFS/-   > |-- .magic-   > |-- .obj-   > |   |-- 12to8q3vDp7ApyKEQk2LQ_2nrvs=-   > |   |   |-- .label (=alice's label)-   > |   |   '-- objqZeR5w-   > |   |-- c_EkXYGrmrSit9j_8VjP_-8DgaM=-   > |   |   |-- .label (=label bob \/ alice)-   > |   |   |-- objQaiwuA-   > |   |   '-- objXIBabq-   > |   |       |-- alice -> ../../12to8q3vDp7ApyKEQk2LQ_2nrvs=/objqZeR5w-   > |   |       |-- bob -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objtsePnc-   > |   |       '-- messages -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objQaiwuA-   > |   |-- jX7q5Kb8_G4GsjgNpOHB17kypQo=-   > |   |   |-- .label (=label of the filesystem root)-   > |   |   '-- objTj5JZD-   > |   |       |-- bobOralice -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objXIBabq-   > |   |       '-- clarice -> ../../wordEFmBzWc7Q6qP-TetDgZaG8A=/objOMh0mj-   > |   |-- oTAUzOt5YoQAyThw89eSgWuig-0=-   > |   |   |-- .label (=bob's label)-   > |   |   |-- objFIQCIm-   > |   |   '-- objtsePnc-   > |   |       '-- secret -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objFIQCIm-   > |   '-- wordEFmBzWc7Q6qP-TetDgZaG8A=-   > |       |-- .label (=clarice's label)-   > |       '-- objOMh0mj-   > '-- ROOT -> .obj/jX7q5Kb8_G4GsjgNpOHB17kypQo=/objTj5JZD-   >--   Observe that every directory object contains symbolic links-   pointing to file or directory objects in the store.--   Accessing any file or directory in the \"friendly\" view requires-   a lookup ('lookupObjPath') of the corresponding object. Each-   path is, however, relative to the root. So, for example,-   looking up @\/aliceOrbob\/bob\/@ actually corresponds to looking-   up @\/lioFS\/ROOT\/aliceOrbob\/bob\/@. This prevents untrusted code-   from accessing objects by guessing filenames and further allows-   untrusted code to pick arbitrary filenames (including @.label@,-   @.obj@, etc.).--   Several precautions are taken to keep the filesystem in a working-   state in case of a crash.  The code tries to maintain the invariant-   that any inconsistencies will either be:--     1. temporary files or directories whose names start with the-        \"@#@\" character, or--     2.  dangling symbolic links.--   Both of these inconsistencies can be checked and cleaned up-   locally without examining the whole file system.  The code tries-   to fix up these inconsistencies on-the-fly as it encounters them.-   However, it could possibly leave some stranded temporary-   @.label@ files. ---}---module LIO.FS ( evalWithRoot-              -- * Creating and finding (labeled) objects-              , lookupObjPath, lookupObjPathP-              , getObjLabelTCB-              , createFileTCB, createDirectoryTCB-              -- * Labeled 'FilePath'-              , LFilePath, labelOfFilePath-              , unlabelFilePath-              , unlabelFilePathP-              , unlabelFilePathTCB-              -- * Misc helper functions-              , cleanUpPath, stripSlash-              ) where---import Prelude hiding (catch)-import LIO.TCB -import Control.Monad (unless)-import System.FilePath-import System.Posix.Files-import System.Directory-import Control.Exception (Exception)-import qualified Control.Exception as E-import qualified Data.ByteString as B-import qualified Data.ByteString.Lazy as LB-import qualified Data.ByteString.Char8 as C-import Data.Serialize-import Data.IORef-import Data.Functor-import Data.Tuple (swap)-import Data.Foldable (foldlM)-import Data.Typeable-import Data.List (isPrefixOf)-import System.IO.Unsafe-import System.IO-import qualified System.IO.Error as IOError--import qualified Data.ByteString.Base64.URL as Codec-import qualified Data.Digest.Pure.SHA as SHA--#if __GLASGOW_HASKELL__ >= 706-import System.Posix.Temp -#else--- Patch to unix package will not be up on Hackage until GHC 7.6, so--- we include the implementation with LIO until this is the case-import System.Posix.Tmp -#endif-------- Filesystem root-------- | Root of labeled filesystem.-rootDir :: IORef FilePath-{-# NOINLINE rootDir #-}-rootDir = unsafePerformIO $ newIORef undefined--getRootDir :: IO FilePath-getRootDir = readIORef rootDir---- | Temporary files have the prefix \'#\'.-tmpPrefix :: FilePath-tmpPrefix = "#"---- | Prefix of object filenames.-objPrefix :: FilePath-objPrefix = "obj"---- | Shadow directory containing the actual FS objects.-objDir :: FilePath-objDir = ".obj"---- | We need to serialize the label in each label directory.-labelFile :: FilePath-labelFile = ".label"---- | Root of the filesystem.-rootLink :: FilePath-rootLink = "ROOT"---- | Magic file. Last file created when the the filesystem is--- initially created. If the magic file is invalid, then it is likely--- that a failure occured in the set up process.-magicFile :: FilePath-magicFile = ".magic"---- | Content written to magic file. -magicContent :: B.ByteString-magicContent = B.pack  [ 0x7f, 0x45, 0x4c, 0x46, 0x01-                       , 0x01, 0x01, 0x00, 0x00, 0x00-                       , 0x00, 0x00, 0x00, 0x00, 0x00-                       , 0x00, 0xde, 0xad, 0xbe, 0xef]---- | Filesystem errors-data FSErr = FSRootCorrupt -- ^ Root structure is corrupt-           | FSRootInvalid -- ^ Root is invalid (must be absolute).-      deriving Typeable--instance Exception FSErr--instance Show FSErr where-  show FSRootCorrupt = "Root structure is corrupt"-  show FSRootInvalid = "Root is invalid (must be absolute)"-  ---- | 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, then 'lbot' is used as the--- root label.-evalWithRoot :: (Serialize l, LabelState l p s)-            => FilePath    -- ^ Filesystem root-            -> Maybe l     -- ^ Label of root-            -> LIO l p s a -- ^ LIO action-            -> s           -- ^ Initial state-            -> IO (a, l)-evalWithRoot path ml act s = setRootOrInitFS >> evalLIO act s-  where setRootOrInitFS = do-          unless (isAbsolute path) $ throwIO FSRootInvalid-          exists <- doesDirectoryExist path-          let l = maybe lbot id ml-          if exists-            then checkFS path-            else initFS l path---- | Initialize the filesystem with a given label and root file path.-initFS :: (Label l, Serialize l)-       => l             -- ^ Label of root-       -> FilePath      -- ^ Path to the filesystem root-       -> IO ()-initFS l path = do-  unless (isAbsolute path) $ throwIO FSRootInvalid-  -- Create root of filesystem-  createDirectory path-  -- Create the shadow object store-  createDirectory (path </> objDir)-    `onException` (removeDirectory path)-  -- Set the root filesystem:-  writeIORef rootDir path-  rootObj <- newDirObj l-  linkRoot rootObj-  -- Create magic file:-  B.writeFile (path </> magicFile) magicContent---- | Check the filesystem structure.-checkFS :: FilePath -> IO ()-checkFS path = do-  -- check that the ROOT link exists-  rootStat <- getSymbolicLinkStatus $ path </> rootLink-  unless (isSymbolicLink rootStat) $ throwIO FSRootCorrupt-  -- find obj dir:-  hasObjDir <- doesDirectoryExist $ path </> objDir-  unless hasObjDir $ throwIO FSRootCorrupt-  -- check magic file:-  magicOK <- (B.readFile (path </> magicFile) >>= \c -> return (c==magicContent))-               `catchIO` (return False)-  unless magicOK $ throwIO FSRootCorrupt-  writeIORef rootDir path-------- Objects--- ---- | Encoding of a label into a filepath. We need to take the hash--- of a label (as opposed to e.g. just 64-base encoding of the label)--- in order to keep the filename lengths to a reasonable size.-encodeLabel :: (Serialize l, Label l) => l -> FilePath-encodeLabel l = enc . SHA.bytestringDigest . SHA.sha1 $ encodeLazy l-  where enc = C.unpack . Codec.encode . B.concat . LB.toChunks---- | An object can be a directory or a file.-data Object  = DirObj  FilePath         -- ^ Directory object-             | FileObj Handle FilePath  -- ^ File object-             deriving (Eq, Show)---- | A wrapper for a new, not yet commited, object.-newtype NewObject = New Object-              deriving (Eq, Show)---- | Create a new directory object with a given label.-newDirObj :: (Serialize l, Label l) => l -> IO NewObject-newDirObj l = newObj l $ \p -> (New . DirObj) <$> mkTmpObjDir p---- | Create a new file object with a given label and 'IOMode'.-newFileObj :: (Serialize l, Label l) => l -> IOMode -> IO NewObject-newFileObj l m = newObj l $ \p -> (New . uncurry FileObj) <$> mkTmpObjFile m p---- | Create a new temporary unique object directory. The function retries if--- there exists an object with the same name but no 'tmpPrefix'.-mkTmpObjDir :: FilePath -> IO FilePath-mkTmpObjDir path = do-  dir <- mkdtemp $ path </> (tmpPrefix ++ objPrefix) -  exists <- doesDirectoryExist (rmTmpPrefix dir)-  if exists-    then do ignoreErr $ removeDirectory dir-            mkTmpObjDir path-    else return dir----- | Create a new temporary unique object file. The function retries if--- there exists an object with the same name but no 'tmpPrefix'.-mkTmpObjFile :: IOMode -> FilePath -> IO (Handle, FilePath)-mkTmpObjFile mode path = do-  res@(file, h) <- mkstemp $ path </> (tmpPrefix ++ objPrefix)-  exists <- doesFileExist (rmTmpPrefix file)-  if exists-    then do hClose h -            ignoreErr $ removeFile file-            mkTmpObjFile mode path-    else return . swap $ res---- | Create a new file or directory object (given the make temporary--- object functino). For example, we can create a new file object as:------ > newDirObj l = newObj l $ \p -> (New . DirObj) <$> mkTmpObjDir p------ or a new directory object as------ > newFileObj l m = newObj l $ \p ->--- >                    (New . uncurry FileObj) <$> mkTmpObjFile m p)--- -newObj :: (Serialize l, Label l)-       => l                           -- ^ Label of object-       -> (FilePath -> IO NewObject)  -- ^ Object creation function-       -> IO NewObject-newObj l mkFunc = getLabelDir l >>= mkFunc---- | Create the label directory (and corresponding 'labelFile') in 'objDir'.-getLabelDir :: (Serialize l, Label l) => l -> IO FilePath-getLabelDir l = do-  oRoot <- (</> objDir) <$> getRootDir-  let dir = oRoot </> encodeLabel l-  createDirectoryIfMissing True dir-  createLabelFileIfMissing dir l-  return dir---- | This function creates a 'labelFile' for the given label--- directory.  It also verifies that the label in the file is the--- same as the given label (as another thread might have created the--- file, or a previous write might have corrupted the file). If the--- file is invalid, it removes the existing label file and writes--- the given label. An assumption made here is that there is a 1-to-1--- correspondence between a label and its encoding (i.e., 'encodeLabel'--- is a bijection).-createLabelFileIfMissing :: (Serialize l, Label l) => FilePath -> l ->  IO ()-createLabelFileIfMissing dir l = do-  let file = dir </> labelFile-  exists <- doesFileExist file-  unless exists $ createLabelFile file-  -- It's possible for another thread to have created the file, and so-  -- we need to make sure that we agree on the label:-  valid <- checkLabelFile file-  unless valid $ (ignoreErr $ removeFile file) >> createLabelFileIfMissing dir l-    where createLabelFile file = do-            (h,f) <- mkTmpObjFile WriteMode dir-            C.hPutStr h (encode l)-            hClose h-            rename f file `E.catch` (\e -> -              removeFile f >> unless (IOError.isAlreadyExistsError e) (throwIO e))-          checkLabelFile file = do-            c <- B.readFile file-            case decode c of-              Left _   -> return False-              Right l' -> return (l == l')----- | Link the 'rootLink' to an object directory.-linkRoot :: NewObject -> IO ()-linkRoot newO@(New o) = do-  root <- getRootDir-  newObjPath <- case o of-                  DirObj p -> return p-                  _        -> throwIO . userError $ "Root must be a directory."-  let objPath = rmTmpPrefix newObjPath-  let name = root </> rootLink-  createSymbolicLink (objPath `rmPrefixDir` root) name-    `onException` (cleanUpNewObj newO)-  rename newObjPath objPath `onException` (do ignoreErr $ removeFile name-                                              cleanUpNewObj newO)---- | Link without returning object.-linkObj_ :: FilePath -> NewObject -> IO ()-linkObj_ f n = linkObj f n >> return ()----- | Link a filepath to an object.-linkObj :: FilePath -> NewObject -> IO Object-linkObj name' newO@(New o) = do-  root <- getRootDir-  let newObjPath = case o of-                     DirObj p    -> p-                     FileObj _ p -> p-      objPath = rmTmpPrefix newObjPath-  let name = root </>  rootLink </> name'-      relObjPath = (".." </> ".." </> (objPath `rmPrefixDir` (root </> objDir)))-  createSymbolicLink relObjPath name `onException` (cleanUpNewObj newO)-  rename newObjPath objPath `onException` (do ignoreErr $ removeFile name-                                              cleanUpNewObj newO)-  return $ case o of-             DirObj _    -> DirObj objPath-             FileObj h _ -> FileObj h objPath---- | It's possible that either a program crashed before renaming a--- 'NewObject' into a 'Object', or that another thread is calling--- 'linkObj' and for some reason is being slow between the--- 'createSymbolicLink' and 'rename' calls.  Either way it should be--- fine for us just to 'rename' the 'NewObject', because the link to--- the object would not exist if the 'NewObject' were not ready to be--- renamed. This function is primarily used when traversing the--- filesystem tree with 'pathTaintTCB'.-fixObjLink :: FilePath -> IO ()-fixObjLink f = do-  exists <- catchIO (getFileStatus f >> return True) (return False)-  unless exists $ ignoreErr $ rename (tmpPrefix ++ f) f---- | Clean up a newly created object. If the object is a temporary--- directory, remove it. If it's a file, close the handle, and remove--- the file.-cleanUpNewObj :: NewObject -> IO ()-cleanUpNewObj (New o) = ignoreErr $ case o of -                                      DirObj p -> removeDirectory p-                                      FileObj h p -> hClose h >> removeFile p---- | 'Label' associated with a 'FilePath'.-newtype LFilePath l = LFilePathTCB (Labeled l FilePath)---- | Get the label of a labeled  filepath.-labelOfFilePath :: Label l =>  LFilePath l -> l-labelOfFilePath (LFilePathTCB x) = labelOf x---- | Trusted version of 'unlabelFilePath' that ignores IFC.-unlabelFilePathTCB :: (Label l) => LFilePath l -> FilePath-unlabelFilePathTCB (LFilePathTCB l) = unlabelTCB l---- | Same as 'unlabelFilePath' but uses privileges to unlabel the--- filepath.-unlabelFilePathP :: (LabelState l p s)-                 => p -> LFilePath l -> LIO l p s FilePath-unlabelFilePathP p' (LFilePathTCB l) = withCombinedPrivs p' $ \p -> unlabelP p l---- | Unlabel a filepath. If the path corresponds to a directory, you--- can now get the contents of the directory; if it's a file, you can--- open the file.-unlabelFilePath :: LabelState l p s-                 => LFilePath l -> LIO l p s FilePath-unlabelFilePath = unlabelFilePathP noPrivs---- | Given a pathname (forced to be relative to the root of the--- labeled filesystem), find the path to the corresponding object.--- The current label is raised to reflect all the directories traversed.--- Note that if the object 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.------ Additionally, 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@.-lookupObjPath :: (LabelState l p s, Serialize l)-              => FilePath  -- ^ Path to object-              -> LIO l p s (LFilePath l)-lookupObjPath = lookupObjPathP noPrivs---- | Same as 'lookupObjPath' but takes an additional privilege object--- that is exercised when raising the current label.-lookupObjPathP :: (LabelState l p s, Serialize l)-               => p         -- ^ Privilege -               -> FilePath  -- ^ Path to object-               -> LIO l p s (LFilePath l)-lookupObjPathP p' f' = withCombinedPrivs p' $ \p -> do-  f <- cleanUpPath f'-  root <- ioTCB $ getRootDir-  pathTaintTCB p root rootLink-  let dirs = splitDirectories f-  dir <- foldlM (\a b ->  pathTaintTCB p a b >> return (a </> b))-                (root </> rootLink)-                (safeinit dirs)-  let objPath = (dir </> safelast dirs)-  l <- getObjLabelTCB objPath-  return . LFilePathTCB $ labelTCB l objPath-    where safelast [] = ""-          safelast x  = last x----- | Read the label file of an object. Note that because the format--- of the supplied path is not checked this function is considered to--- be in the @TCB@.-getObjLabelTCB :: (Serialize l, LabelState l p s) => FilePath -> LIO l p s l-getObjLabelTCB objPath = rtioTCB $ do-  root <- getRootDir-  symLink <- readSymbolicLink objPath-  let absObjPath = root </> objDir </>-                      ((symLink `rmPrefixDir` (".." </> ".."))-                                `rmPrefixDir` objDir)-  lS  <- C.readFile $ (takeDirectory absObjPath) </> labelFile-  case decode lS of-    Left _  -> throwIO . userError $ "Invalid label file."-    Right l ->  return l ---- | Given a privilege, root-path prefix and a directory/file within--- the prefix, read the 'labelFile' of the root-path prefix, raising--- the current label to reflect this. This function is used to taint --- a process that traverses a filesystem tree. The function is @TCB@--- because we do not check any properties of the root -- it is--- primarily used by 'lookupObjPathP'.-pathTaintTCB :: (Serialize l, LabelState l p s)-              => p -> FilePath -> FilePath -> LIO l p s ()-pathTaintTCB p root f' = do-  let f = stripSlash f'-  rootL <- rtioTCB $ readSymbolicLink (root </> f)-  let objPath = root </> rootL-  ioTCB $ fixObjLink objPath-  lS <- rtioTCB $ C.readFile (objPath </> ".." </> labelFile)-  case decode lS of-    Left _ -> throwIO . userError $ "Invalid label file."-    Right l -> taintP p l---- | 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 :: LabelState l p s => FilePath -> LIO l p s FilePath -cleanUpPath f = rtioTCB $ doit $ splitDirectories . normalise . stripSlash $ f-  where doit []          = return []-        doit ("..":[])   = return "/"-        doit ("..":_)    = throwIO $ IOError.mkIOError IOError.doesNotExistErrorType-                              "Illegal filename" Nothing (Just ".." )-        doit (_:"..":xs) = doit xs-        doit (".":xs)    = doit xs-        doit (x:xs)      = (x </>) <$> doit xs-  ------- Creating and linking directory and file objects------- | Create a directory object with the given label and link the--- supplied path to the object.-createDirectoryTCB :: (Serialize l, Label l) => l -> FilePath -> IO ()-createDirectoryTCB l p = do-  obj <- newDirObj l-  linkObj_ p obj---- | Create a file object with the given label and link the--- supplied path to the object. The handle to the file is returned.-createFileTCB :: (Serialize l, Label l) => l -> FilePath -> IOMode -> IO Handle-createFileTCB l p m = do-  obj <- newFileObj l m-  (FileObj h _) <- linkObj p obj-  return h--------- Helper functions------- | Remove the prefix from a list (usually 'FilePath').-rmPrefix :: Eq a => [a] -- ^ String-                 -> [a] -- ^ Prefix-                 -> [a]-rmPrefix s pre = if pre `isPrefixOf` s-                   then drop (length pre) s-                   else s---- | Remove the 'tmpPrefix' prefix from a file or directory.-rmTmpPrefix :: FilePath -> FilePath-rmTmpPrefix path =-  let ds = splitDirectories path-  in (joinPath $ safeinit ds) -     </> ((last ds) `rmPrefix` tmpPrefix)----- | @rmPrefixDir path prefix@ removes @prefix@ from @path@.-rmPrefixDir :: FilePath -> FilePath -> FilePath-rmPrefixDir path prefix = -  if prefix `isPrefixOf` path-    then let p = splitDirectories path-             x = splitDirectories prefix-         in joinPath $ drop (length x) p-    else path---- | Ignore 'IOException's.-ignoreErr :: IO () -> IO ()-ignoreErr m = catchIO m (return ())---- | Same as 'catch', but only catches 'IOException's.-catchIO :: IO a -> IO a -> IO a-catchIO a h = E.catch a ((const :: a -> E.IOException -> a) h)---- | Same as 'init', but does not crash on empty list.-safeinit :: [a] -> [a]-safeinit [] = []-safeinit x  = init x

@@ -0,0 +1,267 @@+{-# 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           Prelude hiding (catch)++import           Data.Serialize+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           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, Serialize 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 `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 . encodeLazy++-- | 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 = decodeLazy . 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 `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 })

@@ -0,0 +1,97 @@+{-# 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,342 +1,549 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702 {-# LANGUAGE Trustworthy #-}-#endif-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FunctionalDependencies #-}+{-# LANGUAGE ConstraintKinds,+             FlexibleInstances,+             FlexibleContexts,+             TypeSynonymInstances,+             MultiParamTypeClasses #-}+{- |  --- | This module abstracts the basic 'FileHandle' methods provided by--- the system library, and provides an 'LHandle' ('Labeled' 'Handle')--- type that can be manipulated from within the 'LIO' Monad.--- (There is no notion of changeable current working directory in--- the 'LIO' Monad, nor symbolic links.)------ The actual storage of labeled files is handled by the "LIO.FS"--- module.------ /IMPORTANT:/ To use a labeled filesystem you must use 'evalWithRoot',--- otherwise any actions built using the combinators of this module will--- crash.------ An example use is 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 @/@.-module LIO.Handle (-                  -- * LIO with filesystem support-                    evalWithRoot-                  -- * Generic Handle operations-                  , DirectoryOps(..)-                  , CloseOps(..)-                  , HandleOps(..)-                  , readFile, writeFile, writeFileL+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(..)-                  -- * LIO Handle-                  , LHandle, labelOfHandle -                  -- ** Privileged combinators-                  , getDirectoryContentsP-                  , createDirectoryP-                  , openFileP-                  , hCloseP-                  , hFlushP +                  , BufferMode(..)+                    -- * File operations+                  , openFile, openFileP+                  , hClose, hCloseP+                  , hFlush, hFlushP+                  , HandleOps(..)                   , hGetP                   , hGetNonBlockingP                   , hGetContentsP+                  , hGetLineP                   , hPutP                   , hPutStrP                   , hPutStrLnP-                  , readFileP, writeFileP, writeFileLP+                  -- ** 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 --#if __GLASGOW_HASKELL__ >= 702-import safe Prelude hiding (catch, readFile, writeFile)-import safe System.IO (IOMode(..))-import safe qualified System.IO as IO-#else import Prelude hiding (catch, readFile, writeFile)-import System.IO (IOMode(..))-import qualified System.IO as IO-#endif -import LIO.TCB-import LIO.FS-import Data.Serialize-import qualified System.Directory as IO-import System.FilePath-import qualified Data.ByteString.Lazy as L-import qualified Data.ByteString.Lazy.Char8 as LC+import           Data.Serialize+import qualified Data.ByteString.Char8 as S8+import qualified Data.ByteString.Lazy.Char8 as L8 +import           Control.Monad+import           Control.Exception (throwIO) --- | Class used to abstract reading and creating directories, and--- opening (possibly creating) files.-class (Monad m) => DirectoryOps h m | m -> h where-  -- | Get the contents of a directory.-  getDirectoryContents :: FilePath -> m [FilePath]-  -- | Create a directory at the supplied path.-  -- The LIO instance labels the directory with the current label.-  createDirectory      :: FilePath -> m ()-  -- | Open handle to manage the file at the supplied path.-  openFile             :: FilePath -> IOMode -> m h --- | Class used to abstract close and flush operations on handles.-class (Monad m) => CloseOps h m where-  hClose :: h -> m ()-  hFlush :: h -> m ()+import           System.IO (IOMode(..), BufferMode(..), Handle)+import qualified System.IO as IO+import qualified System.Directory as IO+import           System.FilePath --- | Class used to abstract reading and writing from and to handles,--- respectively.-class (CloseOps h m) => HandleOps h b m where-  hGet            :: h -> Int -> m b-  hGetNonBlocking :: h -> Int -> m b-  hGetContents    :: h -> m b-  hPut            :: h -> b -> m ()-  hPutStr         :: h -> b -> m ()-  hPutStr         = hPut-  hPutStrLn       :: h -> b -> m ()+import           LIO+import           LIO.Labeled.TCB+import           LIO.TCB+import           LIO.FS.TCB  ----- Standard IO Handle Operations+-- LIO related -- -instance DirectoryOps IO.Handle IO where-  getDirectoryContents = IO.getDirectoryContents-  createDirectory      = IO.createDirectory-  openFile             = IO.openBinaryFile+-- | Serialize 'MonadLIO'+type SMonadLIO l m = (SLabel l, MonadLIO l m) -instance CloseOps IO.Handle IO where-  hClose = IO.hClose-  hFlush = IO.hFlush -instance HandleOps IO.Handle L.ByteString IO where-  hGet            = L.hGet-  hGetNonBlocking = L.hGetNonBlocking-  hGetContents    = L.hGetContents-  hPut            = L.hPut-  hPutStrLn       = LC.hPutStrLn+-- | 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 -- --- | A labeled handle.-data LHandle l = LHandleTCB l IO.Handle---- | Get the label of a labeled handle.-labelOfHandle :: Label l => LHandle l -> l-labelOfHandle (LHandleTCB l _) = l--instance (Serialize l, LabelState l p s)-          => DirectoryOps (LHandle l) (LIO l p s) where-  getDirectoryContents = getDirectoryContentsP noPrivs-  createDirectory  f   = do l <- getLabel -                            createDirectoryP noPrivs l f-  openFile f m         = do l <- getLabel -                            openFileP noPrivs (Just l) f m+-- | 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 --- | 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 (of course, using privileges to--- keep the current label unchanged when possible). Note that, unlike--- the standard Haskell 'getDirectoryContents', we first normalise the--- path by collapsing all the @..@'s. (The LIO filesystem does not--- support links.)-getDirectoryContentsP :: (LabelState l p s, Serialize l)+-- | Same as 'getDirectoryContents', but uses privileges when raising+-- the current label.+getDirectoryContentsP :: (SMonadLIO l m, Priv l p)                       => p              -- ^ Privilege                       -> FilePath       -- ^ Directory-                      -> LIO l p s [FilePath]-getDirectoryContentsP p' dir = withCombinedPrivs p' $ \p -> do-  path <- lookupObjPathP p dir >>= unlabelFilePathP p-  rtioTCB $ IO.getDirectoryContents path+                      -> 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 current label (after traversing the filesystem to the--- directory path) must flow to the supplied label which in turn must--- flow to the current label (of course, using privileges to bypass--- certain restrictions). If this information flow restriction is--- satisfied, the directory is created.-createDirectoryP :: (LabelState l p s, Serialize l)+-- | 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-                 -> LIO l p s ()-createDirectoryP p ldir path' = withCombinedPrivs p $ \priv -> do-  path <- cleanUpPath path'-  aguardP priv ldir-  lcDir <- lookupObjPathP priv (containingDir path)-  wguardP priv $ labelOfFilePath lcDir-  rtioTCB $ createDirectoryTCB ldir path-    where stripLastSlash = (reverse . stripSlash . reverse)-          containingDir = takeDirectory . ([pathSeparator] </>)-                                        .  stripLastSlash+                 -> 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+-- --- | Given a set of privileges, a new (maybe) label of a file, a filepath--- and the handle 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 --- (of course, using privileges to minimize the taint). Additionally the--- label of the file (new or existing) must be between the current label--- and clearance. If the file is created, it is further required that the --- current process be able to write to the containing directory.-openFileP :: (LabelState l p s, Serialize l)+-- 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 of handle-          -> LIO l p s (LHandle l)-openFileP p mlfile path' mode = withCombinedPrivs p $ \priv -> do-  path <- cleanUpPath path'-  let containingDir = takeDirectory path-      fileName      = takeFileName  path-  -- check that the supplied label is bounded by current label and clearance:-  maybe (return ()) (aguardP priv) mlfile-  -- lookup object corresponding to containing dir:-  lcDir <- lookupObjPathP priv containingDir -  -- unlabel the containing dir object:-  actualCDir <- unlabelFilePathP priv lcDir  -  let objPath = actualCDir </> fileName -- actual object path-  exists <- rtioTCB $ IO.doesFileExist objPath+          -> 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 l <- getObjLabelTCB objPath -- label of object-             aguardP priv l -- make sure we can actually read the file-             -- NOTE: if mode == ReadMode, we might want to instead do-             -- aguardP priv (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 <- rtioTCB $ IO.openFile objPath mode-             return $ LHandleTCB l h-     else case mlfile of-           Nothing -> throwIO $ userError "openFileP: File label missing."+     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-             wguardP priv (labelOfFilePath lcDir) -- can write to containing dir-             aguardP priv l -- make sure we can actually read the file-             -- NOTE: the latter is necessary as looking up the containing-             -- directory object might have raised the current label.-             h <- ioTCB $ createFileTCB l objPath mode-             return $ LHandleTCB l h-            --instance (LabelState l p s) => CloseOps (LHandle l) (LIO l p s) where-  hClose = hCloseP noPrivs-  hFlush = hFlushP noPrivs+             -- 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 -instance (LabelState l p s, CloseOps (LHandle l) (LIO l p s)-         , HandleOps IO.Handle b IO) =>-           HandleOps (LHandle l) b (LIO l p s) where-  hGet            = hGetP noPrivs-  hGetNonBlocking = hGetNonBlockingP noPrivs-  hGetContents    = hGetContentsP noPrivs-  hPut            = hPutP noPrivs-  hPutStrLn       = hPutStrLnP noPrivs+-- | 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 :: (LabelState l p s) => p -> LHandle l -> LIO l p s ()-hCloseP p' (LHandleTCB l h) = withCombinedPrivs p' $ \p ->-  wguardP p l >> rtioTCB (hClose h)+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 :: (LabelState l p s) => p -> LHandle l -> LIO l p s ()-hFlushP p' (LHandleTCB l h) = withCombinedPrivs p' $ \p ->-  wguardP p l >> rtioTCB (hFlush h)+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 :: (LabelState l p s, HandleOps IO.Handle b IO)-      => p              -- ^ Privileges-      -> LHandle l      -- ^ Labeled handle-      -> Int            -- ^ Number of bytes to read-      -> LIO l p s b-hGetP p' (LHandleTCB l h) n = withCombinedPrivs p' $ \p ->-  wguardP p l >> rtioTCB (hGet h n)+hGetP :: (Priv l p, Serialize 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 :: (LabelState l p s, HandleOps IO.Handle b IO)-                 => p -> LHandle l -> Int -> LIO l p s b-hGetNonBlockingP p' (LHandleTCB l h) n = withCombinedPrivs p' $ \p ->-  wguardP p l >> rtioTCB (hGetNonBlocking h n)+hGetNonBlockingP :: (Priv l p, Serialize 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 :: (LabelState l p s, HandleOps IO.Handle b IO)-              => p -> LHandle l -> LIO l p s b-hGetContentsP p' (LHandleTCB l h) = withCombinedPrivs p' $ \p ->-  wguardP p l >> rtioTCB (hGetContents h)+hGetContentsP :: (Priv l p, Serialize 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, Serialize 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 :: (LabelState l p s, HandleOps IO.Handle b IO)-      => p -> LHandle l -> b -> LIO l p s ()-hPutP p' (LHandleTCB l h) s = withCombinedPrivs p' $ \p ->-  wguardP p l >> rtioTCB (hPut h s)+hPutP :: (Priv l p, Serialize 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 :: (LabelState l p s, HandleOps IO.Handle b IO)-          => p -> LHandle l -> b -> LIO l p s ()+hPutStrP :: (Priv l p, Serialize 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 :: (LabelState l p s, HandleOps IO.Handle b IO)-            => p -> LHandle l -> b -> LIO l p s ()-hPutStrLnP p' (LHandleTCB l h) s = withCombinedPrivs p' $ \p ->-  wguardP p l >> rtioTCB (hPutStrLn h s)+hPutStrLnP :: (Priv l p, Serialize 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 (Byte)String.-readFile :: (DirectoryOps h m, HandleOps h b m) => FilePath -> m b-readFile path = openFile path ReadMode >>= hGetContents---- | Write a (Byte)String to a file.-writeFile :: (DirectoryOps h m, HandleOps h b m, OnExceptionTCB m)-          => FilePath -> b -> m ()-writeFile path contents = bracketTCB (openFile path WriteMode) hClose-                          (flip hPut contents)+-- | 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 IO.Handle b IO, LabelState l p s, Serialize l) =>-             p -> FilePath -> LIO l p s b-readFileP p' path =  withCombinedPrivs p' $ \p ->-  openFileP p Nothing path ReadMode >>= hGetContentsP p+readFileP :: (HandleOps Handle b IO, Priv l p, Serialize l)+          => p -> FilePath -> LIO l b+readFileP p file = openFileP p Nothing file ReadMode >>= hGetContentsP p --- | Same as 'writeFile' but uses privilege in opening the file.-writeFileP  :: (HandleOps IO.Handle b IO, LabelState l p s, Serialize l) =>-               p -> FilePath -> b -> LIO l p s ()-writeFileP p' path contents = withCombinedPrivs p' $ \privs -> do-  l <- getLabel-  bracketTCB (openFileP privs (Just l) path WriteMode) (hCloseP privs)-             (flip (hPutP privs) contents)+-- | 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 also takes the label of the file.-writeFileL  :: (HandleOps IO.Handle b IO, LabelState l p s, Serialize l) =>-               l -> FilePath -> b -> LIO l p s ()-writeFileL = writeFileLP noPrivs+-- | Same as 'writeFile' but uses privilege when opening, writing and+-- closing the file.+writeFileP  :: (HandleOps Handle b IO, Priv l p, Serialize 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) --- | Same as 'writeFileL' but uses privilege in opening the file.-writeFileLP  :: (HandleOps IO.Handle b IO, LabelState l p s, Serialize l) =>-               p -> l -> FilePath -> b -> LIO l p s ()-writeFileLP p' l path contents = withCombinedPrivs p' $ \privs -> do-  bracketTCB (openFileP privs (Just l) path WriteMode) (hCloseP privs)-             (flip (hPutP privs) 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

@@ -1,13 +1,139 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Safe #-}-#endif--- |This module implements labeled IORefs.  The interface is analogous--- to "Data.IORef", but the operations take place in the LIO monad.--- (See "LIO.LIORef.TCB" for documentation.)--- Moreover, reading the LIORef calls taint, while writing it calls--- aguard. This module exports only the safe subset (non TCB) of the--- @LIORef@ module -- trusted code can import "LIO.LIORef.TCB".-module LIO.LIORef ( module LIO.LIORef.Safe) where+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE ConstraintKinds,+             FlexibleContexts #-} -import LIO.LIORef.Safe+{- |++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+restricted according to the label. This module is analogous to+"Data.IORef", but the operations take place in the 'LIO' monad.++-}+++module LIO.LIORef (+    LIORef+  -- * Basic Functions+  -- ** Create labeled 'IORef's+  , newLIORef, newLIORefP+  -- ** Read 'LIORef's+  , readLIORef, readLIORefP+  -- ** Write 'LIORef's+  , writeLIORef, writeLIORefP+  -- ** Modify 'LIORef's+  , modifyLIORef, modifyLIORefP+  , atomicModifyLIORef, atomicModifyLIORefP+  ) where++import           LIO+import           LIO.LIORef.TCB++--+-- Create labeled 'IORef's+--++-- | 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+          => l                  -- ^ Label of reference+          -> a                  -- ^ Initial value+          -> m (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++--+-- Read 'LIORef's+--++-- | Read the value of a labeled reference. A read succeeds only if the+-- label of the reference is below the current clearance. Moreover,+-- 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++-- | 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++--+-- Write 'LIORef's+--++-- | Write a new value into a labeled reference. A write succeeds if+-- 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++-- | 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++--+-- Modify 'LIORef's+--++-- | Mutate the contents of a labeled reference. For the mutation to+-- succeed it must be that the current label can flow to the label of the+-- reference, and the label of the reference can flow to the current+-- clearance. Note that because a modifier is provided, the reference+-- contents are not observable by the outer computation and so it is not+-- required that the current label be raised. It is, however, required+-- that the label of the reference be bounded by the current label and+-- clearance (as checked by the underlying 'guardAlloc' guard).+modifyLIORef :: Label l+             =>  LIORef l a            -- ^ Labeled reference+             -> (a -> a)               -- ^ Modifier+             -> LIO l ()+modifyLIORef = modifyLIORefP NoPrivs++-- | 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++-- | Atomically modifies the contents of an 'LIORef'. It is required+-- that the label of the reference be above the current label, but+-- below the current clearance. Moreover, since this function can be+-- used to directly read the value of the stored reference, the+-- computation is \"tainted\" by the reference label (i.e., the+-- current label is raised to the 'join' of the current and reference+-- 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++-- | 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

@@ -1,19 +0,0 @@-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)-{-# LANGUAGE Trustworthy #-}-#endif---- |This module exports the safe subset of the "LIO.LIORef.TCB" module.--- It is important that untrusted code be limited to this subset; information--- flow can easily be violated if the TCB functions are exported.-module LIO.LIORef.Safe ( module LIO.LIORef.TCB ) where-import LIO.LIORef.TCB ( LIORef-                      , newLIORef, labelOfLIORef-                      , readLIORef, writeLIORef-                      , modifyLIORef-                      , atomicModifyLIORef-                      , newLIORefP-                      , readLIORefP, writeLIORefP-                      , modifyLIORefP-                      , atomicModifyLIORefP-                      )

@@ -1,162 +1,94 @@-{-# LANGUAGE CPP #-}-#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702) && (__GLASGOW_HASKELL__ < 704)-{-# LANGUAGE SafeImports #-}-#endif-#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 704) {-# LANGUAGE Unsafe #-}-#endif--- |This module implements labeled IORefs.  The interface is analogous--- to "Data.IORef", but the operations take place in the LIO monad.-module LIO.LIORef.TCB (-- * Basic Functions-                        LIORef-                      , newLIORef, labelOfLIORef-                      , readLIORef, writeLIORef-                      , modifyLIORef-                      , atomicModifyLIORef-                      -- * Privileged Functions-                      , newLIORefP-                      , readLIORefP, writeLIORefP-                      , modifyLIORefP-                      , atomicModifyLIORefP-                      -- * Unsafe (TCB) Functions-                      , newLIORefTCB-                      , readLIORefTCB, writeLIORefTCB-                      , modifyLIORefTCB-                      , atomicModifyLIORefTCB-                      ) where+{- | -import LIO.TCB+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". -#if defined(__GLASGOW_HASKELL__) && (__GLASGOW_HASKELL__ >= 702)-import safe Data.IORef-#else-import Data.IORef-#endif +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. --- | An @LIORef@ is an @IORef@ with an associated, static label. --- The restriction of an immutable label come from the fact that it--- is possible to leak information  through the label itself.--- Hence, LIO is /flow-insensitive/. Of course, you can create an--- @LIORef@ of 'Labeled' to get a limited form of flow-sensitivity.-data LIORef l a = LIORefTCB l (IORef a)+-}+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 --- | 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 :: (LabelState l p s)-           => p -> l -> a -> LIO l p s (LIORef l a)-newLIORefP p' l a = withCombinedPrivs p' $ \p -> do-  aguardP p l-  ior <- rtioTCB $ newIORef a-  return $ LIORefTCB l ior --- | 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.-newLIORef :: (LabelState l p s)-          => l                      -- ^ Label of reference-          -> a                      -- ^ Initial value-          -> LIO l p s (LIORef l a) -- ^ Mutable reference-newLIORef l x = getPrivileges >>= \p -> newLIORefP p l x+-- | 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.+                            } --- | Trusted constructor that creates labeled references.-newLIORefTCB :: (LabelState l p s) => l -> a -> LIO l p s (LIORef l a)-newLIORefTCB l a = do-  ior <- rtioTCB $ newIORef a-  return $ LIORefTCB l ior+-- | Get the label of an 'LIORef'.+instance LabelOf LIORef where+  labelOf = labelOfLIORef --- | Get the label of a reference.-labelOfLIORef :: (Label l) => LIORef l a -> l-labelOfLIORef (LIORefTCB l _) = l+--+-- Create labeled 'IORef's+-- --- | Same as 'readLIORef' except @readLIORefP@ takes a privilege object--- which is used when the current label is raised.-readLIORefP :: (LabelState l p s) => p -> LIORef l a -> LIO l p s a-readLIORefP p' (LIORefTCB l r) = withCombinedPrivs p' $ \p -> do-  taintP p l -  rtioTCB $ readIORef r+-- | 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 --- | Read the value of a labeled refernce. A read succeeds only if the--- label of the reference is below the current clearance. Moreover,--- the current label is raised to the join of the current label and--- the reference label. To avoid failures use 'labelOfLIORef' to check--- that a read will suceed.-readLIORef :: (LabelState l p s) => LIORef l a -> LIO l p s a-readLIORef x = getPrivileges >>= \p -> readLIORefP p x +--+-- Write 'LIORef's+--  -- | Trusted function used to read the value of a reference without -- raising the current label.-readLIORefTCB :: (LabelState l p s) => LIORef l a -> LIO l p s a-readLIORefTCB (LIORefTCB _ r) = rtioTCB $ readIORef r---- | 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 :: (LabelState l p s)-             => p -> LIORef l a -> a -> LIO l p s ()-writeLIORefP p' (LIORefTCB l r) a = withCombinedPrivs p' $ \p -> do-  aguardP p l -  rtioTCB $ writeIORef r a+readLIORefTCB :: MonadLIO l m => LIORef l a -> m a+readLIORefTCB = liftLIO . ioTCB . readIORef . unlabelLIORefTCB --- | Write a new value into a labeled reference. A write succeeds if--- the current label can-flow-to the label of the reference, and the--- label of the reference can-flow-to the current clearance.-writeLIORef :: (LabelState l p s) => LIORef l a -> a -> LIO l p s ()-writeLIORef x a = getPrivileges >>= \p -> writeLIORefP p x a+--+-- Write 'LIORef's+--  -- | Trusted function used to write a new value into a labeled -- reference, ignoring IFC.-writeLIORefTCB :: (LabelState l p s) => LIORef l a -> a -> LIO l p s ()-writeLIORefTCB (LIORefTCB _ r) a = rtioTCB $ writeIORef r a---- | 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 :: (LabelState l p s)-              =>  p -> LIORef l a -> (a -> a) -> LIO l p s ()-modifyLIORefP p' (LIORefTCB l r) f = withCombinedPrivs p' $ \p -> do-  aguardP p l -  rtioTCB $ modifyIORef r f+writeLIORefTCB :: MonadLIO l m => LIORef l a -> a -> m ()+writeLIORefTCB lr a = liftLIO . ioTCB $! writeIORef (unlabelLIORefTCB lr) a --- | Mutate the contents of a labeled reference. For the mutation to--- succeed it must be that the current label can-flow-to the label of--- the reference, and the label of the reference can-flow-to the--- current clearance. Note that because a modifer is provided, the--- reference contents are not observable by the outer computation and--- so it is not required that the current label be raised.-modifyLIORef :: (LabelState l p s)-             =>  LIORef l a            -- ^ Labeled reference-             -> (a -> a)               -- ^ Modifier-             -> LIO l p s ()-modifyLIORef x f = getPrivileges >>= \p -> modifyLIORefP p x f+--+-- Modify 'LIORef's+--  -- | Trusted function that mutates the contents on an 'LIORef', -- ignoring IFC.-modifyLIORefTCB :: (LabelState l p s)-                =>  LIORef l a -> (a -> a) -> LIO l p s ()-modifyLIORefTCB (LIORefTCB _ r) f = rtioTCB $ modifyIORef r f----- | Same as 'atomicModifyLIORef' except @atomicModifyLIORefP@ takes--- a set of privileges which are accounted for in label comparisons.-atomicModifyLIORefP :: (LabelState l p s) =>-                       p -> LIORef l a -> (a -> (a, b)) -> LIO l p s b-atomicModifyLIORefP p' (LIORefTCB l r) f = withCombinedPrivs p' $ \p -> do-  aguardP p l-  rtioTCB $ atomicModifyIORef r f---- | Atomically modifies the contents of an 'LIORef'. It is required--- that the label of the reference be above the current label, but--- below the current clearance. -atomicModifyLIORef :: (LabelState l p s) =>-                      LIORef l a -> (a -> (a, b)) -> LIO l p s b-atomicModifyLIORef x f = getPrivileges >>= \p -> atomicModifyLIORefP p x f+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 :: (LabelState l p s)-                      => LIORef l a -> (a -> (a, b)) -> LIO l p s b-atomicModifyLIORefTCB (LIORefTCB _ r) f = rtioTCB $ atomicModifyIORef r f+atomicModifyLIORefTCB :: MonadLIO l m => LIORef l a -> (a -> (a, b)) -> m b+atomicModifyLIORefTCB lr f =+  liftLIO . ioTCB $! atomicModifyIORef (unlabelLIORefTCB lr) f 

@@ -0,0 +1,160 @@+{-# LANGUAGE Safe #-}+{- | ++Labels are a way of describing who can observe and modify data.  There+is a partial order, generally pronounced \"can flow to\" on labels.+In LIO we write this partial order ``canFlowTo`` (in the literature it+is usually written as &#8849;).++The idea is that data labeled @L_1@ may affect data labeled @L_2@+only if @L_1@ ``canFlowTo`` @L_2@.  The 'LIO' monad (see "LIO.Core")+keeps track of the current label of the executing code (accessible via+the 'getLabel' function).  Code may attempt to perform various IO or+memory operations on labeled data.  Hence, touching data may change+the current label (or throw an exception if an operation would violate+flow restrictions).++If the current label is @L_cur@, then it is only permissible to read+data labeled @L_r@ if @L_r ``canFlowTo`` L_cur@.  This is sometimes+termed \"no read up\" in the literature; however, because the partial+order allows for incomparable labels (i.e., two labels @L_1@ and @L_2@+such that @not (L_1 ``canFlowTo`` L_2) && not (L_2 ``canFlowTo``+L_1)@), a more appropriate phrasing would be \"read only what can flow+to your label\".  Note that, rather than throw an exception, reading+data will often just increase the current label to ensure that @L_r+``canFlowTo`` L_cur@.  The LIO monad keeps a second label, called the+/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+a piece of LIO code from accessing anything above @L_clear@.++Conversely, it is only permissible to modify data labeled @L_w@ when+@L_cur``canFlowTo`` L_w@, a property often cited as \"no write down\",+but more accurately characterized as \"write only what you can flow+to\".  In practice, there are very few IO abstractions (namely,+mutable references) in which it is possible to do a pure write that+doesn't also involve observing some state.  For instance, writing to a+file handle and not getting an exception tells you that the handle is+not closed.  Thus, in practice, the requirement for modifying data+labeled @L_w@ is almost always that @L_cur ``canFlowTo`` L_w@ and @L_w+``canFlowTo`` L_cur@, i.e., @L_cur == L_w@.++Note that higher labels are neither more nor less privileged than+lower ones.  Simply, the higher one's label is, the more things one+can read.  Conversely, the lower one's label, the more things one can+write.  But, because labels are a partial and not a total order, some+data may be completely inaccessible to a particular computation; for+instance, if the current label is @L_cur@, the current clearance is+@C_cur@, and some data is labeled @L_d@, such that @not (L_cur+``canFlowTo`` L_d || L_d ``canFlowTo`` C_cur)@, then the current+thread can neither read nor write the data, at least without invoking+some privilege.++LIO is polymorphic in the label type. It is solely required that every+implementation of a label (usually called a "label format") be an+instance of the 'Label' class. This class provides a generic interface+to labels: they must define the 'canFlowTo' relation, some minimal+element 'bottom', some maximum element 'top', and two binary operators+on how to combine labels: the least upper bound ('lub') and greatest+lower bound ('glb').++Since LIO associates labels with different data types, it is useful to+be able to access the label of such objects (when the label is solely+protected by the current label). To this end, LIO provides the+'LabelOf' type class for which different labeled objects+implementations provide an instance.++-}++module LIO.Label (+  -- * Labels+    Label(..), upperBound, lowerBound+  -- * 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>).+-- Specifically, it is necessary to define a bottom element+-- 'bottom' (in literature, written as &#8869;), a top element 'top' (in+-- literature, written as &#8868;), a join, or least upper bound, 'lub'+-- (in literature, written as &#8852;), a meet, or greatest lower bound,+-- '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+  -- | /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 ``canFlowTo`` L_3@,+  --+  -- * @L_2 ``canFlowTo`` L_3@, and+  --+  -- * There is no label @L_4 /= L_3 @ such that+  --   @L_1 ``canFlowTo`` L_4@, @L_2 ``canFlowTo`` L_4@, and+  --   @L_4 ``canFlowTo`` L_3@.  In other words @L_3@ is the least+  --   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_3 ``canFlowTo`` L_1@,+  --+  -- * @L_3 ``canFlowTo`` L_2@, and+  --+  -- * There is no label @L_4 /= L_3@ such that+  --   @L_4 ``canFlowTo`` L_1@, @L_4 ``canFlowTo`` L_1@, and+  --   @L_3 ``canFlowTo`` L_4@.  In other words @L_3@ is the greatest+  --   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+  -- 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@.+  --+  -- * 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@.+  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:+-- +-- > newtype LVal l a = LValTCB (l, a)+-- +-- Then, you may wish to allow untrusted code to read the label of any+-- @LVal@s but not necessarily the actual value. To do so, simply+-- provide an instance for @LabelOf@:+-- +-- > instance LabelOf LVal where+-- >   labelOf (LValTCB lv) = fst lv+class LabelOf t where+  -- | Get the label of a type kinded @* -> *@+  labelOf :: Label l => t l a -> l+  

@@ -0,0 +1,187 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE ConstraintKinds,+             FlexibleContexts #-}++{- |++A data type 'Labeled' protects access to pure values (hence, we refer+to values of type @'Label' a@ as /labeled values/).  The role of+labeled values is to allow users to associate heterogeneous labels (see+"LIO.Label") with values. Although LIO\'s current label protects all+values in scope with the current label, 'Labeled' values allow for+more fine grained protection. Moreover, trusted code may easily+inspect 'Labeled' values, for instance, when inserting values into a+database.++Without the appropriate privileges, one cannot produce a pure+/unlabeled/ value that depends on a secret 'Labeled' value, or+conversely produce a high-integrity 'Labeled' value based on pure+data.  This module exports functions for creating labeled values+('label'), using the values protected by 'Labeled' by unlabeling them+('unlabel'), and changing the value of a labeled value without+inspection ('relabelLabeledP', 'taintLabeled', 'untaintLabeled').  A+'Functor'-like class ('LabeledFunctor') on 'Labeled' is also defined+in this module.++-}++module LIO.Labeled (+    Labeled+  -- * Label values+  , label, labelP+  -- * Unlabel values+  , unlabel, unlabelP+  -- * Relabel values+  , relabelLabeledP+  , taintLabeled, taintLabeledP , untaintLabeled, untaintLabeledP+  -- * Labeled functor+  -- $functor+  , LabeledFunctor(..)+  ) where++import           LIO.Label+import           LIO.Core+import           LIO.Privs+import           LIO.Labeled.TCB+import           Control.Monad++-- | Returns label of a 'Labeled' type.+instance LabelOf Labeled where+  labelOf = labelOfLabeled++--+-- Label values+--++-- | Function to construct a 'Labeled' from a label and pure value.  If+-- the current label is @lcurrent@ and the current clearance is+-- @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++-- | Constructs a 'Labeled' using privilege to allow the `Labeled`'s+-- label to be below the current label.  If the current label is+-- @lcurrent@ and the current clearance is @ccurrent@, then the privilege+-- @p@ and label @l@ specified must satisfy @canFlowTo p lcurrent l@ and+-- @l ``canFlowTo`` ccurrent@.  Note that privilege is not used to bypass+-- 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 p l a = do+  guardAllocP p l+  return $! labelTCB l a++--+-- Unlabel values+--++-- | Within the 'LIO' monad, this function takes a 'Labeled' and returns+-- the underlying value.  Thus, in the 'LIO' monad one can say:+--+-- > x <- unlabel (xv :: Labeled SomeLabelType Int)+--+-- And now it is possible to use the value of @x :: Int@, which is the+-- pure value of what was stored in @xv@.  Of course, @unlabel@ also+-- raises the current label.  If raising the label would exceed the+-- 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++-- | 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++--+-- 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.+--+-- Consequently @relabelP p l lv@ throws an 'InsufficientPrivs'+-- exception if+--+-- @'canFlowToP' p l ('labelOf' lv) && 'canFlowToP' p ('labelOf' lv) l@+--+-- 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++-- | 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+-- the current label and clearance, though the resulting label may not be+-- 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++-- | 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++-- | 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)+untaintLabeledP p target lv =+  relabelLabeledP p (partDowngradeP p (labelOf lv) target) lv+++{- $functor++Making 'Labeled' an instance of 'Functor' is problematic because:++1. 'fmap' would have type @Labeled l a -> (a -> b) -> Labeled b@ and thus +    creating /new/ labeled values above the current clearance or below+    the current label would be feasible (given one such value).+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@+   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)

@@ -0,0 +1,52 @@+{-# 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,88 +0,0 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Safe #-}-#endif-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE RankNTypes #-}---- | This module generalizes 'throw' and 'catch' (from "Control.Exception")--- to methods that can be defined on multiple monads.-module LIO.MonadCatch (MonadCatch(..), genericBracket) where--import Prelude hiding (catch)-import Control.Exception (Exception, SomeException)-import qualified Control.Exception as E---- | @MonadCatch@ is the class used to generalize the standard IO--- @catch@ and @throwIO@ functions to methods that can be defined in--- multiple monads.--- Minimal definition requires: @mask@, @throwIO@, @catch@, and--- @onException@.-class (Monad m) => MonadCatch m where-    -- | Executes a computation with asynchronous exceptions masked.-    -- See "Control.Exception" for more details.-    mask             :: ((forall a. m a -> m a) -> m b)  -- ^ Function-    -- that takes a mask-restoring function as argument and returns an-    -- action to execute.-                     -> m b-    -- | Like 'mask', but does not pass a restore action to the argument.-    mask_            :: m a -> m a-    mask_ io         = mask $ \_ -> io-    -- | A variant of @throwIO@ that can be used within the monad.-    throwIO          :: (Exception e) => e -> m a-    -- | Simplest exception-catching function.-    catch            :: (Exception e) => m a        -- ^ Computation to run -                                      -> (e -> m a) -- ^ Handler-                                      -> m a-    -- | Version of 'catch' with the arguments swapped around.-    handle           :: (Exception e) => (e -> m a) -> m a -> m a-    handle           = flip catch-    -- | Performs an action and a subsequent action if an exceptino is raised.-    onException      :: m a  -- ^ Computation to run first-                     -> m b  -- ^ Computation to run after, if-                             -- an exception was raised.-                     -> m a-    onException io h = io `catch` \e -> h >> throwIO (e :: SomeException)-    -- | This function allows you to execute an action with an initial-    -- \"acquire resource\" and final \"release resource\" as @bracket@-    -- of "Control.Exception".-    bracket          :: m b        -- ^ Computation to run first-                     -> (b -> m c) -- ^ Computation to run last-                     -> (b -> m a) -- ^ Computation to run in-between-                     -> m a-    bracket          = genericBracket onException-    -- | Variant of 'bracket' where the return value from the first-    -- computation is not required. -    bracket_         :: m a -> m b -> m c -> m c-    bracket_ a b c   = bracket a (const b) (const c)-    -- | Performs an action and a subsequent action.-    finally          :: m a -- ^ Computation to run first-                     -> m b -- ^ Computation to run after-                     -> m a-    finally a b      = mask $ \restore -> do-                         r <- restore a `onException` b-                         _ <- b-                         return r--instance MonadCatch IO where-    mask        = E.mask-    throwIO     = E.throwIO-    catch       = E.catch-    onException = E.onException-    bracket     = E.bracket---- | Given some general @onException@ function, @genericBracket@--- allows you to execute an action with an initial \"acquire resource\"--- and final \"release resource\" as @bracket@ of "Control.Exception".-genericBracket :: (MonadCatch m) =>-                  (m b -> m c -> m b) -- ^ On exception function-               -> m a                 -- ^ Action to perform first-               -> (a -> m c)          -- ^ Action to perform last-               -> (a -> m b)          -- ^ Action to perform in-between-               -> m b                 -- ^ Result of in-between action-genericBracket myOnException m1 m3 m2 =-    mask $ \restore -> do-      a <- m1-      b <- restore (m2 a) `myOnException` (m3 a)-      _ <- m3 a-      return b

@@ -1,31 +0,0 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Trustworthy #-}-#endif-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE OverlappingInstances #-}---- | This module provides a function 'liftLIO' for executing 'LIO'--- computations from transformed versions of the 'LIO' monad.--- There is also a method 'liftIO', which is a synonym for 'liftLIO',--- to help with porting code that expects to run in the @IO@ monad.-module LIO.MonadLIO (MonadLIO(..)) where--import LIO.TCB (LIO, LabelState)-import Control.Monad.Trans (MonadTrans(..))---- |  MonadIO-like class.-class (Monad m, LabelState l p s) => MonadLIO m l p s | m -> l p s where-    liftLIO :: LIO l p s a -> m a-    liftIO  :: LIO l p s a -> m a-    liftIO  = liftLIO--instance (LabelState l p s) => MonadLIO (LIO l p s) l p s where-    liftLIO = id--instance (MonadLIO m l p s, MonadTrans t, Monad (t m))-         => MonadLIO (t m) l p s where-   liftLIO = lift . liftLIO

@@ -0,0 +1,96 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE MultiParamTypeClasses,+             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/.++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. ++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. ++-}++module LIO.Privs (+  -- * Privilege descriptions+    PrivDesc(..)+  -- * Privileges+  , Priv(..)+  , NoPrivs(..)+  ) where++import Data.Monoid++import LIO.Label+import LIO.Privs.TCB++-- | 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+    -- | 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+    -- from @L_1@ to @L_2@.  Note that @'canFlowTo' L_1 L_2@ implies+    -- @'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++    -- | 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/+    -- possible privileges, then @L_r == L_g@.+    --+    -- More specifically, @L_r@ is the greatest lower bound of the+    -- set of all labels @L_l@ satisfying:+    --+    --   1. @ L_g ⊑ L_l@, and+    --+    --   2. @ L ⊑ₚ L_l@.+    --+    -- Operationally, @partDowngradeP@ captures the minimum change required+    -- to the current label when viewing data labeled @L_l@.  A common+    -- pattern is to use the result of 'getLabel' as @L_g@ (i.e., the+    -- 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+                   -> l  -- ^ Label from which data must flow+                   -> l  -- ^ Goal label+                   -> l  -- ^ Result++--+-- No privileges+--++-- | 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+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

@@ -0,0 +1,57 @@+{-# 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

@@ -1,60 +0,0 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 702-{-# LANGUAGE Trustworthy #-}-#endif---- | This module exports the subset of symbols in the "LIO.TCB" module--- that are safe for untrusted code to access.  See the "LIO.TCB"--- module for documentation.--module LIO.Safe ( Label(..)-                 , Priv(..), noPrivs-                 , getPrivileges, withPrivileges-                 , withCombinedPrivs -                 , dropPrivileges -                 , LIO, LabelState-                 , evalLIO-                 , getLabel, setLabelP-                 , getClearance, lowerClr, lowerClrP, withClearance-                 , labelOf-                 , label, labelP-                 , unlabel, unlabelP-                 , taintLabeled-                 , untaintLabeled, untaintLabeledP-                 , relabelP-                 , toLabeled, toLabeledP, discard, discardP-                 , taint, taintP-                 , wguard, wguardP, aguard, aguardP-                 , Labeled-                 , LabelFault(..)-                 , catchP, handleP, onExceptionP, bracketP-                 , evaluate-                 , PrivDesc-                 , Gate, mkGate, mkGateP, callGate-                 ) where--import LIO.TCB ( Label(..)-               , Priv(..), noPrivs-               , getPrivileges, withPrivileges-               , withCombinedPrivs -               , dropPrivileges -               , LIO, LabelState-               , evalLIO-               , getLabel, setLabelP-               , getClearance, lowerClr, lowerClrP, withClearance-               , labelOf-               , label, labelP-               , unlabel, unlabelP-               , taintLabeled-               , untaintLabeled, untaintLabeledP-               , relabelP-               , toLabeled, toLabeledP, discard, discardP-               , taint, taintP-               , wguard, wguardP, aguard, aguardP-               , Labeled-               , LabelFault(..)-               , catchP, handleP, onExceptionP, bracketP-               , evaluate-               , PrivDesc-               , Gate, mkGate, mkGateP, callGate-               )

@@ -1,1201 +1,185 @@-{-# LANGUAGE CPP #-}-#if __GLASGOW_HASKELL__ >= 704-{-# LANGUAGE Unsafe #-}-#endif-{-# LANGUAGE DeriveFunctor #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE ExistentialQuantification #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE FunctionalDependencies #-}---- | This module implements the core of the Labeled IO library for--- information flow control in Haskell.  It provides a monad, 'LIO',--- that is intended to be used as a replacement for the IO monad in--- untrusted code.  The idea is for untrusted code to provide a--- computation in the 'LIO' monad, which trusted code can then safely--- execute through the 'evalLIO' function.  (Though usually a wrapper--- function is employed depending on the type of labels used by an--- application.  For example, with "LIO.DCLabel", you would use--- 'evalDC' to execute an untrusted computation. There are also--- abbreviations for the 'LIO' monad type of a particular--- label--for instance 'DC'.)------ A data structure 'Labeled' (labeled value) protects access to pure--- values.  Without the appropriate privileges, one cannot produce a--- pure value that depends on a secret 'Labeled', or conversely produce a--- high-integrity 'Labeled' based on pure data.  The function 'toLabeled'--- allows one to seal off the results of an LIO computation inside an--- 'Labeled' without tainting the current flow of execution.  'unlabel'--- conversely allows one to use the value stored within a 'Labeled'.------ We note that using 'toLabeled' is /not/ safe with respect to--- the termination covert channel. Specifically, LIO with 'toLabeled'--- is only termination-insensitive non-interfering. For a--- termination-sensitive 'toLabeled'-like function, see "LIO.Concurrent".--- --- Any code that imports this module is part of the--- /Trusted Computing Base/ (TCB) of the system.  Hence, untrusted--- code must be prevented from importing this module.  The exported--- symbols ending @...TCB@ can be used to violate label protections--- even from within pure code or the LIO Monad.  A safe subset of--- these symbols is exported by the "LIO.Safe" module, which is how--- untrusted code should access the core label functionality.--- ("LIO.Safe" is also re-exported by "LIO", the main gateway to--- this library.)----module LIO.TCB (-- * Basic Label Functions-                -- $labels-                Label(..)-                -- * Basic Privilige Functions-                -- $privs-               , Priv(..), noPrivs-               , getPrivileges-               , setPrivileges-               , withPrivileges-               , withCombinedPrivs-               , dropPrivileges -               -- * Labeled IO Monad (LIO)-               -- $LIO-               , LIO(..), LabelState-               , evalLIO, runLIO-               , newState-               , getLabel, setLabelP-               , getClearance, lowerClr, lowerClrP-               , withClearance-               -- * Labeled Values-               , Labeled-               , labelOf-               , label, labelP-               , unlabel, unlabelP-               , taintLabeled-               , untaintLabeled, untaintLabeledP-               , relabelP-               , toLabeled, toLabeledP, discard, discardP-               -- ** LIO Guards-               -- $guards-               , taint, taintP-               , wguard, wguardP-               , aguard, aguardP-               -- * Labeled Exceptions-               -- $lexception-               -- ** Exception type thrown by LIO library-               , LabelFault(..)-               -- ** Throwing and Catching Labeled Exceptions-               -- $throw-               , LabeledException(..)-               , MonadCatch(..)-               , catchP, handleP-               , onExceptionP, bracketP-               , evaluate-               -- * Gates-               -- $gates-               , PrivDesc(..)-               , Gate(..)-               , mkGate, mkGateP-               , callGate-               -- * Unsafe (TCB) Operations-               -- ** Basic Label Functions-               , PrivTCB, MintTCB(..)-               -- ** Labeled IO Monad (LIO)-               , LIOstate(..)-               , getTCB, putTCB-               , getLabelStateTCB, putLabelStateTCB-               , setLabelTCB, lowerClrTCB-               -- ** Labeled Values-               , ShowTCB(..), ReadTCB(..)-               , labelTCB, unlabelTCB-               -- ** Labeled Exceptions-               , catchTCB, OnExceptionTCB(..)-               , ioTCB, rtioTCB-               -- ** Gates-               , mkGateTCB, callGateTCB-               ) where--import Prelude hiding (catch)-import Control.Exception hiding (catch, handle, throw, throwIO,-                                 onException, block, unblock,-                                 evaluate, finally, mask)-import qualified Control.Exception as E-import Data.Monoid-import Data.Typeable-import Data.Functor-import Data.IORef-import Control.Applicative-import Text.Read (minPrec)-import LIO.MonadCatch--import Control.Monad.Error-import Control.Monad.State.Lazy hiding (put, get)-------------------------------------------------------------------------- Basic label functions --------------------------------------------------------------------------------------------------------------------{- $labels--Labels are a way of describing who can observe and modify data.  There-is a partial order, generally pronounced \"can flow to\" on labels.-In Haskell we write this partial order ``leq`` (in the literature it-is usually written as &#8849;).--The idea is that data labeled @L_1@ should affect data labeled-@L_2@ only if @L_1@ ``leq`` @L_2@, (i.e., @L_1@ /can flow to/-@L_2@).  The 'LIO' monad keeps track of the current label of the-executing code (accessible via the 'getLabel' function).  Code may-attempt to perform various IO or memory operations on labeled data.-Touching data may change the current label (or throw an exception-if an operation would violate can-flow-to restrictions).--If the current label is @L_cur@, then it is only permissible to-read data labeled @L_r@ if @L_r ``leq`` L_cur@.  This is sometimes-termed \"no read up\" in the literature; however, because the partial-order allows for incomparable labels (i.e., two labels @L_1@ and-@L_2@ such that @not (L_1 ``leq`` L_2) && not (L_2 ``leq`` L_1)@),-a more appropriate phrasing would be \"read only what can flow to-your label\".  Note that, rather than throw an exception, reading-data will often just increase the current label to ensure that-@L_r ``leq`` L_cur@.  The LIO monad keeps a second label, called-the /clearance/ (see 'getClearance'), that represents the highest-value the current thread can raise its label to. The purpose of-clearance is to enforce of discretionary access control: you can-set the clearance to a label @L_clear@ as to prevent a piece of-LIO code from reading anything above @L_clear@.--Conversely, it is only permissible to modify data labeled @L_w@-when @L_cur``leq`` L_w@, a property often cited as \"no write-down\", but more accurately characterized as \"write only what you-can flow to\".  In practice, there are very few IO abstractions-(namely, mutable references) in which it is possible to do a pure-write that doesn't also involve observing some state.  For instance,-writing to a file handle and not getting an exception tells you that-the handle is not closed.  Thus, in practice, the requirement for-modifying data labeled @L_w@ is almost always that @L_cur == L_w@.--Note that higher labels are neither more nor less privileged than-lower ones.  Simply, the higher one's label is, the more things one-can read.  Conversely, the lower one's label, the more things one can-write.  But, because labels are a partial and not a total order, -some data may be completely inaccessible to a particular computation;-for instance, if the current label is @L_cur@, the current clearance-  is @C_cur@, and some data is labeled @Ld_@, such that @not (L_cur-``leq`` L_d || L_d ``leq`` C_cur)@, then the current thread can-neither read nor write the data, at least without invoking some-privilege.--}--{- | This class defines a label format, corresponding to a bounded-lattice. Specifically, it is necessary to define a bottom element-'lbot' (in literature, written as &#8869;), a top element 'ltop'-(in literature, written as &#8868;), a join, or least upper bound,-'lub' (in literature, written as &#8852;), a meet, or greatest lower-bound, 'glb' (in literature, written as &#8851;), and of course the-can-flow-to partial-order 'leq' (in literature, written as &#8849;).--}-class (Eq a, Show a, Read a, Typeable a) => Label a where-    -- | Bottom-    lbot :: a-    -- | Top-    ltop :: a-    -- | Least upper bound (join) of two labels-    lub :: a -> a -> a-    -- | Greatest lower bound (meet) of two labels-    glb :: a -> a -> a-    -- | Can-flow-to relation-    leq :: a -> a -> Bool-------------------------------------------------------------------------- Basic privilege functions ----------------------------------------------------------------------------------------------------------------{- $privs--Privilege comes from a separate class called 'Priv', representing the-ability to bypass the protection of certain labels.  Essentially,-privilege allows you to behave as if @L_1 ``leq`` 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 ``leq`` L_2)@ is called-/downgrading/.--The basic method of the 'Priv' object is 'leqp', which performs the-more permissive can-flow-to check in the presence of particular-privileges (in literature this relation is a pre-order, commonly-written as &#8849;&#8346;).  Many 'LIO' operations have variants-ending @...P@ that take a privilege argument to act in a more-permissive way.  It is also possible to execute an 'LIO' action with-a set of privileges (without explicitly using the @...P@ combinators)-using the 'withPrivileges' combinator.  Practicing the /principle of-least privilege/, it is recommended that 'withPrivileges' only be-used in small blocks of code in which many operations require the-same privileges. It is safer to use @...P@ operators and privileges-explicitly.--All 'Priv' types are monoids, and so can be combined with 'mappend'.-How to create 'Priv' objects is specific to the particular label-type in use.  The method used is 'mintTCB', but the arguments depend-on the particular label type.  (Of course, the symbol 'mintTCB'-must not be available to untrusted code.)---}----- | @PrivTCB@ is a method-less class whose only purpose is to be--- unavailable to unprivileged code.  Since @(PrivTCB t) =>@ is in the--- context of class 'Priv' and unprivileged code cannot create new--- instances of the @PrivTCB@ class, this ensures unprivileged code--- cannot create new instances of the 'Priv' class either, even though--- the symbol 'Priv' is exported by "LIO.Base" and visible to--- untrusted code.-class PrivTCB t where---- | This class defines privileges and the more-permissive relation--- ('leqp') on labels using privileges. Additionally, it defines--- 'lostar' which is used to compute the smallest difference between--- two labels given a set of privilege.-class (Label l, Monoid p, PrivTCB p) => Priv l p where-    -- | The \"can-flow-to given privileges\" pre-order used to-    -- compare two labels in the presence of privileges.-    -- If @'leqp' p L_1 L_2@ holds, then privileges @p@ are sufficient to-    -- downgrade data from @L_1@ to @L_2@.  Note that @'leq' L_1 L_2@-    -- implies @'leq' p L_1 L_2@ for all @p@, but for some labels and-    -- privileges, 'leqp' will hold even where 'leq' does not.-    leqp :: p -> l -> l -> Bool-    leqp p a b = lostar p a b `leq` b--    -- | Roughly speaking, @L_r = lostar 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 ``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-    -- set of all labels @L_l@ satisfying:-    ---    --   1. @ L_g &#8849; L_l@, and-    ---    --   2. @ L &#8849;&#8346; L_l@.-    ---    -- Operationally, @lostar@ captures the minimum change required to-    -- the current label when viewing data labeled @L_l@.  A common-    -- pattern is to use the result of 'getLabel' as @L_g@ (i.e.,-    -- the 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.  For example, 'taintP' could be-    -- implemented as:-    ---    -- @-    --    taintP p l = do lcurrent <- 'getLabel'-    --                    'taint' (lostar p l lcurrent)-    -- @-    lostar :: p                 -- ^ Privileges-           -> l                 -- ^ Label from which data must flow-           -> l                 -- ^ Goal label-           -> l                 -- ^ Result--class MintTCB t i where-    -- |A function that mints new objects (such as instances of-    -- 'Priv') in a way that only privileged code should be allowed to-    -- do.  Because the MintTCB method is only available to-    -- priviledged code, other modules imported by unpriviledged code-    -- can define instances of mintTCB.-    mintTCB :: i -> t---- | Alias for 'mempty'.-noPrivs :: Monoid p => p-noPrivs = mempty-------------------------------------------------------------------------- Labeled IO --------------------------------------------------------------------------------------------------------------------------------- $LIO--- --- The 'LIO' monad is a wrapper around 'IO' that keeps track of the--- current label and clearance.  It is possible to raise one's label--- or lower one's clearance without privilege, but moving in the other--- direction requires appropriate privilege. The 'LIO' monad also--- keeps track of a set of privileges, used within a 'withPrivileges'--- block.------ 'LIO' is parameterized by three types.  The first is the--- particular label type.  The second type is the type of underlying--- privileges.  The third type is state specific to and functionally--- determined by the label type.  Trusted label implementation code--- can use 'getTCB' and 'putTCB' to get and set the label state.---- | Empty class used to specify the functional dependency between a--- label and it state.-class (Priv l p, Label l) => LabelState l p s | l -> s, l -> p where----- | Internal state of an 'LIO' computation.-data LIOstate l p s = LIOstate { labelState :: s -- ^ label-specific state-                               , lioL :: l       -- ^ current label-                               , lioC :: l       -- ^ current clearance-                               , lioP :: p       -- ^ current privileges-                               }---- | LIO monad is a State monad transformer with IO as the underlying--- monad.-newtype LIO l p s a = LIO (StateT (LIOstate l p s) IO a)-    deriving (Functor, Applicative, Monad)----- | Get internal state.-getTCB :: (LabelState l p s) => LIO l p s (LIOstate l p s)-getTCB = mkLIO $ \s -> return (s, s)---- | Put internal state.-putTCB :: (LabelState l p s) => LIOstate l p s -> LIO l p s ()-putTCB s = mkLIO $ \_ -> return (() , s)---- | Returns label-specific state of the 'LIO' monad.  This is the--- data specified as the second argument of 'evalLIO', whose type is--- @s@ in the monad @LIO l s@.-getLabelStateTCB :: (LabelState l p s) => LIO l p s s-getLabelStateTCB = labelState <$> getTCB---- | Sets the label-specific state of the 'LIO' monad.  See 'getTCB'.-putLabelStateTCB :: (LabelState l p s) => s -> LIO l p s ()-putLabelStateTCB ls = getTCB >>= putTCB . update-    where update s = s { labelState = ls }---- | Generate a fresh state to pass 'runLIO' when invoking it for the--- first time. The current label is set to 'lbot', the current--- clearance is set to 'ltop', and the current privileges are set to--- none.-newState :: (LabelState l p s) => s -> LIOstate l p s-newState s = LIOstate { labelState = s-                      , lioL = lbot-                      , lioC = ltop-                      , lioP = noPrivs }---- | Lift an IO computation into @LIO@.-mkLIO :: (LabelState l p s)-      => (LIOstate l p s -> IO (a, LIOstate l p s)) -> LIO l p s a-mkLIO = LIO . StateT---- | Given an LIO computation and state, run it.-unLIO :: (LabelState l p s)-      => LIO l p s a -> LIOstate l p s -> IO (a, LIOstate l p s)-unLIO (LIO m) = runStateT m---- | Execute an LIO action. The label on exceptions are removed.--- See 'evalLIO'.-runLIO :: forall l p s a. (LabelState l p s)-       => LIO l p s a -> LIOstate l p s -> IO (a, LIOstate l p s)-runLIO m s = unLIO m s `catch` (throwIO . delabel)-    where delabel :: LabeledException l -> SomeException-          delabel (LabeledExceptionTCB _ e) = e---- | Produces an 'IO' computation that will execute a particular '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--it just can't execute them without access to--- 'ioTCB'.)-evalLIO :: (LabelState l p s) =>-           LIO l p s a -- ^ The LIO computation to execute-        -> s          -- ^ Initial value of label-specific state-        -> IO (a, l)  -- ^ IO computation that will execute first argument-evalLIO m s = do (a, ls) <- runLIO m (newState s)-                 return (a, lioL ls)---- | Returns the current value of the thread's label.-getLabel :: (LabelState l p s) => LIO l p s l-getLabel = lioL <$> getTCB---- | Returns the current value of the thread's clearance.-getClearance :: (LabelState l p s) => LIO l p s l-getClearance = lioC <$> getTCB----- | Returns the current privileges.-getPrivileges :: (LabelState l p s) => LIO l p s p-getPrivileges = lioP <$> getTCB---- | Execute an LIO action with a set of underlying privileges. Within--- a @withPrivileges@ block, the supplied privileges are used in every --- even (non @...P@) operation.  For instance,------ >  unlabelP p x------ can instead be written as:------ >  withPrivileges p $ unlabel x------ The original privileges of the thread are restored after--- the action is executed within the @withPrivileges@ block.--- The @withPrivileges@ combinator provides a middle-ground between--- a fully explicit, but safe, privilege use (@...P@ combinators),--- and an implicit, but less safe, interface (provide getter/setter,--- and always use underlying privileges). It allows for the use--- of implicit privileges by explicitly enclosing the code with a--- @withPrivileges@ block.-withPrivileges :: (LabelState l p s) => p -> LIO l p s a -> LIO l p s a-withPrivileges p m = do-  p0 <- getPrivileges-  setPrivileges p-  -- restore privileges even if an exception is thrown-  m `finallyTCB` setPrivileges p0---- | Execute an 'LIO' action with the combination of the supplied--- privileges (usually passed to @...P@ functions) and current--- privileges.-withCombinedPrivs :: LabelState l p s => p -> (p -> LIO l p s a) -> LIO l p s a-withCombinedPrivs p0 io = do-  p1 <- getPrivileges-  io (p0 `mappend` p1)---- | Set the underlying privileges. Although this function is not--- unsafe, it is not exported by "LIO.Safe" as it provides a higher security--- risk. Users are encouraged to use 'withPrivileges'.-setPrivileges :: (LabelState l p s) => p -> LIO l p s ()-setPrivileges p = do s <- getTCB-                     putTCB $ s { lioP = p }---- | Drop all privileges. It is useful to remove all privileges when--- executing some untrusted code withing a 'withPrivileges' block.-dropPrivileges :: (LabelState l p s) => LIO l p s ()-dropPrivileges = setPrivileges noPrivs---- | If the current label is @oldLabel@ and the current clearance is--- @clearance@, this function allows code to raise the label to--- any value @newLabel@ such that--- @oldLabel ``leq`` newLabel && newLabel ``leq`` clearance@. --- Note that there is no @setLabel@ variant without the @...P@--- because the 'taint' function provides essentially the same--- functionality that @setLabel@ would.-setLabelP :: (LabelState l p s) => p -> l -> LIO l p s ()-setLabelP p' l = withCombinedPrivs p' $ \p -> do-  s <- getTCB-  if leqp p (lioL s) l-    then putTCB s { lioL = l }-    else throwIO LerrPriv---- | Set the current label to anything, with no security check.-setLabelTCB :: (LabelState l p s) => l -> LIO l p s ()-setLabelTCB l = do s <- getTCB-                   if l `leq` lioC s-                      then putTCB s { lioL = l }-                      else throwIO LerrClearance---- | Reduce the current clearance. One cannot raise the current label--- or create object with labels higher than the current clearance.-lowerClr :: (LabelState l p s) => l -> LIO l p s ()-lowerClr l = getTCB >>= doit-    where doit s | not $ l `leq` lioC s = throwIO LerrClearance-                 | not $ lioL s `leq` l = throwIO LerrLow-                 | otherwise            = putTCB s { lioC = l }---- | Raise the current clearance (undoing the effects of 'lowerClr').--- This requires privileges.-lowerClrP :: (LabelState l p s) => p -> l -> LIO l p s ()-lowerClrP p' l = withCombinedPrivs p' $ \p -> getTCB >>= doit p-    where doit p s | not $ leqp p l $ lioC s = throwIO LerrPriv-                   | not $ lioL s `leq` l = throwIO LerrLow-                   | otherwise            = putTCB s { lioC = l }---- | Set the current clearance to anything, with no security check.-lowerClrTCB :: (LabelState l p s) => l -> LIO l p s ()-lowerClrTCB l = getTCB >>= doit-    where doit s | not $ lioL s `leq` l =-            throwIO $ LerrInval ("Cannot lower the current clearance"-                                 ++ " below current label.")-                 | otherwise            = putTCB s { lioC = l }---- | Lowers the clearance of a computation, then restores the--- clearance to its previous value.  Useful to wrap around a--- computation if you want to be sure you can catch exceptions thrown--- by it.  Also useful to wrap around 'toLabeled' to ensure that the--- computation does not access data exceeding a particular label.  If--- @withClearance@ is given a label that can't flow to the current--- clearance, then the clearance is lowered to the greatest lower--- bound of the label supplied and the current clearance.------ 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 'lowerClrP'.-withClearance :: (LabelState l p s) => l -> LIO l p s a -> LIO l p s a-withClearance l m = do-  s <- getTCB-  putTCB s { lioC = l `glb` lioC s }-  a <- m-  putTCB s { lioC = lioC s }-  return a---- | 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' instead of 'ioTCB'.-ioTCB :: (LabelState l p s) => IO a -> LIO l p s a-ioTCB a = mkLIO $ \s -> do-  r <- a-  return (r, s)---- | 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 'catch' or--- 'catchP'.  This function's name stands for \"re-throw io\".-rtioTCB :: (LabelState l p s) => IO a -> LIO l p s a-rtioTCB io = do-  l <- getLabel-  ioTCB $ io `catch` (throwIO . LabeledExceptionTCB l)-------------------------------------------------------------------------- Labeled value ------------------------------------------------------------------------------------------------------------------------------ | @Labeled@ is a type representing labeled data.  -data Labeled l t = LabeledTCB l t-  deriving (Typeable)---- | Returns label of a 'Labeled' type.-labelOf :: Label l => Labeled l a -> l-labelOf (LabeledTCB l _) = l---- | Function to construct a 'Labeled' from a label and pure value.  If--- the current label is @lcurrent@ and the current clearance is--- @ccurrent@, then the label @l@ specified must satisfy--- @lcurrent ``leq`` l && l ``leq`` ccurrent@.-label :: (LabelState l p s) => l -> a -> LIO l p s (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 @lcurrent@--- and the current clearance is @ccurrent@, then the privilege @p@ and--- label @l@ specified must satisfy--- @(leqp p lcurrent l) && l ``leq`` ccurrent@.--- Note that privilege is not used to bypass the clearance.  You must--- use 'lowerClrP' to raise the clearance first if you wish to--- create an 'Labeled' at a higher label than the current clearance.-labelP :: (LabelState l p s) => p -> l -> a -> LIO l p s (Labeled l a)-labelP p' l a = withCombinedPrivs p' $ \p -> getTCB >>= doit p-    where doit p s | not $ l `leq` lioC s    = throwIO LerrClearance-                   | not $ leqp p (lioL s) l = throwIO LerrLow-                   | otherwise               = return $ LabeledTCB l a---- | Trusted constructor that creates labeled values.-labelTCB :: Label l => l -> a -> Labeled l a-labelTCB = LabeledTCB---- | Within the 'LIO' monad, this function takes a 'Labeled' and returns--- the value.  Thus, in the 'LIO' monad one can say:------ > x <- unlabel (xv :: Labeled SomeLabelType Int)------ And now it is possible to use the value of @x@, which is the pure--- value of what was stored in @xv@.  Of course, @unlabel@ also raises--- the current label.  If raising the label would exceed the current--- clearance, then @unlabel@ throws 'LerrClearance'.--- However, you can use 'labelOf' to check if 'unlabel' will succeed--- without throwing an exception.-unlabel :: (LabelState l p s) => Labeled l a -> LIO l p s 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.  Will still throw 'LerrClearance' under the same--- circumstances as 'unlabel'.-unlabelP :: (LabelState l p s) => p -> Labeled l a -> LIO l p s a-unlabelP p' (LabeledTCB la a) =  withCombinedPrivs p' $ \p ->-                                  taintP p la >> return a---- | Extracts the value from an 'Labeled', discarding the label and any--- protection.-unlabelTCB :: Label l => Labeled l a -> a-unlabelTCB (LabeledTCB _ a) = a---- | Raises the label of a 'Labeled' to the 'lub' of it's current label--- and the value supplied.  The label supplied must be less than the--- current clearance, though the resulting label may not be if the--- 'Labeled' is already above the current thread's clearance.-taintLabeled :: (LabelState l p s)-              => l -> Labeled l a -> LIO l p s (Labeled l a)-taintLabeled l (LabeledTCB la a) = do-  aguard l-  return $ LabeledTCB (lub l la) a----- | Downgrades the label of a 'Labeled' as much as possible given the--- current privilege.-untaintLabeled :: (LabelState l p s)-               => l -> Labeled l a -> LIO l p s (Labeled l a)-untaintLabeled = untaintLabeledP noPrivs---- | Same as 'untaintLabeled' but combines the current privilege with the--- supplied privilege when downgrading the label.-untaintLabeledP :: (LabelState l p s)-                => p -> l -> Labeled l a -> LIO l p s (Labeled l a)-untaintLabeledP p target lbld =-  relabelP p (lostar p (labelOf lbld) target) lbld---- | Relabeles a @Labeled@ value if the given privilege combined--- with the current privileges permits it.-relabelP :: (LabelState l p s)-        => p -> l -> Labeled l a -> LIO l p s (Labeled l a)-relabelP p' lbl (LabeledTCB la a) = withCombinedPrivs p' $ \p ->-   if leqp p lbl la && leqp p la lbl-     then return $ LabeledTCB lbl a-     else throwIO LerrPriv---- | @toLabeled@ is the dual of 'unlabel'.  It allows one to invoke--- computations that would raise the current label, but without--- actually raising the label.  Instead, the result of the--- 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 'catch', which is futher within--- a @toLabeled@ block, infromation can be leaked. Consider the--- following program that uses 'DCLabel's. (Note that 'discard' is--- simply @toLabeled@ that throws throws the result away.)------  > main = evalDC' $ do---  >   lRef <- newLIORef lbot ""---  >   hRef <- newLIORef ltop "secret" ---  >   -- brute force:---  >   forM_ ["fun", "secret"] $ \guess -> do---  >     stash <- readLIORef lRef---  >     writeLIORef lRef $ stash ++ "\n" ++ guess ++ ":"---  >     discard ltop $ do ---  >       catch ( discard ltop $ do---  >                 secret <- readLIORef hRef---  >                 when (secret == guess) $ throwIO . userError $ "got it!"---  >             ) (\(e :: IOError) -> return ())---  >       l <- getLabel---  >       when (l == lbot) $ do stash <- readLIORef lRef---  >                             writeLIORef lRef $ stash ++ "no!"---  >   readLIORef lRef---  >     where evalDC' act = do (r,l) <- evalDC act---  >                            putStrLn r---  >                            putStrLn $ "label = " ++ prettyShow l------  The output of the program is:------  > $ ./new---  > ---  > fun:no!---  > secret:---  > label = <True , False>------ Note that the current label is 'lbot' (which in DCLabels is--- @<True , False>@), and the secret is leaked. The fundamental issue--- is that the outer 'discard' allows for the current label to remain--- low even though the 'catch' raised the current label when the--- secret was found (and thus exception was throw). As a consequence,--- 'toLabeled' catches all exceptions, and returns a 'Labeled'--- value that may have a labeled exception as wrapped by @throw@.--- All exceptions within the outer computation, including--- IFC violation attempts, are essentially rethrown when performing--- an 'unlabel'.------ DEPRECATED: @toLabeled@ is susceptible to termination attacks.----toLabeled :: (LabelState l p s)-          => l -- ^ Label of result and upper bound on-               --  inner-computations' observation-          -> LIO l p s a -- ^ Inner computation-          -> LIO l p s (Labeled l a)-toLabeled = toLabeledP noPrivs-{-# DEPRECATED toLabeled "toLabeled is susceptible to termination attacks" #-}---- | Same as 'toLabeled' but allows one to supply a privilege object--- when comparing the initial and final label of the computation.------ DEPRECATED: @toLabeledP@ is susceptible to termination attacks.----toLabeledP :: (LabelState l p s)-           => p -> l -> LIO l p s a -> LIO l p s (Labeled l a)-toLabeledP p' l m = withCombinedPrivs p' $ \p -> do-  aguardP p l-  save_s <- getTCB-  res <- (Right <$> m) `catchTCB` (return . Left . lubErr l)-  s <- getTCB-  let lastL = lioL s-  putTCB s { lioL = lioL save_s, lioC = lioC save_s, lioP = lioP save_s }-  return . labelTCB l $-    if leqp p lastL l-      then either E.throw id res-      else let l' = lub lastL l-           in E.throw . mkErr . lub l' $ either getELabel (const l') res-    where mkErr le = LabeledExceptionTCB le $ toException LerrLow-          lubErr lnew (LabeledExceptionTCB le e) =-                  LabeledExceptionTCB (le `lub` lnew) e-          getELabel (LabeledExceptionTCB le _) = le-{-# DEPRECATED toLabeledP "toLabeledP is susceptible to termination attacks" #-}----- | Executes a computation that would raise the current label, but--- discards the result so as to keep the label the same.  Used when--- one only cares about the side effects of a computation.  For--- instance, if @log_handle@ is an 'LHandle' with a high label, one--- can execute------ @---   discard ltop $ 'hputStrLn' log_handle \"Log message\"--- @------ to create a log message without affecting the current label. ------ DEPRECATED: discard is susceptible to termination attacks.----discard :: (LabelState l p s) =>  l -> LIO l p s a -> LIO l p s ()-discard = discardP noPrivs-{-# DEPRECATED discard "discard is susceptible to termination attacks" #-}---- | Same as 'discard', but uses privileges when comparing initial and--- final label of the computation.-discardP :: (LabelState l p s) => p -> l -> LIO l p s a -> LIO l p s ()-discardP p l m = void $ toLabeledP p l m-{-# DEPRECATED discardP "discardP is susceptible to termination attacks" #-}------ | It would be a security issue to make certain objects a member of--- the 'Show' class, but nonetheless it is useful to be able to--- examine such objects when debugging.  The 'showTCB' method can be used--- to examine such objects.-class ShowTCB a where-    showTCB :: a -> String--instance (Label l, Show a) => ShowTCB (Labeled l a) where-    showTCB (LabeledTCB l t) = show t ++ " {" ++ show l ++ "}"---- | It is useful to have the dual of 'ShowTCB', @ReadTCB@, that allows--- for the reading of 'Labeled's that were written using 'showTCB'. Only--- @readTCB@ (corresponding to 'read') and @readsPrecTCB@ (corresponding--- to 'readsPrec') are implemented.-class ReadTCB a where-  readsPrecTCB :: Int -> ReadS a-  readTCB :: String -> a-  readTCB str = check $ readsPrecTCB minPrec str-    where check []                          = error "readTCB: no parse"-          check [(x,rst)] | all (==' ') rst = x-                         | otherwise        = error "readTCB: no parse"-          check _                           = error "readTCB: ambiguous parse"--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)-------------------------------------------------------------------------- LIO guards -------------------------------------------------------------------------------------------------------------------------------{- $guards--   Guards are used by privileged code to check that the invoking,-   unprivileged code has access to particular data.  If the current-   label is @lcurrent@ and the current clearance is @ccurrent@, then-   the following checks should be performed when accessing data-   labeled @ldata@:--   * When /reading/ an object labeled @ldata@, it must be the case-     that @ldata ``leq`` lcurrent@.  This check is performed by the-     'taint' function, so named becuase it \"taints\" the current LIO-     context by raising @lcurrent@ until @ldata ``leq`` lcurrent@.-     (Specifically, it does this by computing the least upper bound of-     the two labels with the 'lub' method of the 'Label' class.)-     However, if after doing this it would be the case that-     @not (lcurrent ``leq`` ccurrent)@, then 'taint' throws exception-     'LerrClearance' rather than raising the current label.--   * When /writing/ an object, it should be the case that @ldata-     ``leq`` lcurrent && lcurrent ``leq`` ldata@.  (As stated, this is-     the same as saying @ldata == lcurrent@, but the two are different-     when using 'leqp' instead of 'leq'.)  This is ensured by the-     'wguard' (write guard) function, which does the equivalent of-     'taint' to ensure the target label @ldata@ can flow to the-     current label, then throws an exception if @lcurrent@ cannot flow-     back to the target label.--   * When /creating/ or /allocating/ objects, it is permissible for-     them to be higher than the current label, so long as they are-     bellow the current clearance.  In other words, it must be the-     case that @lcurrent ``leq`` ldata && ldata ``leq`` ccurrent@.-     This is ensured by the 'aguard' (allocation guard) function.--The 'taintP', 'wguardP',  and 'aguardP' functions are variants of the-above that take privilege to be more permissive and raise the current-label less. ---}---- | General (internal) taint function.  Uses @mylub@ instead of--- 'lub', so that privileges can optionally be passed in. Throws--- 'LerrClearance' if raising the current label would exceed the--- current clearance.-gtaint :: (LabelState l p s) =>-          (l -> l -> l)         -- ^ @mylub@ function-       -> l                     -- ^ @l@ - Label to taint with-       -> LIO l p s ()-gtaint mylub l = do-  s <- getTCB-  let lnew = l `mylub` (lioL s)-  if lnew `leq` lioC s-     then putTCB s { lioL = lnew }-     else ioTCB $ E.throwIO $ LabeledExceptionTCB (lioL s)-          (toException LerrClearance)---- |Use @taint l@ in trusted code before observing an object labeled--- @l@.  This will raise the current label to a value @l'@ such that--- @l ``leq`` l'@, or throw @'LerrClearance'@ if @l'@ would have to be--- higher than the current clearance.-taint :: (LabelState l p s) => l -> LIO l p s ()-taint = gtaint lub---- |Like 'taint', but use privileges to reduce the amount of taint--- required.  Note that unlike 'setLabelP', @taintP@ will never lower--- the current label.  It simply uses privileges to avoid raising the--- label as high as 'taint' would raise it.-taintP :: (LabelState l p s)-       => p              -- ^Privileges to invoke-       -> l              -- ^Label to taint to if no privileges-       -> LIO l p s ()-taintP p' l = withCombinedPrivs p' $ \p -> gtaint (lostar p) l---- |Use @wguard l@ in trusted code before modifying an object labeled--- @l@.  If @l'@ is the current label, then this function ensures that--- @l' ``leq`` l@ before doing the same thing as @'taint' l@.  Throws--- @'LerrHigh'@ if the current label @l'@ is too high.-wguard :: (LabelState l p s) => l -> LIO l p s ()-wguard = wguardP noPrivs---- |Like 'wguard', but takes privilege argument to be more permissive.-wguardP :: (LabelState l p s) => p -> l -> LIO l p s ()-wguardP p' l = withCombinedPrivs p' $ \p -> do-  l' <- getLabel-  if leqp p l' l-    then taintP p l-    else throwIO LerrHigh---- |Ensures the label argument is between the current IO label and--- current IO clearance.  Use this function in code that allocates--- objects--untrusted code shouldn't be able to create an object--- labeled @l@ unless @aguard l@ does not throw an exception.-aguard :: (LabelState l p s) => l -> LIO l p s ()-aguard = aguardP noPrivs---- | Like 'aguardP', but takes privilege argument to be more permissive.-aguardP :: (LabelState l p s) => p -> l -> LIO l p s ()-aguardP p' newl = withCombinedPrivs p' $ \p -> do-  c <- getClearance-  l <- getLabel-  unless (newl `leq` c)  $ throwIO LerrClearance-  unless (leqp p l newl) $ throwIO LerrLow--------------------------------------------------------------------------- Labeled Exceptions -----------------------------------------------------------------------------------------------------------------------{- $lexception--LIO throws 'LabelFault' exceptions when an information flow violation-is to occur. In general, such exceptions are handled in the outer,-trusted IO code block that executes untrusted LIO code. However, it is-sometimes desirable for untrusted code to throw exceptions. To this-end we provide an implementation of labeled exceptions, as \"normal\"-exceptions are unsafe and can be used to leak information.  We-describe the interface below.---}---- | Violation of information flow conditions, or label checks should--- throw exceptions of type @LabelFault@. The @LerrInval@ constructor--- takes a string parameter -- it is important that trusted code use--- this carefully and aovid leaking information through it.-data LabelFault = LerrLow           -- ^ Requested label too low-                | LerrHigh          -- ^ Current label too high-                | LerrClearance     -- ^ Label would exceed clearance-                | LerrPriv          -- ^ Insufficient privileges-                | LerrInval String  -- ^ Invalid request-                deriving Typeable--instance Show LabelFault where-  show LerrLow       = "LerrLow: Requested label is too low"-  show LerrHigh      = "LerrHigh: Requested label is too high"-  show LerrClearance = "LerrClearance: Label would exceed clearance"-  show LerrPriv      = "LerrPriv: Insufficient privileges"-  show (LerrInval s) = "LerrInval: " ++ s--instance Exception LabelFault---{- $throw--   We must re-define the 'throwIO' and 'catch' functions to work in-   the 'LIO' monad.  A complication is that exceptions could-   potentially leak information.  For instance, within a block of code-   wrapped by 'discard', 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.  For-   compatibility, the 'throwIO', 'catch', and 'onException' functions-   are now methods that work in both the 'IO' or 'LIO' monad.--   If an exception is uncaught in the 'LIO' monad, the 'evalLIO'-   function will unlabel and 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.)--   Wherever possible, however, code should use the 'catchP' and-   'onExceptionP' variants that use whatever privilege is available to-   downgrade the exception.  Privileged code that must always run some-   cleanup function can use the 'onExceptionTCB' and 'bracketTCB'-   functions to run the cleanup code on all exceptions.--   /Note/:  Do not use 'throw' (as opposed to 'throwIO') 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-   of the 'evalLIO' function.  Similarly, asynchronous exceptions-   (such as divide by zero or undefined values in lazily evaluated-   expressions) cannot be caught within the 'LIO' monad.---}---- | A labeled exception is simply an exception associated with a label.-data LabeledException l = LabeledExceptionTCB l SomeException-  deriving (Typeable)--instance Label l => Show (LabeledException l) where-    show (LabeledExceptionTCB l e) = show e ++ " {" ++ show l ++ "}"--instance (Label l) => Exception (LabeledException l)--instance (LabelState l p s) => MonadCatch (LIO l p s) where-    mask k = mkLIO $ \s -> E.mask (fun k s)-      where fun :: (LabelState l p s)-                => ((forall a. LIO l p s a -> LIO l p s a) -> LIO l p s b)-                -> LIOstate l p s-                -> (forall a. IO a -> IO a) -> IO (b, LIOstate l p s)-            -- a little bit of magic:-            fun lioMask s = \ioRestore ->-              unLIO' s $ lioMask $ \lioRestore -> do-                            s'  <- getTCB-                            ref <- ioTCB $ newIORef s'-                            res <- ioTCB $ ioRestore $ do-                              (a,s'') <- unLIO lioRestore s'-                              writeIORef ref s''-                              return a-                            s'' <- ioTCB $ readIORef ref-                            putTCB s''-                            return res-            unLIO' s act = unLIO act s-    -- | It is not possible to catch pure exceptions from within the 'LIO'-    -- monad, but @throwIO@ wraps up an exception with the current label,-    -- so that it can be caught with 'catch' or 'catchP'..-    throwIO e = do-      l <- getLabel-      ioTCB $ E.throwIO $ LabeledExceptionTCB l (toException e)--    -- | Basic function for catching labeled exceptions. (The fact that-    -- they are labeled is hidden from the handler.)-    ---    -- > catch = catchP noPrivs-    ---    catch = catchP noPrivs---- | Catches an exception, so long as the label at the point where the--- exception was thrown can flow to the label at which @catchP@ is--- invoked, modulo the privileges specified.  Note that the handler--- raises the current label to the joint of the current label and --- exception label.-catchP :: (Exception e, LabelState l p s)-       => p   -- ^ Privileges with which to downgrade exception-       -> LIO l p s a        -- ^ Computation to run-       -> (e -> LIO l p s a) -- ^ Exception handler-       -> LIO l p s a        -- ^ Result of computation or handler-catchP p' io handler = withCombinedPrivs p' $ \p -> do-  clr <- getClearance-  io `catchTCB` (\e@(LabeledExceptionTCB le se) ->-      case fromException se of-        Just e' | le `leq` clr -> taintP p le >> handler e'-        _                      -> throwIO e)---- | Trusted catch functin.-catchTCB :: (LabelState l p s)-         => LIO l p s a        -- ^ Computation to run-         -> (LabeledException l -> LIO l p s a) -- ^ Exception handler-         -> LIO l p s a        -- ^ Result of computation or handler-catchTCB io handler = do-  s <- getTCB-  (a, s') <- ioTCB $ do-    (unLIO io s) `E.catch` (\e -> unLIO (handler e) s)-  putTCB s'-  return a---- | Version of 'catchP' with arguments swapped.-handleP :: (Exception e, LabelState l p s)-        => p   -- ^ Privileges with which to downgrade exception-        -> (e -> LIO l p s a) -- ^ Exception handler-        -> LIO l p s a        -- ^ Computation to run-        -> LIO l p s a        -- ^ Result of computation or handler-handleP p = flip (catchP p)---- | '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--- raised label.-onExceptionP :: (LabelState l p s)-             => p           -- ^ Privileges to downgrade exception-             -> LIO l p s a -- ^ The computation to run-             -> LIO l p s b -- ^ Handler to run on exception-             -> LIO l p s a -- ^ Result if no exception thrown-onExceptionP p io what = catchP p io-   (\e -> what >> throwIO (e :: SomeException))---- | Like standard 'E.bracket', but with privileges to downgrade--- exception.-bracketP :: (LabelState l p s)-         => p                     -- ^ Priviliges used to downgrade-         -> LIO l p s a           -- ^ Computation to run first-         -> (a -> LIO l p s c)    -- ^ Computation to run last-         -> (a -> LIO l p s b)    -- ^ Computation to run in-between-         -> LIO l p s b-bracketP p' f l i = withCombinedPrivs p' $ \p ->-  genericBracket (onExceptionP p) f l i---- | 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 :: (LabelState l p s) => a -> LIO l p s a-evaluate = rtioTCB . E.evaluate---- | For privileged code that needs to catch all exceptions in some--- cleanup function.  Note that for the 'LIO' monad, these methods do--- /not/ label the exceptions.  It is assumed that you will use--- 'rtioTCB' instead of 'ioTCB' for IO within the computation arguments--- of these methods.-class (MonadCatch m) => OnExceptionTCB m where-    onExceptionTCB :: m a -> m b -> m a-    finallyTCB     :: m a -> m b -> m a-    finallyTCB a b = mask $ \restore -> do-                       r <- restore a `onExceptionTCB` b-                       _ <-  b-                       return r-    bracketTCB     :: m a -> (a -> m c) -> (a -> m b) -> m b-    bracketTCB     = genericBracket onExceptionTCB--instance OnExceptionTCB IO where-    onExceptionTCB = E.onException-    bracketTCB     = E.bracket--instance (LabelState l p s) => OnExceptionTCB (LIO l p s) where-    onExceptionTCB io cleanup = io `catchTCB` (\e -> do void cleanup -                                                        ioTCB $ E.throwIO e)--instance (LabelState l p s) => MonadError IOException (LIO l p s) where-    throwError = throwIO-    catchError = catch-------------------------------------------------------------------------- Gates ------------------------------------------------------------------------------------------------------------------------------------{- $gates--LIO provides a basic implementation of /gates/, useful in providing-controlled RPC-like services where the client and service provider are-in mutual distrust. --A service provider uses 'mkGate' to create a gate data type 'Gate l d-a'.  The type parameter @l@ indicates the 'Label' type used to protect-the gate computation; the label value @ is bounded by the current-label and clearance at the time of creation.  The gate computation-itself is of type @d -> a@, where @d@, an instance of 'PrivDesc'.-Since gates are invoked with 'callGate', the service provider has the-guarantee that the client (the callee) owns the privileges-corresponding to the privilege description @d@. In effect, this allows-a client to \"prove\" to the service provider that they own certain-privileges without entrusting the service with its privileges.-The gate computation can analyze this privilege description when-determining the result.--A client invokes a gate with 'callGate', which unlabels the gate-computation and applies the gate computation to the description of the-supplied privilege.---}---- | Class used to describe privileges in a meaningful manner.-class (PrivTCB p, Show d) => PrivDesc p d | p -> d where-  -- | Get privilege description-  privDesc :: p -> d---- | A Gate is a wrapper for a 'Labeled' type.-newtype Gate l d a = Gate (Labeled l (d -> a))-  deriving (Typeable)---- | Create a gate given a gate label and computation.--- The label of the gate must be bounded by the current label and--- clearance.-mkGate :: (LabelState l p s, PrivDesc p d)-       => l                   -- ^ Label of gate-       -> (d -> a)            -- ^ Gate omputation-       -> LIO l p s (Gate l d a)-mkGate = mkGateP noPrivs---- | Same as 'mkGate', but uses privileges when making the gate.-mkGateP :: (LabelState l p s, PrivDesc p d)-        => p                   -- ^ Privileges-        -> l                   -- ^ Label of gate-        -> (d -> a)            -- ^ Gate computation-        -> LIO l p s (Gate l d a)-mkGateP p l f = Gate <$> labelP p l f---- | Same as 'mkGate', but ignores IFC.-mkGateTCB :: (LabelState l p s, PrivDesc p d)-          => l            -- ^ Label of gate-          -> (d -> a)     -- ^ Gate action-          -> Gate l d a-mkGateTCB l f = Gate (labelTCB l f)---- | Given a labeled gate and privilege, execute the gate computation.--- The current label is raised to the join of the gate and current--- label, clearance permitting. It is important to note that--- @callGate@ invokes the gate computation with the privilege--- description and /not/ the actual privilege.-callGate :: (LabelState l p s, PrivDesc p d)-         => Gate l d a   -- ^ Gate-         -> p            -- ^ Privilege used to unlabel gate action-         -> LIO l p s a-callGate (Gate lf) p = withCombinedPrivs p $ \pAmp -> do-  f <- unlabelP pAmp lf-  return $ f (privDesc p)---- | Same as 'callGate', but does not raise label in accessing the--- gate computation.-callGateTCB :: (LabelState l p s, PrivDesc p d)-            => Gate l d a   -- ^ Gate-            -> p            -- ^ Privilege used to unlabel gate action-            -> a-callGateTCB (Gate lf) p = unlabelTCB lf $ privDesc p+{-# LANGUAGE Unsafe #-}+{-# LANGUAGE GeneralizedNewtypeDeriving,+             MultiParamTypeClasses,+             FunctionalDependencies,+             FlexibleInstances,+             DeriveDataTypeable #-}++{- | ++This module exports ++* 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.++* Combinators for executing 'IO' actions.++The documentation and external, safe 'LIO' interface is provided in+"LIO.Core".++-}++module LIO.TCB (+  -- * LIO monad+    LIO(..), MonadLIO(..)+  -- ** Internal state+  , LIOState(..)+  , getLIOStateTCB, putLIOStateTCB, updateLIOStateTCB +  -- * Exceptions+  , LabeledException(..)+  -- ** Throw and catch+  , unlabeledThrowTCB, catchTCB+  -- * Executing IO actions+  , ioTCB, rethrowIoTCB+  -- * 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           LIO.Label++--+-- LIO Monad+--++-- | Internal state of an 'LIO' computation.+data LIOState l = LIOState { lioLabel     :: !l -- ^ Current label.+                           , lioClearance :: !l -- ^ Current clearance.+                           } deriving (Eq, Show, Read)++-- | The @LIO@ monad is a state monad, with 'IO' as the underlying monad,+-- that carries along a /current label/ ('lioLabel') and /current clearance/+-- ('lioClearance'). The current label imposes restrictions on+-- what the current computation may read and write (e.g., no writes to+-- public channels after reading sensitive data).  Since the current+-- label can be raised to be permissive in what a computation observes,+-- 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)++--+-- 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++--+-- Internal state+--++-- | 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)++-- | Set internal state.+putLIOStateTCB :: Label l => LIOState l -> LIO l ()+putLIOStateTCB s = LIOTCB . StateT $! \_ -> return ((), s)++-- | Update the internal state given some function.+updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()+updateLIOStateTCB f = do+  s <- getLIOStateTCB+  putLIOStateTCB $! f s+++--+-- Exceptions+--++-- | A labeled exception is simply an exception associated with a label.+data LabeledException l = LabeledExceptionTCB !l SomeException+  deriving (Show, Typeable)++instance Label l => Exception (LabeledException l)++-- | 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++-- | 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++--+-- Executing IO actions+--++-- | 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++-- | 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)+++--+-- Trusted 'Show' and 'Read'+--++-- | It would be a security issue to make certain objects a member of+-- the 'Show' class, but nonetheless it is useful to be able to+-- examine such objects when debugging.  The 'showTCB' method can be used+-- to examine such objects.+class ShowTCB a where+    showTCB :: a -> String++-- | It is useful to have the dual of 'ShowTCB', @ReadTCB@, that allows+-- for the reading of strings that were created using 'showTCB'. Only+-- @readTCB@ (corresponding to 'read') and @readsPrecTCB@ (corresponding+-- to 'readsPrec') are implemented.+class ReadTCB a where+  -- | Trusted 'readsPrec'+  readsPrecTCB :: Int -> ReadS a+  -- | Trusted 'read'+  readTCB :: String -> a+  readTCB str = check $ readsPrecTCB minPrec str+    where check []                          = error "readTCB: no parse"+          check [(x,rst)] | all (==' ') rst = x+                         | otherwise        = error "readTCB: no parse"+          check _                           = error "readTCB: ambiguous parse"

@@ -1,112 +0,0 @@-{-# LANGUAGE ForeignFunctionInterface #-}-#if __GLASGOW_HASKELL__ >= 701-{-# LANGUAGE Trustworthy #-}-#endif--------------------------------------------------------------------------------- |--- Module      :  System.Posix.Tmp--- Copyright   :  (c) Volker Stolz <vs@foldr.org>---                    Deian Stefan <deian@cs.stanford.edu>--- This is a copy of the /latest/ @System.Posix.Temp@ module. Because--- @Temp@ will not be made available until GHC 7.6, we are including--- the core functions here.-----------------------------------------------------------------------------------module System.Posix.Tmp (-        mkstemp, mkstemps, mkdtemp-    ) where--#include "HsTmp.h"--import Foreign.C-import System.IO-import System.Posix.IO-import System.Posix.Types--#if __GLASGOW_HASKELL__ > 700-import System.Posix.Internals (withFilePath, peekFilePath)--#elif __GLASGOW_HASKELL__ > 611-import System.Posix.Internals (withFilePath)--peekFilePath :: CString -> IO FilePath-peekFilePath = peekCString--#else-withFilePath :: FilePath -> (CString -> IO a) -> IO a-withFilePath = withCString--peekFilePath :: CString -> IO FilePath-peekFilePath = peekCString-#endif--#if HAVE_MKSTEMP-foreign import ccall unsafe "HsUnix.h __hstmp_mkstemp"-  c_mkstemp :: CString -> IO CInt-#endif---- | Make a unique filename and open it for reading\/writing. The returned--- 'FilePath' is the (possibly relative) path of the created file, which is--- padded with 6 random characters. The argument is the desired prefix of the--- filepath of the temporary file to be created.-mkstemp :: String -> IO (FilePath, Handle)-#if HAVE_MKSTEMP-mkstemp template' = do-  let template = template' ++ "XXXXXX"-  withFilePath template $ \ ptr -> do-    fd <- throwErrnoIfMinus1 "mkstemp" (c_mkstemp ptr)-    name <- peekFilePath ptr-    h <- fdToHandle (Fd fd)-    return (name, h)-#else-mkstemp = error "System.Posix.Temp.mkstemp: not supported"-#endif--#if HAVE_MKSTEMPS-foreign import ccall unsafe "HsUnix.h __hstmp_mkstemps"-  c_mkstemps :: CString -> CInt -> IO CInt-#endif---- | Make a unique filename with a given prefix and suffix and open it for--- reading\/writing. The returned 'FilePath' is the (possibly relative) path of--- the created file, which contains  6 random characters in between the prefix--- and suffix. The first argument is the desired prefix of the filepath of the--- temporary file to be created. The second argument is the suffix of the--- temporary file to be created.------ If you are using as system that doesn't support the mkstemps glibc function--- (supported in glibc > 2.11) then this function simply throws an error.-mkstemps :: String -> String -> IO (FilePath, Handle)-#if HAVE_MKSTEMPS-mkstemps prefix suffix = do-  let template = prefix ++ "XXXXXX" ++ suffix-      lenOfsuf = (fromIntegral $ length suffix) :: CInt-  withFilePath template $ \ ptr -> do-    fd <- throwErrnoIfMinus1 "mkstemps" (c_mkstemps ptr lenOfsuf)-    name <- peekFilePath ptr-    h <- fdToHandle (Fd fd)-    return (name, h)-#else-mkstemps = error "System.Posix.Temp.mkstemps: not supported"-#endif--#if HAVE_MKDTEMP-foreign import ccall unsafe "HsUnix.h __hstmp_mkdtemp"-  c_mkdtemp :: CString -> IO CString-#endif---- | Make a unique directory. The returned 'FilePath' is the path of the--- created directory, which is padded with 6 random characters. The argument is--- the desired prefix of the filepath of the temporary directory to be created.-mkdtemp :: String -> IO FilePath-mkdtemp template' = do-#if HAVE_MKDTEMP-  let template = template' ++ "XXXXXX"-  withFilePath template $ \ ptr -> do-    _ <- throwErrnoIfNull "mkdtemp" (c_mkdtemp ptr)-    name <- peekFilePath ptr-    return name-#else-mkdtemp = error "System.Posix.Temp.mkdtemp: not supported"-#endif

@@ -1,19 +0,0 @@-#include "HsTmp.h"--#if HAVE_MKSTEMP-int __hstmp_mkstemp(char *filetemplate) {-    return (mkstemp(filetemplate));-}-#endif--#if HAVE_MKSTEMPS-int __hstmp_mkstemps(char *filetemplate, int suffixlen) {-    return (mkstemps(filetemplate, suffixlen));-}-#endif--#if HAVE_MKDTEMP-char *__hstmp_mkdtemp(char *filetemplate) {-    return (mkdtemp(filetemplate));-}-#endif