lio 0.10.0.0 → 0.11.0.0

raw patch · 21 files changed

+1534/−1530 lines, 21 filesdep +hashablePVP ok

version bump matches the API change (PVP)

Dependencies added: hashable

API changes (from Hackage documentation)

Files

• LIO.hs +15/−20
• LIO/Concurrent.hs +69/−53
• LIO/Concurrent/LMVar.hs +29/−27
• LIO/Core.hs +146/−183
• LIO/DCLabel.hs +469/−81
• LIO/DCLabel/Core.hs +0/−318
• LIO/DCLabel/DSL.hs +0/−182
• LIO/DCLabel/Privs.hs +0/−78
• LIO/Delegate.hs +130/−0
• LIO/Error.hs +173/−0
• LIO/Exception.hs +8/−7
• LIO/LIORef.hs +32/−15
• LIO/Label.hs +240/−117
• LIO/Labeled.hs +23/−28
• LIO/Privs.hs +0/−213
• LIO/Run.hs +35/−4
• LIO/TCB.hs +111/−100
• LIO/TCB/Concurrent.hs +0/−44
• LIO/TCB/DCLabel.hs +0/−22
• LIO/TCB/LObj.hs +20/−12
• lio.cabal +34/−26

@@ -3,41 +3,36 @@  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") and privileges (documented in "LIO.Privs").+"LIO.Core"), with support for labels and privileges (documented in+"LIO.Label") and labeled values (documented in "LIO.Labeled"). -Certain symbols in the lio library, particularly those in+Certain symbols in the LIO library, particularly those in "LIO.Exception", use the same names as their 'IO' equivalents in the-system libraries.  Hence main modules that mostly include 'IO' code-and only need to invoke 'LIO' code should import "LIO.Run" (or+system libraries.  Hence main modules consisting mostly of 'IO' code+that simply need to run 'LIO' code should import "LIO.Run" (or "LIO.DCLabel") to avoid polluting their namespaces.  Most code will need to use a particular label format, which needs to-be imported separately.  For instance:+be imported separately.  Hence, a typical set of imports for an+untrusted LIO module is:  @  import "LIO"- -- Import your favorite label format:  import "LIO.DCLabel" @ -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.- -}  module LIO ( -    module LIO.Label+    module LIO.Core+  , module LIO.Delegate   , module LIO.Exception-  , module LIO.Core+  , module LIO.Label   , module LIO.Labeled-  , module LIO.Privs   ) where -import LIO.Core-import LIO.Exception-import LIO.Label-import LIO.Labeled-import LIO.Privs+import safe LIO.Core+import safe LIO.Delegate+import safe LIO.Exception+import safe LIO.Label+import safe LIO.Labeled

