-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Labeled IO Information Flow Control Library
--
-- The Labeled IO (LIO) library provides information flow control
-- for incorporating untrusted code within Haskell applications. Most
-- code should import module LIO and whichever label type the
-- application is using (e.g., LIO.DCLabel). The core
-- functionality of the library is documented in LIO.TCB. LIO was
-- implemented by David Mazieres
-- (http://www.scs.stanford.edu/~dm/), Deian Stefan
-- (http://www.scs.stanford.edu/~deian/), Alejandro Russo
-- (http://www.cse.chalmers.se/~russo/) and John C. Mitchell
-- (http://www.stanford.edu/~jcm/). The extended version of our
-- paper, that includes the proofs is available here:
-- http://www.scs.stanford.edu/~deian/pubs/stefan:2011:flexible-ext.pdf.
-- The library depends on the DCLabel module. You can read more
-- on DC Labels here:
-- http://www.scs.stanford.edu/~deian/dclabels/.
@package lio
@version 0.1.3
-- | This module generalizes throw and catch (from
-- Control.Exception) to methods that can be defined on multiple
-- monads.
module LIO.MonadCatch
-- | MonadCatch is the class used to generalize the standard IO
-- catch and throwIO functions to methods that can be
-- defined in multiple monads. Minimal definition requires:
-- mask, throwIO, catch, and
-- onException.
class Monad m => MonadCatch m where mask_ io = mask $ \ _ -> io handle = flip catch onException io h = io `catch` \ e -> h >> throwIO (e :: SomeException) bracket = genericBracket onException bracket_ a b c = bracket a (const b) (const c) finally a b = mask $ \ restore -> do { r <- restore a `onException` b; _ <- b; return r }
mask :: MonadCatch m => ((forall a. m a -> m a) -> m b) -> m b
mask_ :: MonadCatch m => m a -> m a
throwIO :: (MonadCatch m, Exception e) => e -> m a
catch :: (MonadCatch m, Exception e) => m a -> (e -> m a) -> m a
handle :: (MonadCatch m, Exception e) => (e -> m a) -> m a -> m a
onException :: MonadCatch m => m a -> m b -> m a
bracket :: MonadCatch m => m b -> (b -> m c) -> (b -> m a) -> m a
bracket_ :: MonadCatch m => m a -> m b -> m c -> m c
finally :: MonadCatch m => m a -> m b -> m a
-- | Given some general onException function,
-- genericBracket allows you to execute an action with an
-- initial "acquire resource" and final "release resource" as
-- bracket of Control.Exception.
genericBracket :: MonadCatch m => (m b -> m c -> m b) -> m a -> (a -> m c) -> (a -> m b) -> m b
instance [safe] MonadCatch IO
-- | This module implements the core of the Labeled IO library for
-- information flow control in Haskell. It provides a monad, LIO,
-- that is intended to be used as a replacement for the IO monad in
-- untrusted code. The idea is for untrusted code to provide a
-- computation in the LIO monad, which trusted code can then
-- safely execute through the evalLIO function. (Though usually a
-- wrapper function is employed depending on the type of labels used by
-- an application. For example, with LIO.DCLabel, you would use
-- evalDC to execute an untrusted computation. There are also
-- abbreviations for the LIO monad type of a particular label--for
-- instance DC.)
--
-- A data structure Labeled (labeled value) protects access to
-- pure values. Without the appropriate privileges, one cannot produce a
-- pure value that depends on a secret Labeled, or conversely
-- produce a high-integrity Labeled based on pure data. The
-- function toLabeled allows one to seal off the results of an LIO
-- computation inside an Labeled without tainting the current flow
-- of execution. unlabel conversely allows one to use the value
-- stored within a Labeled.
--
-- We note that using toLabeled is not safe with respect to
-- the termination covert channel. Specifically, LIO with
-- toLabeled is only termination-insensitive non-interfering. For
-- a termination-sensitive toLabeled-like function, see
-- LIO.Concurrent.
--
-- Any code that imports this module is part of the Trusted Computing
-- Base (TCB) of the system. Hence, untrusted code must be prevented
-- from importing this module. The exported symbols ending
-- ...TCB can be used to violate label protections even from
-- within pure code or the LIO Monad. A safe subset of these symbols is
-- exported by the LIO.Safe module, which is how untrusted code
-- should access the core label functionality. (LIO.Safe is also
-- re-exported by LIO, the main gateway to this library.)
module LIO.TCB
-- | This class defines a label format, corresponding to a bounded lattice.
-- Specifically, it is necessary to define a bottom element lbot
-- (in literature, written as ⊥), a top element ltop (in
-- literature, written as ⊤), a join, or least upper bound, lub
-- (in literature, written as ⊔), a meet, or greatest lower bound,
-- glb (in literature, written as ⊓), and of course the
-- can-flow-to partial-order leq (in literature, written as ⊑).
class (Eq a, Show a, Read a, Typeable a) => Label a
lbot :: Label a => a
ltop :: Label a => a
lub :: Label a => a -> a -> a
glb :: Label a => a -> a -> a
leq :: Label a => a -> a -> Bool
-- | This class defines privileges and the more-permissive relation
-- (leqp) on labels using privileges. Additionally, it defines
-- lostar which is used to compute the smallest difference between
-- two labels given a set of privilege.
class (Label l, Monoid p, PrivTCB p) => Priv l p where leqp p a b = lostar p a b `leq` b
leqp :: Priv l p => p -> l -> l -> Bool
lostar :: Priv l p => p -> l -> l -> l
-- | Alias for mempty.
noPrivs :: Monoid p => p
-- | Returns the current privileges.
getPrivileges :: LabelState l p s => LIO l p s p
-- | Set the underlying privileges. Although this function is not unsafe,
-- it is not exported by LIO.Safe as it provides a higher security
-- risk. Users are encouraged to use withPrivileges.
setPrivileges :: LabelState l p s => p -> LIO l p s ()
-- | Execute an LIO action with a set of underlying privileges. Within a
-- withPrivileges block, the supplied privileges are used in
-- every even (non ...P) operation. For instance,
--
--
-- unlabelP p x
--
--
-- can instead be written as:
--
--
-- withPrivileges p $ unlabel x
--
--
-- The original privileges of the thread are restored after the action is
-- executed within the withPrivileges block. The
-- withPrivileges combinator provides a middle-ground between a
-- fully explicit, but safe, privilege use (...P combinators),
-- and an implicit, but less safe, interface (provide getter/setter, and
-- always use underlying privileges). It allows for the use of implicit
-- privileges by explicitly enclosing the code with a
-- withPrivileges block.
withPrivileges :: LabelState l p s => p -> LIO l p s a -> LIO l p s a
-- | Execute an LIO action with the combination of the supplied
-- privileges (usually passed to ...P functions) and current
-- privileges.
withCombinedPrivs :: LabelState l p s => p -> (p -> LIO l p s a) -> LIO l p s a
-- | Drop all privileges. It is useful to remove all privileges when
-- executing some untrusted code withing a withPrivileges block.
dropPrivileges :: LabelState l p s => LIO l p s ()
-- | LIO monad is a State monad transformer with IO as the underlying
-- monad.
newtype LIO l p s a
LIO :: (StateT (LIOstate l p s) IO a) -> LIO l p s a
-- | Empty class used to specify the functional dependency between a label
-- and it state.
class (Priv l p, Label l) => LabelState l p s | l -> s, l -> p
-- | Produces an IO computation that will execute a particular
-- LIO computation. Because untrusted code cannot execute
-- IO computations, this function should only be useful within
-- trusted code. No harm is done from exposing the evalLIO
-- symbol to untrusted code. (In general, untrusted code is free to
-- produce IO computations--it just can't execute them without
-- access to ioTCB.)
evalLIO :: LabelState l p s => LIO l p s a -> s -> IO (a, l)
-- | Execute an LIO action. The label on exceptions are removed. See
-- evalLIO.
runLIO :: LabelState l p s => LIO l p s a -> LIOstate l p s -> IO (a, LIOstate l p s)
-- | Generate a fresh state to pass runLIO when invoking it for the
-- first time. The current label is set to lbot, the current
-- clearance is set to ltop, and the current privileges are set to
-- none.
newState :: LabelState l p s => s -> LIOstate l p s
-- | Returns the current value of the thread's label.
getLabel :: LabelState l p s => LIO l p s l
-- | If the current label is oldLabel and the current clearance is
-- clearance, this function allows code to raise the label to
-- any value newLabel such that oldLabel `leq`
-- newLabel && newLabel `leq` clearance. Note that
-- there is no setLabel variant without the ...P
-- because the taint function provides essentially the same
-- functionality that setLabel would.
setLabelP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Returns the current value of the thread's clearance.
getClearance :: LabelState l p s => LIO l p s l
-- | Reduce the current clearance. One cannot raise the current label or
-- create object with labels higher than the current clearance.
lowerClr :: LabelState l p s => l -> LIO l p s ()
-- | Raise the current clearance (undoing the effects of lowerClr).
-- This requires privileges.
lowerClrP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Lowers the clearance of a computation, then restores the clearance to
-- its previous value. Useful to wrap around a computation if you want to
-- be sure you can catch exceptions thrown by it. Also useful to wrap
-- around toLabeled to ensure that the computation does not access
-- data exceeding a particular label. If withClearance is given
-- a label that can't flow to the current clearance, then the clearance
-- is lowered to the greatest lower bound of the label supplied and the
-- current clearance.
--
-- Note that if the computation inside withClearance acquires
-- any Privs, it may still be able to raise its clearance above
-- the supplied argument using lowerClrP.
withClearance :: LabelState l p s => l -> LIO l p s a -> LIO l p s a
-- | Labeled is a type representing labeled data.
data Labeled l t
-- | Returns label of a Labeled type.
labelOf :: Label l => Labeled l a -> l
-- | Function to construct a Labeled from a label and pure value. If
-- the current label is lcurrent and the current clearance is
-- ccurrent, then the label l specified must satisfy
-- lcurrent `leq` l && l `leq` ccurrent.
label :: LabelState l p s => l -> a -> LIO l p s (Labeled l a)
-- | Constructs a Labeled using privilege to allow the
-- Labeled's label to be below the current label. If the current
-- label is lcurrent and the current clearance is
-- ccurrent, then the privilege p and label l
-- specified must satisfy (leqp p lcurrent l) && l
-- `leq` ccurrent. Note that privilege is not used to bypass
-- the clearance. You must use lowerClrP to raise the clearance
-- first if you wish to create an Labeled at a higher label than
-- the current clearance.
labelP :: LabelState l p s => p -> l -> a -> LIO l p s (Labeled l a)
-- | Within the LIO monad, this function takes a Labeled and
-- returns the value. Thus, in the LIO monad one can say:
--
--
-- x <- unlabel (xv :: Labeled SomeLabelType Int)
--
--
-- And now it is possible to use the value of x, which is the
-- pure value of what was stored in xv. Of course,
-- unlabel also raises the current label. If raising the label
-- would exceed the current clearance, then unlabel throws
-- LerrClearance. However, you can use labelOf to check if
-- unlabel will succeed without throwing an exception.
unlabel :: LabelState l p s => Labeled l a -> LIO l p s a
-- | Extracts the value of an Labeled just like unlabel, but
-- takes a privilege argument to minimize the amount the current label
-- must be raised. Will still throw LerrClearance under the same
-- circumstances as unlabel.
unlabelP :: LabelState l p s => p -> Labeled l a -> LIO l p s a
-- | Raises the label of a Labeled to the lub of it's current
-- label and the value supplied. The label supplied must be less than the
-- current clearance, though the resulting label may not be if the
-- Labeled is already above the current thread's clearance.
taintLabeled :: LabelState l p s => l -> Labeled l a -> LIO l p s (Labeled l a)
-- | Downgrades the label of a Labeled as much as possible given the
-- current privilege.
untaintLabeled :: LabelState l p s => l -> Labeled l a -> LIO l p s (Labeled l a)
-- | Same as untaintLabeled but combines the current privilege with
-- the supplied privilege when downgrading the label.
untaintLabeledP :: LabelState l p s => p -> l -> Labeled l a -> LIO l p s (Labeled l a)
-- | Relabeles a Labeled value if the given privilege combined
-- with the current privileges permits it.
relabelP :: LabelState l p s => p -> l -> Labeled l a -> LIO l p s (Labeled l a)
-- | toLabeled is the dual of unlabel. It allows one to
-- invoke computations that would raise the current label, but without
-- actually raising the label. Instead, the result of the computation is
-- packaged into a Labeled with a supplied label. (Of couse, the
-- computation executed by toLabeled must most observe any data
-- whose label exceeds the supplied label.)
--
-- To get at the result of the computation one will have to call
-- unlabel and raise the label, but this can be postponed, or done
-- inside some other call to toLabeled. This suggests that the
-- provided label must be above the current label and below the current
-- clearance.
--
-- Note that toLabeled always restores the clearance to whatever
-- it was when it was invoked, regardless of what occurred in the
-- computation producing the value of the Labeled. This highlights
-- one main use of clearance: to ensure that a Labeled computed
-- does not exceed a particular label.
--
-- If an exception is thrown within a toLabeled block, such that
-- the outer context is withing a catch, which is futher within a
-- toLabeled block, infromation can be leaked. Consider the
-- following program that uses DCLabels. (Note that
-- discard is simply toLabeled that throws throws the
-- result away.)
--
--
-- main = evalDC' $ do
-- lRef <- newLIORef lbot ""
-- hRef <- newLIORef ltop "secret"
-- -- brute force:
-- forM_ ["fun", "secret"] $ \guess -> do
-- stash <- readLIORef lRef
-- writeLIORef lRef $ stash ++ "\n" ++ guess ++ ":"
-- discard ltop $ do
-- catch ( discard ltop $ do
-- secret <- readLIORef hRef
-- when (secret == guess) $ throwIO . userError $ "got it!"
-- ) (\(e :: IOError) -> return ())
-- l <- getLabel
-- when (l == lbot) $ do stash <- readLIORef lRef
-- writeLIORef lRef $ stash ++ "no!"
-- readLIORef lRef
-- where evalDC' act = do (r,l) <- evalDC act
-- putStrLn r
-- putStrLn $ "label = " ++ prettyShow l
--
--
-- The output of the program is:
--
--
-- $ ./new
--
-- fun:no!
-- secret:
-- label = <True , False>
--
--
-- Note that the current label is lbot (which in DCLabels is
-- True , False), and the secret is leaked. The
-- fundamental issue is that the outer discard allows for the
-- current label to remain low even though the catch raised the
-- current label when the secret was found (and thus exception was
-- throw). As a consequence, toLabeled catches all exceptions, and
-- returns a Labeled value that may have a labeled exception as
-- wrapped by throw. All exceptions within the outer
-- computation, including IFC violation attempts, are essentially
-- rethrown when performing an unlabel.
--
-- DEPRECATED: toLabeled is susceptible to termination attacks.
toLabeled :: LabelState l p s => l -> LIO l p s a -> LIO l p s (Labeled l a)
-- | Same as toLabeled but allows one to supply a privilege object
-- when comparing the initial and final label of the computation.
--
-- DEPRECATED: toLabeledP is susceptible to termination attacks.
toLabeledP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s (Labeled l a)
-- | Executes a computation that would raise the current label, but
-- discards the result so as to keep the label the same. Used when one
-- only cares about the side effects of a computation. For instance, if
-- log_handle is an LHandle with a high label, one can
-- execute
--
--
-- discard ltop $ hputStrLn log_handle "Log message"
--
--
-- to create a log message without affecting the current label.
--
-- DEPRECATED: discard is susceptible to termination attacks.
discard :: LabelState l p s => l -> LIO l p s a -> LIO l p s ()
-- | Same as discard, but uses privileges when comparing initial and
-- final label of the computation.
discardP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s ()
-- | Use taint l in trusted code before observing an object
-- labeled l. This will raise the current label to a value
-- l' such that l `leq` l', or throw
-- LerrClearance if l' would have to be higher
-- than the current clearance.
taint :: LabelState l p s => l -> LIO l p s ()
-- | Like taint, but use privileges to reduce the amount of taint
-- required. Note that unlike setLabelP, taintP will
-- never lower the current label. It simply uses privileges to avoid
-- raising the label as high as taint would raise it.
taintP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Use wguard l in trusted code before modifying an object
-- labeled l. If l' is the current label, then this
-- function ensures that l' `leq` l before doing the same
-- thing as taint l. Throws LerrHigh if
-- the current label l' is too high.
wguard :: LabelState l p s => l -> LIO l p s ()
-- | Like wguard, but takes privilege argument to be more
-- permissive.
wguardP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Ensures the label argument is between the current IO label and current
-- IO clearance. Use this function in code that allocates
-- objects--untrusted code shouldn't be able to create an object labeled
-- l unless aguard l does not throw an exception.
aguard :: LabelState l p s => l -> LIO l p s ()
-- | Like aguardP, but takes privilege argument to be more
-- permissive.
aguardP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Violation of information flow conditions, or label checks should throw
-- exceptions of type LabelFault. The LerrInval
-- constructor takes a string parameter -- it is important that trusted
-- code use this carefully and aovid leaking information through it.
data LabelFault
-- | Requested label too low
LerrLow :: LabelFault
-- | Current label too high
LerrHigh :: LabelFault
-- | Label would exceed clearance
LerrClearance :: LabelFault
-- | Insufficient privileges
LerrPriv :: LabelFault
-- | Invalid request
LerrInval :: String -> LabelFault
-- | A labeled exception is simply an exception associated with a label.
data LabeledException l
LabeledExceptionTCB :: l -> SomeException -> LabeledException l
-- | MonadCatch is the class used to generalize the standard IO
-- catch and throwIO functions to methods that can be
-- defined in multiple monads. Minimal definition requires:
-- mask, throwIO, catch, and
-- onException.
class Monad m => MonadCatch m where mask_ io = mask $ \ _ -> io handle = flip catch onException io h = io `catch` \ e -> h >> throwIO (e :: SomeException) bracket = genericBracket onException bracket_ a b c = bracket a (const b) (const c) finally a b = mask $ \ restore -> do { r <- restore a `onException` b; _ <- b; return r }
mask :: MonadCatch m => ((forall a. m a -> m a) -> m b) -> m b
mask_ :: MonadCatch m => m a -> m a
throwIO :: (MonadCatch m, Exception e) => e -> m a
catch :: (MonadCatch m, Exception e) => m a -> (e -> m a) -> m a
handle :: (MonadCatch m, Exception e) => (e -> m a) -> m a -> m a
onException :: MonadCatch m => m a -> m b -> m a
bracket :: MonadCatch m => m b -> (b -> m c) -> (b -> m a) -> m a
bracket_ :: MonadCatch m => m a -> m b -> m c -> m c
finally :: MonadCatch m => m a -> m b -> m a
-- | Catches an exception, so long as the label at the point where the
-- exception was thrown can flow to the label at which catchP is
-- invoked, modulo the privileges specified. Note that the handler raises
-- the current label to the joint of the current label and exception
-- label.
catchP :: (Exception e, LabelState l p s) => p -> LIO l p s a -> (e -> LIO l p s a) -> LIO l p s a
-- | Version of catchP with arguments swapped.
handleP :: (Exception e, LabelState l p s) => p -> (e -> LIO l p s a) -> LIO l p s a -> LIO l p s a
-- | onException cannot run its handler if the label was raised in
-- the computation that threw the exception. This variant allows
-- privileges to be supplied, so as to catch exceptions thrown with a
-- raised label.
onExceptionP :: LabelState l p s => p -> LIO l p s a -> LIO l p s b -> LIO l p s a
-- | Like standard bracket, but with privileges to downgrade
-- exception.
bracketP :: LabelState l p s => p -> LIO l p s a -> (a -> LIO l p s c) -> (a -> LIO l p s b) -> LIO l p s b
-- | Forces its argument to be evaluated to weak head normal form when the
-- resultant LIO action is executed. This is simply a wrapper for
-- Control.Exception's evaluate.
evaluate :: LabelState l p s => a -> LIO l p s a
-- | Class used to describe privileges in a meaningful manner.
class (PrivTCB p, Show d) => PrivDesc p d | p -> d
privDesc :: PrivDesc p d => p -> d
-- | A Gate is a wrapper for a Labeled type.
newtype Gate l d a
Gate :: (Labeled l (d -> a)) -> Gate l d a
-- | Create a gate given a gate label and computation. The label of the
-- gate must be bounded by the current label and clearance.
mkGate :: (LabelState l p s, PrivDesc p d) => l -> (d -> a) -> LIO l p s (Gate l d a)
-- | Same as mkGate, but uses privileges when making the gate.
mkGateP :: (LabelState l p s, PrivDesc p d) => p -> l -> (d -> a) -> LIO l p s (Gate l d a)
-- | Given a labeled gate and privilege, execute the gate computation. The
-- current label is raised to the join of the gate and current label,
-- clearance permitting. It is important to note that callGate
-- invokes the gate computation with the privilege description and
-- not the actual privilege.
callGate :: (LabelState l p s, PrivDesc p d) => Gate l d a -> p -> LIO l p s a
-- | PrivTCB is a method-less class whose only purpose is to be
-- unavailable to unprivileged code. Since (PrivTCB t) => is
-- in the context of class Priv and unprivileged code cannot
-- create new instances of the PrivTCB class, this ensures
-- unprivileged code cannot create new instances of the Priv class
-- either, even though the symbol Priv is exported by
-- LIO.Base and visible to untrusted code.
class PrivTCB t
class MintTCB t i
mintTCB :: MintTCB t i => i -> t
-- | Internal state of an LIO computation.
data LIOstate l p s
LIOstate :: s -> l -> l -> p -> LIOstate l p s
-- | label-specific state
labelState :: LIOstate l p s -> s
-- | current label
lioL :: LIOstate l p s -> l
-- | current clearance
lioC :: LIOstate l p s -> l
-- | current privileges
lioP :: LIOstate l p s -> p
-- | Get internal state.
getTCB :: LabelState l p s => LIO l p s (LIOstate l p s)
-- | Put internal state.
putTCB :: LabelState l p s => LIOstate l p s -> LIO l p s ()
-- | Returns label-specific state of the LIO monad. This is the data
-- specified as the second argument of evalLIO, whose type is
-- s in the monad LIO l s.
getLabelStateTCB :: LabelState l p s => LIO l p s s
-- | Sets the label-specific state of the LIO monad. See
-- getTCB.
putLabelStateTCB :: LabelState l p s => s -> LIO l p s ()
-- | Set the current label to anything, with no security check.
setLabelTCB :: LabelState l p s => l -> LIO l p s ()
-- | Set the current clearance to anything, with no security check.
lowerClrTCB :: LabelState l p s => l -> LIO l p s ()
-- | 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
showTCB :: ShowTCB a => a -> String
-- | It is useful to have the dual of ShowTCB, ReadTCB,
-- that allows for the reading of Labeleds that were written using
-- showTCB. Only readTCB (corresponding to read)
-- and readsPrecTCB (corresponding to readsPrec) are
-- implemented.
class ReadTCB a where 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"
readsPrecTCB :: ReadTCB a => Int -> ReadS a
readTCB :: ReadTCB a => String -> a
-- | Trusted constructor that creates labeled values.
labelTCB :: Label l => l -> a -> Labeled l a
-- | Extracts the value from an Labeled, discarding the label and
-- any protection.
unlabelTCB :: Label l => Labeled l a -> a
-- | Trusted catch functin.
catchTCB :: LabelState l p s => LIO l p s a -> (LabeledException l -> LIO l p s a) -> LIO l p s a
-- | For privileged code that needs to catch all exceptions in some cleanup
-- function. Note that for the LIO monad, these methods do
-- not label the exceptions. It is assumed that you will use
-- rtioTCB instead of ioTCB for IO within the computation
-- arguments of these methods.
class MonadCatch m => OnExceptionTCB m where finallyTCB a b = mask $ \ restore -> do { r <- restore a `onExceptionTCB` b; _ <- b; return r } bracketTCB = genericBracket onExceptionTCB
onExceptionTCB :: OnExceptionTCB m => m a -> m b -> m a
finallyTCB :: OnExceptionTCB m => m a -> m b -> m a
bracketTCB :: OnExceptionTCB m => m a -> (a -> m c) -> (a -> m b) -> m b
-- | Lifts an IO computation into the LIO monad. Note that
-- exceptions thrown within the IO computation cannot directly be
-- caught within the LIO computation. Thus, you will generally
-- want to use rtioTCB instead of ioTCB.
ioTCB :: LabelState l p s => IO a -> LIO l p s a
-- | Lifts an IO computation into the LIO monad. If the
-- IO computation throws an exception, it labels the exception
-- with the current label so that the exception can be caught with
-- catch or catchP. This function's name stands for
-- "re-throw io".
rtioTCB :: LabelState l p s => IO a -> LIO l p s a
-- | Same as mkGate, but ignores IFC.
mkGateTCB :: (LabelState l p s, PrivDesc p d) => l -> (d -> a) -> Gate l d a
-- | Same as callGate, but does not raise label in accessing the
-- gate computation.
callGateTCB :: (LabelState l p s, PrivDesc p d) => Gate l d a -> p -> a
instance Typeable2 Labeled
instance Typeable LabelFault
instance Typeable1 LabeledException
instance Typeable3 Gate
instance Functor (LIO l p s)
instance Applicative (LIO l p s)
instance Monad (LIO l p s)
instance LabelState l p s => MonadError IOException (LIO l p s)
instance LabelState l p s => OnExceptionTCB (LIO l p s)
instance OnExceptionTCB IO
instance LabelState l p s => MonadCatch (LIO l p s)
instance Label l => Exception (LabeledException l)
instance Label l => Show (LabeledException l)
instance Exception LabelFault
instance Show LabelFault
instance (Label l, Read l, Read a) => ReadTCB (Labeled l a)
instance (Label l, Show a) => ShowTCB (Labeled l a)
-- | This module implements labeled IORefs. The interface is analogous to
-- Data.IORef, but the operations take place in the LIO monad.
module LIO.LIORef.TCB
-- | An LIORef is an IORef with an associated, static
-- label. The restriction of an immutable label come from the fact that
-- it is possible to leak information through the label itself. Hence,
-- LIO is flow-insensitive. Of course, you can create an
-- LIORef of Labeled to get a limited form of
-- flow-sensitivity.
data LIORef l a
-- | To create a new reference the label of the reference must be below the
-- thread's current clearance and above the current label. If this is the
-- case, the reference is built.
newLIORef :: LabelState l p s => l -> a -> LIO l p s (LIORef l a)
-- | Get the label of a reference.
labelOfLIORef :: Label l => LIORef l a -> l
-- | Read the value of a labeled refernce. A read succeeds only if the
-- label of the reference is below the current clearance. Moreover, the
-- current label is raised to the join of the current label and the
-- reference label. To avoid failures use labelOfLIORef to check
-- that a read will suceed.
readLIORef :: LabelState l p s => LIORef l a -> LIO l p s a
-- | Write a new value into a labeled reference. A write succeeds if the
-- current label can-flow-to the label of the reference, and the label of
-- the reference can-flow-to the current clearance.
writeLIORef :: LabelState l p s => LIORef l a -> a -> LIO l p s ()
-- | Mutate the contents of a labeled reference. For the mutation to
-- succeed it must be that the current label can-flow-to the label of the
-- reference, and the label of the reference can-flow-to the current
-- clearance. Note that because a modifer is provided, the reference
-- contents are not observable by the outer computation and so it is not
-- required that the current label be raised.
modifyLIORef :: LabelState l p s => LIORef l a -> (a -> a) -> LIO l p s ()
-- | Atomically modifies the contents of an LIORef. It is required
-- that the label of the reference be above the current label, but below
-- the current clearance.
atomicModifyLIORef :: LabelState l p s => LIORef l a -> (a -> (a, b)) -> LIO l p s b
-- | Same as newLIORef except newLIORefP takes a set of
-- privileges which are accounted for in comparing the label of the
-- reference to the current label and clearance.
newLIORefP :: LabelState l p s => p -> l -> a -> LIO l p s (LIORef l a)
-- | Same as readLIORef except readLIORefP takes a
-- privilege object which is used when the current label is raised.
readLIORefP :: LabelState l p s => p -> LIORef l a -> LIO l p s a
-- | Same as writeLIORef except writeLIORefP takes a set of
-- privileges which are accounted for in comparing the label of the
-- reference to the current label and clearance.
writeLIORefP :: LabelState l p s => p -> LIORef l a -> a -> LIO l p s ()
-- | Same as modifyLIORef except modifyLIORefP takes a set
-- of privileges which are accounted for in comparing the label of the
-- reference to the current label and clearance.
modifyLIORefP :: LabelState l p s => p -> LIORef l a -> (a -> a) -> LIO l p s ()
-- | Same as atomicModifyLIORef except atomicModifyLIORefP
-- takes a set of privileges which are accounted for in label
-- comparisons.
atomicModifyLIORefP :: LabelState l p s => p -> LIORef l a -> (a -> (a, b)) -> LIO l p s b
-- | Trusted constructor that creates labeled references.
newLIORefTCB :: LabelState l p s => l -> a -> LIO l p s (LIORef l a)
-- | Trusted function used to read the value of a reference without raising
-- the current label.
readLIORefTCB :: LabelState l p s => LIORef l a -> LIO l p s a
-- | Trusted function used to write a new value into a labeled reference,
-- ignoring IFC.
writeLIORefTCB :: LabelState l p s => LIORef l a -> a -> LIO l p s ()
-- | Trusted function that mutates the contents on an LIORef,
-- ignoring IFC.
modifyLIORefTCB :: LabelState l p s => LIORef l a -> (a -> a) -> LIO l p s ()
-- | Trusted function used to atomically modify the contents of a labeled
-- reference, ignoring IFC.
atomicModifyLIORefTCB :: LabelState l p s => LIORef l a -> (a -> (a, b)) -> LIO l p s b
-- | This module exports the safe subset of the LIO.LIORef.TCB
-- module. It is important that untrusted code be limited to this subset;
-- information flow can easily be violated if the TCB functions are
-- exported.
module LIO.LIORef.Safe
-- | This module implements labeled IORefs. The interface is analogous to
-- Data.IORef, but the operations take place in the LIO monad.
-- (See LIO.LIORef.TCB for documentation.) Moreover, reading the
-- LIORef calls taint, while writing it calls aguard. This module exports
-- only the safe subset (non TCB) of the LIORef module --
-- trusted code can import LIO.LIORef.TCB.
module LIO.LIORef
-- | This module provides an implementation for labeled MVars. A labeled
-- MVar, of type LMVar l a, is a mutable location that
-- can be in of of two states; an LMVar can be empty, or it can be
-- full (with a value of tye a). The location is protected by a
-- label of type l. As in the case of LIORefs (see
-- LIO.LIORef), this label is static and does not change according
-- to the content placed into the location.
--
-- LMVars can be used to build synchronization primitives and
-- communication channels (LMVars themselves are single-place
-- channels). We refer to Control.Concurrent.MVar for the full
-- documentation on MVars.
module LIO.Concurrent.LMVar.TCB
-- | An LMVar is a labeled synchronization variable (an
-- MVar) that can be used by concurrent threads to communicate.
data LMVar l a
-- | This function returns the label of a labeled MVar.
labelOfLMVar :: Label l => LMVar l a -> l
-- | Create a new labeled MVar, in an empty state. Note that the supplied
-- label must be above the current label and below the current clearance.
newEmptyLMVar :: LabelState l p s => l -> LIO l p s (LMVar l a)
-- | Same as newEmptyLMVar except it takes a set of privileges which
-- are accounted for in comparing the label of the MVar to the current
-- label and clearance.
newEmptyLMVarP :: LabelState l p s => p -> l -> LIO l p s (LMVar l a)
-- | Create a new labeled MVar, in an filled state with the supplied value.
-- Note that the supplied label must be above the current label and below
-- the current clearance.
newLMVar :: LabelState l p s => l -> a -> LIO l p s (LMVar l 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 :: LabelState l p s => p -> l -> a -> LIO l p s (LMVar l a)
-- | Return contents of the LMVar. Note that a take consists of a
-- read and a write, since it observes whether or not the LMVar is
-- full, and thus the current label must be the same as that of the
-- LMVar (of course, this is not the case when using privileges).
-- Hence, if the label of the LMVar is below the current
-- clearance, we raise the current label to the join of the current label
-- and the label of the MVar and read the contents of the MVar.
-- If the LMVar is empty, takeLMVar blocks.
takeLMVar :: LabelState l p s => LMVar l a -> LIO l p s a
-- | Same as takeLMVar except takeLMVarP takes a privilege
-- object which is used when the current label is raised.
takeLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s a
-- | Puts a value into an LMVar. Note that a put consists of a read
-- and a write, since it observes whether or not the LMVar is
-- empty, and so the current label must be the same as that of the
-- LMVar (of course, this is not the case when using privileges).
-- As in the takeLMVar case, if the label of the LMVar is
-- below the current clearance, we raise the current label to the join of
-- the current label and the label of the MVar and put the value into the
-- MVar. If the LMVar is full, putLMVar blocks.
putLMVar :: LabelState l p s => LMVar l a -> a -> LIO l p s ()
-- | Same as putLMVar except putLMVarP takes a privilege
-- object which is used when the current label is raised.
putLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s ()
-- | Combination of takeLMVar and putLMVar. Read the value,
-- and just put it back. As specified for readMVar, this operation
-- is atomic iff there is no other thread calling putLMVar for
-- this LMVar.
readLMVar :: LabelState l p s => LMVar l a -> LIO l p s a
-- | Same as readLMVar except readLMVarP takes a privilege
-- object which is used when the current label is raised.
readLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s a
-- | Takes a value from an LMVar, puts a new value into the
-- LMvar, and returns the taken value. Like the other
-- LMVar operations it is required that the label of the
-- LMVar be above the current label and below the current
-- clearance. Moreover, the current label is raised to accommodate for
-- the observation. This operation is atomic iff there is no other thread
-- calling putLMVar for this LMVar.
swapLMVar :: LabelState l p s => LMVar l a -> a -> LIO l p s a
-- | Same as swapLMVar except swapLMVarP takes a privilege
-- object which is used when the current label is raised.
swapLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s a
-- | Non-blocking version of takeLMVar. It returns Nothing
-- if the LMVar is empty, otherwise it returns Just
-- value, emptying the LMVar.
tryTakeLMVar :: LabelState l p s => LMVar l a -> LIO l p s (Maybe a)
-- | Same as tryTakeLMVar, but uses priviliges when raising current
-- label.
tryTakeLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s (Maybe a)
-- | Non-blocking version of putLMVar. It returns True if
-- the LMVar was empty and the put succeeded, otherwise it returns
-- False.
tryPutLMVar :: LabelState l p s => LMVar l a -> a -> LIO l p s Bool
-- | Same as tryPutLMVar, but uses privileges when raising current
-- label.
tryPutLMVarP :: LabelState l p s => p -> LMVar l a -> a -> LIO l p s Bool
-- | Check the status of an LMVar, i.e., whether it is empty. The
-- function succeeds if the label of the LMVar is below the
-- current clearance -- the current label is raised to the join of the
-- LMVar label and the current label. Note that this function only
-- returns a snapshot of the state.
isEmptyLMVar :: LabelState l p s => LMVar l a -> LIO l p s Bool
-- | Same as isEmptyLMVar, but uses privileges when raising current
-- label.
isEmptyLMVarP :: LabelState l p s => p -> LMVar l a -> LIO l p s Bool
-- | Exception-safe wrapper for working with an LMVar. The original
-- contents of the LMVar will be restored if the supplied action
-- throws an exception. The function is atomic only if there is no other
-- thread that performs a putLMVar.
withLMVar :: LabelState l p s => LMVar l a -> (a -> LIO l p s b) -> LIO l p s b
-- | Same as withLMVar, but uses privileges when performing label
-- comparisons/raises.
withLMVarP :: LabelState l p s => p -> LMVar l a -> (a -> LIO l p s b) -> LIO l p s b
-- | Trusted function used to create an empty LMVar, ignoring IFC.
newEmptyLMVarTCB :: LabelState l p s => l -> LIO l p s (LMVar l a)
-- | Trusted function used to create an LMVar with the supplied
-- value, ignoring IFC.
newLMVarTCB :: LabelState l p s => l -> a -> LIO l p s (LMVar l a)
-- | Read the contents of an LMVar, ignoring IFC.
takeLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s a
-- | Put a value into an LMVar, ignoring IFC.
putLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s ()
-- | Trusted function used to read (take and put) an LMVar, ignoring
-- IFC.
readLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s a
-- | Trusted function that swaps value of LMVar, ignoring IFC.
swapLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s a
-- | Same as tryTakeLMVar, but ignorses IFC.
tryTakeLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s (Maybe a)
-- | Same as tryPutLMVar, but ignorses IFC.
tryPutLMVarTCB :: LabelState l p s => LMVar l a -> a -> LIO l p s Bool
-- | Same as isEmptyLMVar, but ignorses IFC.
isEmptyLMVarTCB :: LabelState l p s => LMVar l a -> LIO l p s Bool
-- | Same as withLMVar, but ignores IFC.
withLMVarTCB :: LabelState l p s => LMVar l a -> (a -> LIO l p s b) -> LIO l p s b
-- | This module exposes the concurrent interface to LIO. Specifically, it
-- implements labeled fork (lFork) and wait
-- (lWait). We strongly suggest these primitives over
-- toLabeled as they are termination-senstivie.
module LIO.Concurrent
-- | Same as lFork, but the supplied set of priviliges are accounted
-- for when performing label comparisons.
lForkP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s (LRes l a)
-- | Labeled fork. lFork allows one to invoke computations taht
-- would otherwise raise the current label, but without actually raising
-- the label. The computation is executed in a separate thread and writes
-- its result into a labeled result (whose label is supplied). To observe
-- the result of the computation, or if the computation has terminated,
-- one will have to call lWait and raise the current label. Of
-- couse, as in toLabeled, this can be postponed until the result
-- is needed.
--
-- lFork takes a label, which corresponds to the label of the
-- result. It is require that this label is above the current label, and
-- below the current clearance. Moreover, the supplied computation must
-- not read anything more sensitive, i.e., with a label above the
-- supplied label --- doing so will result in an exception (whose label
-- will reflect this observation) being thrown.
--
-- If an exception is thrown in the inner computation, the exception
-- label will be raised to the join of the result label and original
-- exception label.
--
-- Not that, compared to toLabeled, lFork immediately
-- returns a labeled result of type LRes, which is essentially a
-- "future", or "promise". Moreover, to guarantee that the computation
-- has completed, it is important that some thread actually touch the
-- future, i.e., perform an lWait.
lFork :: LabelState l p s => l -> LIO l p s a -> LIO l p s (LRes l a)
-- | Same as lWait, but uses priviliges in label checks and raises.
lWaitP :: LabelState l p s => p -> LRes l a -> LIO l p s a
-- | Given a labeled result (a future), lWait returns the
-- unwrapped result (blocks, if necessary). For lWait to
-- succeed, the label of the result must be above the current label and
-- below the current clearnce. Moreover, before block-reading,
-- lWait raises the current label to the join of the current
-- label and label of result. If the thread lWait is terminates
-- with an exception (for example if it violates clearance), the exceptin
-- is rethrown. Similarly, if the thread reads values above the result
-- label, an exception is thrown in place of the result.
lWait :: LabelState l p s => LRes l a -> LIO l p s a
-- | This module exports a safe subset of the labeled MVar interface. See
-- LIO.Concurrent.LMVar.TCB for the documentation.
module LIO.Concurrent.LMVar.Safe
-- | This module implements labeled MVars. The interface is
-- analogous to Control.Concurrent.MVar, but the operations take
-- place in the LIO monad. Moreover, taking and putting MVars
-- calls a write guard wguard as every read implies a write and
-- vice versa. This module exports only the safe subset (non-TCB) of the
-- LMVar module trusted code can import
-- LIO.Concurrent.LMVar.TCB. The interface is documented in
-- LIO.Concurrent.LMVar.TCB.
module LIO.Concurrent.LMVar
-- | This module implements a labeled filesystem as a file store in which a
-- label is associated with every file and directory. The module
-- LIO.Handle provides an interface for working with labeled
-- directories and files -- this module provides the underlying low-level
-- (mostly trusted) interface.
--
-- The file store contains 3 components:
--
--
-- - .magic file containing a sequence of pre-defined bytes.
-- The existence of this file and correct contents indicates that the
-- file store and root of the labeled filesystem were created before any
-- system crash.
-- - .obj directory containing all the objects (files and
-- directories) in the filesystem, organized according to the object's
-- label.
-- - ROOT symbolic link pointing to a directory object in
-- .obj, representing the root of the filesystem.
--
--
-- As the details of .magic and ROOT are straight
-- forward, we now focus on the details of .obj.
--
-- Each object is stored in .obj in a directory corresponding to
-- the label of the file. For example, an object protected by
-- bob's label will exist as:
--
--
-- .obj/oTAUzOt5YoQAyThw89eSgWuig-0=/obj012345
--
--
-- where oTAUzOt5YoQAyThw89eSgWuig-0= is the base64url encoding
-- of the (SHA-224 hash of) label bob, and obj012345 is
-- the object's name. Each label directory also contains a
-- .label file whose contents correspond to the serialization of
-- the label. Hence, for example,
--
--
-- .obj/oTAUzOt5YoQAyThw89eSgWuig-0=/.label
--
--
-- would have bob's label.
--
-- Every object in a label directory is either a file or a directory. If
-- the object is a directory, its contents will strictly have symbolic
-- links to objects in the file store. This is more easily understood
-- using an example.
--
-- Consider the following familiar filesystem layout, containing 4
-- directories and 2 files:
--
--
-- /
-- |-- bobOralice (type: directory, label: bob \/ alice)
-- | |-- alice (type: directory, label: alice)
-- | |-- bob (type: directory, label: bob)
-- | | '-- secret (type: file , label: bob)
-- | '-- messages (type: file , label: bob \/ alice)
-- '-- clarice (type: directory, label: clarice)
--
--
-- Suppose we take /lioFS as the location of the file store for
-- our labeled filesystem. The above files and directories will have the
-- same layout in our file system, but each file/directory points to an
-- object in the object store (.obj), as shown below.
--
--
-- /lioFS/ROOT
-- |-- bobOralice -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objXIBabq
-- | |-- alice -> ../../12to8q3vDp7ApyKEQk2LQ_2nrvs=/objqZeR5w
-- | |-- bob -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objtsePnc
-- | | '-- secret -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objFIQCIm
-- | '-- messages -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objQaiwuA
-- '-- clarice -> ../../wordEFmBzWc7Q6qP-TetDgZaG8A=/objOMh0mj
--
--
-- Note that, to a user, the interface (see LIO.Handle) is
-- unchanged and they do not need to handle or understand the underlying
-- file store. We refer to this view as "friendly". The file store for
-- the above layout is:
--
--
-- /lioFS/
-- |-- .magic
-- |-- .obj
-- | |-- 12to8q3vDp7ApyKEQk2LQ_2nrvs=
-- | | |-- .label (=alice's label)
-- | | '-- objqZeR5w
-- | |-- c_EkXYGrmrSit9j_8VjP_-8DgaM=
-- | | |-- .label (=label bob \/ alice)
-- | | |-- objQaiwuA
-- | | '-- objXIBabq
-- | | |-- alice -> ../../12to8q3vDp7ApyKEQk2LQ_2nrvs=/objqZeR5w
-- | | |-- bob -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objtsePnc
-- | | '-- messages -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objQaiwuA
-- | |-- jX7q5Kb8_G4GsjgNpOHB17kypQo=
-- | | |-- .label (=label of the filesystem root)
-- | | '-- objTj5JZD
-- | | |-- bobOralice -> ../../c_EkXYGrmrSit9j_8VjP_-8DgaM=/objXIBabq
-- | | '-- clarice -> ../../wordEFmBzWc7Q6qP-TetDgZaG8A=/objOMh0mj
-- | |-- oTAUzOt5YoQAyThw89eSgWuig-0=
-- | | |-- .label (=bob's label)
-- | | |-- objFIQCIm
-- | | '-- objtsePnc
-- | | '-- secret -> ../../oTAUzOt5YoQAyThw89eSgWuig-0=/objFIQCIm
-- | '-- wordEFmBzWc7Q6qP-TetDgZaG8A=
-- | |-- .label (=clarice's label)
-- | '-- objOMh0mj
-- '-- ROOT -> .obj/jX7q5Kb8_G4GsjgNpOHB17kypQo=/objTj5JZD
--
--
-- Observe that every directory object contains symbolic links pointing
-- to file or directory objects in the store.
--
-- Accessing any file or directory in the "friendly" view requires a
-- lookup (lookupObjPath) of the corresponding object. Each path
-- is, however, relative to the root. So, for example, looking up
-- /aliceOrbob/bob/ actually corresponds to looking up
-- /lioFS/ROOT/aliceOrbob/bob/. This prevents untrusted code
-- from accessing objects by guessing filenames and further allows
-- untrusted code to pick arbitrary filenames (including .label,
-- .obj, etc.).
--
-- Several precautions are taken to keep the filesystem in a working
-- state in case of a crash. The code tries to maintain the invariant
-- that any inconsistencies will either be:
--
--
-- - temporary files or directories whose names start with the
-- "#" character, or
-- - dangling symbolic links.
--
--
-- Both of these inconsistencies can be checked and cleaned up locally
-- without examining the whole file system. The code tries to fix up
-- these inconsistencies on-the-fly as it encounters them. However, it
-- could possibly leave some stranded temporary .label files.
module LIO.FS
-- | Same as evalLIO, but takes two additional parameters
-- corresponding to the path of the labeled filesystem store and the
-- label of the root. If the labeled filesystem store does not exist, it
-- is created at the specified path with the root having the supplied
-- label. If the filesystem does exist, the supplied label is ignored and
-- thus unnecessary. However, if the root label is not provided and the
-- filesystem has not been initialized, then lbot is used as the
-- root label.
evalWithRoot :: (Serialize l, LabelState l p s) => FilePath -> Maybe l -> LIO l p s a -> s -> IO (a, l)
-- | Given a pathname (forced to be relative to the root of the labeled
-- filesystem), find the path to the corresponding object. The current
-- label is raised to reflect all the directories traversed. Note that if
-- the object does not exist an exception will be thrown; the label of
-- the exception will be the join of all the directory labels up to the
-- lookup failure.
--
-- Additionally, this function cleans up the path before doing the
-- lookup, so e.g., path foobar/.. will first be
-- rewritten to /foo and thus no traversal to bar. Note
-- that this is a more permissive behavior than forcing the read of
-- .. from bar.
lookupObjPath :: (LabelState l p s, Serialize l) => FilePath -> LIO l p s (LFilePath l)
-- | Same as lookupObjPath but takes an additional privilege object
-- that is exercised when raising the current label.
lookupObjPathP :: (LabelState l p s, Serialize l) => p -> FilePath -> LIO l p s (LFilePath l)
-- | Read the label file of an object. Note that because the format of the
-- supplied path is not checked this function is considered to be in the
-- TCB.
getObjLabelTCB :: (Serialize l, LabelState l p s) => FilePath -> LIO l p s l
-- | Create a file object with the given label and link the supplied path
-- to the object. The handle to the file is returned.
createFileTCB :: (Serialize l, Label l) => l -> FilePath -> IOMode -> IO Handle
-- | Create a directory object with the given label and link the supplied
-- path to the object.
createDirectoryTCB :: (Serialize l, Label l) => l -> FilePath -> IO ()
-- | Label associated with a FilePath.
data LFilePath l
-- | Get the label of a labeled filepath.
labelOfFilePath :: Label l => LFilePath l -> l
-- | Unlabel a filepath. If the path corresponds to a directory, you can
-- now get the contents of the directory; if it's a file, you can open
-- the file.
unlabelFilePath :: LabelState l p s => LFilePath l -> LIO l p s FilePath
-- | Same as unlabelFilePath but uses privileges to unlabel the
-- filepath.
unlabelFilePathP :: LabelState l p s => p -> LFilePath l -> LIO l p s FilePath
-- | Trusted version of unlabelFilePath that ignores IFC.
unlabelFilePathTCB :: Label l => LFilePath l -> FilePath
-- | Cleanup a file path, if it starts out with a .., we consider
-- this invalid as it can be used explore parts of the filesystem that
-- should otherwise be unaccessible. Similarly, we remove any .
-- from the path.
cleanUpPath :: LabelState l p s => FilePath -> LIO l p s FilePath
-- | Remove any pathSeparators from the front of a file path.
stripSlash :: FilePath -> FilePath
instance Typeable FSErr
instance Eq Object
instance Show Object
instance Eq NewObject
instance Show NewObject
instance Show FSErr
instance Exception FSErr
-- | This module abstracts the basic FileHandle methods provided
-- by the system library, and provides an LHandle (Labeled
-- Handle) type that can be manipulated from within the
-- LIO Monad. (There is no notion of changeable current working
-- directory in the LIO Monad, nor symbolic links.)
--
-- The actual storage of labeled files is handled by the LIO.FS
-- module.
--
-- IMPORTANT: To use a labeled filesystem you must use
-- evalWithRoot, otherwise any actions built using the combinators
-- of this module will crash.
--
-- An example use is shown below:
--
--
-- main = dcEvalWithRoot "/tmp/lioFS" $ do
-- createDirectoryP p lsecrets "secrets"
-- writeFileP p ("secrets" </> "alice" ) "I like Bob!"
-- where p = ...
-- lsecrets = ....
--
--
-- The file store for the labeled filesystem (see LIO.FS) will be
-- created in /tmp/lioFS, but this is transparent and the user
-- can think of the filesystem as having root /.
module LIO.Handle
-- | Same as evalLIO, but takes two additional parameters
-- corresponding to the path of the labeled filesystem store and the
-- label of the root. If the labeled filesystem store does not exist, it
-- is created at the specified path with the root having the supplied
-- label. If the filesystem does exist, the supplied label is ignored and
-- thus unnecessary. However, if the root label is not provided and the
-- filesystem has not been initialized, then lbot is used as the
-- root label.
evalWithRoot :: (Serialize l, LabelState l p s) => FilePath -> Maybe l -> LIO l p s a -> s -> IO (a, l)
-- | Class used to abstract reading and creating directories, and opening
-- (possibly creating) files.
class Monad m => DirectoryOps h m | m -> h
getDirectoryContents :: DirectoryOps h m => FilePath -> m [FilePath]
createDirectory :: DirectoryOps h m => FilePath -> m ()
openFile :: DirectoryOps h m => FilePath -> IOMode -> m h
-- | Class used to abstract close and flush operations on handles.
class Monad m => CloseOps h m
hClose :: CloseOps h m => h -> m ()
hFlush :: CloseOps h m => h -> m ()
-- | Class used to abstract reading and writing from and to handles,
-- respectively.
class CloseOps h m => HandleOps h b m where hPutStr = hPut
hGet :: HandleOps h b m => h -> Int -> m b
hGetNonBlocking :: HandleOps h b m => h -> Int -> m b
hGetContents :: HandleOps h b m => h -> m b
hPut :: HandleOps h b m => h -> b -> m ()
hPutStr :: HandleOps h b m => h -> b -> m ()
hPutStrLn :: HandleOps h b m => h -> b -> m ()
-- | Reads a file and returns the contents of the file as a (Byte)String.
readFile :: (DirectoryOps h m, HandleOps h b m) => FilePath -> m b
-- | Write a (Byte)String to a file.
writeFile :: (DirectoryOps h m, HandleOps h b m, OnExceptionTCB m) => FilePath -> b -> m ()
-- | Same as writeFile but also takes the label of the file.
writeFileL :: (HandleOps Handle b IO, LabelState l p s, Serialize l) => l -> FilePath -> b -> LIO l p s ()
-- | See openFile
data IOMode :: *
ReadMode :: IOMode
WriteMode :: IOMode
AppendMode :: IOMode
ReadWriteMode :: IOMode
-- | A labeled handle.
data LHandle l
-- | Get the label of a labeled handle.
labelOfHandle :: Label l => LHandle l -> l
-- | Get the contents of a directory. The current label is raised to the
-- join of the current label and that of all the directories traversed to
-- the leaf directory (of course, using privileges to keep the current
-- label unchanged when possible). Note that, unlike the standard Haskell
-- getDirectoryContents, we first normalise the path by collapsing
-- all the ..'s. (The LIO filesystem does not support links.)
getDirectoryContentsP :: (LabelState l p s, Serialize l) => p -> FilePath -> LIO l p s [FilePath]
-- | Create a directory at the supplied path with the given label. The
-- current label (after traversing the filesystem to the directory path)
-- must flow to the supplied label which in turn must flow to the current
-- label (of course, using privileges to bypass certain restrictions). If
-- this information flow restriction is satisfied, the directory is
-- created.
createDirectoryP :: (LabelState l p s, Serialize l) => p -> l -> FilePath -> LIO l p s ()
-- | Given a set of privileges, a new (maybe) label of a file, a filepath
-- and the handle mode, open (and possibly create) the file. If the file
-- exists the supplied label is not necessary; otherwise it must be
-- supplied. The current label is raised to reflect all the traversed
-- directories (of course, using privileges to minimize the taint).
-- Additionally the label of the file (new or existing) must be between
-- the current label and clearance. If the file is created, it is further
-- required that the current process be able to write to the containing
-- directory.
openFileP :: (LabelState l p s, Serialize l) => p -> Maybe l -> FilePath -> IOMode -> LIO l p s (LHandle l)
-- | Close a labeled file handle.
hCloseP :: LabelState l p s => p -> LHandle l -> LIO l p s ()
-- | Flush a labeled file handle.
hFlushP :: LabelState l p s => p -> LHandle l -> LIO l p s ()
-- | Read n bytes from the labeled handle, using privileges when
-- performing label comparisons and tainting.
hGetP :: (LabelState l p s, HandleOps Handle b IO) => p -> LHandle l -> Int -> LIO l p s b
-- | Same as hGetP, but will not block waiting for data to become
-- available. Instead, it returns whatever data is available. Privileges
-- are used in the label comparisons and when raising the current label.
hGetNonBlockingP :: (LabelState l p s, HandleOps Handle b IO) => p -> LHandle l -> Int -> LIO l p s b
-- | Read the entire labeled handle contents and close handle upon reading
-- EOF. Privileges are used in the label comparisons and when
-- raising the current label.
hGetContentsP :: (LabelState l p s, HandleOps Handle b IO) => p -> LHandle l -> LIO l p s b
-- | Output the given (Byte)String to the specified labeled handle.
-- Privileges are used in the label comparisons and when raising the
-- current label.
hPutP :: (LabelState l p s, HandleOps Handle b IO) => p -> LHandle l -> b -> LIO l p s ()
-- | Synonym for hPutP.
hPutStrP :: (LabelState l p s, HandleOps Handle b IO) => p -> LHandle l -> b -> LIO l p s ()
-- | Output the given (Byte)String with an appended newline to the
-- specified labeled handle. Privileges are used in the label comparisons
-- and when raising the current label.
hPutStrLnP :: (LabelState l p s, HandleOps Handle b IO) => p -> LHandle l -> b -> LIO l p s ()
-- | Same as readFile but uses privilege in opening the file.
readFileP :: (HandleOps Handle b IO, LabelState l p s, Serialize l) => p -> FilePath -> LIO l p s b
-- | Same as writeFile but uses privilege in opening the file.
writeFileP :: (HandleOps Handle b IO, LabelState l p s, Serialize l) => p -> FilePath -> b -> LIO l p s ()
-- | Same as writeFileL but uses privilege in opening the file.
writeFileLP :: (HandleOps Handle b IO, LabelState l p s, Serialize l) => p -> l -> FilePath -> b -> LIO l p s ()
instance (LabelState l p s, CloseOps (LHandle l) (LIO l p s), HandleOps Handle b IO) => HandleOps (LHandle l) b (LIO l p s)
instance LabelState l p s => CloseOps (LHandle l) (LIO l p s)
instance (Serialize l, LabelState l p s) => DirectoryOps (LHandle l) (LIO l p s)
instance HandleOps Handle ByteString IO
instance CloseOps Handle IO
instance DirectoryOps Handle IO
-- | This module provides bindings for the DCLabel module, with
-- some renaming to resolve name clashes. The delegation of privilege and
-- other trusted code is not exported by this module and code wishing to
-- use this should import DCLabel.TCB.
module LIO.DCLabel
-- | A DCLabel category set.
type DCCatSet = Component
-- | A DCLabel (untrusted) privilege.
type DCPriv = Priv
-- | A DCLabel privilege.
type DCPrivTCB = TCBPriv
-- | The type for Labeled values uinsg DCLabel as the label.
type DCLabeled a = Labeled DCLabel a
-- | The monad for LIO computations using DCLabel as the label.
type DC = LIO DCLabel DCPrivTCB ()
-- | Runs a computation in the LIO Monad, returning both the computation's
-- result and the label of the result.
evalDC :: DC a -> IO (a, DCLabel)
-- | Same as evalDC, but with support for filesystem.
evalDCWithRoot :: FilePath -> Maybe DCLabel -> DC a -> IO (a, DCLabel)
-- | A DC Label gate
type DCGate = Gate DCLabel DCPriv
-- | Label corresponding to public data.
lpub :: DCLabel
instance Typeable DCLabel
instance Typeable Component
instance Typeable Conj
instance Typeable Disj
instance LabelState DCLabel DCPrivTCB ()
instance PrivDesc DCPrivTCB DCPriv
instance Priv DCLabel TCBPriv
instance MintTCB TCBPriv Principal
instance MintTCB TCBPriv Priv
instance PrivTCB TCBPriv
instance Label DCLabel
-- | This module provides a function liftLIO for executing
-- LIO computations from transformed versions of the LIO
-- monad. There is also a method liftIO, which is a synonym for
-- liftLIO, to help with porting code that expects to run in the
-- IO monad.
module LIO.MonadLIO
-- | MonadIO-like class.
class (Monad m, LabelState l p s) => MonadLIO m l p s | m -> l p s where liftIO = liftLIO
liftLIO :: MonadLIO m l p s => LIO l p s a -> m a
liftIO :: MonadLIO m l p s => LIO l p s a -> m a
instance [overlap ok] (MonadLIO m l p s, MonadTrans t, Monad (t m)) => MonadLIO (t m) l p s
instance [overlap ok] LabelState l p s => MonadLIO (LIO l p s) l p s
-- | This module exports the subset of symbols in the LIO.TCB module
-- that are safe for untrusted code to access. See the LIO.TCB
-- module for documentation.
module LIO.Safe
-- | This class defines a label format, corresponding to a bounded lattice.
-- Specifically, it is necessary to define a bottom element lbot
-- (in literature, written as ⊥), a top element ltop (in
-- literature, written as ⊤), a join, or least upper bound, lub
-- (in literature, written as ⊔), a meet, or greatest lower bound,
-- glb (in literature, written as ⊓), and of course the
-- can-flow-to partial-order leq (in literature, written as ⊑).
class (Eq a, Show a, Read a, Typeable a) => Label a
lbot :: Label a => a
ltop :: Label a => a
lub :: Label a => a -> a -> a
glb :: Label a => a -> a -> a
leq :: Label a => a -> a -> Bool
-- | This class defines privileges and the more-permissive relation
-- (leqp) on labels using privileges. Additionally, it defines
-- lostar which is used to compute the smallest difference between
-- two labels given a set of privilege.
class (Label l, Monoid p, PrivTCB p) => Priv l p where leqp p a b = lostar p a b `leq` b
leqp :: Priv l p => p -> l -> l -> Bool
lostar :: Priv l p => p -> l -> l -> l
-- | Alias for mempty.
noPrivs :: Monoid p => p
-- | Returns the current privileges.
getPrivileges :: LabelState l p s => LIO l p s p
-- | Execute an LIO action with a set of underlying privileges. Within a
-- withPrivileges block, the supplied privileges are used in
-- every even (non ...P) operation. For instance,
--
--
-- unlabelP p x
--
--
-- can instead be written as:
--
--
-- withPrivileges p $ unlabel x
--
--
-- The original privileges of the thread are restored after the action is
-- executed within the withPrivileges block. The
-- withPrivileges combinator provides a middle-ground between a
-- fully explicit, but safe, privilege use (...P combinators),
-- and an implicit, but less safe, interface (provide getter/setter, and
-- always use underlying privileges). It allows for the use of implicit
-- privileges by explicitly enclosing the code with a
-- withPrivileges block.
withPrivileges :: LabelState l p s => p -> LIO l p s a -> LIO l p s a
-- | Execute an LIO action with the combination of the supplied
-- privileges (usually passed to ...P functions) and current
-- privileges.
withCombinedPrivs :: LabelState l p s => p -> (p -> LIO l p s a) -> LIO l p s a
-- | Drop all privileges. It is useful to remove all privileges when
-- executing some untrusted code withing a withPrivileges block.
dropPrivileges :: LabelState l p s => LIO l p s ()
-- | LIO monad is a State monad transformer with IO as the underlying
-- monad.
data LIO l p s a
-- | Empty class used to specify the functional dependency between a label
-- and it state.
class (Priv l p, Label l) => LabelState l p s | l -> s, l -> p
-- | Produces an IO computation that will execute a particular
-- LIO computation. Because untrusted code cannot execute
-- IO computations, this function should only be useful within
-- trusted code. No harm is done from exposing the evalLIO
-- symbol to untrusted code. (In general, untrusted code is free to
-- produce IO computations--it just can't execute them without
-- access to ioTCB.)
evalLIO :: LabelState l p s => LIO l p s a -> s -> IO (a, l)
-- | Returns the current value of the thread's label.
getLabel :: LabelState l p s => LIO l p s l
-- | If the current label is oldLabel and the current clearance is
-- clearance, this function allows code to raise the label to
-- any value newLabel such that oldLabel `leq`
-- newLabel && newLabel `leq` clearance. Note that
-- there is no setLabel variant without the ...P
-- because the taint function provides essentially the same
-- functionality that setLabel would.
setLabelP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Returns the current value of the thread's clearance.
getClearance :: LabelState l p s => LIO l p s l
-- | Reduce the current clearance. One cannot raise the current label or
-- create object with labels higher than the current clearance.
lowerClr :: LabelState l p s => l -> LIO l p s ()
-- | Raise the current clearance (undoing the effects of lowerClr).
-- This requires privileges.
lowerClrP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Lowers the clearance of a computation, then restores the clearance to
-- its previous value. Useful to wrap around a computation if you want to
-- be sure you can catch exceptions thrown by it. Also useful to wrap
-- around toLabeled to ensure that the computation does not access
-- data exceeding a particular label. If withClearance is given
-- a label that can't flow to the current clearance, then the clearance
-- is lowered to the greatest lower bound of the label supplied and the
-- current clearance.
--
-- Note that if the computation inside withClearance acquires
-- any Privs, it may still be able to raise its clearance above
-- the supplied argument using lowerClrP.
withClearance :: LabelState l p s => l -> LIO l p s a -> LIO l p s a
-- | Returns label of a Labeled type.
labelOf :: Label l => Labeled l a -> l
-- | Function to construct a Labeled from a label and pure value. If
-- the current label is lcurrent and the current clearance is
-- ccurrent, then the label l specified must satisfy
-- lcurrent `leq` l && l `leq` ccurrent.
label :: LabelState l p s => l -> a -> LIO l p s (Labeled l a)
-- | Constructs a Labeled using privilege to allow the
-- Labeled's label to be below the current label. If the current
-- label is lcurrent and the current clearance is
-- ccurrent, then the privilege p and label l
-- specified must satisfy (leqp p lcurrent l) && l
-- `leq` ccurrent. Note that privilege is not used to bypass
-- the clearance. You must use lowerClrP to raise the clearance
-- first if you wish to create an Labeled at a higher label than
-- the current clearance.
labelP :: LabelState l p s => p -> l -> a -> LIO l p s (Labeled l a)
-- | Within the LIO monad, this function takes a Labeled and
-- returns the value. Thus, in the LIO monad one can say:
--
--
-- x <- unlabel (xv :: Labeled SomeLabelType Int)
--
--
-- And now it is possible to use the value of x, which is the
-- pure value of what was stored in xv. Of course,
-- unlabel also raises the current label. If raising the label
-- would exceed the current clearance, then unlabel throws
-- LerrClearance. However, you can use labelOf to check if
-- unlabel will succeed without throwing an exception.
unlabel :: LabelState l p s => Labeled l a -> LIO l p s a
-- | Extracts the value of an Labeled just like unlabel, but
-- takes a privilege argument to minimize the amount the current label
-- must be raised. Will still throw LerrClearance under the same
-- circumstances as unlabel.
unlabelP :: LabelState l p s => p -> Labeled l a -> LIO l p s a
-- | Raises the label of a Labeled to the lub of it's current
-- label and the value supplied. The label supplied must be less than the
-- current clearance, though the resulting label may not be if the
-- Labeled is already above the current thread's clearance.
taintLabeled :: LabelState l p s => l -> Labeled l a -> LIO l p s (Labeled l a)
-- | Downgrades the label of a Labeled as much as possible given the
-- current privilege.
untaintLabeled :: LabelState l p s => l -> Labeled l a -> LIO l p s (Labeled l a)
-- | Same as untaintLabeled but combines the current privilege with
-- the supplied privilege when downgrading the label.
untaintLabeledP :: LabelState l p s => p -> l -> Labeled l a -> LIO l p s (Labeled l a)
-- | Relabeles a Labeled value if the given privilege combined
-- with the current privileges permits it.
relabelP :: LabelState l p s => p -> l -> Labeled l a -> LIO l p s (Labeled l a)
-- | toLabeled is the dual of unlabel. It allows one to
-- invoke computations that would raise the current label, but without
-- actually raising the label. Instead, the result of the computation is
-- packaged into a Labeled with a supplied label. (Of couse, the
-- computation executed by toLabeled must most observe any data
-- whose label exceeds the supplied label.)
--
-- To get at the result of the computation one will have to call
-- unlabel and raise the label, but this can be postponed, or done
-- inside some other call to toLabeled. This suggests that the
-- provided label must be above the current label and below the current
-- clearance.
--
-- Note that toLabeled always restores the clearance to whatever
-- it was when it was invoked, regardless of what occurred in the
-- computation producing the value of the Labeled. This highlights
-- one main use of clearance: to ensure that a Labeled computed
-- does not exceed a particular label.
--
-- If an exception is thrown within a toLabeled block, such that
-- the outer context is withing a catch, which is futher within a
-- toLabeled block, infromation can be leaked. Consider the
-- following program that uses DCLabels. (Note that
-- discard is simply toLabeled that throws throws the
-- result away.)
--
--
-- main = evalDC' $ do
-- lRef <- newLIORef lbot ""
-- hRef <- newLIORef ltop "secret"
-- -- brute force:
-- forM_ ["fun", "secret"] $ \guess -> do
-- stash <- readLIORef lRef
-- writeLIORef lRef $ stash ++ "\n" ++ guess ++ ":"
-- discard ltop $ do
-- catch ( discard ltop $ do
-- secret <- readLIORef hRef
-- when (secret == guess) $ throwIO . userError $ "got it!"
-- ) (\(e :: IOError) -> return ())
-- l <- getLabel
-- when (l == lbot) $ do stash <- readLIORef lRef
-- writeLIORef lRef $ stash ++ "no!"
-- readLIORef lRef
-- where evalDC' act = do (r,l) <- evalDC act
-- putStrLn r
-- putStrLn $ "label = " ++ prettyShow l
--
--
-- The output of the program is:
--
--
-- $ ./new
--
-- fun:no!
-- secret:
-- label = <True , False>
--
--
-- Note that the current label is lbot (which in DCLabels is
-- True , False), and the secret is leaked. The
-- fundamental issue is that the outer discard allows for the
-- current label to remain low even though the catch raised the
-- current label when the secret was found (and thus exception was
-- throw). As a consequence, toLabeled catches all exceptions, and
-- returns a Labeled value that may have a labeled exception as
-- wrapped by throw. All exceptions within the outer
-- computation, including IFC violation attempts, are essentially
-- rethrown when performing an unlabel.
--
-- DEPRECATED: toLabeled is susceptible to termination attacks.
toLabeled :: LabelState l p s => l -> LIO l p s a -> LIO l p s (Labeled l a)
-- | Same as toLabeled but allows one to supply a privilege object
-- when comparing the initial and final label of the computation.
--
-- DEPRECATED: toLabeledP is susceptible to termination attacks.
toLabeledP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s (Labeled l a)
-- | Executes a computation that would raise the current label, but
-- discards the result so as to keep the label the same. Used when one
-- only cares about the side effects of a computation. For instance, if
-- log_handle is an LHandle with a high label, one can
-- execute
--
--
-- discard ltop $ hputStrLn log_handle "Log message"
--
--
-- to create a log message without affecting the current label.
--
-- DEPRECATED: discard is susceptible to termination attacks.
discard :: LabelState l p s => l -> LIO l p s a -> LIO l p s ()
-- | Same as discard, but uses privileges when comparing initial and
-- final label of the computation.
discardP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s ()
-- | Use taint l in trusted code before observing an object
-- labeled l. This will raise the current label to a value
-- l' such that l `leq` l', or throw
-- LerrClearance if l' would have to be higher
-- than the current clearance.
taint :: LabelState l p s => l -> LIO l p s ()
-- | Like taint, but use privileges to reduce the amount of taint
-- required. Note that unlike setLabelP, taintP will
-- never lower the current label. It simply uses privileges to avoid
-- raising the label as high as taint would raise it.
taintP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Use wguard l in trusted code before modifying an object
-- labeled l. If l' is the current label, then this
-- function ensures that l' `leq` l before doing the same
-- thing as taint l. Throws LerrHigh if
-- the current label l' is too high.
wguard :: LabelState l p s => l -> LIO l p s ()
-- | Like wguard, but takes privilege argument to be more
-- permissive.
wguardP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Ensures the label argument is between the current IO label and current
-- IO clearance. Use this function in code that allocates
-- objects--untrusted code shouldn't be able to create an object labeled
-- l unless aguard l does not throw an exception.
aguard :: LabelState l p s => l -> LIO l p s ()
-- | Like aguardP, but takes privilege argument to be more
-- permissive.
aguardP :: LabelState l p s => p -> l -> LIO l p s ()
-- | Labeled is a type representing labeled data.
data Labeled l t
-- | Violation of information flow conditions, or label checks should throw
-- exceptions of type LabelFault. The LerrInval
-- constructor takes a string parameter -- it is important that trusted
-- code use this carefully and aovid leaking information through it.
data LabelFault
-- | Requested label too low
LerrLow :: LabelFault
-- | Current label too high
LerrHigh :: LabelFault
-- | Label would exceed clearance
LerrClearance :: LabelFault
-- | Insufficient privileges
LerrPriv :: LabelFault
-- | Invalid request
LerrInval :: String -> LabelFault
-- | Catches an exception, so long as the label at the point where the
-- exception was thrown can flow to the label at which catchP is
-- invoked, modulo the privileges specified. Note that the handler raises
-- the current label to the joint of the current label and exception
-- label.
catchP :: (Exception e, LabelState l p s) => p -> LIO l p s a -> (e -> LIO l p s a) -> LIO l p s a
-- | Version of catchP with arguments swapped.
handleP :: (Exception e, LabelState l p s) => p -> (e -> LIO l p s a) -> LIO l p s a -> LIO l p s a
-- | onException cannot run its handler if the label was raised in
-- the computation that threw the exception. This variant allows
-- privileges to be supplied, so as to catch exceptions thrown with a
-- raised label.
onExceptionP :: LabelState l p s => p -> LIO l p s a -> LIO l p s b -> LIO l p s a
-- | Like standard bracket, but with privileges to downgrade
-- exception.
bracketP :: LabelState l p s => p -> LIO l p s a -> (a -> LIO l p s c) -> (a -> LIO l p s b) -> LIO l p s b
-- | Forces its argument to be evaluated to weak head normal form when the
-- resultant LIO action is executed. This is simply a wrapper for
-- Control.Exception's evaluate.
evaluate :: LabelState l p s => a -> LIO l p s a
-- | Class used to describe privileges in a meaningful manner.
class (PrivTCB p, Show d) => PrivDesc p d | p -> d
-- | A Gate is a wrapper for a Labeled type.
data Gate l d a
-- | Create a gate given a gate label and computation. The label of the
-- gate must be bounded by the current label and clearance.
mkGate :: (LabelState l p s, PrivDesc p d) => l -> (d -> a) -> LIO l p s (Gate l d a)
-- | Same as mkGate, but uses privileges when making the gate.
mkGateP :: (LabelState l p s, PrivDesc p d) => p -> l -> (d -> a) -> LIO l p s (Gate l d a)
-- | Given a labeled gate and privilege, execute the gate computation. The
-- current label is raised to the join of the gate and current label,
-- clearance permitting. It is important to note that callGate
-- invokes the gate computation with the privilege description and
-- not the actual privilege.
callGate :: (LabelState l p s, PrivDesc p d) => Gate l d a -> p -> LIO l p s a
-- | This is the main module to be included by code using the Labeled IO
-- (LIO) library. The core of the library is documented in the
-- LIO.TCB module. Note, however, that unprivileged code must not
-- be allowed to import LIO.TCB--instead, a module LIO.Safe
-- exports just the safe symbols from LIO.TCB. This module,
-- LIO, re-exports LIO.Safe as well as a few other handy
-- modules. For many modules it should be the only import necessary.
--
-- Certain symbols in the LIO library supersede variants in the standard
-- Haskell libraries. Thus, depending on the modules imported and
-- functions used, you may wish to import LIO with commands like these:
--
--
-- import Prelude hiding (catch)
-- import Control.Exception hiding (throwIO, catch, handle, onException
-- , bracket, block, unblock)
-- import LIO
--
--
-- The LIO variants of the system functions hidden in the above import
-- commands are designed to work in both the IO and LIO monads, making it
-- easier to have both types of code in the same module.
--
-- Warning: For security, at a minimum untrusted code must not be allowed
-- to do any of the following:
--
--
-- - Import LIO.TCB,
-- - Use any symbols with names ending ...TCB,
-- - Use the foreign keyword,
-- - Use functions such as unsafePerformIO,
-- unsafeInterleaveIO, inlinePerformIO,
-- - Use language extensions such as Generalized Newtype Deriving and
-- Stand-alone Deriving to extend LIO types (such as by deriving an
-- instance of Show for Lref, or deriving an
-- instance of the MonadTrans class for LIO,
-- which would allow untrusted code to bypass all security with
-- lift),
-- - Manually define typeOf methods (as this would cause the
-- supposedly safe cast method to make usafe casts);
-- automatically deriving Typeable should be safe.
-- - Define new Ix instances (which could produce out of
-- bounds array references).
--
--
-- In general, pragmas and imports should be highly scrutinized. For
-- example, most of the Foreign class of modules are probably
-- dangerous. With GHC 7.2, we use the SafeHaskell extension to enforce
-- these restrictions.
module LIO