-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Labeled IO Information Flow Control Library
--
-- 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.
--
-- 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.)
-- 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.
--
-- 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.
@package lio
@version 0.10.0.0
-- | 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 ⊑).
--
-- 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.
--
-- Conversely, it is only permissible to modify data labeled L_w
-- when L_cur`canFlowTo` L_w, a property often cited as
-- "no write down", but more accurately characterized as "write only what
-- you can flow to". In practice, there are very few IO abstractions
-- (namely, mutable references) in which it is possible to do a pure
-- write that doesn't also involve observing some state. For instance,
-- writing to a file handle and not getting an exception tells you that
-- the handle is not closed. Thus, in practice, the requirement for
-- modifying data labeled L_w is almost always that L_cur
-- `canFlowTo` L_w and L_w `canFlowTo` L_cur,
-- i.e., L_cur == L_w.
--
-- Note that higher labels are neither more nor less privileged than
-- lower ones. Simply, the higher one's label is, the more things one can
-- read. Conversely, the lower one's label, the more things one can
-- write. But, because labels are a partial and not a total order, some
-- data may be completely inaccessible to a particular computation; for
-- instance, if the current label is L_cur, the current
-- clearance is C_cur, and some data is labeled L_d,
-- such that not (L_cur `canFlowTo` L_d || L_d
-- `canFlowTo` C_cur), then the current thread can neither
-- read nor write the data, at least without invoking some privilege.
--
-- LIO is polymorphic in the label type. It is solely required that every
-- implementation of a label (usually called a label format) be an
-- instance of the Label class. This class provides a generic
-- interface to labels: they must define the canFlowTo relation,
-- some minimal element bottom, some maximum element
-- top, and two binary operators on how to combine labels: the
-- least upper bound (lub) and greatest lower bound (glb).
--
-- Since LIO associates labels with different data types, it is useful to
-- be able to access the label of such objects (when the label is solely
-- protected by the current label). To this end, LIO provides the
-- LabelOf type class for which different labeled objects
-- implementations provide an instance.
module LIO.Label
-- | 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 ⊥), a top element
-- top (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 canFlowTo (in literature, written
-- as ⊑).
class (Eq l, Show l) => Label l
lub :: Label l => l -> l -> l
glb :: Label l => l -> l -> l
canFlowTo :: Label l => 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
-- LVals 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
labelOf :: LabelOf t => t l a -> l
-- | 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.
--
--
-- The documentation and external, safe LIO interface is provided
-- in LIO.Core.
module LIO.TCB
-- | Internal state of an LIO computation.
data LIOState l
LIOState :: !l -> !l -> LIOState l
-- | Current label.
lioLabel :: LIOState l -> !l
-- | Current clearance.
lioClearance :: LIOState l -> !l
-- | 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 :: (IORef (LIOState l) -> IO a) -> LIO l a
unLIOTCB :: LIO l a -> IORef (LIOState l) -> IO a
-- | Get internal state. This function is not actually unsafe, but to avoid
-- future security bugs we leave all direct access to the internal state
-- to trusted code.
getLIOStateTCB :: LIO l (LIOState l)
-- | Set internal state.
putLIOStateTCB :: LIOState l -> LIO l ()
-- | Update the internal state given some function.
modifyLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()
-- | Deprecated: Use modifyLIOStateTCB instead
updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()
-- | Lifts an IO computation into the LIO monad. Note that
-- exceptions thrown within the IO computation cannot directly be
-- caught within the LIO computation. Thus, you will generally
-- want to use rethrowIoTCB.
ioTCB :: IO a -> LIO l a
-- | A newtype wrapper that can be used by trusted code to bless
-- privileges. Privilege-related functions are defined in
-- LIO.Privs, but the constructor, PrivTCB, allows one to
-- mint arbitrary privileges and hence must be located in this file.
newtype Priv a
PrivTCB :: a -> Priv a
-- | Labeled l a is a value that associates a label of type
-- l with a value of type a. Labeled values allow users
-- to label data with a label other than the current label. In an
-- embedded setting this is akin to having first class labeled values.
-- Note that Labeled is an instance of LabelOf, which
-- effectively means that the label of a Labeled value is usually
-- just protected by the current label. (Of course if you have a nested
-- labeled value then the label on the inner labeled value's label is the
-- outer label.)
data Labeled l t
LabeledTCB :: !l -> t -> Labeled l t
-- | An uncatchable exception hierarchy use to terminate an untrusted
-- thread. Wrap the uncatchable exception in UncatchableTCB before
-- throwing it to the thread. runLIO will subsequently unwrap
-- the UncatchableTCB constructor.
--
-- Note this can be circumvented by mapException, which should be
-- made unsafe.
data UncatchableTCB
UncatchableTCB :: e -> UncatchableTCB
-- | Simple utility function that strips UncatchableTCB from around
-- an exception.
makeCatchable :: SomeException -> SomeException
-- | 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 strings that were created 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
instance Typeable2 LIO
instance Typeable UncatchableTCB
instance Typeable1 Priv
instance Typeable2 Labeled
instance Eq l => Eq (LIOState l)
instance Show l => Show (LIOState l)
instance Read l => Read (LIOState l)
instance Show a => Show (Priv a)
instance Eq a => Eq (Priv a)
instance (Label l, Read l, Read a) => ReadTCB (Labeled l a)
instance (Label l, Show a) => ShowTCB (Labeled l a)
instance LabelOf Labeled
instance Monoid p => Monoid (Priv p)
instance Exception UncatchableTCB
instance Show UncatchableTCB
instance Applicative (LIO l)
instance Functor (LIO l)
instance Monad (LIO l)
-- | Exception routines much like the IO ones in
-- Control.Exception (we duplicate the documentation below). There
-- are two differences, however. First, LIO does not allow masking of
-- asynchronous exceptions (since these are relied upon to kill a
-- misbehaving thread). Hence, routines like onException are not
-- guaranteed to run if a thread is unconditionally killed. Second, in a
-- few cases (such as lWait) it is possible for the current
-- label to be raised above the current clearance as an exception is
-- thrown, in which case these functions do not catch the exception,
-- either, since code cannot run under such circumstances.
module LIO.Exception
-- | Any type that you wish to throw or catch as an exception must be an
-- instance of the Exception class. The simplest case is a new
-- exception type directly below the root:
--
--
-- data MyException = ThisException | ThatException
-- deriving (Show, Typeable)
--
-- instance Exception MyException
--
--
-- The default method definitions in the Exception class do what
-- we need in this case. You can now throw and catch
-- ThisException and ThatException as exceptions:
--
--
-- *Main> throw ThisException `catch` \e -> putStrLn ("Caught " ++ show (e :: MyException))
-- Caught ThisException
--
--
-- In more complicated examples, you may wish to define a whole hierarchy
-- of exceptions:
--
--
-- ---------------------------------------------------------------------
-- -- Make the root exception type for all the exceptions in a compiler
--
-- data SomeCompilerException = forall e . Exception e => SomeCompilerException e
-- deriving Typeable
--
-- instance Show SomeCompilerException where
-- show (SomeCompilerException e) = show e
--
-- instance Exception SomeCompilerException
--
-- compilerExceptionToException :: Exception e => e -> SomeException
-- compilerExceptionToException = toException . SomeCompilerException
--
-- compilerExceptionFromException :: Exception e => SomeException -> Maybe e
-- compilerExceptionFromException x = do
-- SomeCompilerException a <- fromException x
-- cast a
--
-- ---------------------------------------------------------------------
-- -- Make a subhierarchy for exceptions in the frontend of the compiler
--
-- data SomeFrontendException = forall e . Exception e => SomeFrontendException e
-- deriving Typeable
--
-- instance Show SomeFrontendException where
-- show (SomeFrontendException e) = show e
--
-- instance Exception SomeFrontendException where
-- toException = compilerExceptionToException
-- fromException = compilerExceptionFromException
--
-- frontendExceptionToException :: Exception e => e -> SomeException
-- frontendExceptionToException = toException . SomeFrontendException
--
-- frontendExceptionFromException :: Exception e => SomeException -> Maybe e
-- frontendExceptionFromException x = do
-- SomeFrontendException a <- fromException x
-- cast a
--
-- ---------------------------------------------------------------------
-- -- Make an exception type for a particular frontend compiler exception
--
-- data MismatchedParentheses = MismatchedParentheses
-- deriving (Typeable, Show)
--
-- instance Exception MismatchedParentheses where
-- toException = frontendExceptionToException
-- fromException = frontendExceptionFromException
--
--
-- We can now catch a MismatchedParentheses exception as
-- MismatchedParentheses, SomeFrontendException or
-- SomeCompilerException, but not other types, e.g.
-- IOException:
--
--
-- *Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: MismatchedParentheses))
-- Caught MismatchedParentheses
-- *Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: SomeFrontendException))
-- Caught MismatchedParentheses
-- *Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: SomeCompilerException))
-- Caught MismatchedParentheses
-- *Main> throw MismatchedParentheses catch e -> putStrLn ("Caught " ++ show (e :: IOException))
-- *** Exception: MismatchedParentheses
--
class (Typeable e, Show e) => Exception e
toException :: Exception e => e -> SomeException
fromException :: Exception e => SomeException -> Maybe e
-- | The SomeException type is the root of the exception type
-- hierarchy. When an exception of type e is thrown, behind the
-- scenes it is encapsulated in a SomeException.
data SomeException :: *
SomeException :: e -> SomeException
throwLIO :: Exception e => e -> LIO l a
-- | A simple wrapper around IO catch. The only subtlety is that code is
-- not allowed to run unless the current label can flow to the current
-- clearance. Hence, if the label exceeds the clearance, the exception is
-- not caught. (Only a few conditions such as lWait or raising
-- the clearance within scopeClearance can lead to the label
-- exceeding the clarance, and an exception is always thrown at the time
-- this happens.)
catch :: (Label l, Exception e) => LIO l a -> (e -> LIO l a) -> LIO l a
-- | A version of catch with the arguments swapped around.
handle :: (Label l, Exception e) => (e -> LIO l a) -> LIO l a -> LIO l a
-- | Similar to catch, but returns an Either result which is
-- (Right a) if no exception of type e was
-- raised, or (Left ex) if an exception of type
-- e was raised and its value is ex. If any other type
-- of exception is raised than it will be propogated up to the next
-- enclosing exception handler.
try :: (Label l, Exception a1) => LIO l a -> LIO l (Either a1 a)
-- | Like finally, but only performs the final action if there was
-- an exception raised by the computation.
onException :: Label l => LIO l a -> LIO l b -> LIO l a
-- | A variant of bracket where the return value from the first
-- computation is not required.
finally :: Label l => LIO l a -> LIO l b -> LIO l a
-- | When you want to acquire a resource, do some work with it, and then
-- release the resource, it is a good idea to use bracket,
-- because bracket will install the necessary exception handler to
-- release the resource in the event that an exception is raised during
-- the computation. If an exception is raised, then bracket will re-raise
-- the exception (after performing the release).
bracket :: Label l => LIO l a -> (a -> LIO l c) -> (a -> LIO l b) -> LIO l b
-- | Forces its argument to be evaluated to weak head normal form when the
-- resultant LIO action is executed.
evaluate :: a -> LIO l a
-- | 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
-- | 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 canFlowToPrivDesc p a b = partDowngradePrivDesc p a b `canFlowTo` b
canFlowToPrivDesc :: PrivDesc l p => p -> l -> l -> Bool
partDowngradePrivDesc :: PrivDesc l p => p -> l -> l -> l
-- | TODO(dm): document
canFlowToP :: PrivDesc l p => Priv p -> l -> l -> Bool
-- | TODO(dm): document
partDowngradeP :: PrivDesc l p => Priv p -> l -> l -> l
-- | 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.
data Priv a
privDesc :: Priv a -> a
-- | Generic privilege type used to denote the lack of privileges.
data NoPrivs
noPrivs :: Priv NoPrivs
-- | 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.
data Gate d a
-- | Create a gate given a computation from a privilege description. Note
-- that because of currying type a may itself be a function type
-- and thus gates can take arguments in addition to the privilege
-- descriptoin.
gate :: (d -> a) -> Gate d a
-- | 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 -> Priv p -> a
instance Show NoPrivs
instance Read NoPrivs
instance Label l => PrivDesc l NoPrivs
instance Monoid NoPrivs
-- | This module contains functions to launch LIO computations from
-- within the IO monad. These functions are not useful from within
-- LIO code (but not harmful either, since their types are in the
-- IO monad).
--
-- This module is intended to be imported into your Main module, for use
-- in invoking LIO code. The functions are also available via
-- LIO and LIO.Core, but those modules will clutter your
-- namespace with symbols you don't need in the IO monad.
module LIO.Run
-- | Internal state of an LIO computation.
data LIOState l
LIOState :: !l -> !l -> LIOState l
-- | Current label.
lioLabel :: LIOState l -> !l
-- | Current clearance.
lioClearance :: LIOState l -> !l
-- | Execute an LIO action, returning its result and the final label
-- state as a pair. Note that it returns a pair whether or not the
-- LIO action throws an exception. Forcing the result value will
-- re-throw the exception, but the label state will always be valid.
--
-- See also evalLIO.
runLIO :: LIO l a -> LIOState l -> IO (a, LIOState l)
-- | Given an LIO computation and some initial state, return an IO
-- action which when executed will perform the IFC-safe LIO computation.
--
-- Because untrusted code cannot execute IO computations, this
-- function should only be useful within trusted code. No harm is done
-- from exposing the evalLIO symbol to untrusted code. (In
-- general, untrusted code is free to produce IO computations, but
-- it cannot execute them.)
--
-- Unlike runLIO, this function throws an exception if the
-- underlying LIO action terminates with an exception.
evalLIO :: LIO l a -> LIOState l -> IO a
-- | This module implements the core of the Labeled IO (LIO) library for
-- information flow control (IFC) in Haskell. It provides a monad,
-- LIO, that is intended to be used as a replacement for the
-- IO monad in untrusted code. The idea is for untrusted code to
-- provide a computation in the LIO monad, which trusted code can
-- then safely execute through using evalLIO-like functions.
-- Though, usually a wrapper function is employed depending on the type
-- of labels used by an application. For example, with
-- LIO.DCLabel trusted code would evalDC to execute an
-- untrusted computation.
--
-- Labels are a way of describing who can observe and modify data. (A
-- detailed consideration of labels is given in LIO.Label.) LIO
-- associates a current label with every LIO computation.
-- The current label effectively tracks the sensitivity of all the data
-- that the computation has observed. For example, if the computation has
-- read a "secret" mutable refernce (see LIO.LIORef) and then the
-- result of a "top-secret" thread (see LIO.Concurrent) then the
-- current label will be at least "top-secret". The role of the current
-- label is two-fold. First, the current label protects all the data in
-- scope -- it is the label associated with any unlabeled data.
-- For example, the current label is the label on constants such as
-- 3 or "tis a string". More interestingly, consider
-- reading a "secret" file:
--
--
-- bs <- readFile "/secret/file.txt"
--
--
-- Though the label in the file store may be "secret", bs has
-- type ByteString, which is not explicitly labeled. Hence, to
-- protect the contents (bs) the current label must be at least
-- "secret" before executing readFile. More generally, if the
-- current label is L_cur, then it is only permissible to read
-- data labeled L_r if L_r `canFlowTo` L_cur.
-- Note that, rather than throw an exception, reading data will often
-- just increase the current label to ensure that L_r
-- `canFlowTo` L_cur using taint.
--
-- Second, the current label prevents inforation leaks into public
-- channels. Specifically, it is only permissible to modify, or write to,
-- data labeled L_w when L_cur`canFlowTo` L_w.
-- Thus, it the following attempt to leak the secret bs would
-- fail:
--
--
-- writeFile "/public/file.txt" bs
--
--
-- In addition to the current label, the LIO monad keeps a second label,
-- the current clearance (accessible via the getClearance
-- function). The clearance can be used to enforce a "need-to-know"
-- policy since it represents the highest value the current label can be
-- raised to. In other words, if the current clearance is
-- L_clear then the computation cannot create, read or write to
-- objects labeled L such that L `canFlowTo`
-- L_clear does not hold.
--
-- This module exports the LIO monad, functions to access the
-- internal state (e.g., getLabel and getClearance),
-- functions for raising and catching exceptions, and IFC guards.
-- Exceptions are core to LIO since they provide a way to deal with
-- potentially-misbehaving untrusted code. Specifically, when a
-- computation is about to violate IFC (as writeFile above), an
-- exception is raised. Guards provide a useful abstraction for dealing
-- with labeled objects; they should be used before performing a
-- read-only, write-only, or read-write operation on a labeled object.
-- The remaining core, but not all, abstractions are exported by
-- LIO.
module LIO.Core
-- | 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.
data LIO l a
-- | Synonym for monad in which LIO is the base monad.
class (Monad m, Label l) => MonadLIO l m | m -> l
liftLIO :: MonadLIO l m => LIO l a -> m a
-- | Internal state of an LIO computation.
data LIOState l
LIOState :: !l -> !l -> LIOState l
-- | Current label.
lioLabel :: LIOState l -> !l
-- | Current clearance.
lioClearance :: LIOState l -> !l
-- | Given an LIO computation and some initial state, return an IO
-- action which when executed will perform the IFC-safe LIO computation.
--
-- Because untrusted code cannot execute IO computations, this
-- function should only be useful within trusted code. No harm is done
-- from exposing the evalLIO symbol to untrusted code. (In
-- general, untrusted code is free to produce IO computations, but
-- it cannot execute them.)
--
-- Unlike runLIO, this function throws an exception if the
-- underlying LIO action terminates with an exception.
evalLIO :: LIO l a -> LIOState l -> IO a
-- | Execute an LIO action, returning its result and the final label
-- state as a pair. Note that it returns a pair whether or not the
-- LIO action throws an exception. Forcing the result value will
-- re-throw the exception, but the label state will always be valid.
--
-- See also evalLIO.
runLIO :: LIO l a -> LIOState l -> IO (a, LIOState l)
-- | Returns the current value of the thread's label.
getLabel :: Label l => LIO l l
-- | Raise the current label to the provided label, which must be between
-- the current label and clearance. See taint.
setLabel :: Label l => l -> LIO 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.
setLabelP :: PrivDesc l p => Priv p -> l -> LIO l ()
-- | Returns the current value of the thread's clearance.
getClearance :: Label l => LIO l l
-- | Lower the current clearance. The new clerance must be between the
-- current label and clerance. One cannot raise the current label or
-- create object with labels higher than the current clearance.
setClearance :: Label l => l -> LIO l ()
-- | Raise the current clearance (undoing the effects of
-- setClearance) by exercising privileges. If the current label is
-- l and current clearance is c, then setClearanceP
-- p cnew succeeds only if the new clearance is can flow to the
-- current clearance (modulo privileges), i.e., canFlowToP p
-- cnew c must hold. Additionally, the current label must flow to
-- the new clearance, i.e., l `canFlowTo` cnew must hold.
setClearanceP :: PrivDesc l p => Priv p -> l -> LIO l ()
-- | Runs an LIO action and re-sets the current clearance to its
-- previous value once the action returns. In particular, if the action
-- lowers the current clearance, the clearance will be restored upon
-- return.
--
-- Note that scopeClearance always restores the clearance. If
-- that causes the clearance to drop below the current label, a
-- ClearanceViolation exception is thrown. That exception can only
-- be caught outside a second scopeClearance that restores the
-- clearance to higher than the current label.
scopeClearance :: Label l => LIO l a -> LIO l a
-- | Lowers the clearance of a computation, then restores the clearance to
-- its previous value (actually, to the upper bound of the current label
-- and previous value). Useful to wrap around a computation if you want
-- to be sure you can catch exceptions thrown by it. The supplied
-- clearance label must be bounded by the current label and clearance as
-- enforced by guardAlloc.
--
-- Note that if the computation inside withClearance acquires
-- any Privs, it may still be able to raise its clearance above
-- the supplied argument using setClearanceP.
withClearance :: Label l => l -> LIO l a -> LIO l a
-- | Same as withClearance, but uses privileges when applying
-- guardAllocP to the supplied label.
withClearanceP :: PrivDesc l p => Priv p -> l -> LIO l a -> LIO l a
-- | Exceptions thrown when some IFC restriction is about to be violated.
data MonitorFailure
-- | Current label would exceed clearance, or object label is above
-- clearance.
ClearanceViolation :: MonitorFailure
-- | Clearance would be below current label, or object label is not above
-- current label.
CurrentLabelViolation :: MonitorFailure
-- | Insufficient privileges. Thrown when lowering the current label or
-- raising the clearance cannot be accomplished with the supplied
-- privileges.
InsufficientPrivs :: MonitorFailure
-- | Generic can-flow-to failure, use with VMonitorFailure
CanFlowToViolation :: MonitorFailure
ResultExceedsLabel :: MonitorFailure
-- | Verbose version of MonitorFailure also carrying around a
-- detailed message.
data VMonitorFailure
VMonitorFailure :: MonitorFailure -> String -> VMonitorFailure
-- | Generic monitor failure.
monitorFailure :: VMonitorFailure -> MonitorFailure
-- | Detailed message of failure.
monitorMessage :: VMonitorFailure -> String
-- | Ensures the label argument is between the current IO label and current
-- IO clearance. Use this function in code that allocates
-- objects--untrusted code shouldn't be able to create an object labeled
-- l unless guardAlloc l does not throw an exception.
-- Similarly use this guard in any code that writes to an object labeled
-- l for which the write has no observable side-effects.
--
-- If the label does not flow to clearance ClearanceViolation is
-- thrown; if the current label does not flow to the argument label
-- CurrentLabelViolation is thrown.
guardAlloc :: Label l => l -> LIO l ()
-- | 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 ()
-- | Use taint l in trusted code before observing an object
-- labeled l. This will raise the current label to a value
-- l' such that l `canFlowTo` l', or throw
-- ClearanceViolation if l' would have to be higher than
-- the current clearance.
taint :: Label l => l -> LIO l ()
-- | Like taint, but use privileges to reduce the amount of taint
-- required. Note that taintP will never lower the current
-- label. It simply uses privileges to avoid raising the label as high as
-- taint would raise it.
taintP :: PrivDesc l p => Priv p -> l -> LIO l ()
-- | Use guardWrite l in any (trusted) code before modifying an
-- object labeled l, for which a the modification can be
-- observed, i.e., the write implies a read.
--
-- The implementation of guardWrite is straight forward:
--
--
-- guardWrite l = taint l >> guardAlloc l
--
--
-- This guarantees that l `canFlowTo` the current label
-- (and clearance), and that the current label `canFlowTo`
-- l.
guardWrite :: Label l => l -> LIO l ()
-- | Like guardWrite, but takes privilege argument to be more
-- permissive.
guardWriteP :: PrivDesc l p => Priv p -> l -> LIO l ()
instance Typeable MonitorFailure
instance Typeable VMonitorFailure
instance Show MonitorFailure
instance Label l => MonadLIO l (LIO l)
instance Exception VMonitorFailure
instance Show VMonitorFailure
instance Exception MonitorFailure
-- | A data type Labeled protects access to pure values (hence, we
-- refer to values of type Label a as labeled
-- values). The role of labeled values is to allow users to associate
-- heterogeneous labels (see LIO.Label) with values. Although
-- LIO's current label protects all values in scope with the current
-- label, Labeled values allow for more fine grained protection.
-- Moreover, trusted code may easily inspect Labeled values, for
-- instance, when inserting values into a database.
--
-- Without the appropriate privileges, one cannot produce a pure
-- unlabeled value that depends on a secret Labeled value,
-- or conversely produce a high-integrity Labeled value based on
-- pure data. This module exports functions for creating labeled values
-- (label), using the values protected by Labeled by
-- unlabeling them (unlabel), and changing the value of a labeled
-- value without inspection (relabelLabeledP, taintLabeled,
-- untaintLabeled). A Functor-like class
-- (LabeledFunctor) on Labeled is also defined in this
-- module.
module LIO.Labeled
-- | Labeled l a is a value that associates a label of type
-- l with a value of type a. Labeled values allow users
-- to label data with a label other than the current label. In an
-- embedded setting this is akin to having first class labeled values.
-- Note that Labeled is an instance of LabelOf, which
-- effectively means that the label of a Labeled value is usually
-- just protected by the current label. (Of course if you have a nested
-- labeled value then the label on the inner labeled value's label is the
-- outer label.)
data Labeled l t
-- | Function to construct a Labeled from a label and pure value. If
-- the current label is lcurrent and the current clearance is
-- ccurrent, then the label l specified must satisfy
-- lcurrent `canFlowTo` l && l `canFlowTo`
-- ccurrent. Otherwise an exception is thrown (see
-- guardAlloc).
label :: Label l => l -> a -> LIO l (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 canFlowTo p lcurrent l and l
-- `canFlowTo` ccurrent. Note that privilege is not used to
-- bypass the clearance. You must use setClearanceP to raise the
-- clearance first if you wish to create an Labeled at a higher
-- label than the current clearance.
labelP :: PrivDesc l p => Priv p -> l -> a -> LIO l (Labeled l a)
-- | Within the LIO monad, this function takes a Labeled and
-- returns the underlying value. Thus, in the LIO monad one can
-- say:
--
--
-- x <- unlabel (xv :: Labeled SomeLabelType Int)
--
--
-- And now it is possible to use the value of x :: Int, which is
-- the pure value of what was stored in xv. Of course,
-- unlabel also raises the current label. If raising the label
-- would exceed the current clearance, then unlabel throws
-- ClearanceViolation. However, you can use labelOf to
-- check if unlabel will succeed without throwing an exception.
unlabel :: Label l => Labeled l a -> LIO l 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. Function will throw ClearanceViolation under
-- the same circumstances as unlabel.
unlabelP :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a
-- | Relabels a Labeled value to the supplied label if the given
-- privilege privileges permits it. An exception is thrown unless the
-- following two conditions hold:
--
--
-- - The new label must be between the current label and clearance
-- (modulo privileges), as enforced by guardAllocP.
-- - The old label must flow to the new label (again modulo
-- privileges), as enforced by canFlowToP.
--
relabelLabeledP :: PrivDesc l p => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)
-- | Raises the label of a Labeled to the upperBound of
-- it's current label and the value supplied. The label supplied must be
-- bounded by the current label and clearance, though the resulting label
-- may not be if the Labeled is already above the current thread's
-- clearance. If the supplied label is not bounded then
-- taintLabeled will throw an exception (see guardAlloc).
taintLabeled :: Label l => l -> Labeled l a -> LIO l (Labeled l a)
-- | Same as taintLabeled, but uses privileges when comparing the
-- current label to the supplied label. In other words, this function can
-- be used to lower the label of the labeled value by leveraging the
-- supplied privileges.
taintLabeledP :: PrivDesc l p => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)
-- | Downgrades a label.
untaintLabeledP :: PrivDesc l p => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)
-- | Similar to fmap, apply function to the Labeled value.
-- The label of the returned value is the least upper bound of the
-- current label and label of the supplied labeled value.
lFmap :: Label l => Labeled l a -> (a -> b) -> LIO l (Labeled l b)
-- | Similar to ap, apply function (wrapped by Labeled) to
-- the labeld value. The label of the returned value is the least upper
-- bound of the current label, label of the supplied labeled value, and
-- label of the supplied function.
lAp :: Label l => Labeled l (a -> b) -> Labeled l a -> LIO l (Labeled l b)
-- | This module provides routines for safely exposing IO functions in the
-- LIO monad. At a high level, certain IO objects such as handles
-- can be associated with a label via LObj, while certain
-- operations can then be blessed (via blessTCB) to operate on
-- such LObj objects.
--
-- For example, trusted code might define the following:
--
--
-- import qualified System.IO as IO
--
-- type Handle = LObj DCLabel IO.Handle
--
-- hPutStrLn :: LObj DCLabel IO.Handle -> String -> LIO DCLabel ()
-- hPutStrLn h = blessTCB IO.hPutStrLn noPrivs h
--
-- hGetLine :: LObj DCLabel IO.Handle -> LIO DCLabel String
-- hGetLine h = blessTCB IO.hGetLine noPrivs h
--
--
-- Then application-specific trusted code can wrap a specific label
-- around each Handle using the LObjTCB constructor.
module LIO.TCB.LObj
data LObj label object
LObjTCB :: !label -> !object -> LObj label object
-- | This function can be used to turn an IO function into an
-- LIO one. The LIO version expects a LObj argument,
-- and before performing any IO uses guardWrite to check that the
-- current label can write the label in the LObj object.
--
-- Note that io and lio are function types (of up to
-- nine arguments), which must be the same in all types except the monad.
-- For example, if io is Int -> String -> IO (),
-- then lio must be Int -> String -> LIO l ().
blessTCB :: (GuardIO l io lio, Label l) => (a -> io) -> (LObj l a) -> lio
-- | 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
class GuardIO l io lio | l io -> lio
guardIOTCB :: GuardIO l io lio => (LIO l ()) -> io -> lio
instance Typeable2 LObj
instance GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r)
instance GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r)
instance GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r)
instance GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r)
instance GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r)
instance GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r)
instance GuardIO l (a1 -> a2 -> a3 -> a4 -> IO r) (a1 -> a2 -> a3 -> a4 -> LIO l r)
instance GuardIO l (a1 -> a2 -> a3 -> IO r) (a1 -> a2 -> a3 -> LIO l r)
instance GuardIO l (a1 -> a2 -> IO r) (a1 -> a2 -> LIO l r)
instance GuardIO l (a1 -> IO r) (a1 -> LIO l r)
instance GuardIO l (IO r) (LIO l r)
instance (Label l, Show t) => ShowTCB (LObj l t)
instance LabelOf LObj
-- | Mutable reference in the LIO monad. As with other objects in
-- LIO, mutable references have an associated label that is used to
-- impose restrictions on its operations. In fact, labeled references
-- (LIORefs) are simply labeled IORefs with read and write
-- access restricted according to the label. This module is analogous to
-- Data.IORef, but the operations take place in the LIO
-- monad.
module LIO.LIORef
-- | An LIORef is an IORef with an associated, fixed
-- label. The restriction to an immutable label come from the fact that
-- it is possible to leak information through the label itself, if we
-- wish to allow LIORef to be an instance of LabelOf. Of
-- course, you can create an LIORef of Labeled to get a
-- limited form of flow-sensitivity.
type LIORef l a = LObj l (IORef a)
-- | To create a new reference the label of the reference must be below the
-- thread's current clearance and above the current label. If this is the
-- case, the reference is built. Otherwise an exception will be thrown by
-- the underlying guardAlloc guard.
newLIORef :: Label l => l -> a -> LIO l (LIORef l 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)
-- | Read the value of a labeled reference. A read succeeds only if the
-- label of the reference is below the current clearance. Moreover, the
-- current label is raised to the join of the current label and the
-- reference label. To avoid failures (introduced by the taint
readLIORef :: Label l => LIORef l a -> LIO l a
-- | 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
-- | Write a new value into a labeled reference. A write succeeds if the
-- current label can-flow-to the label of the reference, and the label of
-- the reference can-flow-to the current clearance. Otherwise, an
-- exception is raised by the underlying guardAlloc guard.
writeLIORef :: Label l => LIORef l a -> a -> LIO l ()
-- | 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 ()
-- | Mutate the contents of a labeled reference. For the mutation to
-- succeed it must be that the current label can flow to the label of the
-- reference, and the label of the reference can flow to the current
-- clearance. Note that because a modifier is provided, the reference
-- contents are not observable by the outer computation and so it is not
-- required that the current label be raised. It is, however, required
-- that the label of the reference be bounded by the current label and
-- clearance (as checked by the underlying guardAlloc guard).
modifyLIORef :: Label l => LIORef l a -> (a -> a) -> LIO l ()
-- | 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 ()
-- | Atomically modifies the contents of an LIORef. It is required
-- that the label of the reference be above the current label, but below
-- the current clearance. Moreover, since this function can be used to
-- directly read the value of the stored reference, the computation is
-- "tainted" by the reference label (i.e., the current label is raised to
-- the join of the current and reference labels). These checks
-- and label raise are done by guardWrite, which will raise an
-- exception if any of the IFC conditions cannot be satisfied.
atomicModifyLIORef :: Label l => LIORef l a -> (a -> (a, b)) -> LIO l b
-- | 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
-- | This module implements labeled MVars. The interface is
-- analogous to Control.Concurrent.MVar, but the operations take
-- place in the LIO monad. A labeled MVar, of type
-- LMVar l a, is a mutable location that can be in of of
-- two states; an LMVar can be empty, or it can be full (with a
-- value of tye a). The location is protected by a label of type
-- l. As in the case of LIORefs (see
-- LIO.LIORef), this label is fixed and does not change according
-- to the content placed into the location. Different from
-- LIORefs, taking and putting LMVars calls the write
-- guard guardWrite to enforce sound information flow control.
--
-- 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
-- | An LMVar is a labeled synchronization variable (an
-- MVar) that can be used by concurrent threads to communicate.
type LMVar l a = LObj l (MVar a)
-- | Create a new labeled MVar, in an empty state. Note that the supplied
-- label must be above the current label and below the current clearance.
-- An exception will be thrown by the underlying guardAlloc if
-- this is not the case.
newEmptyLMVar :: Label l => l -> LIO l (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 :: PrivDesc l p => Priv p -> l -> LIO l (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 :: Label l => l -> a -> LIO l (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 :: PrivDesc l p => Priv p -> l -> a -> LIO l (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.
-- The underlying guard guardWrite will throw an exception if any
-- of the IFC checks fail. If the Finally, like MVars if the
-- LMVar is empty, takeLMVar blocks.
takeLMVar :: Label l => LMVar l a -> LIO l a
-- | 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
-- | 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)
-- | Same as tryTakeLMVar, but uses priviliges when raising current
-- label.
tryTakeLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l (Maybe 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. Moreover if these IFC restrictions fail, the underlying
-- guardWrite throws an exception. If the LMVar is full,
-- putLMVar blocks.
putLMVar :: Label l => LMVar l a -> a -> LIO l ()
-- | 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 ()
-- | 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
-- | Same as tryPutLMVar, but uses privileges when raising current
-- label.
tryPutLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> a -> LIO l Bool
-- | Combination of takeLMVar and putLMVar. Read the value,
-- and just put it back. This operation is not atomic, and can can result
-- in unexpected outcomes if another thread is simultaneously calling a
-- function such as putLMVar, tryTakeLMVarP, or
-- isEmptyLMVar for this LMVar.
readLMVar :: Label l => LMVar l a -> LIO l a
-- | 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
-- | Takes a value from an LMVar, puts a new value into the
-- LMvar, and returns the taken value. Like the other
-- LMVar operations it is required that the label of the
-- LMVar be above the current label and below the current
-- clearance. Moreover, the current label is raised to accommodate for
-- the observation. The underlying guardWrite throws an exception
-- if this cannot be accomplished. This operation is atomic iff there is
-- no other thread calling putLMVar for this LMVar.
swapLMVar :: Label l => LMVar l a -> a -> LIO l a
-- | 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
-- | Check the status of an LMVar, i.e., whether it is empty. The
-- function succeeds if the label of the LMVar is below the
-- current clearance -- the current label is raised to the join of the
-- LMVar label and the current label. Note that this function only
-- returns a snapshot of the state and does not modify it -- hence the
-- underlying guard is taint and not guardWrite.
isEmptyLMVar :: Label l => LMVar l a -> LIO l Bool
-- | Same as isEmptyLMVar, but uses privileges when raising current
-- label.
isEmptyLMVarP :: PrivDesc l p => Priv p -> LMVar l a -> LIO l Bool
-- | This module exports LabeledResults 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
-- | 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 :: !ThreadId -> !l -> !(MVar ()) -> !(IORef (LResStatus l a)) -> LabeledResult l a
-- | Thread executing the computation
lresThreadIdTCB :: LabeledResult l a -> !ThreadId
-- | Label of the tresult
lresLabelTCB :: LabeledResult l a -> !l
lresBlockTCB :: LabeledResult l a -> !(MVar ())
-- | Result (when it is ready), or the label at which the thread
-- terminated, if that label could not flow to lresLabelTCB.
lresStatusTCB :: LabeledResult l a -> !(IORef (LResStatus l a))
data LResStatus l a
LResEmpty :: LResStatus l a
LResLabelTooHigh :: !l -> LResStatus l a
LResResult :: a -> LResStatus l a
instance (Show l, Show a) => Show (LResStatus l a)
instance LabelOf LabeledResult
-- | 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.
--
-- In addition to this, LIO also provides lFork and lWait
-- which allow forking of a computation that is restricted from reading
-- data more sensitive than a given upper bound. This limit is different
-- from clearance in that it allows the computation to spawn additional
-- threads with an upper bound above said upper bound label, but below
-- the clearance. The lFork function should be used whenever an
-- LIO computation wishes to execute a sub-computation that may raise the
-- current label (up to the supplied upper bound). To this end, the
-- current label only needs to be raised when the computation is
-- interested in reading the result of the sub-computation. The role of
-- lWait is precisely this: raise the current label and return the
-- result of such a sub-computation.
module LIO.Concurrent
-- | 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
-- | Same as lFork, but the supplied set of priviliges are accounted
-- for when performing label comparisons.
lForkP :: PrivDesc l p => Priv p -> l -> LIO l a -> LIO l (LabeledResult l a)
-- | Labeled fork. lFork allows one to invoke computations that
-- would otherwise raise the current label, but without actually raising
-- the label. The computation is executed in a separate thread and writes
-- its result into a labeled result (whose label is supplied). To observe
-- the result of the computation, or if the computation has terminated,
-- one will have to call lWait and raise the current label. Of
-- couse, this can be postponed until the result is needed.
--
-- lFork takes a label, which corresponds to the label of the
-- result. It is required that this label be between the current label
-- and clearance as enforced by a call to guardAlloc. Moreover,
-- the supplied computation must not terminate with its label above the
-- result label; doing so will result in an exception (whose label will
-- reflect this observation) being thrown in the thread reading the
-- result.
--
-- If an exception is thrown in the inner computation, the exception
-- label will be raised to the join of the result label and original
-- exception label.
--
-- Note that lFork immediately returns a LabeledResult,
-- which is essentially a "future", or "promise". This prevents
-- timing/termination attacks in which the duration of the forked
-- computation affects the duration of the lFork.
--
-- To guarantee that the computation has completed, it is important that
-- some thread actually touch the future, i.e., perform an lWait.
lFork :: Label l => l -> LIO l a -> LIO l (LabeledResult l a)
-- | Execute an LIO computation in a new lightweight thread.
forkLIO :: LIO l () -> LIO l ()
-- | Same as lWait, but uses priviliges in label checks and raises.
lWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l a
-- | Given a LabeledResult (a future), lWait returns the
-- unwrapped result (blocks, if necessary). For lWait to
-- succeed, the label of the result must be above the current label and
-- below the current clearance. Moreover, before block-reading,
-- lWait raises the current label to the join of the current
-- label and label of result. An exception is thrown by the underlying
-- guardWrite if this is not the case. Additionally, if the thread
-- terminates with an exception (for example if it violates clearance),
-- the exception is rethrown by lWait. Similarly, if the thread
-- reads values above the result label, an exception is thrown in place
-- of the result.
lWait :: Label l => LabeledResult l a -> LIO l a
-- | Same as trylWait, but uses priviliges in label checks and
-- raises.
trylWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l (Maybe a)
-- | Same as lWait, but does not block waiting for result.
trylWait :: Label l => LabeledResult l a -> LIO l (Maybe a)
-- | A version of timedlWait that takes privileges. The privileges
-- are used both to downgrade the result (if necessary), and to try
-- catching any ResultExceedsLabel before the timeout period (if
-- possible).
timedlWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> Int -> LIO l a
-- | Like lWait, with two differences. First, a timeout is specified
-- and the thread is unconditionally killed after this timeout (if it has
-- not yet returned a value). Second, if the thread's result exceeds its
-- label timedWait and exceeds what the calling thread can
-- observe, consumes the whole timeout and throws a
-- ResultExceedsLabel exception you can catch (i.e., it never
-- raises the label above the clearance).
timedlWait :: Label l => LabeledResult l a -> Int -> LIO l a
-- | 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
-- Components (sometimes called category sets). Each
-- Component (or formula) is a conjunction (implemented in terms
-- of Sets) of Clauses (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 Principals, , 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 ⊑ L_2. The ⊑ 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 ⋁ P_2, True> ⊑ <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> ⊑
-- <True,P_1 ⋁ 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
-- | 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 :: ByteString -> Principal
-- | Get the principal name.
principalName :: Principal -> ByteString
-- | Generate a principal from a String. (To create one from a
-- ByteString, just use the Principal constructor
-- directly.)
principal :: String -> Principal
-- | A clause or disjunction category is a set of Principals.
-- Logically the set corresponds to a disjunction of the principals.
newtype Clause
Clause :: Set Principal -> Clause
-- | Get underlying principal-set.
unClause :: Clause -> Set Principal
-- | Clause constructor
clause :: Set Principal -> Clause
-- | A component is a set of clauses, i.e., a formula (conjunction of
-- disjunction of Principals). DCFalse corresponds to
-- logical False, while DCFormula Set.empty corresponds
-- to logical True.
data Component
-- | Logical False
DCFalse :: Component
-- | Conjunction of disjunction categories
DCFormula :: !(Set Clause) -> Component
-- | Get underlying clause-set.
unDCFormula :: Component -> !(Set Clause)
-- | Logical True.
dcTrue :: Component
-- | Logical False.
dcFalse :: Component
-- | Arbitrary formula from a clause.
dcFormula :: Set Clause -> Component
-- | Is the component True.
isTrue :: Component -> Bool
-- | Is the component False.
isFalse :: Component -> Bool
-- | A DCLabel is a pair of secrecy and integrity
-- Components.
data DCLabel
DCLabel :: !Component -> !Component -> DCLabel
-- | Extract secrecy component of a label
dcSecrecy :: DCLabel -> !Component
-- | Extract integrity component of a label
dcIntegrity :: DCLabel -> !Component
-- | dcLabel secrecyComponent integrityComponent creates a label,
-- reducing each component to CNF.
dcLabel :: Component -> Component -> DCLabel
-- | Label contstructor. Note: the components should already be reduced.
dcLabelNoReduce :: Component -> Component -> DCLabel
-- | Element in the DCLabel lattice corresponding to public data. dcPub
-- = < True, True > . This corresponds to data that is not
-- secret nor trustworthy.
dcPub :: DCLabel
-- | Element in the DCLabel lattice corresponding to the most secret and
-- least trustworthy data. dcTop = < False, True > .
dcTop :: DCLabel
-- | Element in the DCLabel lattice corresponding to the least secret and
-- most trustworthy data. dcTop = < True, False > .
dcBottom :: DCLabel
-- | Reduce component to conjunction normal form by removing clauses
-- implied by other.
dcReduce :: Component -> Component
-- | Logical implication.
dcImplies :: Component -> Component -> Bool
-- | Logical conjunction
dcAnd :: Component -> Component -> Component
-- | Logical disjunction
dcOr :: Component -> Component -> Component
instance [safe] Typeable Principal
instance [safe] Typeable Clause
instance [safe] Typeable Component
instance [safe] Typeable DCLabel
instance [safe] Eq Principal
instance [safe] Ord Principal
instance [safe] Eq Clause
instance [safe] Eq Component
instance [safe] Eq DCLabel
instance [safe] Label DCLabel
instance [safe] Bounded DCLabel
instance [safe] Show DCLabel
instance [safe] PrivDesc DCLabel Component
instance [safe] Monoid Component
instance [safe] Show Component
instance [safe] Show Clause
instance [safe] Ord Clause
instance [safe] Show Principal
-- | This module implements a simple, embedded domain specific language to
-- create Components, 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 Principals,
-- 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 Principals, 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 Components, 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
-- | Create a DCLabel from a secrecy ToComponent and
-- integrity ToComponent. E.g.:
--
--
-- "secrecy" %% "integrity"
--
--
--
-- infix 5 %%
--
(%%) :: (ToComponent a, ToComponent b) => a -> b -> DCLabel
-- | Disjunction of two Principal-based elements.
--
--
-- infixl 7 \/
--
(\/) :: (ToComponent a, ToComponent b) => a -> b -> Component
-- | Conjunction of two Principal-based elements.
--
--
-- infixl 6 /\
--
(/\) :: (ToComponent a, ToComponent b) => a -> b -> Component
-- | Convert a type (e.g., Clause, Principal) to a label
-- component.
class ToComponent a
toComponent :: ToComponent a => a -> Component
-- | Convert a list of list of Principals to a Component.
-- Each inner list is considered to correspond to a Clause.
fromList :: [[Principal]] -> Component
-- | Convert a Component to a list of list of Principals if
-- the Component does not have the value DCFalse. In the
-- latter case the function returns an exception.
toList :: Component -> [[Principal]]
-- | Logical falsehood can be thought of as the component containing every
-- possible principal, hence impossible to express:
--
--
-- impossible = dcFalse
--
impossible :: Component
-- | Logical truth can be thought of as the component containing no
-- specific principal, hence imposing no restrictions:
--
--
-- unrestricted = dcTrue
--
unrestricted :: Component
instance [safe] ToComponent Bool
instance [safe] ToComponent String
instance [safe] ToComponent Principal
instance [safe] ToComponent Clause
instance [safe] ToComponent (Priv Component)
instance [safe] ToComponent Component
-- | 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).
--
-- Certain symbols in the lio library, particularly those in
-- LIO.Exception, use the same names as their IO
-- equivalents in the system libraries. Hence main modules that mostly
-- include IO code and only need to invoke LIO code should
-- import LIO.Run (or LIO.DCLabel) to avoid polluting their
-- namespaces.
--
-- Most code will need to use a particular label format, which needs to
-- be imported separately. For instance:
--
--
-- import 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
-- | Privileges allow a piece of code to bypass certain information flow
-- restrictions imposed by labels. A privilege is simply a conjunction of
-- disjunctions of Principals, 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
-- | 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
-- | The empty privilege, or no privileges, corresponds to logical
-- True.
noPriv :: DCPriv
-- | 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
-- | 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 Principals in the
-- Clause. This function can be used to make such checks.
dcOwns :: DCPrivDesc -> Clause -> Bool
-- | Disjunction Category Labels (DCLabels) 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.
module LIO.DCLabel
-- | 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 :: ByteString -> Principal
-- | Get the principal name.
principalName :: Principal -> ByteString
-- | Generate a principal from a String. (To create one from a
-- ByteString, just use the Principal constructor
-- directly.)
principal :: String -> Principal
-- | A clause or disjunction category is a set of Principals.
-- Logically the set corresponds to a disjunction of the principals.
data Clause
-- | Clause constructor
clause :: Set Principal -> Clause
-- | A component is a set of clauses, i.e., a formula (conjunction of
-- disjunction of Principals). DCFalse corresponds to
-- logical False, while DCFormula Set.empty corresponds
-- to logical True.
data Component
-- | Logical True.
dcTrue :: Component
-- | Logical False.
dcFalse :: Component
-- | Arbitrary formula from a clause.
dcFormula :: Set Clause -> Component
-- | Is the component True.
isTrue :: Component -> Bool
-- | Is the component False.
isFalse :: Component -> Bool
-- | A DCLabel is a pair of secrecy and integrity
-- Components.
data DCLabel
-- | Extract secrecy component of a label
dcSecrecy :: DCLabel -> Component
-- | Extract integrity component of a label
dcIntegrity :: DCLabel -> Component
-- | dcLabel secrecyComponent integrityComponent creates a label,
-- reducing each component to CNF.
dcLabel :: Component -> Component -> DCLabel
-- | Element in the DCLabel lattice corresponding to public data. dcPub
-- = < True, True > . This corresponds to data that is not
-- secret nor trustworthy.
dcPub :: DCLabel
-- | Element in the DCLabel lattice corresponding to the most secret and
-- least trustworthy data. dcTop = < False, True > .
dcTop :: DCLabel
-- | Element in the DCLabel lattice corresponding to the least secret and
-- most trustworthy data. dcTop = < True, False > .
dcBottom :: DCLabel
-- | LIOState with underlying label being DCLabel
type DCState = LIOState DCLabel
-- | Default, starting state for a DC computation. The current label
-- is public (i.e., dcPub) and the current clearance is
-- top.
defaultState :: DCState
-- | The monad for LIO computations using DCLabel as the label.
type DC = LIO DCLabel
-- | Evaluate computation in the DC monad.
evalDC :: DC a -> IO a
-- | Evaluate computation in the DC monad.
runDC :: DC a -> IO (a, DCState)
-- | Similar to evalLIO, but catches any exceptions thrown by
-- untrusted code with throwLIO.
tryDC :: DC a -> IO (Either SomeException a, DCState)
-- | Type synonym for MonadLIO.
type MonadDC m = MonadLIO DCLabel m
-- | DC Labeled values.
type DCLabeled = Labeled DCLabel
-- | DC Labeled LIORefs.
type DCRef a = LIORef DCLabel a
-- | DC Gate.
type DCGate = Gate DCPrivDesc
-- | 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
-- | The all privilege corresponds to logical False
allPrivTCB :: DCPriv