@@ -1,52 +1,54 @@ {-# LANGUAGE Trustworthy #-} {- | -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.+This module provides concurrency abstractions for 'LIO'.  The most+basic function, 'forkLIO', spawns a computation in a new light-weight+thread (analogous to 'forkIO'). -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.+'lFork' spawns a forked thread that returns a result other threads can+wait for (using 'lWait').  The label of such a thread's result must be+specified at the time the thread is spawned with 'lFork'.  Should the+'lFork'ed thread terminate with its current label be above the+specified result label, 'lWait' will throw an exception of type+'ResultExceedsLabel' in any thread waiting for the result. +Learing that a spawned thread has terminated by catching a+'ResultExceedsLabel' may cause the label of the waiting thread to+rise, possibly above the current clearance (in which case the+exception cannot be caught).  As an alternative, 'timedlWait'+unconditionally kills a spawned thread if it has not terminated at an+observable label within a certain time period.  'timedlWait' is+guaranteed both to terminate and not to throw exceptions that cannot+be caught at the current label.+ -} module LIO.Concurrent (-    LabeledResult-  -- * Forking new threads-  , lForkP, lFork, forkLIO+  -- * Forking simple threads+    forkLIO+  -- * Forking threads that return results+  , LabeledResult+  , lFork, lForkP   -- * Waiting on threads-  , lWaitP, lWait-  , trylWaitP, trylWait-  , timedlWaitP, timedlWait+  , ResultExceedsLabel(..)+  , lWait, lWaitP+  , trylWait, trylWaitP+  , timedlWait, timedlWaitP   -- * Labeled MVars   , module LIO.Concurrent.LMVar   ) where  -import qualified Control.Concurrent as IO-import qualified Control.Exception as IO-import Control.Monad-import Data.IORef+import safe qualified Control.Concurrent as IO+import safe qualified Control.Exception as IO+import safe Control.Monad+import safe Data.IORef -import LIO.Concurrent.LMVar-import LIO.Core-import LIO.Exception-import LIO.Label-import LIO.Privs+import safe LIO.Concurrent.LMVar+import safe LIO.Core+import safe LIO.Exception+import safe LIO.Error+import safe LIO.Label import LIO.TCB-import LIO.TCB.Concurrent   --@@ -73,12 +75,7 @@ -- label and clearance as enforced by a call to 'guardAlloc'. -- Moreover, the supplied computation must not terminate with its -- label above the result label; doing so will result in an exception--- (whose label will reflect this observation) being thrown in the--- thread reading the result.------ If an exception is thrown in the inner computation, the exception--- label will be raised to the join of the result label and original--- exception label.+-- being thrown in the thread reading the result. --  -- Note that @lFork@ immediately returns a 'LabeledResult', which is -- essentially a \"future\", or \"promise\". This prevents@@ -97,14 +94,14 @@ -- for when performing label comparisons. lForkP :: PrivDesc l p =>           Priv p -> l -> LIO l a -> LIO l (LabeledResult l a)-lForkP p l lio = do-  guardAllocP p l+lForkP p l (LIOTCB action) = do+  withContext "lForkP" $ guardAllocP p l   mv <- ioTCB IO.newEmptyMVar   st <- ioTCB $ newIORef LResEmpty   s0 <- getLIOStateTCB   tid <- ioTCB $ IO.mask $ \unmask -> IO.forkIO $ do     sp <- newIORef s0-    ea <- IO.try $ unmask $ unLIOTCB lio sp+    ea <- IO.try $ unmask $ action sp     LIOState lEnd _ <- readIORef sp     writeIORef st $ case ea of       _ | not (lEnd `canFlowTo` l) -> LResLabelTooHigh lEnd@@ -124,7 +121,7 @@ -- the result must be above the current label and below the current -- 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+-- exception is thrown by the underlying 'taint' 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,@@ -134,14 +131,19 @@  -- | Same as 'lWait', but uses priviliges in label checks and raises. lWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l a-lWaitP p (LabeledResultTCB _ l mv st) = taintP p l >> go+lWaitP p (LabeledResultTCB _ l mv st) =+  withContext "lWaitP" (taintP p l) >> go   where go = ioTCB (readIORef st) >>= check         check LResEmpty = ioTCB (IO.readMVar mv) >> go         check (LResResult a) = return $! a         check (LResLabelTooHigh lnew) = do           modifyLIOStateTCB $ \s -> s {-            lioLabel = partDowngradeP p lnew (lioLabel s) }-          throwLIO ResultExceedsLabel+            lioLabel = downgradeP p lnew `lub` lioLabel s }+          throwLIO ResultExceedsLabel {+              relContext = []+            , relLocation = "lWaitP"+            , relDeclaredLabel = l+            , relActualLabel = Just lnew }   -- | Same as 'lWait', but does not block waiting for result.@@ -151,13 +153,17 @@ -- | Same as 'trylWait', but uses priviliges in label checks and raises. trylWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l (Maybe a) trylWaitP p (LabeledResultTCB _ rl _ st) =-  taintP p rl >> ioTCB (readIORef st) >>= check+  withContext "trylWaitP" (taintP p rl) >> ioTCB (readIORef st) >>= check   where check LResEmpty = return Nothing         check (LResResult a) = return . Just $! a         check (LResLabelTooHigh lnew) = do           curl <- getLabel           if canFlowToP p lnew curl-            then throwLIO ResultExceedsLabel+            then throwLIO ResultExceedsLabel {+                     relContext = []+                   , relLocation = "trylWaitP"+                   , relDeclaredLabel = rl+                   , relActualLabel = Just lnew }             else return Nothing  @@ -165,10 +171,14 @@ -- | Like 'lWait', with two differences.  First, a timeout is -- specified and the thread is unconditionally killed after this -- timeout (if it has not yet returned a value).  Second, if the--- thread's result exceeds its label @timedWait@ and exceeds what the--- calling thread can observe, consumes the whole timeout and throws a+-- thread's result exceeds what the calling thread can observe,+-- @timedlWait@ consumes the whole timeout and throws a -- 'ResultExceedsLabel' exception you can catch (i.e., it never raises -- the label above the clearance).+--+-- Because this function can alter the result by killing a thread, it+-- requires the label of the 'LabeledResult' to be both readable and+-- writable at the current label. timedlWait :: Label l => LabeledResult l a -> Int -> LIO l a timedlWait = timedlWaitP noPrivs @@ -177,7 +187,9 @@ -- catching any 'ResultExceedsLabel' before the timeout period (if -- possible). timedlWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> Int -> LIO l a-timedlWaitP p lr@(LabeledResultTCB t _ mvb _) to = trylWaitP p lr >>= go+timedlWaitP p lr@(LabeledResultTCB t rl mvb _) to =+  withContext "timedlWaitP" $ do guardWriteP p rl+                                 trylWaitP p lr >>= go   where go (Just a) = return a         go Nothing = do           mvk <- ioTCB $ IO.newEmptyMVar@@ -186,5 +198,9 @@             IO.throwTo t (UncatchableTCB IO.ThreadKilled)           ioTCB $ IO.readMVar mvb           trylWaitP p lr >>= maybe-            (ioTCB (IO.takeMVar mvk) >> throwLIO ResultExceedsLabel)+            (ioTCB (IO.takeMVar mvk) >> throwLIO failure)             (\a -> ioTCB (IO.killThread tk) >> return a)+        failure = ResultExceedsLabel { relContext = []+                                     , relLocation = "timedWaitP"+                                     , relDeclaredLabel = rl+                                     , relActualLabel = Nothing }

@@ -7,7 +7,7 @@ "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+full (with a value of type @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@@ -40,11 +40,11 @@   , isEmptyLMVar, isEmptyLMVarP   ) where -import Control.Concurrent.MVar+import safe Control.Concurrent.MVar -import LIO.Label-import LIO.Core-import LIO.Privs+import safe LIO.Core+import safe LIO.Error+import safe LIO.Label import LIO.TCB import LIO.TCB.LObj @@ -63,14 +63,16 @@ newEmptyLMVar :: Label l               => l                -- ^ Label of @LMVar@               -> LIO l (LMVar l a)    -- ^ New mutable location-newEmptyLMVar l = guardAlloc l >> ioTCB (LObjTCB l `fmap` newEmptyMVar)+newEmptyLMVar l = do+  withContext "newEmptyLMVar" $ guardAlloc l+  ioTCB (LObjTCB l `fmap` newEmptyMVar)  -- | Same as 'newEmptyLMVar' except it takes a set of privileges which -- are accounted for in comparing the label of the MVar to the current -- label and clearance. newEmptyLMVarP :: PrivDesc l p => Priv p -> l -> LIO l (LMVar l a) newEmptyLMVarP p l = do-  guardAllocP p l+  withContext "newEmptyLMVarP" $ guardAllocP p l   ioTCB $ LObjTCB l `fmap` newEmptyMVar  -- | Create a new labeled MVar, in an filled state with the supplied@@ -80,14 +82,16 @@          => l                       -- ^ Label of @LMVar@          -> a                       -- ^ Initial value of @LMVar@          -> LIO l (LMVar l a)       -- ^ New mutable location-newLMVar l a = guardAlloc l >> ioTCB (LObjTCB l `fmap` newMVar a)+newLMVar l a = do+  withContext "newLMVar" $ guardAlloc l+  ioTCB (LObjTCB l `fmap` newMVar a)  -- | Same as 'newLMVar' except it takes a set of privileges which are -- accounted for in comparing the label of the MVar to the current label -- and clearance. newLMVarP :: PrivDesc l p => Priv p -> l -> a -> LIO l (LMVar l a) newLMVarP p l a = do-  guardAllocP p l+  withContext "newLMVarP" $ guardAllocP p l   ioTCB $ LObjTCB l `fmap` newMVar a  --@@ -102,26 +106,26 @@ -- 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@+-- Finally, like 'MVars' if the 'LMVar' is empty, @takeLMVar@ -- blocks. takeLMVar :: Label l => LMVar l a -> LIO l a-takeLMVar = blessTCB takeMVar+takeLMVar = blessTCB "takeLMVar" takeMVar  -- | Same as 'takeLMVar' except @takeLMVarP@ takes a privilege object -- which is used when the current label is raised. takeLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l a-takeLMVarP = blessPTCB takeMVar+takeLMVarP = blessPTCB "takeLMVarP" takeMVar  -- | Non-blocking version of 'takeLMVar'. It returns @Nothing@ if the -- 'LMVar' is empty, otherwise it returns @Just@ value, emptying the -- 'LMVar'. tryTakeLMVar :: Label l => LMVar l a -> LIO l (Maybe a)-tryTakeLMVar = blessTCB tryTakeMVar+tryTakeLMVar = blessTCB "tryTakeLMVar" tryTakeMVar  -- | Same as 'tryTakeLMVar', but uses priviliges when raising current -- label. tryTakeLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l (Maybe a)-tryTakeLMVarP = blessPTCB tryTakeMVar+tryTakeLMVarP = blessPTCB "tryTakeLMVar" tryTakeMVar  -- -- Put 'LMVar'@@ -140,21 +144,21 @@          => LMVar l a   -- ^ Source 'LMVar'          -> a           -- ^ New value          -> LIO l ()-putLMVar = blessTCB putMVar+putLMVar = blessTCB "putLMVar" putMVar  -- | Same as 'putLMVar' except @putLMVarP@ takes a privilege object -- which is used when the current label is raised. putLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l ()-putLMVarP = blessPTCB putMVar+putLMVarP = blessPTCB "putLMVarP" putMVar  -- | Non-blocking version of 'putLMVar'. It returns @True@ if the -- 'LMVar' was empty and the put succeeded, otherwise it returns @False@. tryPutLMVar :: Label l => LMVar l a -> a -> LIO l Bool-tryPutLMVar = blessTCB tryPutMVar+tryPutLMVar = blessTCB "tryPutLMVar" tryPutMVar  -- | Same as 'tryPutLMVar', but uses privileges when raising current label. tryPutLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l Bool-tryPutLMVarP = blessPTCB tryPutMVar+tryPutLMVarP = blessPTCB "tryPutLMVarP" tryPutMVar  -- -- Read 'LMVar'@@ -166,12 +170,12 @@ -- a function such as 'putLMVar', 'tryTakeLMVarP', or 'isEmptyLMVar' -- for this 'LMVar'. readLMVar :: Label l => LMVar l a -> LIO l a-readLMVar = blessTCB readMVar+readLMVar = blessTCB "readLMVar" readMVar  -- | Same as 'readLMVar' except @readLMVarP@ takes a privilege object -- which is used when the current label is raised. readLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l a-readLMVarP = blessPTCB readMVar+readLMVarP = blessPTCB "readLMVarP" readMVar  -- -- Swap 'LMVar'@@ -188,12 +192,12 @@           => LMVar l a          -- ^ Source @LMVar@           -> a                  -- ^ New value           -> LIO l a            -- ^ Taken value-swapLMVar = blessTCB swapMVar+swapLMVar = blessTCB "swapLMVar" swapMVar  -- | Same as 'swapLMVar' except @swapLMVarP@ takes a privilege object -- which is used when the current label is raised. swapLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l a-swapLMVarP = blessPTCB swapMVar+swapLMVarP = blessPTCB "swapLMVarP" swapMVar  -- -- Check state of 'LMVar'@@ -202,12 +206,10 @@ -- | 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'.+-- label and the current label. isEmptyLMVar :: Label l => LMVar l a -> LIO l Bool-isEmptyLMVar = blessTCB isEmptyMVar+isEmptyLMVar = blessTCB "isEmptyLMVar" isEmptyMVar  -- | Same as 'isEmptyLMVar', but uses privileges when raising current label. isEmptyLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l Bool-isEmptyLMVarP = blessPTCB isEmptyMVar+isEmptyLMVarP = blessPTCB "isEmptyLMVarP" isEmptyMVar

@@ -2,70 +2,60 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE 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.+This module implements the core of the Labeled IO (LIO) information+flow control (IFC) library.  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+'evalLIO' and similar functions (e.g., 'evalDC' in+"LIO.DCLabel#v:evalDC"). -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 constants such as @3@ or @\"tis a-string\"@. More interestingly, consider reading a \"secret\" file:+Unlike 'IO', the 'LIO' monad keeps track of a /current label/+(accessible via the 'getLabel' function) during each 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 reference (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\".  Labels are described+in more detail in the documentation for "LIO.Label", as well as the+documentation for particular label formats (such as "LIO.DCLabel"). -> bs <- readFile "/secret/file.txt"+The role of the current label is two-fold:  First, the current label+protects all pure values currently in scope.  For example, the current+label is the label on constants (such as @3@ and @\"tis a string\"@)+as well as function arguments.  More interestingly, consider reading a+secret reference: -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'.+> val <- readLIORef secret -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:+Though the label of @secret@ may be \"secret\", @val@ is not+explicitly labeled.  Hence, to protect the contents of the 'LIORef'+that has been read into @val@, the current label must be at least+\"secret\" before returning from @readLIORef@.  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, instead of+throwing an exception, reading data often just increases the current+label to ensure that @l_r ``canFlowTo`` l_cur@.  This is acomplished+using a function such as 'taint'. -> writeFile "/public/file.txt" bs+The second purpose of the current label is to prevent 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,+the following attempt to leak the @val@ after reading it from a secret+'LIORef' would fail: +> writeLIORef public val+ 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+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".+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) == False@.  -} @@ -81,78 +71,89 @@   , getClearance, setClearance, setClearanceP   , scopeClearance, withClearance, withClearanceP   -- * Exceptions thrown by LIO-  -- $lioExceptions-  , MonitorFailure(..)-  , VMonitorFailure(..)+  , AnyLabelError(..), LabelError(..), InsufficientPrivs(..)   -- * Guards   -- $guards-  -- ** Allocate/write-only++  -- ** Allocate/write-only guards   , guardAlloc, guardAllocP-  -- ** Read-only+  -- ** Read-only guards   , taint, taintP-  -- ** Write+  -- ** Read-write guards   , guardWrite, guardWriteP   ) where  -import qualified Control.Exception as IO-import Control.Monad-import Data.IORef-import Data.Typeable+import safe qualified Control.Exception as IO+import safe Control.Monad+import safe Data.IORef -import LIO.Exception+import safe LIO.Error+import safe LIO.Exception+import safe LIO.Label+import safe LIO.Run import LIO.TCB-import LIO.Label-import LIO.Privs-import LIO.Run   -- -- Internal state -- --- | Returns the current value of the thread's label.+-- | Returns the value of the thread's current label. getLabel :: Label l => LIO l l getLabel = lioLabel `liftM` getLIOStateTCB  --- | Raise the current label to the provided label, which must be+-- | Raises the current label to the provided label, which must be -- between the current label and clearance. See 'taint'. setLabel :: Label l => l -> LIO l ()-setLabel = setLabelP noPrivs+setLabel l = withContext "setLabel" $ do+  guardAlloc l+  modifyLIOStateTCB $ \s -> s { lioLabel = l }  -- | 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@.+-- @clearance@, this function allows code to raise the current label+-- to any value @newLabel@ such that @'canFlowToP' priv oldLabel+-- newLabel && 'canFlowTo' newLabel clearance@.  (Note the privilege+-- argument affects the label check, not the clearance check; call+-- 'setClearanceP' first to raise the clearance.) setLabelP :: PrivDesc l p => Priv p -> l -> LIO l ()-setLabelP p l = do-  guardAllocP p l `catch`-      \(_ :: MonitorFailure) -> throwLIO InsufficientPrivs+setLabelP p l = withContext "setLabelP" $ do+  guardAllocP p l   modifyLIOStateTCB $ \s -> s { lioLabel = l } --- | Returns the current value of the thread's clearance.+-- | Returns the thread's current clearance. getClearance :: Label l => LIO l l getClearance = lioClearance `liftM` getLIOStateTCB --- | Lower the current clearance. The new clerance must be between--- the current label and clerance. One cannot raise the current label--- or create object with labels higher than the current clearance.+-- | Lowers the current clearance.  The new clerance must be between+-- the current label and previous current clerance.  One cannot raise+-- the current label or create object with labels higher than the+-- current clearance. setClearance :: Label l => l -> LIO l ()-setClearance = setClearanceP noPrivs+setClearance cnew = do+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB+  unless (canFlowTo l cnew && canFlowTo cnew c) $+    labelError "setClearance" [cnew]+  putLIOStateTCB $ LIOState l cnew --- | Raise the current clearance (undoing the effects of--- 'setClearance') by exercising privileges. If the current label is+-- | Raises 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.+-- clearance (modulo privileges), i.e., @'canFlowToP' p cnew c ==+-- True@.  Additionally, the current label must flow to the new+-- clearance, i.e., @l ``canFlowTo`` cnew@ == True.+-- +-- Since LIO guards that are used when reading/writing data (e.g.,+-- 'guardAllocP') do not use privileges when comparing labels with the+-- current clearance, code must always raise the current clearance, to+-- read/write data above the current clearance. setClearanceP :: PrivDesc l p => Priv p -> l -> LIO l () setClearanceP p cnew = do-  LIOState l c <- getLIOStateTCB-  unless (canFlowToP p cnew c) $! throwLIO InsufficientPrivs-  unless (l `canFlowTo` cnew)  $! throwLIO CurrentLabelViolation+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB+  unless (canFlowTo l cnew && canFlowToP p cnew c) $+    labelErrorP "setClearanceP" p [cnew]   putLIOStateTCB $ LIOState l cnew  -- | Runs an 'LIO' action and re-sets the current clearance to its@@ -166,21 +167,26 @@ -- be caught outside a second @scopeClearance@ that restores the -- clearance to higher than the current label. scopeClearance :: Label l => LIO l a -> LIO l a-scopeClearance lio = LIOTCB $ \sp -> do+scopeClearance (LIOTCB action) = LIOTCB $ \sp -> do   LIOState _ c <- readIORef sp-  ea <- IO.try $ unLIOTCB lio sp+  ea <- IO.try $ action sp   LIOState l _ <- readIORef sp   writeIORef sp (LIOState l c)   if l `canFlowTo` c     then either (IO.throwIO :: SomeException -> IO a) return ea-    else IO.throwIO ClearanceViolation+    else IO.throwIO LabelError { lerrContext = []+                               , lerrFailure = "scopeClearance"+                               , lerrCurLabel = l+                               , lerrCurClearance = c+                               , lerrPrivs = []+                               , lerrLabels = [] } --- | 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'.+-- | Temporarily lowers the clearance for a computation, then restores+-- it.  Equivalent to:+--+-- @+-- withClearance c lio = 'scopeClearance' $ 'setClearance' c >> lio+-- @ --  -- Note that if the computation inside @withClearance@ acquires any -- 'Priv's, it may still be able to raise its clearance above the@@ -188,63 +194,17 @@ withClearance :: Label l => l -> LIO l a -> LIO l a withClearance c lio = scopeClearance $ setClearance c >> lio --- | Same as 'withClearance', but uses privileges when applying--- 'guardAllocP' to the supplied label.+-- | A variant of 'withClearance' that takes privileges.  Equivalent+-- to:+--+-- @+-- withClearanceP p c lio = 'scopeClearance' $ 'setClearanceP' p c >> lio+-- @ withClearanceP :: PrivDesc l p => Priv p -> l -> LIO l a -> LIO l a withClearanceP p c lio = scopeClearance $ setClearanceP p c >> lio   ----- 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'-                    | ResultExceedsLabel-                    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 -- @@ -260,9 +220,9 @@      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@.+     lcurrent@.  Specifically, it does this by computing the least+     upper bound or 'lub' of the two labels.  (Note 'taint' will fail+     if the new label cannot flow to the current clearance.)     * When /creating/ or /allocating/ objects, it is permissible for      them to be higher than the current label, so long as they are@@ -279,13 +239,12 @@      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'.-+Note that a write /always/ implies a read.  Hence, when writing to an+object for which you can observe the result (which is frequently the+case), you must use 'guardWrite'.  However, when performing a write+for which there are no observable side-effects to the writer, i.e.,+you cannot observe the success or failure of the write, then it is+safe to use 'guardAlloc'.  The 'taintP', 'guardAllocP',  and 'guardWriteP' functions are variants of the above that take privilege to be more permissive and raise the@@ -304,22 +263,20 @@ -- 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 :: Label l => l -> LIO l ()-guardAlloc = guardAllocP noPrivs+guardAlloc newl = do+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB+  unless (canFlowTo l newl && canFlowTo newl c) $+    labelError "guardAllocP" [newl]  -- | 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 :: PrivDesc l p => Priv p -> l -> LIO l () guardAllocP p newl = do-  c <- getClearance-  l <- getLabel-  unless (canFlowToP p l newl) $! throwLIO CurrentLabelViolation-  unless (newl `canFlowTo` c)  $! throwLIO ClearanceViolation+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB+  unless (canFlowToP p l newl && canFlowTo newl c) $+    labelErrorP "guardAllocP" p [newl]  -- -- Read@@ -327,10 +284,15 @@  -- | 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.+-- @l ``canFlowTo`` l'@, or throw a 'LabelError' exception if @l'@+-- would have to be higher than the current clearance. taint :: Label l => l -> LIO l ()-taint = taintP noPrivs+taint newl = do+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB+  let l' = l `lub` newl+  unless (l' `canFlowTo` c) $ labelError "taint" [newl]+  modifyLIOStateTCB $ \s -> s { lioLabel = l' }+    -- | Like 'taint', but use privileges to reduce the amount of taint -- required.  Note that @taintP@ will never lower the current label.@@ -338,40 +300,41 @@ -- 'taint' would raise it. taintP :: PrivDesc l p => Priv p -> l -> LIO l () taintP p newl = do-  c <- getClearance-  l <- getLabel-  let l' = partDowngradeP p newl l-  unless (l' `canFlowTo` c) $! throwLIO ClearanceViolation+  LIOState { lioLabel = l, lioClearance = c } <- getLIOStateTCB+  let l' = l `lub` downgradeP p newl+  unless (l' `canFlowTo` c) $ labelErrorP "taintP" p [newl]   modifyLIOStateTCB $ \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,+-- object labeled @l@, for which 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+-- > guardWrite l = guardAlloc l >> taint l -- -- This guarantees that @l@ ``canFlowTo`` the current label (and -- clearance), and that the current label ``canFlowTo`` @l@. -- guardWrite :: Label l => l -> LIO l ()-guardWrite = guardWriteP noPrivs+guardWrite newl = withContext "guardWrite" $ do+  guardAlloc newl+  taint newl --- | Like 'guardWrite', but takes privilege argument to be more+-- | Like 'guardWrite', but takes a privilege argument to be more -- permissive. guardWriteP :: PrivDesc l p => Priv p -> l -> LIO l ()-guardWriteP p newl = do-  taintP      p newl+guardWriteP p newl = withContext "guardWriteP" $ do   guardAllocP p newl+  taintP p newl  -- -- Monad base --  -- | Synonym for monad in which 'LIO' is the base monad.-class (Monad m, Label l) => MonadLIO l m | m -> l where+class (Label l, Monad m) => MonadLIO l m | m -> l where   -- | Lift an 'LIO' computation.   liftLIO :: LIO l a -> m a 

@@ -1,116 +1,504 @@ {-# LANGUAGE Trustworthy #-}-{-# LANGUAGE MultiParamTypeClasses,-             ConstraintKinds,-             TypeSynonymInstances #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE MultiParamTypeClasses #-}  {-|  /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".+encodes authority, secrecy restrictions, and integrity properties+using propositional logic. +A 'DCLabel' consists of two boolean formulas over 'Principal's.  Each+formula is in conjunctive normal form, represented by type 'CNF'.  The+first 'CNF' ('dcSecrecy') specifies what combinations of principals+are allowed to make data public.  The second 'CNF' ('dcIntegrity')+specifies which combinations of principals have endorsed the integrity+of the data.++The '%%' operator allows one to construct a 'DCLabel' by joining a+secrecy 'CNF' on the left with an integrity 'CNF' on the right.  A+'DCLabel' can also be directly constructed with the constructor+'DCLabel'.  However, '%%' has the added convenience of accepting any+argument types that are instances of 'ToCNF'.++For example, the following expresses data that can be exported by the+principal \"Alice\" and may have been written by anybody:  @\"Alice\"+'%%' 'True'@.  (@'toCNF' 'True'@ indicates a trivially satisfiable+label component, which in this case means a label conveying no+integrity properties.)++A 'CNF' is created using the ('\/') and ('/\') operators.  The+disjunction operator ('\/') is used to compute a 'CNF' equivalent to+the disjunciton of two 'Principal's, 'Strings', or 'CNF's. For+example:++  @+p1 = 'principal' \"p1\"+p2 = 'principal' \"p2\"+p3 = 'principal' \"p3\"+e1 = p1 '\/' p2+e2 = e1 '\/' \"p4\"+  @++Similarly, the conjunction operator ('/\') creates 'CNF' as a+conjunction of 'Principal's, 'String's, 'Disjunction's, or 'CNF's.++  @+e3 = p1 '\/' p2+e4 = e1 '/\' \"p4\" '/\' p3+  @++Note that because a 'CNF' formula is stored as a conjunction of+'Disjunction's, it is much more efficient to apply '/\' to the result+of '\/' than vice versa.  It would be logical for '/\' to have higher+fixity than '\/'.  Unfortunately, this makes formulas harder to read+(given the convention of AND binding more tightly than OR).  Hence+'\/' and '/\' have been given the same fixity but different+associativities, preventing the two from being mixed in the same+expression without explicit parentheses.++Consider the following, example:++  @+cnf1 = (\"Alice\" '\/' \"Bob\") '/\' \"Carla\"+cnf2 = \"Alice\" '/\' \"Carla\"+dc1 = cnf1 '%%' cnf2+dc2 = \"Djon\" '%%' \"Alice\"+pr = PrivTCB $ \"Alice\" '/\' \"Carla\"+  @++This will result in the following:++>>> dc1+"Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla"+>>> dc2+"Djon" %% "Alice"+>>> canFlowTo dc1 dc2+False+>>> canFlowToP pr dc1 dc2+True+ -}  module LIO.DCLabel (-  -- ** Principals-    Principal(..), principal-  -- ** Clauses-  , Clause, clause-  -- ** Components-  , Component, dcTrue, dcFalse, dcFormula-  , isTrue, isFalse-  -- ** Labels-  , DCLabel, dcSecrecy, dcIntegrity, dcLabel-  , dcPub, dcTop, dcBottom-  -- ** Privileges-  , module LIO.DCLabel.Privs-  -- ** DSL-  , module LIO.DCLabel.DSL-  -- * Synonyms for "LIO"-  -- $dcMonad-  , DCState, defaultState-  , DC, evalDC, runDC, tryDC-  , MonadDC-  -- ** Labeled values-  , DCLabeled-  -- ** Labeled references-  , DCRef-  -- ** Gates-  , DCGate+  -- * Top-level aliases and functions+    DC, DCPriv, DCLabeled, dcDefaultState, evalDC, tryDC+  -- * Main types and functions+  , Principal, principalBS, principal+  , DCLabel(..), dcPublic, (%%), (/\), (\/)+  , CNF, ToCNF(..)+  -- * Lower-level functions+  , principalName+  , Disjunction, dToSet, dFromList+  , cTrue, cFalse, cToSet, cFromList   ) where -import qualified Control.Exception as IO+import safe Control.Applicative+import safe Data.Bits+import safe qualified Data.ByteString as S+import Data.Hashable+import safe Data.List+import safe Data.Monoid+import safe Data.Set (Set)+import safe qualified Data.Set as Set+import safe Data.String+import safe Data.Typeable+import safe Data.Word+import safe Text.Read -import LIO.Core-import LIO.Labeled-import LIO.Privs-import LIO.LIORef-import LIO.DCLabel.Core-import LIO.DCLabel.Privs-import LIO.DCLabel.DSL+import safe LIO.Exception (SomeException)+import safe LIO.Core+import safe LIO.Label+import safe LIO.Labeled+import safe LIO.Run +type SetTag = Word64+ ----- LIO synonyms+-- Principals -- +-- | A @Principal@ is a primitive source of authority, represented as+-- a string.  The interpretation of principal strings is up to the+-- application.  Reasonable schemes include encoding user names,+-- domain names, and/or URLs in the 'Principal' type.+data Principal = Principal !S.ByteString {-# UNPACK #-} !SetTag+                 deriving (Ord, Typeable) --- | DC 'Labeled' values.-type DCLabeled = Labeled DCLabel+instance Show Principal where+  showsPrec _ (Principal n _) = shows n --- | DC Labeled 'LIORef's.-type DCRef a = LIORef DCLabel a+instance Read Principal where+  readsPrec d s = do+    (name, rest) <- readsPrec d s+    return (principalBS name, rest) +instance Eq Principal where+  (Principal n1 t1) == (Principal n2 t2) = t1 == t2 && n1 == n2 --- | DC 'Gate'.-type DCGate = Gate DCPrivDesc+-- | Extract the name of a principal as a strict 'S.ByteString'.+-- (Use 'show' to get it as a regular 'String'.)+principalName :: Principal -> S.ByteString+{-# INLINE principalName #-}+principalName (Principal n _) = n +-- | Create a principal from a strict 'S.ByteString'.+principalBS :: S.ByteString -> Principal+principalBS bs = Principal bs bloom+  where hv = hash bs+        bloom = bit (hv .&. 0x3f)+                .|. (bit $ shiftR hv 6 .&. 0x3f)+                .|. (bit $ shiftR hv 12 .&. 0x3f)++-- | Create a principal from a 'String'.  The 'String' is packed into+-- a 'S.ByteString' using 'fromString', which will almost certainly+-- give unexpected results for non-ASCII unicode code points.+principal :: String -> Principal+principal = principalBS . fromString+ ----- DC monad+-- Disjunctive clauses (a.k.a. "disjunction categories") -- -{- $dcMonad+-- | Represents a disjunction of 'Principal's, or one clause of a+-- 'CNF'.  There is generally not much need to work directly with+-- @Disjunction@s unless you need to serialize and de-serialize them+-- (by means of 'dToSet' and 'dFromList').+data Disjunction = Disjunction !(Set Principal) {-# UNPACK #-} !SetTag+                   deriving (Typeable) -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'.+-- | Expose the set of 'Principal's being ORed together in a+-- 'Disjunction'.+dToSet :: Disjunction -> Set Principal+dToSet (Disjunction ps _) = ps --}+instance Eq Disjunction where+  (Disjunction ps1 t1) == (Disjunction ps2 t2) = t1 == t2 && ps1 == ps2 --- | Type synonym for 'MonadLIO'.-type MonadDC m = MonadLIO DCLabel m+instance Ord Disjunction where+  compare (Disjunction ps1 _) (Disjunction ps2 _) =+    case compare (Set.size ps1) (Set.size ps2) of+      EQ -> compare ps1 ps2+      o  -> o --- | 'LIOState' with underlying label being 'DCLabel'-type DCState = LIOState DCLabel+instance Show Disjunction where+  showsPrec _ (Disjunction ps _)+    | Set.size ps == 0 = ("False" ++)+    | Set.size ps == 1 = shows $ Set.findMin ps+    | otherwise = showParen True $+        foldr1 (\l r -> l . (" \\/ " ++) . r) $ map shows $ Set.toList ps --- | 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 = dcTop }+-- | Note that a disjunction containing more than one element /must/+-- be surrounded by parentheses to parse correctly.+instance Read Disjunction where+  readPrec = false <++ clause <++ single+    where false = do False <- readPrec; return dFalse+          single = dSingleton <$> readPrec+          clause = parens $ prec minPrec $ do+            let next = do Symbol "\\/" <- lexP+                          liftA2 (:) readPrec next+                       <++ pure []+            dFromList <$> liftA2 (:) readPrec next --- | The monad for LIO computations using 'DCLabel' as the label.+instance Monoid Disjunction where+  mempty = dFalse+  mappend = dUnion++dFalse :: Disjunction+dFalse = Disjunction Set.empty 0++dSingleton :: Principal -> Disjunction+dSingleton p@(Principal _ t) = Disjunction (Set.singleton p) t++dUnion :: Disjunction -> Disjunction -> Disjunction+dUnion (Disjunction ps1 t1) (Disjunction ps2 t2) =+  Disjunction (Set.union ps1 ps2) (t1 .|. t2)++-- | Convert a list of 'Principal's into a 'Disjunction'.+dFromList :: [Principal] -> Disjunction+dFromList pl = Disjunction (Set.fromList pl) tres+  where tres = foldl' (\tl (Principal _ tr) -> tl .|. tr) 0 pl++-- | Returns 'True' iff the first disjunction is a subset of the second.+dImplies :: Disjunction -> Disjunction -> Bool+dImplies (Disjunction ps1 t1) (Disjunction ps2 t2)+  | t1 .&. t2 /= t1 = False+  | otherwise       = ps1 `Set.isSubsetOf` ps2++--+-- Conjunctive Normal Form (CNF) Formulas+--++-- | A boolean formula in Conjunctive Normal Form.  @CNF@ is used to+-- describe 'DCLabel' privileges, as well to provide each of the two+-- halves of a 'DCLabel'.+newtype CNF = CNF (Set Disjunction) deriving (Eq, Ord, Typeable)++-- | Convert a 'CNF' to a 'Set' of 'Disjunction's.  Mostly useful if+-- you wish to serialize a 'DCLabel'.+cToSet :: CNF -> Set Disjunction+{-# INLINE cToSet #-}+cToSet (CNF ds) = ds++instance Show CNF where+  showsPrec d (CNF ds)+    | Set.size ds == 0 = ("True" ++)+    | Set.size ds == 1 = shows $ Set.findMin ds+    | otherwise = showParen (d > 7) $+        foldr1 (\l r -> l . (" /\\ " ++) . r) $ map shows $ Set.toList ds++instance Read CNF where+  readPrec = true <++ formula <++ single+    where true = do True <- readPrec; return cTrue+          single = cSingleton <$> readPrec+          formula = parens $ prec 7 $ do+            let next = do Symbol "/\\" <- lexP+                          liftA2 (:) readPrec next+                       <++ pure []+            cFromList <$> liftA2 (:) readPrec next++instance Monoid CNF where+  mempty = cTrue+  mappend = cUnion+  +-- | A 'CNF' that is always @True@--i.e., trivially satisfiable.  When+-- @'dcSecrecy' = cTrue@, it means data is public.  When+-- @'dcIntegrity' = cTrue@, it means data carries no integrity+-- guarantees.  As a description of privileges, @cTrue@ conveys no+-- privileges; @'canFlowToPrivDesc' cTrue l1 l2@ is equivalent to+-- @'canFlowTo' l1 l2@.+--+-- Note that @'toCNF' 'True' = cTrue@.  Hence @'dcPublic' = 'DCLabel'+-- cTrue cTrue@.+cTrue :: CNF+cTrue = CNF $ Set.empty++-- | A 'CNF' that is always @False@.  If @'dcSecrecy' = cFalse@, then+-- no combination of principals is powerful enough to make the data+-- public.  For that reason, @cFalse@ generally shouldn't appear in a+-- data label.  However, it is convenient to include as the+-- 'dcSecrecy' component of 'lioClearance' to indicate a thread may+-- arbitrarily raise its label.+--+-- @'dcIntegrity' = cFalse@ indicates impossibly much integrity--i.e.,+-- data that no combination of principals is powerful enough to modify+-- or have created.  Generally this is not a useful concept.+--+-- As a privilege description, @cFalse@ indicates impossibly high+-- privileges (i.e., higher than could be achieved through any+-- combination of 'Principal's).  @cFalse ``speaksFor`` p@ for any+-- 'CNF' @p@.  This can be a useful concept for bootstrapping+-- privileges within the 'DC' monad itself.  For instance, the result+-- of @'privInit' cFalse@ can be passed to fully-trusted 'DC' code,+-- which can in turn use 'delegate' to create arbitrary finite+-- privileges to pass to less privileged code.+cFalse :: CNF+cFalse = CNF $ Set.singleton dFalse++cSingleton :: Disjunction -> CNF+cSingleton = CNF . Set.singleton++setAny :: (a -> Bool) -> Set a -> Bool+setAny prd = Set.foldr' (\a -> (prd a ||)) False++setAll :: (a -> Bool) -> Set a -> Bool+setAll prd = Set.foldr' (\a -> (prd a &&)) True++cInsert :: Disjunction -> CNF -> CNF+cInsert dnew c@(CNF ds)+  | setAny (`dImplies` dnew) ds = c+  | otherwise = CNF $ Set.insert dnew $ Set.filter (not . (dnew `dImplies`)) ds++cUnion :: CNF -> CNF -> CNF+cUnion c (CNF ds) = Set.foldr cInsert c ds++cOr :: CNF -> CNF -> CNF+cOr (CNF ds1) (CNF ds2) =+  cFromList $ [dUnion d1 d2 | d1 <- Set.toList ds1, d2 <- Set.toList ds2]++-- | Convert a list of 'Disjunction's into a 'CNF'.  Mostly useful if+-- you wish to de-serialize a 'CNF'.+cFromList :: [Disjunction] -> CNF+cFromList = Set.foldr cInsert cTrue . Set.fromList++cImplies1 :: CNF -> Disjunction -> Bool+cImplies1 (CNF ds) d = setAny (`dImplies` d) ds++cImplies :: CNF -> CNF -> Bool+cImplies c (CNF ds) = setAll (c `cImplies1`) ds++--+-- DCLabel+--++-- | Main DCLabel type.  @DCLabel@s use 'CNF' boolean formulas over+-- principals to express authority exercised by a combination of+-- principals.  A @DCLabel@ contains two 'CNF's.  One, 'dcSecrecy',+-- specifies the minimum authority required to make data with the+-- label completely public.  The second, 'dcIntegrity', expresses the+-- minimum authority that was used to endorse data with the label, or,+-- for mutable objects, the minimum authority required to modify the+-- object.+--+-- @DCLabel@s are more conveniently expressed using the '%%' operator,+-- with 'dcSecrecy' on the left and 'dcIntegrity' on the right, i.e.:+-- @(@/dcSecrecyValue/ '%%' /dcIntegrityValue/@)@.+--+-- @DCLabel@s enforce the following relations:+--+--   * If @cnf1@ and @cnf2@ are 'CNF's describing authority, then+--   @cnf1 ``speaksFor`` cnf2@ if and only if @cnf1@ logically implies+--   @cnf2@ (often written @cnf1 &#x27f9; cnf2@).  For example,+--   @(\"A\" '/\' \"B\") ``speaksFor`` 'toCNF' \"A\"@, while @'toCNF'+--   \"A\" ``speaksFor`` (\"A\" '\/' \"C\")@.+--+--   * Given two @DCLabel@s @dc1 = (s1 '%%' i1)@ and @dc2 = (s2 '%%'+--   i2)@, @dc1 ``canFlowTo`` dc2@ (often written @dc1@ &#8849; @dc2@)+--   if and only if @s2 ``speaksFor`` s1 && i1 ``speaksFor`` i2@.  In+--   other words, data can flow in the direction of requiring more+--   authority to make it public or removing integrity endorsements.+--+--   * Given two @DCLabel@s @dc1 = (s1 '%%' i1)@ and @dc 2 = (s2 '%%'+--   i2)@, and a @p::'CNF'@ representing privileges,+--   @'canFlowToPrivDesc' p dc1 dc2@ (often written @dc1@+--   &#8849;&#8346; @dc2@) if and only if @(p '/\' s2) ``speaksFor``+--   s2 && (p '/\' i1) ``speaksFor`` i2@.+data DCLabel = DCLabel { dcSecrecy :: !CNF+                         -- ^ Describes the authority required to make+                         -- the data public.+                       , dcIntegrity :: !CNF+                         -- ^ Describes the authority with which+                         -- immutable data was endorsed, or the+                         -- authority required to modify mutable data.+                       } deriving (Eq, Ord, Typeable)++instance Show DCLabel where+  showsPrec d (DCLabel sec int) =+    showParen (d > 5) $ shows sec . (" %% " ++) . shows int++instance Read DCLabel where+  readPrec = parens $ prec 5 $ do+    sec <- readPrec+    Symbol "%%" <- lexP+    int <- readPrec+    return $ DCLabel sec int++-- |+-- > dcPublic = True %% True+--+-- This label corresponds to public data with no integrity guarantees.+-- For instance, an unrestricted Internet socket should be labeled+-- @dcPublic@.  The significance of @dcPublic@ is that given data+-- labeled @(s %% i)@, @s@ is the exact minimum authority required to+-- transition the data to @dcPublic@.  Conversely, given data labeled+-- @dcPublic@, @i@ is the exact authority required to transition the+-- data to @(s %% i)@ (assuming sufficient clearance).+dcPublic :: DCLabel+dcPublic = True %% True++-- | As a type, a 'CNF' is always a conjunction of 'Disjunction's of+-- 'Principal's.  However, mathematically speaking, a single+-- 'Principal' or single 'Disjunction' is also a degenerate example of+-- conjunctive normal form.  Class 'ToCNF' abstracts over the+-- differences between these types, promoting them all to 'CNF'.+class ToCNF c where toCNF :: c -> CNF+instance ToCNF CNF where toCNF = id+instance ToCNF (Priv CNF) where toCNF = privDesc+instance ToCNF Disjunction where toCNF = cSingleton+instance ToCNF Principal where toCNF = toCNF . dSingleton+instance ToCNF [Char] where toCNF = toCNF . principal+instance ToCNF Bool where+  toCNF True = cTrue+  toCNF False = cFalse++-- | The primary way of creating a 'DCLabel'.  The secrecy component+-- goes on the left, while the integrity component goes on the right,+-- e.g.:+--+-- > label = secrecyCNF %% integrityCNF+--+-- Unlike the 'DCLabel' constructor, the arguments can be any instance+-- of 'ToCNF'.  @%%@ has fixity:+--+-- > infix 6 %%+(%%) :: (ToCNF a, ToCNF b) => a -> b -> DCLabel+a %% b = toCNF a `DCLabel` toCNF b+infix 6 %%++-- | Compute a conjunction of two 'CNF's or 'ToCNF' instances.+--+-- Has fixity:+--+-- > infixr 7 /\+(/\) :: (ToCNF a, ToCNF b) => a -> b -> CNF+a /\ b = toCNF a `cUnion` toCNF b+infixr 7 /\++-- | Compute a disjunction of two 'CNF's or 'ToCNF' instances.  Note+-- that this can be an expensive operation if the inputs have many+-- conjunctions.+--+-- The fixity is specifically chosen so that @&#92;&#47;@ and '/\'+-- cannot be mixed in the same expression without parentheses:+--+-- > infixl 7 \/+(\/) :: (ToCNF a, ToCNF b) => a -> b -> CNF+a \/ b = toCNF a `cOr` toCNF b+infixl 7 \/++instance Label DCLabel where+  lub (DCLabel s1 i1) (DCLabel s2 i2) = DCLabel (cUnion s1 s2) (cOr i1 i2)+  glb (DCLabel s1 i1) (DCLabel s2 i2) = DCLabel (cOr s1 s2) (cUnion i1 i2)+  canFlowTo (DCLabel s1 i1) (DCLabel s2 i2) = cImplies s2 s1 && cImplies i1 i2++instance SpeaksFor CNF where+  {-# INLINE speaksFor #-}+  speaksFor = cImplies++dcMaxDowngrade :: CNF -> DCLabel -> DCLabel+dcMaxDowngrade p (DCLabel (CNF ds) int) = DCLabel sec (cUnion p int)+  where sec = CNF $ Set.filter (not . cImplies1 p) ds++instance PrivDesc DCLabel CNF where+  downgradeP = dcMaxDowngrade+  canFlowToP p (DCLabel s1 i1) (DCLabel s2 i2) =+    cImplies (cUnion p s2) s1 && cImplies (cUnion p i1) i2++--+-- Type aliases+--++-- | A common default starting state, where @'lioLabel' = 'dcPublic'@+-- and @'lioClearance' = False '%%' True@ (i.e., the highest+-- possible clearance).+dcDefaultState :: LIOState DCLabel+dcDefaultState = LIOState { lioLabel = dcPublic+                          , lioClearance = False %% True }++-- | The main monad type alias to use for 'LIO' computations that are+-- specific to 'DCLabel's. type DC = LIO DCLabel +-- | 'DCLabel' privileges are expressed as a 'CNF' of the principals+-- whose authority is being exercised.+type DCPriv = Priv CNF --- | Evaluate computation in the 'DC' monad.-evalDC :: DC a -> IO a-evalDC act = evalLIO act defaultState+-- | An alias for 'Labeled' values labeled with a 'DCLabel'.+type DCLabeled = Labeled DCLabel --- | Evaluate computation in the 'DC' monad.-runDC :: DC a -> IO (a, DCState)-runDC act = runLIO act defaultState+-- | Wrapper function for running @'LIO' 'DCLabel'@ computations.+--+-- @+-- evalDC dc = 'evalLIO' dc 'dcDefaultState'+-- @+evalDC :: DC a -> IO a+evalDC dc = evalLIO dc dcDefaultState --- | Similar to 'evalLIO', but catches any exceptions thrown by--- untrusted code with 'throwLIO'.-tryDC :: DC a -> IO (Either IO.SomeException a, DCState)-tryDC act = runDC act >>= tryit-  where tryit (a, s) = do-          ea <- IO.try (IO.evaluate a)-          return (ea, s)+-- | 'DCLabel' wrapper for 'tryLIO':+--+-- @+-- tryDC dc = 'tryLIO' dc 'dcDefaultState'+-- @+tryDC :: DC a -> IO (Either SomeException a, LIOState DCLabel)+tryDC dc = tryLIO dc dcDefaultState

@@ -1,318 +0,0 @@-{-# LANGUAGE Safe #-}-{-# LANGUAGE DeriveDataTypeable #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-|--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, dcTop, dcBottom-  -- * Internal-  , dcReduce, dcImplies-  , dcAnd, dcOr-  ) where--import qualified Data.ByteString.Char8 as S8-import Data.List (intercalate)-import Data.Monoid-import Data.Set (Set)-import qualified Data.Set as Set-import Data.Typeable--import LIO.Label-import LIO.Privs------- 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.ByteString-                                -- ^ Get the principal name.-                              } deriving (Eq, Ord, Typeable)--instance Show Principal where-  showsPrec _ = shows . principalName---- | Generate a principal from a 'String'.  (To create one from a--- 'S8.ByteString', just use the 'Principal' constructor directly.)-principal :: String -> Principal-principal = Principal . S8.pack------- Category - disjunction clauses------- | 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@(Clause uc)-         | Set.size uc == 1 = show . head . Set.toList $ uc-         | otherwise =-              let ps = map show . Set.toList $! unClause c-              in parens . intercalate " \\/ " $! ps-    where parens x = "(" ++ x ++ ")"---- | Clause constructor-clause :: Set Principal -> Clause-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 = show False-         | isTrue c  = show True-         | otherwise = let cs = map show . Set.toList $! unDCFormula c-                       in intercalate " /\\ " $! cs---- | Privileges can be combined using 'mappend'-instance Monoid Component where-  mempty = dcTrue-  mappend p1 p2 = dcReduce $! p1 `dcAnd` p2--instance PrivDesc DCLabel Component where-  canFlowToPrivDesc pd l1 l2-           | pd == dcTrue = canFlowTo l1 l2-           | otherwise =-    let i1 = dcReduce $ dcIntegrity l1 `dcAnd` pd-        s2 = dcReduce $ dcSecrecy l2   `dcAnd` pd-    in l1 { dcIntegrity = i1 } `canFlowTo` l2 { dcSecrecy = s2 }--  partDowngradePrivDesc pd la lg-               | pd == mempty  = la `lub` lg-               | pd == dcFalse = lg-               | otherwise = -    let sec_a  = dcSecrecy la-        int_a  = dcIntegrity la-        sec_g  = dcSecrecy   lg-        int_g  = dcIntegrity lg-        sec_a' = dcFormula . Set.filter f $ unDCFormula sec_a-        sec_res  = if isFalse sec_a-                then sec_a-                else sec_a' `dcAnd` sec_g-        int_res  = (pd `dcAnd` int_a) `dcOr` int_g-    in dcLabel sec_res int_res-      where f c = not $ pd `dcImplies` (dcFormula . Set.singleton $ c)------ | Logical @True@.-dcTrue :: Component-dcTrue = DCFormula Set.empty---- | 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 -  showsPrec d l = showParen (d > 5) $-    let s = dcSecrecy l-        i = dcIntegrity l-    in showsPrec (d + 1) s . showString " %% " . showsPrec (d + 1) i---- | @dcLabel secrecyComponent integrityComponent@ creates a label,--- reducing each component 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 the most secret--- and least trustworthy data.--- @dcTop = \< False, True \> @.-dcTop :: DCLabel-dcTop = dcLabel dcFalse dcTrue---- | Element in the DCLabel lattice corresponding to the least secret--- and most trustworthy data.--- @dcTop = \< True, False \> @.-dcBottom :: DCLabel-dcBottom = dcLabel dcTrue dcFalse---- | Element in the DCLabel lattice corresponding to public data.--- @dcPub = \< True, True \> @. This corresponds to data that is not--- secret nor trustworthy.-dcPub :: DCLabel-dcPub = DCLabel { dcSecrecy = dcTrue, dcIntegrity = dcTrue }------- Bounded by \< True, False \> and \< False, True \>----instance Bounded DCLabel where-  minBound = dcBottom-  maxBound = dcTop------- Lattice operations-----instance Label DCLabel where-  -- | 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

@@ -1,182 +0,0 @@-{-# LANGUAGE Safe #-}-{-# LANGUAGE FlexibleInstances #-}--{-|-  This module implements a simple, embedded domain specific language-  to create 'Component's, privilage descriptions and labels from-  conjunctions of principal disjunctions.--  A 'DCLabel' consists of a secrecy 'Component' and an integrity-  'Component'.  The '%%' operator allows one to construct a 'DCLabel'-  by joining a secrecy 'Component' (on the left) with an integrity-  'Component' on the right.  This is similar to 'dcLabel', except that-  the arguments can also be instances of 'ToComponent'.  For example,-  the following expresses data that can be exported by the principal-  \"Alice\" and written by anybody:  @\"Alice\" '%%' 'True'@.  (The-  component 'True' or 'dcTrue' indicates a trivially satisfiable label-  component, which in this case means a label with no integrity-  guarantees.)--  A 'Component' or 'DCPrivDesc' is created using the ('\/') and ('/\')-  operators.  The disjunction operator ('\/') is used to create a-  'Clause' from 'Principal's, ByteStrings, or a disjunctive-  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 = PrivTCB $ toComponent $ \"Alice\" '/\' \"Carla\"-  @--  This will result in the following:-->>> dc1-"Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla"->>> dc2-"Djon" %% "Alice"->>> canFlowTo dc1 dc2-False->>> canFlowToP pr dc1 dc2-True---}--module LIO.DCLabel.DSL (-  -- * Operators-    (%%), (\/), (/\), ToComponent(..)-  , fromList, toList-  -- * Aliases-  , impossible, unrestricted-  ) where--import qualified Data.Set as Set--import LIO.Privs-import LIO.DCLabel.Core---- | Convert a type (e.g., 'Clause', 'Principal') to a label component.-class ToComponent a where-  -- | Convert to 'Component'-  toComponent :: a -> Component--infix 5 %%---- | Create a `DCLabel` from a secrecy `ToComponent` and integrity--- `ToComponent`. E.g.:------ @---   \"secrecy\" %% \"integrity\"--- @------ @--- infix 5 %%--- @-(%%) :: (ToComponent a, ToComponent b) => a -> b -> DCLabel-(%%) sec int = dcLabel (toComponent sec) (toComponent int)---- | Identity of 'Component'.-instance ToComponent Component where-  {-# INLINE toComponent #-}-  toComponent = id-instance ToComponent (Priv Component) where-  {-# INLINE toComponent #-}-  toComponent = privDesc--- | Convert singleton 'Clause' to 'Component'.-instance ToComponent Clause    where-  toComponent c = DCFormula $! Set.singleton c--- | Convert singleton 'Principal' to 'Component'.-instance ToComponent Principal where-  toComponent p = toComponent . Clause $! Set.singleton p---- | Convert singleton 'Principal' (in the form of a 'String')to 'Component'.-instance ToComponent String where-  toComponent = toComponent . principal--instance ToComponent Bool where-  {-# INLINE toComponent #-}-  toComponent True = DCFormula Set.empty-  toComponent False = DCFalse--infixl 7 \/-infixl 6 /\---- | Conjunction of two 'Principal'-based elements.--- --- @--- infixl 6 /\--- @----(/\) :: (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, hence impossible to express:------ > impossible = dcFalse----impossible :: Component-impossible = dcFalse---- | Logical truth can be thought of as the component containing--- no specific principal, hence imposing no restrictions:------ > unrestricted = dcTrue----unrestricted :: Component-unrestricted = dcTrue---- | Convert a 'Component' to a list of list of 'Principal's if the--- 'Component' does not have the value 'DCFalse'. In the latter case--- the function returns an exception.-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

@@ -1,78 +0,0 @@-{-# LANGUAGE Trustworthy #-}-{- |--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 qualified Data.Set as Set--import LIO-import LIO.DCLabel.Core-import LIO.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@.-type DCPriv = Priv DCPrivDesc------- Helpers------- | The empty privilege, or no privileges, corresponds to logical--- @True@.-noPriv :: DCPriv-noPriv = PrivTCB 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 $! PrivTCB 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,130 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE DeriveDataTypeable #-}++-- | This module provides two functions useful for delegating+-- privileges.  The 'delegate' function creates a 'Priv' value less+-- powerful than an existing one.  'Gate's provide a mechanism for+-- authenticating calls to closures that embed privileges.+module LIO.Delegate (+    -- * Delegating privileges+    delegate+    -- * Gates+    -- $gateIntro+  , Gate, gate, callGate+    -- ** Gate example+    -- $gateExample+  ) where++import safe Data.Typeable++import safe LIO.Error+import safe LIO.Label+import LIO.TCB++-- | @delegate@ allows you to create a new privilege object that is+-- less powerful than an existing privilege object.  The first+-- argument supplies actual privileges.  The second argument is a+-- 'PrivDesc' describing the desired new privileges.  The call throws+-- an exception unless the privileges supplied 'speaksFor' the+-- privileges requested.+--+-- Note:  If you are looking for a way to create privileges /more/+-- powerful than ones you already have, you can use the 'mappend'+-- function to combine existing privileges.+delegate :: (SpeaksFor p) => Priv p -> p -> Priv p+delegate p1 p2+  | privDesc p1 `speaksFor` p2 = PrivTCB p2+  | otherwise                  = insufficientPrivs "delegate" p1 p2++{- $gateIntro++LIO provides a basic implementation of /gates/, useful in providing+controlled RPC-like services where the client and service provider are+in mutual distrust. ++A service provider uses 'gate' to create a gate data type @'Gate' p a@+given a computation of type @p -> a@. Here, @p@ 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 @p@.  In effect, this+allows a client to \"prove\" to the service provider that they own+certain privileges without entrusting the service with its privileges.+The gate computation can analyze this privilege description before+performing the \"actual\" computation.  The client and server solely+need to trust the implementation of 'callGate'.++-}+++-- | A Gate is a lambda abstraction from a privilege description to an+-- arbitrary type @a@. Applying the gate is accomplished with 'callGate'+-- which takes a privilege argument that is converted to a description+-- before invoking the gate computation.+newtype Gate p a = GateTCB (p -> a) deriving Typeable+-- Note GateTCB is trusted by convention.  Anyone with access to the+-- symbol can call any gate while claiming arbitrary privileges.  In+-- the absence of gates, however, GateTCB doesn't provide any+-- particular privileges.++-- | Create a gate given a computation from a privilege description.+-- Note that because of currying type 'a' may itself be a function+-- type and thus gates can take arguments in addition to the privilege+-- descriptoin.+gate :: (p -> a)  -- ^ Gate computation+     -> Gate p a+{-# INLINE gate #-}+gate = GateTCB++-- | Given a gate and privilege, execute the gate computation.  It is+-- important to note that @callGate@ invokes the gate computation with+-- the privilege description and /NOT/ the privilege itself.+--+-- Note that, in general, code should /not/ provide privileges to+-- functions other than @callGate@ when wishing to call a gate. This+-- function is provided by LIO since it can be easily inspected by+-- both the gate creator and caller to be doing the \"right\" thing:+-- provide the privilege description corresponding to the supplied+-- privilege as \"proof\" without explicitly passing in the privilege.+-- +callGate :: Gate p a -- ^ Gate+         -> Priv p   -- ^ Privilege used as proof-of-ownership+         -> a+{-# INLINE callGate #-}+callGate (GateTCB g) = g . privDesc++{- $gateExample++This example uses "LIO.DCLabel" to demonstrate the use of gates.  The+service provider provides @addGate@ which adds two integers if the+gate is called by a piece of code that owns the \"Alice\" or \"Bob\"+principals. Otherwise, it simply returns @Nothing@.  Though 'privInit'+(in "LIO.Run#v:privInit") allows us to create arbitrary privileges in+the 'IO' monad, the gate restricts access to @addGate@ from within the+'LIO' monad where code cannot create arbitrary privileges.++> import LIO+> import LIO.DCLabel+> import LIO.Run+> +> -- | Add two numbers if the computation is invoked by Alice or Bob.+> addGate :: Gate CNF (Int -> Int -> Maybe Int)+> addGate = gate $ \pd a b ->+>   if pd `speaksFor` "Alice" \/ "Bob"+>   then Just $ a + b+>   else Nothing+> +> main :: IO ()+> main = do+>   alice <- privInit $ toCNF $ "Alice"+>   bob <- privInit $ toCNF $ "Bob"+>   clark <- privInit $ toCNF $ "Clark"+>   putStrLn . show $ [+>       callGate addGate alice 1 2 -- Just 3+>     , callGate addGate bob   3 4 -- Just 7+>     , callGate addGate clark 5 6 -- Nothing+>     ]+> ++-}+

@@ -0,0 +1,173 @@+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE DeriveDataTypeable #-}+{-# LANGUAGE ExistentialQuantification #-}++{- |++This module exports exception types thrown in response to label+failures.  In addition, it provides 'withContext', a function that+annotates any exceptions in the 'AnyLabelError' hierarchy that are+thrown within a given scope.  These annotations should be used to add+function names to exceptions, so as to make it easier to pinpoint the+cause of a label error.++-}++module LIO.Error (+    Annotatable(..), withContext+  , AnyLabelError(..), lerrToException, lerrFromException+  , GenericPrivDesc(..), LabelError(..),  labelError, labelErrorP+  , InsufficientPrivs(..), insufficientPrivs+  , ResultExceedsLabel(..)+  ) where++import safe qualified Control.Exception as IO+import safe Data.Typeable++import safe LIO.Exception+import safe LIO.Label+import LIO.TCB++-- | Class of error messages that can be annotated with context.+class Annotatable e where+  annotate :: String -> e -> e++-- | Parent of all label-related exceptions.+data AnyLabelError = forall e. (Exception e, Annotatable e) =>+                     AnyLabelError e deriving Typeable++instance Show AnyLabelError where+  showsPrec d (AnyLabelError e) = showsPrec d e++instance Annotatable AnyLabelError where+  annotate s (AnyLabelError e) = AnyLabelError $ annotate s e++instance Exception AnyLabelError++-- | Executes an action with a context string which will be added to+-- any label exception thrown.+-- +-- Note: this function wraps an action with a 'catch', and thus may+-- incur a small runtime cost (though it is well under 100 ns on+-- machines we benchmarked).+withContext :: String -> LIO l a -> LIO l a+withContext ctx (LIOTCB act) =+  LIOTCB $ \st -> act st `IO.catch` \e ->+  IO.throwIO $ annotate ctx (e :: AnyLabelError)++-- | Definition of 'toException' for children of 'AnyLabelError' in+-- the exception hierarchy.+lerrToException :: (Exception e, Annotatable e) => e -> SomeException+lerrToException = toException . AnyLabelError++-- | Definition of 'fromException' for children of 'AnyLabelError' in+-- the exception hierarchy.+lerrFromException :: (Exception e) => SomeException -> Maybe e+lerrFromException se = do+  AnyLabelError e <- fromException se+  cast e+++-- | A generic privilege description for recording relevant privileges+-- in exceptions.+data GenericPrivDesc l = forall p. (PrivDesc l p) => GenericPrivDesc p+instance Show (GenericPrivDesc l) where+  showsPrec d (GenericPrivDesc p) = showsPrec d p+++-- | Main error type thrown by label failures in the 'LIO' monad.+data LabelError l = LabelError {+    lerrContext :: [String] -- ^ Annotation of where the failure happened.+  , lerrFailure :: String   -- ^ Actual function that failed.+  , lerrCurLabel :: l       -- ^ Current label at time of error.+  , lerrCurClearance :: l   -- ^ Current clearance at time of error.+  , lerrPrivs :: [GenericPrivDesc l] -- ^ Any privileges involved in error.+  , lerrLabels :: [l]       -- ^ Any labels involved in error.+  } deriving (Show, Typeable)++instance Annotatable (LabelError l) where+  annotate a e = e { lerrContext = a : lerrContext e }++instance Label l => Exception (LabelError l) where+  toException = lerrToException+  fromException = lerrFromException++-- | Throw a label-error exception.+labelError :: (Label l) => String -- ^ Function that failed.+                        -> [l]    -- ^ Labels involved in error.+                        -> LIO l a+labelError fl ls = do+  st <- getLIOStateTCB+  throwLIO LabelError {+      lerrContext = []+    , lerrFailure = fl+    , lerrCurLabel = lioLabel st+    , lerrCurClearance = lioClearance st+    , lerrPrivs = []+    , lerrLabels = ls+    }++-- | Throw a label-error exception.+labelErrorP :: (Label l, PrivDesc l p) => String  -- ^ Function that failed.+                                       -> Priv p  -- ^ Privileges involved.+                                       -> [l]     -- ^ Labels involved.+                                       -> LIO l a+labelErrorP fl p ls = do+  st <- getLIOStateTCB+  throwLIO LabelError {+      lerrContext = []+    , lerrFailure = fl+    , lerrCurLabel = lioLabel st+    , lerrCurClearance = lioClearance st+    , lerrPrivs = [GenericPrivDesc $ privDesc p]+    , lerrLabels = ls+    }+++-- | Error indicating insufficient privileges (independent of the+-- current label).  This exception is thrown by 'delegate', and+-- should also be thrown by gates that receive insufficient privilege+-- descriptions (see "LIO.Delegate").+data InsufficientPrivs = forall p. (SpeaksFor p) => InsufficientPrivs {+    inspContext :: [String]+  , inspFailure :: String+  , inspSupplied :: p+  , inspNeeded :: p+  } deriving (Typeable)++instance Show InsufficientPrivs where+  showsPrec _ (InsufficientPrivs c l s n) =+    ("InsufficientPrivs { inspContext = " ++) . shows c .+    (", inspLocation = " ++) . shows l .+    (", inspSupplied = " ++) . shows s .+    (", inspNeeded = " ++) . shows n .+    (" }" ++)++instance Annotatable InsufficientPrivs where+  annotate a e = e { inspContext = a : inspContext e }++instance Exception InsufficientPrivs where+  toException = lerrToException+  fromException = lerrFromException++-- | Raise 'InsufficientPrivs' error.+insufficientPrivs :: (SpeaksFor p) => String -> Priv p -> p -> a+insufficientPrivs fl supplied needed =+  IO.throw $ InsufficientPrivs [] fl (privDesc supplied) needed+++-- | Error raised when a computation spawned by 'lFork' terminates+-- with its current label above the label of the result.+data ResultExceedsLabel l = ResultExceedsLabel {+    relContext :: [String]+  , relLocation :: String+  , relDeclaredLabel :: l+  , relActualLabel :: Maybe l+  } deriving (Show, Typeable)++instance Annotatable (ResultExceedsLabel l) where+  annotate a e = e { relContext = a : relContext e }++instance (Label l) => Exception (ResultExceedsLabel l) where+  toException = lerrToException+  fromException = lerrFromException

@@ -21,14 +21,15 @@   , onException, finally, bracket, evaluate   ) where -import Control.Exception (Exception(..), SomeException(..))-import qualified Control.Exception as IO-import Control.Monad-import Data.Typeable+import safe Control.Exception (Exception(..), SomeException(..))+import safe qualified Control.Exception as IO+import safe Control.Monad+import safe Data.Typeable  import LIO.TCB-import LIO.Label+import safe LIO.Label +-- | Throw an exception. throwLIO :: Exception e => e -> LIO l a throwLIO = ioTCB . IO.throwIO @@ -40,8 +41,8 @@ -- exceeding the clarance, and an exception is always thrown at the -- time this happens.) catch :: (Label l, Exception e) => LIO l a -> (e -> LIO l a) -> LIO l a-catch io h =-  LIOTCB $ \s -> unLIOTCB io s `IO.catch` \e -> unLIOTCB (safeh e) s+catch (LIOTCB io) h =+  LIOTCB $ \s -> io s `IO.catch` \e -> case safeh e of LIOTCB ioe -> ioe s   where uncatchableType = typeOf (undefined :: UncatchableTCB)         safeh e@(SomeException einner) = do           when (typeOf einner == uncatchableType) $ throwLIO e

@@ -28,10 +28,11 @@   , atomicModifyLIORef, atomicModifyLIORefP   ) where -import Data.IORef-import LIO.Core-import LIO.Label-import LIO.Privs+import safe Data.IORef++import safe LIO.Core+import safe LIO.Error+import safe LIO.Label import LIO.TCB import LIO.TCB.LObj @@ -55,13 +56,17 @@           => l                  -- ^ Label of reference           -> a                  -- ^ Initial value           -> LIO l (LIORef l a) -- ^ Mutable reference-newLIORef = newLIORefP noPrivs+newLIORef l a = do+  withContext "newLIORef" $ guardAlloc l+  ioTCB (LObjTCB l `fmap` newIORef a)  -- | 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 :: PrivDesc l p => Priv p -> l -> a -> LIO l (LIORef l a)-newLIORefP p l a = guardAllocP p l >> ioTCB (LObjTCB l `fmap` newIORef a)+newLIORefP p l a = do+  withContext "newLIORefP" $ guardAllocP p l+  ioTCB (LObjTCB l `fmap` newIORef a)  -- -- Read 'LIORef's@@ -71,14 +76,18 @@ -- 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.+-- guard) use 'labelOf' to check that a read will succeed. readLIORef :: Label l => LIORef l a -> LIO l a-readLIORef (LObjTCB l r) = taint l >> ioTCB (readIORef r)+readLIORef (LObjTCB l r) = do+  withContext "readLIORef" $ taint l+  ioTCB (readIORef r)  -- | Same as 'readLIORef' except @readLIORefP@ takes a privilege object -- which is used when the current label is raised. readLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> LIO l a-readLIORefP p (LObjTCB l r) = taintP p l >> ioTCB (readIORef r)+readLIORefP p (LObjTCB l r) = do+  withContext "readLIORefP" $ taintP p l+  ioTCB (readIORef r)  -- -- Write 'LIORef's@@ -89,13 +98,17 @@ -- label of the reference can-flow-to the current clearance. Otherwise, -- an exception is raised by the underlying 'guardAlloc' guard. writeLIORef :: Label l => LIORef l a -> a -> LIO l ()-writeLIORef (LObjTCB l r) a = guardAlloc l >> ioTCB (writeIORef r a)+writeLIORef (LObjTCB l r) a = do+  withContext "writeLIORef" $ guardAlloc l+  ioTCB (writeIORef r a)  -- | Same as 'writeLIORef' except @writeLIORefP@ takes a set of -- privileges which are accounted for in comparing the label of -- the reference to the current label and clearance. writeLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> a -> LIO l ()-writeLIORefP p (LObjTCB l r) a = guardAllocP p l >> ioTCB (writeIORef r a)+writeLIORefP p (LObjTCB l r) a = do+  withContext "writeLIORefP" $ guardAllocP p l+  ioTCB (writeIORef r a)  -- -- Modify 'LIORef's@@ -113,14 +126,18 @@              =>  LIORef l a            -- ^ Labeled reference              -> (a -> a)               -- ^ Modifier              -> LIO l ()-modifyLIORef (LObjTCB l r) f = guardAlloc l >> ioTCB (modifyIORef r f)+modifyLIORef (LObjTCB l r) f = do+  withContext "modifyLIORef" $ guardAlloc l+  ioTCB (modifyIORef r f)  -- | Same as 'modifyLIORef' except @modifyLIORefP@ takes a set of -- privileges which are accounted for in comparing the label of -- the reference to the current label and clearance. modifyLIORefP :: PrivDesc l p               =>  Priv p -> LIORef l a -> (a -> a) -> LIO l ()-modifyLIORefP p (LObjTCB l r) f = guardAllocP p l >> ioTCB (modifyIORef r f)+modifyLIORefP p (LObjTCB l r) f = do+  withContext "modifyLIORefP" $ guardAllocP p l+  ioTCB (modifyIORef r f)  -- | Atomically modifies the contents of an 'LIORef'. It is required -- that the label of the reference be above the current label, but@@ -132,11 +149,11 @@ -- which will raise an exception if any of the IFC conditions cannot -- be satisfied. atomicModifyLIORef :: Label l => LIORef l a -> (a -> (a, b)) -> LIO l b-atomicModifyLIORef = blessTCB atomicModifyIORef+atomicModifyLIORef = blessTCB "atomicModifyIORef" atomicModifyIORef  -- | Same as 'atomicModifyLIORef' except @atomicModifyLIORefP@ takes -- a set of privileges which are accounted for in label comparisons. atomicModifyLIORefP :: PrivDesc l p                     => Priv p -> LIORef l a -> (a -> (a, b)) -> LIO l b-atomicModifyLIORefP = blessPTCB atomicModifyIORef+atomicModifyLIORefP = blessPTCB "atomicModifyLIORefP" atomicModifyIORef 

@@ -1,141 +1,264 @@-{-# LANGUAGE Safe #-}-{- | +{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DeriveDataTypeable #-} -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@ so as to prevent-a piece of LIO code from accessing anything above @L_clear@.+module LIO.Label (+  -- * Labels+  -- $Labels+    Label(..)+  -- * Privileges+  -- $Privileges+  , SpeaksFor(..), PrivDesc(..)+  , Priv, privDesc+  -- * Empty privileges+  , NoPrivs(..), noPrivs+  ) where -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@.+import safe Data.Monoid+import safe Data.Typeable -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.+import LIO.TCB -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').+{- $Labels -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.+Labels are a way of describing who can observe and modify data.+Labels are governed by a partial order, generally pronounced \"can+flow to.\"  In LIO, we write this relation ``canFlowTo``.  In the+literature, it is usually written &#8849;. --}+At a high level, the purpose of this whole library is to ensure that+data labeled @l1@ may affect data labeled @l2@ only if @l1+``canFlowTo`` l2@.  The 'LIO' monad (see "LIO.Core") ensures this by+keeping track of a /current label/ of the executing thread (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 and will throw an exception in the event that an+operation would violate information flow restrictions. -module LIO.Label (-  -- * Labels-    Label(..)-  -- * Accessing label of labeled values- , LabelOf(..) - ) where+The specific invariant maintained by 'LIO' is, first, that labels on+all previously observed data must flow to a thread's current label.+Second, the current label must flow to the labels of any future+objects the thread will be allowed to modify.  Hence, after a thread+with current label @lcur@ observes data labeled @l1@, it must hold+that @l1 ``canFlowTo`` lcur@.  If the thread is later permitted to+modify an object labeled @l2@, it must hold that @lcur ``canFlowTo``+l2@.  By transitifity of the ``canFlowTo`` relation, it holds that @l1+``canFlowTo` l2@. +-} --- | 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) => Label l where-  -- | /Least/ upper bound, or join, of two labels. For any two labels-  -- @L_1@ and @L_2@, if @L_3 = L_1 \`lub` L_2@, it must be that:+-- | This class defines the operations necessary to make a label into+-- a lattice (see <http://en.wikipedia.org/wiki/Lattice_(order)>).+-- 'canFlowTo' partially orders labels.+-- 'lub' and 'glb' compute the least upper bound and greatest lower+-- bound of two labels, respectively.+class (Eq l, Show l, Typeable l) => Label l where+  -- | Compute the /least upper bound/, or join, of two labels.  When+  -- data carrying two different labels is mixed together in a+  -- document, the @lub@ of the two labels is the lowest safe value+  -- with which to label the result.   ---  -- * @L_1 ``canFlowTo`` L_3@,+  -- More formally, for any two labels @l1@ and @l2@, if @ljoin = l1+  -- \`lub` l2@, it must be that:   ---  -- * @L_2 ``canFlowTo`` L_3@, and+  -- * @L_1 ``canFlowTo`` ljoin@,   ---  -- * 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.+  -- * @L_2 ``canFlowTo`` ljoin@, and+  --+  -- * There is no label @l /= ljoin@ such that @l1 ``canFlowTo`` l@,+  --   @l2 ``canFlowTo`` l@, and @l ``canFlowTo`` ljoin@.  In other+  --   words @ljoin@ is the least element to which both @l1@ and @l2@+  --   can flow.+  --+  -- When used infix, has fixity:+  --+  -- > infixl 5 `lub`   lub :: l -> l -> l-  -- | /Greatest/ lower bound, or meet, of two labels. For any two labels-  -- @L_1@ and @L_2@, if @L_3 = L_1 \`glb` L_2@, it must be that:++  -- | /Greatest lower bound/, or meet, of two labels. For any two+  -- labels @l1@ and @l2@, if @lmeet = l1 \`glb` l2@, it must be+  -- that:   ---  -- * @L_3 ``canFlowTo`` L_1@,+  -- * @lmeet ``canFlowTo`` l1@,   ---  -- * @L_3 ``canFlowTo`` L_2@, and+  -- * @lmeet ``canFlowTo`` l2@, 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.+  -- * There is no label @l /= lmeet@ such that @l ``canFlowTo`` l1@,+  --   @l ``canFlowTo`` l2@, and @lmeet ``canFlowTo`` l@.  In other+  --   words @lmeet@ is the greatest element flowing to both @l1@ and+  --   @l2@.+  --+  -- When used infix, has fixity:+  --+  -- > infixl 5 `glb`   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++  -- | /Can-flow-to/ relation (&#8849;). An entity labeled @l1@ should+  -- be allowed to affect an entity @l2@ only if @l1 \`canFlowTo`+  -- l2@. 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:+  -- satisfy the following laws:   ---  -- * Reflexivity: @L_1 \`canFlowTo` L_1@ for any @L_1@.+  -- * Reflexivity: @l1 \`canFlowTo` l1@ for any @l1@.   ---  -- * Antisymmetry: If @L_1 \`canFlowTo` L_2@ and-  --   @L_2 \`canFlowTo` L_1@ then @L_1 = L_2@.+  -- * Antisymmetry: If @l1 \`canFlowTo` l2@ and+  --   @l2 \`canFlowTo` l1@ then @l1 = l2@.   ---  -- * Transitivity: If @L_1 \`canFlowTo` L_2@ and-  --   @L_2 \`canFlowTo` L_3@ then @L_1 \`canFlowTo` L_3@.+  -- * Transitivity: If @l1 \`canFlowTo` l2@ and+  --   @l2 \`canFlowTo` l3@ then @l1 \`canFlowTo` l3@.+  --+  -- When used infix, has fixity:+  --+  -- > infix 4 `canFlowTo`   canFlowTo :: l -> l -> Bool --- | 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 :: t l a -> l+infixl 5 `lub`, `glb`+infix 4 `canFlowTo`++{- $Privileges ++Privileges are objects the possesion of which allows code to bypass+certain label protections.  An instance of class 'PrivDesc' describes+a pre-order (see <http://en.wikipedia.org/wiki/Preorder>) among labels+in which certain unequal labels become equivalent.  A 'Priv' object+containing a 'PrivDesc' instance allows code to make those unequal+labels equivalent for the purposes of many library functions.+Effectively, a 'PrivDesc' instance /describes/ privileges, while a+'Priv' object /embodies/ them.++Any code is free to construct 'PrivDesc' values describing arbitrarily+powerful privileges.  Security is enforced by preventing safe code+from accessing the constructor for 'Priv' (called 'PrivTCB').  Safe+code can construct arbitrary privileges from the 'IO' monad (using+'privInit' in "LIO.Run#v:privInit"), but cannot do so from the 'LIO'+monad.  Starting from existing privileges, safe code can also+'delegate' lesser privileges (see "LIO.Delegate#v:delegate").++Privileges allow you to behave as if @l1 ``canFlowTo`` l2@ even when+that is not the case, but only for certain pairs of labels @l1@ and+@l2@; which pairs depends on the specific privileges.  The process of+allowing data labeled @l1@ to infulence data labeled @l2@ when @(l1+``canFlowTo`` l2) == False@ is known as /downgrading/.++The core privilege function is 'canFlowToP', which performs a+more permissive can-flow-to check by exercising particular privileges+(in literature this relation is commonly written @&#8849;&#8346;@ for+privileges @p@).  Most core 'LIO' function have variants ending @...P@+that take a privilege argument to act in a more permissive way.++By convention, all 'PrivDesc' instances should also be instances of+'Monoid', allowing privileges to be combined with 'mappend', though+this is not enforced with superclasses.++-}+++-- | Turns privileges into a powerless description of the privileges+-- by unwrapping the 'Priv' newtype.+privDesc :: Priv a -> a+{-# INLINE privDesc #-}+privDesc (PrivTCB a) = a++-- | Every privilege type must be an instance of 'SpeaksFor', which+-- specifies when one privilege value is more powerful than another.+-- If you do not wish to allow delegation, you can simply define+-- @'speaksFor' _ _ = False@.+class (Typeable p, Show p) => SpeaksFor p where+  -- | @speaksFor p1 p2@ returns 'True' iff @p1@ subsumes all the+  -- privileges of @p2@.  In other words, it is safe for 'delegate' to+  -- hand out @p2@ to a caller who already has @p1@.+  --+  -- Has fixity:+  --+  -- > infix 4 `speaksFor`+  speaksFor :: p -> p -> Bool++infix 4 `speaksFor`++-- | This class represents privilege descriptions, which define a+-- pre-order on labels in which distinct labels become equivalent.+-- The pre-oder implied by a privilege description is specified by the+-- method 'canFlowToP'.  In addition, this this class defines a method+-- 'downgradeP', which is important for finding least labels+-- satisfying a privilege equivalence.+--+-- Minimal complete definition: 'downgradeP'.+--+-- (The 'downgradeP' requirement represents the fact that a generic+-- 'canFlowToP' can be implemented efficiently in terms of+-- 'downgradeP', but not vice-versa.)+class (Label l, SpeaksFor p) => PrivDesc l p where+-- Note: SpeaksFor is a superclass for security reasons.  Were it not+-- a superclass, then if a label format ever failed to define+-- SpeaksFor, or defined it in a different module from the PrivDesc+-- instance, then an attacker could produce an vacuous instance that+-- allows all delegation.++    -- | Privileges are described in terms of a pre-order on labels in+    -- which sets of distinct labels become equivalent.  @downgradeP p+    -- l@ returns the lowest of all labels equivalent to @l@ under+    -- privilege description @p@.+    --+    -- Less formally, @downgradeP p l@ returns a label representing+    -- the furthest you can downgrade data labeled @l@ given+    -- privileges described by @p@.+    --+    -- Yet another way to view this function is that @downgradeP p l@+    -- returns the greatest lower bound (under 'canFlowTo') of the set+    -- of all labels @l'@ such that @'canFlowToP' p l' l@.+    downgradeP :: p     -- ^ Privilege description+                  -> l  -- ^ Label to downgrade+                  -> l  -- ^ Lowest label equivelent to input++    -- | @canFlowToP p l1 l2@ determines whether @p@ describes+    -- sufficient privileges to observe data labeled @l1@ and+    -- subsequently write it to an object labeled @l2@.  The function+    -- returns 'True' if and only if either @canFlowTo l1 l2@ or @l1+    -- and l2@ are equivalent under @p@.+    --+    -- The default definition is:+    --+    -- > canFlowToP p l1 l2 = downgradeP p l1 `canFlowTo` l2+    -- +    -- @canFlowToP@ is a method rather than a function so that it can+    -- be optimized in label-specific ways.  However, custom+    -- definitions should behave identically to the default.+    canFlowToP :: p -> l -> l -> Bool+    canFlowToP p l1 l2 = downgradeP p l1 `canFlowTo` l2++instance (SpeaksFor p) => SpeaksFor (Priv p) where+  {-# INLINE speaksFor #-}+  speaksFor p1 p2 = privDesc p1 `speaksFor` privDesc p2++instance (PrivDesc l p) => PrivDesc l (Priv p) where+  {-# INLINE downgradeP #-}+  downgradeP = downgradeP . privDesc+  {-# INLINE canFlowToP #-}+  canFlowToP = canFlowToP . privDesc++--+-- NoPrivs+--++-- | Generic 'PrivDesc' used to denote the lack of privileges.  Works+-- with any 'Label' type.  This is only a privilege description; a+-- more useful symbol is 'noPrivs', which actually embodies the+-- @NoPrivs@ privilege.+data NoPrivs = NoPrivs deriving (Show, Read, Typeable)++instance SpeaksFor NoPrivs where speaksFor _ _ = True++-- | 'downgradeP' 'NoPrivs' is the identify function.  Hence+-- 'canFlowToP' 'NoPrivs' is the same as 'canFlowTo'.+instance Label l => PrivDesc l NoPrivs where downgradeP _ l = l++instance Monoid NoPrivs where+  mempty      = NoPrivs+  mappend _ _ = NoPrivs++-- | 'Priv' object corresponding to 'NoPrivs'.+noPrivs :: Priv NoPrivs+noPrivs = PrivTCB NoPrivs+

@@ -1,7 +1,4 @@ {-# LANGUAGE Trustworthy #-}-{-# LANGUAGE CPP,-             ConstraintKinds,-             FlexibleContexts #-}  {- | @@ -20,31 +17,30 @@ 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+inspection ('relabelLabeledP', 'taintLabeled').  A 'Functor'-like class ('LabeledFunctor') on 'Labeled' is also defined in this module.  -}  module LIO.Labeled (-    Labeled+    Labeled, LabelOf(..)   -- * Label values   , label, labelP   -- * Unlabel values   , unlabel, unlabelP   -- * Relabel values   , relabelLabeledP-  , taintLabeled, taintLabeledP , untaintLabeledP+  , taintLabeled, taintLabeledP    , lFmap, lAp   ) where -import Control.Monad+import safe Control.Monad -import LIO.Exception+import safe LIO.Error+import safe LIO.Label+import safe LIO.Core import LIO.TCB-import LIO.Label-import LIO.Core-import LIO.Privs  -- -- Label values@@ -56,7 +52,9 @@ -- ``canFlowTo`` l && l ``canFlowTo`` ccurrent@. Otherwise an -- exception is thrown (see 'guardAlloc'). label :: Label l => l -> a -> LIO l (Labeled l a)-label = labelP noPrivs+label l a = do+  withContext "label" $ guardAlloc l+  return $ LabeledTCB l a  -- | Constructs a 'Labeled' using privilege to allow the `Labeled`'s -- label to be below the current label.  If the current label is@@ -68,7 +66,7 @@ -- current clearance. labelP :: PrivDesc l p => Priv p -> l -> a -> LIO l (Labeled l a) labelP p l a = do-  guardAllocP p l+  withContext "labelP" $ guardAllocP p l   return $ LabeledTCB l a  --@@ -87,14 +85,14 @@ -- However, you can use 'labelOf' to check if 'unlabel' will succeed -- without throwing an exception. unlabel :: Label l => Labeled l a -> LIO l a-unlabel = unlabelP noPrivs+unlabel (LabeledTCB l v) = withContext "unlabel" (taint l) >> return v  -- | 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 :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a-unlabelP p (LabeledTCB l v) = taintP p l >> return v+unlabelP p (LabeledTCB l v) = withContext "unlabelP" (taintP p l) >> return v  -- -- Relabel values@@ -113,8 +111,9 @@ relabelLabeledP :: PrivDesc l p                 => Priv p -> l -> Labeled l a -> LIO l (Labeled l a) relabelLabeledP p newl (LabeledTCB oldl v) = do-  guardAllocP p newl-  unless (canFlowToP p oldl newl) $ throwLIO InsufficientPrivs+  withContext "relabelLabeledP" $ guardAllocP p newl+  unless (canFlowToP p oldl newl) $+    labelErrorP "relabelLabeledP" p [oldl, newl]   return $ LabeledTCB newl v  -- | Raises the label of a 'Labeled' to the 'upperBound' of it's current@@ -124,7 +123,10 @@ -- the supplied label is not bounded then @taintLabeled@ will throw an -- exception (see 'guardAlloc'). taintLabeled :: Label l => l -> Labeled l a -> LIO l (Labeled l a)-taintLabeled = taintLabeledP noPrivs+taintLabeled l (LabeledTCB lold v) = do+  let lnew = lold `lub` l+  withContext "taintLabeled" $ guardAlloc lnew+  return $ LabeledTCB lnew v  -- | Same as 'taintLabeled', but uses privileges when comparing the -- current label to the supplied label. In other words, this function@@ -134,16 +136,9 @@               => Priv p -> l -> Labeled l a -> LIO l (Labeled l a) taintLabeledP p l (LabeledTCB lold v) = do   let lnew = lold `lub` l-  guardAllocP p lnew+  withContext "taintLabeledP" $ guardAllocP p lnew   return $ LabeledTCB lnew v --- | Downgrades a label.-untaintLabeledP :: PrivDesc l p-                => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)-untaintLabeledP p target lv =-  relabelLabeledP p (partDowngradeP p (labelOf lv) target) lv-- {- $functor  Making 'Labeled' an instance of 'Functor' is problematic because:@@ -174,7 +169,7 @@   -- Result label is joined with current label   let lnew = lold `lub` l   -- `label` checks for clearance violation then labels-  label lnew $ f v+  withContext "lFmap" $ label lnew $ f v   -- | Similar to 'ap', apply function (wrapped by 'Labeled') to the@@ -185,4 +180,4 @@ lAp (LabeledTCB lf f) (LabeledTCB la a) = do   l <- getLabel   let lnew = l `lub` lf `lub` la-  label lnew $ f a+  withContext "lAp" $ label lnew $ f a

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

@@ -9,10 +9,13 @@ -- use in invoking 'LIO' code.  The functions are also available via -- "LIO" and "LIO.Core", but those modules will clutter your namespace -- with symbols you don't need in the 'IO' monad.-module LIO.Run (LIOState(..), runLIO, evalLIO) where+module LIO.Run (LIOState(..), runLIO, tryLIO, evalLIO, privInit) where -import Control.Exception-import Data.IORef+import safe Control.Exception+import safe Data.IORef+import safe Data.Typeable++import safe LIO.Label import LIO.TCB  -- | Execute an 'LIO' action, returning its result and the final label@@ -28,8 +31,18 @@   s1 <- readIORef sp   return (a, s1) +-- | A variant of 'runLIO' that returns results in 'Right' and+-- exceptions in 'Left', much like the standard library 'try'+-- function.+tryLIO :: LIO l a -> LIOState l -> IO (Either SomeException a, LIOState l)+tryLIO lio s0 = runLIO lio s0 >>= tryit+  where tryit (a, s) = do+          ea <- try (evaluate a)+          return (ea, s)++ -- | Given an 'LIO' computation and some initial state, return an IO--- action which when executed will perform the IFC-safe LIO+-- action which, when executed, will perform the IFC-safe LIO -- computation. -- -- Because untrusted code cannot execute 'IO' computations, this function@@ -45,3 +58,21 @@   (a, _) <- runLIO lio s   return $! a +-- | Initialize some privileges (within the 'IO' monad) that can be+-- passed to 'LIO' computations run with 'runLIO' or 'evalLIO'.  This+-- is a pure function, but the result is encapsulated in 'IO' to+-- make the return value inaccessible from 'LIO' computations.+--+-- Note the same effect can be achieved using the 'PrivTCB'+-- constructor, but 'PrivTCB' is easier to misuse and is only available by+-- importing "LIO.TCB".+privInit :: (SpeaksFor p) => p -> IO (Priv p)+privInit p | isPriv p  = fail "privInit called on Priv object"+           | otherwise = return $ PrivTCB p++-- | Uses dynamic typing to return 'True' iff the type of the argument+-- is @'Priv' a@ (for any @a@).  Mostly useful to prevent users from+-- accidentally wrapping 'Priv' objects inside other 'Priv' objects.+isPriv :: (Typeable p) => p -> Bool+isPriv p = typeRepTyCon (typeOf p) == privcon+  where privcon = typeRepTyCon $ typeOf noPrivs

@@ -4,21 +4,16 @@  {- |  -This module exports --* The definition of the 'LIO' monad and relevant trusted state-  access/modifying functions.--* Various other types whose constructors are privileged and must be-  hidden from untrusted code.--* Uncatchable exceptions used to pop threads out of the 'LIO' monad-  unconditionally.--* Combinators for executing 'IO' actions within the 'LIO' monad.+This module exports symbols that must be accessible only to trusted+code.  By convention, the names of such symbols always end+\"@...TCB@\" (short for \"trusted computing base\").  In many cases, a+type is safe to export while its constructor is not.  Hence, only the+constructor ends \"@TCB@\", while the type is re-exported to safe code+(without constructors) to from "LIO.Core". -The documentation and external, safe 'LIO' interface is provided in-"LIO.Core".+Security rests on the fact that untrusted code must be compiled with+@-XSafe@.  Because this module is flagged unsafe, it cannot be+imported from safe modules.  -} @@ -26,26 +21,26 @@   -- * LIO monad     LIOState(..), LIO(..)   -- ** Accessing internal state-  , getLIOStateTCB, putLIOStateTCB, modifyLIOStateTCB, updateLIOStateTCB +  , getLIOStateTCB, putLIOStateTCB, modifyLIOStateTCB   -- * Executing IO actions   , ioTCB   -- * Privileged constructors-  , Priv(..), Labeled(..)+  , Priv(..), Labeled(..), LabelOf(..)   -- * Uncatchable exception type   , UncatchableTCB(..), makeCatchable-  -- * Trusted 'Show' and 'Read'-  , ShowTCB(..), ReadTCB(..)+  -- * Trusted 'Show'+  , ShowTCB(..)+  -- * 'LabeledResult's+  , LabeledResult(..), LResStatus(..)   ) where -import Control.Applicative-import Control.Exception (Exception(..), SomeException(..))-import Control.Monad-import Data.Monoid-import Data.IORef-import Data.Typeable-import Text.Read (minPrec)--import LIO.Label+import safe Control.Applicative+import safe Control.Exception (Exception(..), SomeException(..))+import safe qualified Control.Concurrent as IO+import safe Control.Monad+import safe Data.Monoid+import safe Data.IORef+import safe Data.Typeable  -- -- LIO Monad@@ -56,31 +51,26 @@                            , 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 :: IORef (LIOState l) -> IO a-  } deriving (Typeable)+-- | The @LIO@ monad is a wrapper around 'IO' that keeps track of a+-- /current label/ and /current clearance/.  Safe code cannot execute+-- arbitrary 'IO' actions from the 'LIO' monad.  However, trusted+-- runtime functions can use 'ioTCB' to perform 'IO' actions (which+-- they should only do after appropriately checking labels).+newtype LIO l a = LIOTCB (IORef (LIOState l) -> IO a) deriving (Typeable)  instance Monad (LIO l) where   {-# INLINE return #-}   return = LIOTCB . const . return   {-# INLINE (>>=) #-}-  m >>= k = LIOTCB $ \s -> do-    a <- unLIOTCB m s-    unLIOTCB (k a) s+  (LIOTCB ma) >>= k = LIOTCB $ \s -> do+    a <- ma s+    case k a of LIOTCB mb -> mb s   fail = LIOTCB . const . fail  instance Functor (LIO l) where-  {-# INLINE fmap #-}-  fmap f ma = LIOTCB $ \s -> unLIOTCB ma s >>= return . f+  fmap f (LIOTCB a) = LIOTCB $ \s -> a s >>= return . f+-- fmap typically isn't inlined, so we don't inline our definition,+-- but we do define it in terms of >>= and return (which are inlined)  instance Applicative (LIO l) where   {-# INLINE pure #-}@@ -105,24 +95,19 @@ putLIOStateTCB s = LIOTCB $ \sp -> writeIORef sp $! s  -- | Update the internal state given some function.-modifyLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()+modifyLIOStateTCB :: (LIOState l -> LIOState l) -> LIO l () {-# INLINE modifyLIOStateTCB #-} modifyLIOStateTCB f = do   s <- getLIOStateTCB   putLIOStateTCB (f s) -{-# DEPRECATED updateLIOStateTCB "Use modifyLIOStateTCB instead" #-}-updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()-updateLIOStateTCB = modifyLIOStateTCB- -- -- 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 'rethrowIoTCB'.+-- | Lifts an 'IO' computation into the 'LIO' monad.  This function is+-- dangerous and should only be called after appropriate checks ensure+-- the 'IO' computation will not violate IFC policy. ioTCB :: IO a -> LIO l a {-# INLINE ioTCB #-} ioTCB = LIOTCB . const@@ -131,13 +116,14 @@ -- Exception handling -- --- | An uncatchable exception hierarchy use to terminate an untrusted--- thread.  Wrap the uncatchable exception in 'UncatchableTCB' before--- throwing it to the thread.  'runLIO' will subsequently unwrap the--- 'UncatchableTCB' constructor.+-- | An uncatchable exception hierarchy is used to terminate an+-- untrusted thread.  Wrap the uncatchable exception in+-- 'UncatchableTCB' before throwing it to the thread.  'runLIO' will+-- subsequently unwrap the 'UncatchableTCB' constructor. -- -- Note this can be circumvented by 'IO.mapException', which should be--- made unsafe.+-- made unsafe. In the interim, auditing untrusted code for this is+-- necessary. data UncatchableTCB = forall e. (Exception e) =>                       UncatchableTCB e deriving (Typeable) @@ -159,10 +145,13 @@ -- Privileges -- --- | A newtype wrapper that can be used by trusted code to bless--- privileges.  Privilege-related functions are defined in--- "LIO.Privs", but the constructor, 'PrivTCB', allows one to mint--- arbitrary privileges and hence must be located in this file.+-- | A newtype wrapper that can be used by trusted code to transform a+-- powerless description of privileges into actual privileges.  The+-- constructor, 'PrivTCB', is dangerous as it allows creation of+-- arbitrary privileges.  Hence it is only exported by the unsafe+-- module "LIO.TCB".  A safe way to create arbitrary privileges is to+-- call 'privInit' (see "LIO.Run#v:privInit") from the 'IO' monad+-- before running your 'LIO' computation. newtype Priv a = PrivTCB a deriving (Show, Eq, Typeable)  instance Monoid p => Monoid (Priv p) where@@ -177,53 +166,75 @@ --  -- | @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.)+-- a pure value of type @a@. Labeled values allow users to label data+-- with a label other than the current label.  Note that 'Labeled' is+-- an instance of 'LabelOf', which means that only the /contents/ of a+-- labeled value (the type @t@) is kept secret, not the label.  Of+-- course, if you have a @Labeled@ within a @Labeled@, then the label+-- on the inner value will be protected by the outer label. data Labeled l t = LabeledTCB !l t deriving Typeable -- Note: t cannot be strict if we want things like lFmap. +-- | Trusted 'Show' instance.+instance (Show l, Show a) => ShowTCB (Labeled l a) where+    showTCB (LabeledTCB l a) = show a ++ " {" ++ show l ++ "}"++-- | 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 labeled value or object.  Note the label+  -- must be the second to last type constructor argument.+  labelOf :: t l a -> l+ instance LabelOf Labeled where+  {-# INLINE labelOf #-}   labelOf (LabeledTCB l _) = l --- | Trusted 'Show' instance.-instance (Label l, Show a) => ShowTCB (Labeled l a) where-    showTCB (LabeledTCB l t) = show t ++ " {" ++ show l ++ "}"+--+-- Trusted 'Show'+-- --- | Trusted 'Read' instance.-instance (Label l, Read l, Read a) => ReadTCB (Labeled l a) where-  readsPrecTCB _ str = do (val, str1) <- reads str-                          ("{", str2) <- lex str1-                          (lab, str3) <- reads str2-                          ("}", rest) <- lex str3-                          return (LabeledTCB lab val, rest)+-- | It would be a security issue to make certain objects members of+-- the 'Show' class.  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 + ----- Trusted 'Show' and 'Read'+-- LabeledResult -- --- | 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+-- | Status of a 'LabeledResult'.+data LResStatus l a = LResEmpty+                    | LResLabelTooHigh !l+                    | LResResult a+                      deriving (Show) --- | 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"+-- | A @LabeledResult@ encapsulates a future result from a computation+-- spawned by 'lFork' or 'lForkP'.  See "LIO.Concurrent" for a+-- description of the concurrency abstractions of LIO.+data LabeledResult l a = LabeledResultTCB {+    lresThreadIdTCB :: !IO.ThreadId+    -- ^ Thread executing the computation+  , lresLabelTCB :: !l+    -- ^ Label of the tresult+  , lresBlockTCB :: !(IO.MVar ())+  , lresStatusTCB :: !(IORef (LResStatus l a))+    -- ^ Result (when it is ready), or the label at which the thread+    -- terminated, if that label could not flow to 'lresLabelTCB'.+  }++instance LabelOf LabeledResult where+  labelOf = lresLabelTCB

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

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

@@ -27,25 +27,26 @@ -- around each 'Handle' using the 'LObjTCB' constructor. module LIO.TCB.LObj (LObj(..), blessTCB, blessPTCB, GuardIO(..)) where -import Data.Typeable+import safe Data.Typeable  import safe LIO.Core+import safe LIO.Error import safe LIO.Label-import safe LIO.Privs import LIO.TCB --- | A "@LObj label object@" is a wrapper around an IO abstraction of--- type @object@ (such as a file handle or socket) on which it is safe--- to do @IO@ operations in the 'LIO' monad when the caller can read--- and write a particular label.  It is the job of the trusted code--- constructing such a @LObj@ object to ensure both that the same IO--- object is only ever blessed with one label, and that the+-- | A \"@LObj label object@\" is a wrapper around an IO abstraction+-- of type @object@ (such as a file handle or socket) on which it is+-- safe to do @IO@ operations in the 'LIO' monad when the caller can+-- read and write a particular label.  It is the job of the trusted+-- code constructing such a @LObj@ object to ensure both that the same+-- IO object is only ever blessed with one label, and that the -- abstraction combined with its blessed IO operations (see -- 'blessTCB') cannot be used to communicate with code running at -- different labels. data LObj label object = LObjTCB !label !object deriving (Typeable)  instance LabelOf LObj where+  {-# INLINE labelOf #-}   labelOf (LObjTCB l _) = l  instance (Label l, Show t) => ShowTCB (LObj l t) where@@ -83,6 +84,7 @@   macro(a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10, \         a1 a2 a3 a4 a5 a6 a7 a8 a9 a10) +-- | Class for lifting 'IO' actions. class GuardIO l io lio | l io -> lio where   -- | Lifts an 'IO' action in the 'LIO' monad, executing a guard   -- before calling the function.@@ -101,17 +103,23 @@ -- one.  The 'LIO' version expects a 'LObj' argument, and before -- performing any IO uses 'guardWrite' to check that the current label -- can write the label in the 'LObj' object.+-- +-- The first argument should be the name of the function being defined+-- with @blessTCB@.  Its purpose is to enhance error reporting. -- -- Note that @io@ and @lio@ are function types (of up to nine -- arguments), which must be the same in all types except the monad. -- For example, if @io@ is @Int -> String -> IO ()@, then @lio@ must -- be @Int -> String -> LIO l ()@.-blessTCB :: (GuardIO l io lio, Label l) => (a -> io) -> (LObj l a) -> lio+blessTCB :: (GuardIO l io lio, Label l) =>+            String -> (a -> io) -> (LObj l a) -> lio {-# INLINE blessTCB #-}-blessTCB io (LObjTCB l a) = guardIOTCB (guardWrite l) (io a)+blessTCB name io (LObjTCB l a) =+  guardIOTCB (withContext name $ guardWrite l) (io a)  -- | A variant of 'blessTCB' that takes a privilege argument. blessPTCB :: (GuardIO l io lio, PrivDesc l p) =>-             (a -> io) -> Priv p -> (LObj l a) -> lio+             String -> (a -> io) -> Priv p -> (LObj l a) -> lio {-# INLINE blessPTCB #-}-blessPTCB io p (LObjTCB l a) = guardIOTCB (guardWriteP p l) (io a)+blessPTCB name io p (LObjTCB l a) =+  guardIOTCB (withContext name $ guardWriteP p l) (io a)

@@ -1,5 +1,5 @@ Name:           lio-Version:        0.10.0.0+Version:        0.11.0.0 Cabal-Version:  >= 1.8 Build-type:     Simple License:        GPL@@ -9,38 +9,49 @@ Synopsis:       Labeled IO Information Flow Control Library Category:       Security Description:+   The /Labeled IO/ (LIO) library is an information flow control (IFC)   library. IFC is a mechanism that enforces security policies by   tracking and controlling the flow of information within a system.-  Different from discretionary access control (think UNIX file-  permissions), with IFC you can execute an untrusted computation on-  your secret data and be sure that it does not leak it or overwrite-  it.+  Unlike discretionary access control (such as UNIX file permissions),+  IFC permits scenarios in which untrusted computation may have the+  ability to manipulate secret data without having the ability to+  further disclose that data.    .+   LIO is an IFC library that can be used to implement such untrusted-  computations. LIO provides combinators similar to those of 'IO' for-  performing side-effecting computations (e.g., accessing the-  filesystem, modifying mutable references, throwing exceptions, etc.)+  computations.  LIO provides combinators similar to those of 'IO' for+  performing side-effecting computations (e.g., modifying mutable+  references, forking threads, throwing and catching exceptions, etc.)   To track and control the flow of information, LIO associates a-  security policy, usually called a /label/, with every piece of data.-  A label may, for example, impose a restriction on who can observe,-  propagate, or modify the data labeled as such.  Different from-  standard IO operations, the LIO counterparts usually take an-  additional parameter for the label which they inspect before-  actually performing the (underlying IO) side-effecting computation.-  So, before writing to a file LIO asserts that the write will not-  violate any security policies associated with the file or the data-  to be written.+  security policy, called a /label/, with every piece of data.  A+  label may, for example, impose a restriction on who can observe,+  propagate, or modify the data to which it applies.  Unlike standard+  IO operations, the LIO counterparts check the vailidity of labels+  before performing the (underlying IO) side-effecting computation.+  For example, before writing to a labeled variable, LIO asserts that+  the write will not violate any security policies associated with the+  data to be written.    .    Most code should import module "LIO" and whichever label format the-  application is using (e.g., "LIO.DCLabel"). All untrusted code-  should have type 'LIO', which trusted code can safely execute with-  'evalLIO'. See "LIO" for a description of the core library API.+  application is using (e.g., "LIO.DCLabel" to use the format that+  ships with the library).  Side-effecting code should be specified as+  actions in the 'LIO' monad.  See "LIO.Core" for a description of the+  core library API, "LIO.Label" for a discussion of labels, and+  "LIO.Run" for functions allowing one to run an 'LIO' computation+  from the 'IO' monad. +  . +  WARNING:  For security, untrusted code must always be compiled with+  the @-XSafe@ and @-fpackage-trust@ /SafeHaskell/ flags. See+  <http://www.haskell.org/ghc/docs/latest/html/users_guide/safe-haskell.html>+  for more details on the guarantees provided by SafeHaskell.++ Extra-source-files:   examples/dclabel.hs   examples/gate.hs@@ -56,6 +67,7 @@     base          >= 4.5     && < 5.0    ,containers    ,bytestring+   ,hashable      >= 1.2    GHC-options: -Wall -fno-warn-orphans @@ -67,23 +79,19 @@     LIO.Label     -- * Core library     LIO.Core+    LIO.Error     LIO.Exception     -- * Labeled values     LIO.Labeled     -- * Labeled IORefs     LIO.LIORef     -- * LIO privileges-    LIO.Privs+    LIO.Delegate     -- * Concurrency     LIO.Concurrent     LIO.Concurrent.LMVar     -- * DCLabels     LIO.DCLabel-    LIO.DCLabel.Core-    LIO.DCLabel.Privs-    LIO.DCLabel.DSL     -- * Privileged internals     LIO.TCB     LIO.TCB.LObj-    LIO.TCB.Concurrent-    LIO.TCB.DCLabel