-- 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.
-- Unlike discretionary access control (such as UNIX file permissions),
-- IFC permits scenarios in which untrusted computation may have the
-- ability to manipulate secret data without having the ability to
-- further disclose that data.
--
-- LIO is an IFC library that can be used to implement such untrusted
-- computations. LIO provides combinators similar to those of IO
-- for performing side-effecting computations (e.g., modifying mutable
-- references, forking threads, throwing and catching exceptions, etc.)
-- To track and control the flow of information, LIO associates a
-- security policy, called a label, with every piece of data. A
-- label may, for example, impose a restriction on who can observe,
-- propagate, or modify the data to which it applies. Unlike standard IO
-- operations, the LIO counterparts check the vailidity of labels before
-- performing the (underlying IO) side-effecting computation. For
-- example, before writing to a labeled variable, LIO asserts that the
-- write will not violate any security policies associated with the data
-- to be written.
--
-- Most code should import module LIO and whichever label format
-- the application is using (e.g., LIO.DCLabel to use the format
-- that ships with the library). Side-effecting code should be specified
-- as actions in the LIO monad. See LIO.Core for a
-- description of the core library API, LIO.Label for a discussion
-- of labels, and LIO.Run for functions allowing one to run an
-- LIO computation from the IO monad.
--
-- WARNING: For security, untrusted code must always be compiled with the
-- -XSafe and -fpackage-trust SafeHaskell flags.
-- See
-- http://www.haskell.org/ghc/docs/latest/html/users_guide/safe-haskell.html
-- for more details on the guarantees provided by SafeHaskell.
@package lio
@version 0.11.4.2
-- | This module exports symbols that must be accessible only to trusted
-- code. By convention, the names of such symbols always end
-- "...TCB" (short for "trusted computing base"). In many cases,
-- a type is safe to export while its constructor is not. Hence, only the
-- constructor ends "TCB", while the type is re-exported to safe
-- code (without constructors) from LIO.Core.
--
-- Security rests on the fact that untrusted code must be compiled with
-- -XSafe. Because this module is flagged unsafe, it cannot be
-- imported from safe modules.
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 wrapper around IO that keeps track
-- of a current label and current clearance. Safe code
-- cannot execute arbitrary IO actions from the LIO monad.
-- However, trusted runtime functions can use ioTCB to perform
-- IO actions (which they should only do after appropriately
-- checking labels).
newtype LIO l a
LIOTCB :: (IORef (LIOState l) -> IO a) -> LIO l 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 :: (LIOState l -> LIOState l) -> LIO l ()
-- | Lifts an IO computation into the LIO monad. This
-- function is dangerous and should only be called after appropriate
-- checks ensure the IO computation will not violate IFC policy.
ioTCB :: IO a -> LIO l a
-- | A newtype wrapper that can be used by trusted code to transform a
-- powerless description of privileges into actual privileges. The
-- constructor, PrivTCB, is dangerous as it allows creation of
-- arbitrary privileges. Hence it is only exported by the unsafe module
-- LIO.TCB. A safe way to create arbitrary privileges is to call
-- privInit (see LIO.Run#v:privInit) from the IO
-- monad before running your LIO computation.
newtype Priv a
PrivTCB :: a -> Priv a
-- | Labeled l a is a value that associates a label of type
-- l with a pure value of type a. Labeled values allow
-- users to label data with a label other than the current label. Note
-- that Labeled is an instance of LabelOf, which means that
-- only the contents of a labeled value (the type t) is
-- kept secret, not the label. Of course, if you have a Labeled
-- within a Labeled, then the label on the inner value will be
-- protected by the outer label.
data Labeled l t
LabeledTCB :: !l -> t -> Labeled l t
-- | 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:
--
--
-- data 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 l a) = l
--
class LabelOf t
labelOf :: LabelOf t => t l a -> l
-- | An uncatchable exception hierarchy is used to terminate an untrusted
-- thread. Wrap the uncatchable exception in UncatchableTCB before
-- throwing it to the thread. runLIO will subsequently unwrap
-- the UncatchableTCB constructor.
--
-- Note this can be circumvented by mapException, which should be
-- made unsafe. In the interim, auditing untrusted code for this is
-- necessary.
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 members of the
-- Show class. Nonetheless it is useful to be able to examine such
-- objects when debugging. The showTCB method can be used to
-- examine such objects.
class ShowTCB a
showTCB :: ShowTCB a => a -> String
-- | A LabeledResult encapsulates a future result from a
-- computation spawned by lFork or lForkP. See
-- LIO.Concurrent for a description of the concurrency
-- abstractions of LIO.
data LabeledResult l a
LabeledResultTCB :: !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
-- | This MVar is empty until such point as lresStatusTCB
-- is no longer LResEmpty. Hence, calling readMVar on
-- this field allows one to wait for the thread to terminate.
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))
-- | Status of a LabeledResult.
data LResStatus l a
LResEmpty :: LResStatus l a
LResLabelTooHigh :: !l -> LResStatus l a
LResResult :: a -> LResStatus l 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 (Show l, Show a) => Show (LResStatus l a)
instance LabelOf LabeledResult
instance LabelOf Labeled
instance (Show l, Show a) => ShowTCB (Labeled l a)
instance Monoid p => Monoid (Priv p)
instance Exception UncatchableTCB
instance Show UncatchableTCB
instance Applicative (LIO l)
instance Functor (LIO l)
instance Monad (LIO l)
module LIO.Label
-- | This class defines the operations necessary to make a label into a
-- lattice (see http://en.wikipedia.org/wiki/Lattice_(order)).
-- canFlowTo partially orders labels. lub and glb
-- compute the least upper bound and greatest lower bound of two labels,
-- respectively.
class (Eq l, Show l, Read l, Typeable l) => Label l
lub :: Label l => l -> l -> l
glb :: Label l => l -> l -> l
canFlowTo :: Label l => l -> l -> Bool
-- | Every privilege type must be an instance of SpeaksFor, which is
-- a partial order specifying when one privilege value is at least as
-- powerful as another. If canFlowToP p1 l1 l2 and p2
-- speaksFor p1, then it should also be true that
-- canFlowToP p2 l1 l2.
--
-- As a partial order, SpeaksFor should obey the reflexivity,
-- antisymmetry and transitivity laws. However, if you do not wish to
-- allow delegation of a particular privilege type, you can define
-- speaksFor _ _ = False (which violates the reflexivity
-- law, but is reasonable when you don't want the partial order).
class (Typeable p, Show p) => SpeaksFor p
speaksFor :: SpeaksFor p => p -> p -> Bool
-- | This class represents privilege descriptions, which define a pre-order
-- on labels in which distinct labels become equivalent. The pre-oder
-- implied by a privilege description is specified by the method
-- canFlowToP. In addition, this this class defines a method
-- downgradeP, which is important for finding least labels
-- satisfying a privilege equivalence.
--
-- Minimal complete definition: downgradeP.
--
-- (The downgradeP requirement represents the fact that a generic
-- canFlowToP can be implemented efficiently in terms of
-- downgradeP, but not vice-versa.)
class (Label l, SpeaksFor p) => PrivDesc l p where canFlowToP p l1 l2 = downgradeP p l1 `canFlowTo` l2
downgradeP :: PrivDesc l p => p -> l -> l
canFlowToP :: PrivDesc l p => p -> l -> l -> Bool
-- | A newtype wrapper that can be used by trusted code to transform a
-- powerless description of privileges into actual privileges. The
-- constructor, PrivTCB, is dangerous as it allows creation of
-- arbitrary privileges. Hence it is only exported by the unsafe module
-- LIO.TCB. A safe way to create arbitrary privileges is to call
-- privInit (see LIO.Run#v:privInit) from the IO
-- monad before running your LIO computation.
data Priv a
-- | Turns privileges into a powerless description of the privileges by
-- unwrapping the Priv newtype.
privDesc :: Priv a -> a
-- | Uses dynamic typing to return True iff the type of the argument
-- is Priv a (for any a). Mostly useful to
-- prevent users from accidentally wrapping Priv objects inside
-- other Priv objects or accidentally including real privileges in
-- an exception.
isPriv :: Typeable p => p -> Bool
-- | Generic PrivDesc used to denote the lack of privileges. Works
-- with any Label type. This is only a privilege description; a
-- more useful symbol is noPrivs, which actually embodies the
-- NoPrivs privilege.
data NoPrivs
NoPrivs :: NoPrivs
-- | Priv object corresponding to NoPrivs.
noPrivs :: Priv NoPrivs
instance Typeable NoPrivs
instance Show NoPrivs
instance Read NoPrivs
instance Monoid NoPrivs
instance Label l => PrivDesc l NoPrivs
instance SpeaksFor NoPrivs
instance PrivDesc l p => PrivDesc l (Priv p)
instance SpeaksFor p => SpeaksFor (Priv p)
-- | 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)
-- | A variant of runLIO that returns results in Right and
-- exceptions in Left, much like the standard library try
-- function.
tryLIO :: LIO l a -> LIOState l -> IO (Either SomeException a, LIOState l)
-- | 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
-- | Initialize some privileges (within the IO monad) that can be
-- passed to LIO computations run with runLIO or
-- evalLIO. This is a pure function, but the result is
-- encapsulated in IO to make the return value inaccessible from
-- LIO computations.
--
-- Note the same effect can be achieved using the PrivTCB
-- constructor, but PrivTCB is easier to misuse and is only
-- available by importing LIO.TCB.
privInit :: SpeaksFor p => p -> IO (Priv p)
-- | 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
-- | Throw an exception.
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
-- | This module exports exception types thrown in response to label
-- failures. In addition, it provides withContext, a function that
-- annotates any exceptions in the AnyLabelError hierarchy that
-- are thrown within a given scope. These annotations should be used to
-- add function names to exceptions, so as to make it easier to pinpoint
-- the cause of a label error.
module LIO.Error
-- | Class of error messages that can be annotated with context.
class Annotatable e
annotate :: Annotatable e => String -> e -> e
-- | Executes an action with a context string, which will be added to any
-- label exception thrown.
--
-- Note: this function wraps an action with a catch, and thus may
-- incur a small runtime cost (though it is well under 100 ns on machines
-- we benchmarked).
withContext :: String -> LIO l a -> LIO l a
-- | Parent of all label-related exceptions.
data AnyLabelError
AnyLabelError :: e -> AnyLabelError
-- | Definition of toException for children of AnyLabelError
-- in the exception hierarchy.
lerrToException :: (Exception e, Annotatable e) => e -> SomeException
-- | Definition of fromException for children of
-- AnyLabelError in the exception hierarchy.
lerrFromException :: Exception e => SomeException -> Maybe e
-- | A generic privilege description for recording relevant privileges in
-- exceptions.
data GenericPrivDesc l
GenericPrivDesc :: p -> GenericPrivDesc l
-- | Main error type thrown by label failures in the LIO monad.
data LabelError l
LabelError :: [String] -> String -> l -> l -> [GenericPrivDesc l] -> [l] -> LabelError l
-- | Annotation of where the failure happened.
lerrContext :: LabelError l -> [String]
-- | Actual function that failed.
lerrFailure :: LabelError l -> String
-- | Current label at time of error.
lerrCurLabel :: LabelError l -> l
-- | Current clearance at time of error.
lerrCurClearance :: LabelError l -> l
-- | Any privileges involved in error.
lerrPrivs :: LabelError l -> [GenericPrivDesc l]
-- | Any labels involved in error.
lerrLabels :: LabelError l -> [l]
-- | Throw a label-error exception.
labelError :: Label l => String -> [l] -> LIO l a
-- | Throw a label-error exception.
labelErrorP :: (Label l, PrivDesc l p) => String -> Priv p -> [l] -> LIO l a
-- | Error indicating insufficient privileges (independent of the current
-- label). This exception is thrown by delegate, and should also
-- be thrown by gates that receive insufficient privilege descriptions
-- (see LIO.Delegate).
data InsufficientPrivs
InsufficientPrivs :: [String] -> String -> p -> p -> InsufficientPrivs
inspContext :: InsufficientPrivs -> [String]
inspFailure :: InsufficientPrivs -> String
inspSupplied :: InsufficientPrivs -> p
inspNeeded :: InsufficientPrivs -> p
-- | Raise InsufficientPrivs error.
insufficientPrivs :: SpeaksFor p => String -> p -> p -> a
-- | Error raised when a computation spawned by lFork terminates
-- with its current label above the label of the result.
data ResultExceedsLabel l
ResultExceedsLabel :: [String] -> String -> l -> Maybe l -> ResultExceedsLabel l
relContext :: ResultExceedsLabel l -> [String]
relLocation :: ResultExceedsLabel l -> String
relDeclaredLabel :: ResultExceedsLabel l -> l
relActualLabel :: ResultExceedsLabel l -> Maybe l
instance Typeable AnyLabelError
instance Typeable1 LabelError
instance Typeable InsufficientPrivs
instance Typeable1 ResultExceedsLabel
instance Show l => Show (LabelError l)
instance Show l => Show (ResultExceedsLabel l)
instance Label l => Exception (ResultExceedsLabel l)
instance Annotatable (ResultExceedsLabel l)
instance Exception InsufficientPrivs
instance Annotatable InsufficientPrivs
instance Show InsufficientPrivs
instance Label l => Exception (LabelError l)
instance Annotatable (LabelError l)
instance Show (GenericPrivDesc l)
instance Exception AnyLabelError
instance Annotatable AnyLabelError
instance Show AnyLabelError
-- | This module provides two functions useful for delegating privileges.
-- The delegate function creates a Priv value less powerful
-- than an existing one. Gates provide a mechanism for
-- authenticating calls to closures that embed privileges.
module LIO.Delegate
-- | delegate allows you to create a new privilege object that is
-- less powerful than an existing privilege object. The first argument
-- supplies actual privileges. The second argument is a PrivDesc
-- describing the desired new privileges. The call throws an exception
-- unless the privilege object supplied speaksFor the privilege
-- object requested.
--
-- Note: If you are looking for a way to create privileges more
-- powerful than ones you already have, you can use the mappend
-- function to combine existing privileges.
delegate :: SpeaksFor p => Priv p -> p -> Priv p
-- | 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 p 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 :: (p -> a) -> Gate p a
-- | guardGate name minPriv a creates a simple gate that requires
-- privileges at least as high as minPriv to return the payload
-- or function a. If the privileges supplied are insufficient,
-- an exception of type InsufficientPrivs is thrown. The argument
-- name is used only when an exception is thrown, to make the
-- source of the exception more easily traceable.
--
--
-- guardGate name minPriv a = gate $ \pd ->
-- if pd `speaksFor` minPriv then a
-- else insufficientPrivs name pd minPriv
--
guardGate :: SpeaksFor p => String -> p -> a -> Gate p 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 Typeable2 Gate
-- | This module implements the core of the Labeled IO (LIO) information
-- flow control (IFC) library. It provides a monad, LIO, that is
-- intended to be used as a replacement for the IO monad in
-- untrusted code. The idea is for untrusted code to provide a
-- computation in the LIO monad, which trusted code can then
-- safely execute through evalLIO and similar functions (e.g.,
-- evalDC in LIO.DCLabel#v:evalDC).
--
-- Unlike IO, the LIO monad keeps track of a current
-- label (accessible via the getLabel function) during each
-- computation. The current label effectively tracks the sensitivity of
-- all the data that the computation has observed. For example, if the
-- computation has read a "secret" mutable reference (see
-- LIO.LIORef) and then the result of a "top-secret" thread (see
-- LIO.Concurrent) then the current label will be at least
-- "top-secret". Labels are described in more detail in the documentation
-- for LIO.Label, as well as the documentation for particular
-- label formats (such as LIO.DCLabel).
--
-- The role of the current label is two-fold: First, the current label
-- protects all pure values currently in scope. For example, the current
-- label is the label on constants (such as 3 and "tis a
-- string") as well as function arguments. More interestingly,
-- consider reading a secret reference:
--
--
-- val <- readLIORef secret
--
--
-- Though the label of secret may be "secret", val is
-- not explicitly labeled. Hence, to protect the contents of the
-- LIORef that has been read into val, the current
-- label must be at least "secret" before returning from
-- readLIORef. More generally, if the current label is
-- l_cur, then it is only permissible to read data labeled
-- l_r if l_r `canFlowTo` l_cur. Note that,
-- instead of throwing an exception, reading data often just increases
-- the current label to ensure that l_r `canFlowTo`
-- l_cur. This is acomplished using a function such as taint.
--
-- The second purpose of the current label is to prevent inforation leaks
-- into public channels. Specifically, it is only permissible to modify
-- or write to data labeled l_w when l_cur`canFlowTo`
-- l_w. Thus, the following attempt to leak the val after
-- reading it from a secret LIORef would fail:
--
--
-- writeLIORef public val
--
--
-- In addition to the current label, the LIO monad keeps a second label,
-- the current clearance (accessible via the getClearance
-- function). The clearance can be used to enforce a "need-to-know"
-- policy, since 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) == False.
module LIO.Core
-- | The LIO monad is a wrapper around IO that keeps track
-- of a current label and current clearance. Safe code
-- cannot execute arbitrary IO actions from the LIO monad.
-- However, trusted runtime functions can use ioTCB to perform
-- IO actions (which they should only do after appropriately
-- checking labels).
data LIO l a
-- | Synonym for monad in which LIO is the base monad.
class (Label l, Monad m) => 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 value of the thread's current label.
getLabel :: Label l => LIO l l
-- | Raises the current label to the provided label, which must be between
-- the current label and clearance. See taint.
setLabel :: Label l => l -> LIO l ()
-- | 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 canFlowToP
-- priv oldLabel newLabel && canFlowTo newLabel
-- clearance. (Note the privilege argument affects the label check,
-- not the clearance check; call setClearanceP first to raise the
-- clearance.)
setLabelP :: PrivDesc l p => Priv p -> l -> LIO l ()
-- | Returns the thread's current clearance.
getClearance :: Label l => LIO l l
-- | Lowers the current clearance. The new clerance must be between the
-- current label and previous current clerance. One cannot raise the
-- current label or create object with labels higher than the current
-- clearance.
setClearance :: Label l => l -> LIO l ()
-- | Raises the current clearance (undoing the effects of
-- setClearance) by exercising privileges. If the current label is
-- l and current clearance is c, then setClearanceP
-- p cnew succeeds only if the new clearance is can flow to the
-- current clearance (modulo privileges), i.e., canFlowToP p
-- cnew c == True. Additionally, the current label must flow to the
-- new clearance, i.e., l `canFlowTo` cnew == True.
--
-- Since LIO guards that are used when reading/writing data (e.g.,
-- guardAllocP) do not use privileges when comparing labels with
-- the current clearance, code must always raise the current clearance,
-- to read/write data above the current clearance.
setClearanceP :: PrivDesc l p => Priv p -> l -> LIO l ()
-- | 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
-- | Temporarily lowers the clearance for a computation, then restores it.
-- Equivalent to:
--
--
-- withClearance c lio = scopeClearance $ setClearance c >> lio
--
--
-- Note that if the computation inside withClearance acquires
-- any 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
-- | A variant of withClearance that takes privileges. Equivalent
-- to:
--
--
-- withClearanceP p c lio = scopeClearance $ setClearanceP p c >> lio
--
withClearanceP :: PrivDesc l p => Priv p -> l -> LIO l a -> LIO l a
-- | Parent of all label-related exceptions.
data AnyLabelError
AnyLabelError :: e -> AnyLabelError
-- | Main error type thrown by label failures in the LIO monad.
data LabelError l
LabelError :: [String] -> String -> l -> l -> [GenericPrivDesc l] -> [l] -> LabelError l
-- | Annotation of where the failure happened.
lerrContext :: LabelError l -> [String]
-- | Actual function that failed.
lerrFailure :: LabelError l -> String
-- | Current label at time of error.
lerrCurLabel :: LabelError l -> l
-- | Current clearance at time of error.
lerrCurClearance :: LabelError l -> l
-- | Any privileges involved in error.
lerrPrivs :: LabelError l -> [GenericPrivDesc l]
-- | Any labels involved in error.
lerrLabels :: LabelError l -> [l]
-- | Error indicating insufficient privileges (independent of the current
-- label). This exception is thrown by delegate, and should also
-- be thrown by gates that receive insufficient privilege descriptions
-- (see LIO.Delegate).
data InsufficientPrivs
InsufficientPrivs :: [String] -> String -> p -> p -> InsufficientPrivs
inspContext :: InsufficientPrivs -> [String]
inspFailure :: InsufficientPrivs -> String
inspSupplied :: InsufficientPrivs -> p
inspNeeded :: InsufficientPrivs -> p
-- | 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.
guardAlloc :: Label l => l -> LIO l ()
-- | Like guardAlloc, but takes a privilege argument to be more
-- permissive. Note: privileges are only used when checking that
-- the current label can flow to the target label; guardAllocP
-- still always throws an exception when the target label is higher than
-- the current clearance.
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 a
-- LabelError exception 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 the modification can be observed,
-- i.e., the write implies a read.
--
-- The implementation of guardWrite is straight forward:
--
--
-- guardWrite l = guardAlloc l >> taint l
--
--
-- This guarantees that l `canFlowTo` the current label
-- (and clearance), and that the current label `canFlowTo`
-- l.
guardWrite :: Label l => l -> LIO l ()
-- | Like guardWrite, but takes a privilege argument to be more
-- permissive.
guardWriteP :: PrivDesc l p => Priv p -> l -> LIO l ()
instance Label l => MonadLIO l (LIO l)
-- | 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).
--
-- Two Applicative Functor-like operations are also
-- defined for Labeled data, namely lFmap and lAp.
module LIO.Labeled
-- | Labeled l a is a value that associates a label of type
-- l with a pure value of type a. Labeled values allow
-- users to label data with a label other than the current label. Note
-- that Labeled is an instance of LabelOf, which means that
-- only the contents of a labeled value (the type t) is
-- kept secret, not the label. Of course, if you have a Labeled
-- within a Labeled, then the label on the inner value will be
-- protected by the outer label.
data Labeled l t
-- | 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:
--
--
-- data 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 l a) = l
--
class LabelOf t
labelOf :: LabelOf t => t l a -> l
-- | Function to construct a Labeled value from a label and a 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 value using privilege to allow the value'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 a Labeled value 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
-- value and returns it as an unprotected value of the inner type. For
-- instance, in the LIO monad one can say:
--
--
-- x <- unlabel (lx :: Labeled SomeLabelType Int)
--
--
-- And now it is possible to use the pure value x :: Int, which
-- was previously protected by a label in lx.
--
-- unlabel raises the current label as needed to reflect the
-- fact that the thread's behavior can now depend on the contents of
-- lx. If unlabeling a value would require raising the
-- current label above the current clearance, then unlabel
-- throws an exception of type LabelError. You can use
-- labelOf to check beforehand whether unlabel will
-- succeed.
unlabel :: Label l => Labeled l a -> LIO l a
-- | Extracts the contents of a Labeled value just like
-- unlabel, but takes a privilege argument to minimize the amount
-- the current label must be raised. The privilege is used to raise the
-- current label less than might be required otherwise, but this function
-- does not change the current clarance and still throws a
-- LabelError if the privileges supplied are insufficient to save
-- the current label from needing to exceed the current clearance.
unlabelP :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a
-- | Relabels a Labeled value to the supplied label if the given
-- privileges permit it. An exception is thrown unless the following two
-- conditions hold:
--
--
-- - The new label must be below the current clearance.
-- - The old label and new label must be equal (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 value to the lub 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 value's label 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)
-- | A function similar to fmap for Labeled values. Applies a
-- function to a Labeled value without unlabeling the value
-- or changing the thread's current label. The label of the result is the
-- lub of the current label and that of the supplied
-- Labeled value. Because of laziness, the actual computation on
-- the value of type a will be deferred until a thread with a
-- higher label actually unlabels the result.
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 lub of
-- the thread's current label, the label of the supplied function, and
-- the label of the supplied value.
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 "hPutStrLn" IO.hPutStrLn h
--
-- hPutStrLnP :: DCPriv -> LObj DCLabel IO.Handle -> String -> LIO DCLabel ()
-- hPutStrLnP h = blessPTCB "hPutStrLnP" IO.hPutStrLn h
--
-- hGetLine :: LObj DCLabel IO.Handle -> LIO DCLabel String
-- hGetLine h = blessTCB "hGetLine" IO.hGetLine h
--
--
-- Then application-specific trusted code can wrap a specific label
-- around each Handle using the LObjTCB constructor.
module LIO.TCB.LObj
-- | A "LObj label object" is a wrapper around an IO abstraction
-- of type object (such as a file handle or socket) on which it
-- is safe to do IO operations in the LIO monad when the
-- caller can read and write a the label label. It is the job of
-- the trusted code constructing such a LObj object to ensure
-- both that the same IO object is only ever associated with a single
-- label, and that the abstraction combined with its blessed IO
-- operations (see blessTCB) cannot be used to communicate with
-- code running at different labels.
data LObj label object
LObjTCB :: !label -> !object -> 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.
--
-- The first argument should be the name of the function being defined
-- with blessTCB. Its purpose is to enhance error reporting.
--
-- Note that io and lio are function types (of up to
-- nine arguments), which must be the same in all types except the monad.
-- For example, if io is Int -> String -> IO (),
-- then lio must be Int -> String -> LIO l ().
blessTCB :: (GuardIO l io lio, Label l) => String -> (a -> io) -> (LObj l a) -> lio
-- | A variant of blessTCB that produces an LIO function
-- taking a privilege argument.
blessPTCB :: (GuardIO l io lio, PrivDesc l p) => String -> (a -> io) -> Priv p -> (LObj l a) -> lio
-- | Class for lifting IO actions.
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 comes from the fact that
-- it is possible to leak information through the label itself, since 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)
-- | Create a new reference with a particularlabel. The label specified
-- must be between the thread's current label and clearance, as enforced
-- by guardAlloc.
newLIORef :: Label l => l -> a -> LIO l (LIORef l a)
-- | Same as newLIORef except newLIORefP takes privileges
-- which make the comparison to the current label more permissive, as
-- enforced by guardAllocP.
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 lub of the current label and the
-- reference label. To avoid failures (introduced by the taint
-- guard) use labelOf to check that a read will succeed.
readLIORef :: 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 (using
-- taintP instead of taint).
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.
writeLIORefP :: PrivDesc l p => Priv p -> LIORef l a -> a -> LIO l ()
-- | Mutate the contents of a labeled reference. The mutation is performed
-- by a a pure function, which, because of laziness, is not actually
-- evaluated until such point as a (possibly higher-labeled) thread
-- actually reads the LIORef. The caller of modifyLIORef
-- learns no information about the previous contents the LIORef.
-- For that reason, there is no need to raise the current label. The
-- LIORef's label must still lie between the current label and
-- clearance, however (as enforced by guardAlloc).
modifyLIORef :: Label l => LIORef l a -> (a -> a) -> LIO l ()
-- | Like modifyLIORef, but takes a privilege argument and guards
-- execution with guardAllocP instead of guardAlloc.
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 a
-- LabelError 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 and uses guardWriteP instead of
-- guardWrite.
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 one of
-- two states; an LMVar can be empty, or it can be full (with a
-- value of type 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. Unlike LIORefs, most
-- operations use guardWrite or guardWriteP, reflecting the
-- fact that there is no such thing as read-only or write-only operations
-- on an LMVar.
--
-- 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. 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.
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 provides concurrency abstractions for LIO. The most
-- basic function, forkLIO, spawns a computation in a new
-- light-weight thread (analogous to forkIO).
--
-- lFork spawns a forked thread that returns a result other
-- threads can wait for (using lWait). The label of such a
-- thread's result must be specified at the time the thread is spawned
-- with lFork. Should the lForked thread terminate with its
-- current label be above the specified result label, lWait will
-- throw an exception of type ResultExceedsLabel in any thread
-- waiting for the result.
--
-- Learing that a spawned thread has terminated by catching a
-- ResultExceedsLabel may cause the label of the waiting thread to
-- rise, possibly above the current clearance (in which case the
-- exception cannot be caught). As an alternative, timedlWait
-- unconditionally kills a spawned thread if it has not terminated at an
-- observable label within a certain time period. timedlWait is
-- guaranteed both to terminate and not to throw exceptions that cannot
-- be caught at the current label.
module LIO.Concurrent
-- | Execute an LIO computation in a new lightweight thread.
forkLIO :: LIO l () -> LIO l ()
-- | A LabeledResult encapsulates a future result from a
-- computation spawned by lFork or lForkP. See
-- LIO.Concurrent for a description of the concurrency
-- abstractions of LIO.
data LabeledResult l a
-- | 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 being thrown in the
-- thread reading the result.
--
-- 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)
-- | 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)
-- | Error raised when a computation spawned by lFork terminates
-- with its current label above the label of the result.
data ResultExceedsLabel l
ResultExceedsLabel :: [String] -> String -> l -> Maybe l -> ResultExceedsLabel l
relContext :: ResultExceedsLabel l -> [String]
relLocation :: ResultExceedsLabel l -> String
relDeclaredLabel :: ResultExceedsLabel l -> l
relActualLabel :: ResultExceedsLabel l -> Maybe l
-- | 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
-- taint if this is not the case. Additionally, if the thread
-- terminates with an exception (for example if it violates clearance),
-- the exception is rethrown by lWait. Similarly, if the thread
-- reads values above the result label, an exception is thrown in place
-- of the result.
lWait :: Label l => LabeledResult l a -> LIO l a
-- | Same as lWait, but uses priviliges in label checks and raises.
lWaitP :: PrivDesc l p => Priv p -> LabeledResult l a -> LIO l a
-- | Same as lWait, but does not block waiting for result.
trylWait :: Label l => LabeledResult l a -> LIO l (Maybe 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)
-- | 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 what
-- the calling thread can observe, timedlWait consumes the whole
-- timeout and throws a ResultExceedsLabel exception you can catch
-- (i.e., it never raises the label above the clearance).
--
-- Because this function can alter the result by killing a thread, it
-- requires the label of the LabeledResult to be both readable and
-- writable at the current label.
timedlWait :: Label l => LabeledResult l a -> Int -> LIO l a
-- | 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
-- | Disjunction Category Labels (DCLabels) are a label
-- format that encodes authority, secrecy restrictions, and integrity
-- properties using propositional logic.
--
-- A DCLabel consists of two boolean formulas over
-- Principals. Each formula is in conjunctive normal form,
-- represented by type CNF. The first CNF
-- (dcSecrecy) specifies what combinations of principals are
-- allowed to make data public. The second CNF
-- (dcIntegrity) specifies which combinations of principals have
-- endorsed the integrity of the data.
--
-- The %% operator allows one to construct a DCLabel by
-- joining a secrecy CNF on the left with an integrity CNF
-- on the right. A DCLabel can also be directly constructed with
-- the constructor DCLabel. However, %% has the added
-- convenience of accepting any argument types that are instances of
-- ToCNF.
--
-- For example, the following expresses data that can be exported by the
-- principal "Alice" and may have been written by anybody: "Alice"
-- %% True. (toCNF True
-- indicates a trivially satisfiable label component, which in this case
-- means a label conveying no integrity properties.)
--
-- A CNF is created using the (\/) and (/\)
-- operators. The disjunction operator (\/) is used to compute a
-- CNF equivalent to the disjunciton of two Principals,
-- Strings, or CNFs. For example:
--
--
-- p1 = principal "p1"
-- p2 = principal "p2"
-- p3 = principal "p3"
-- e1 = p1 \/ p2
-- e2 = e1 \/ "p4"
--
--
-- Similarly, the conjunction operator (/\) creates a CNF
-- as a conjunction of Principals, Strings,
-- Disjunctions, or CNFs.
--
--
-- e3 = p1 \/ p2
-- e4 = e1 /\ "p4" /\ p3
--
--
-- Note that because a CNF formula is stored as a conjunction of
-- Disjunctions, it is much more efficient to apply /\ to
-- the result of \/ than vice versa. It would be logical for
-- /\ to have higher fixity than \/. Unfortunately, this
-- makes formulas harder to read (given the convention of AND binding
-- more tightly than OR). Hence \/ and /\ have been given
-- the same fixity but different associativities, preventing the two from
-- being mixed in the same expression without explicit parentheses.
--
-- Consider the following, example:
--
--
-- cnf1 = ("Alice" \/ "Bob") /\ "Carla"
-- cnf2 = "Alice" /\ "Carla"
-- dc1 = cnf1 %% cnf2
-- dc2 = "Djon" %% "Alice"
-- pr = PrivTCB $ "Alice" /\ "Carla"
--
--
-- This will result in the following:
--
--
-- >>> dc1
-- "Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla"
--
-- >>> dc2
-- "Djon" %% "Alice"
--
-- >>> canFlowTo dc1 dc2
-- False
--
-- >>> canFlowToP pr dc1 dc2
-- True
--
--
-- Because the \/ and /\ operators accept strings and
-- Principals as well as CNFs, it is sometimes easy to
-- forget that strings and Principals are not actually
-- CNFs. For example:
--
--
-- >>> "Alice" /\ "Bob" `speaksFor` "Alice" \/ "Bob"
-- True
--
-- >>> "Alice" `speaksFor` "Alice" \/ "Bob"
-- <interactive>:12:21:
-- Couldn't match expected type `[Char]' with actual type `CNF'
--
--
-- To convert a single string or Principal to a CNF, you
-- must use the toCNF method:
--
--
-- >>> toCNF "Alice" `speaksFor` "Alice" \/ "Bob"
-- True
--
module LIO.DCLabel
-- | The main monad type alias to use for LIO computations that are
-- specific to DCLabels.
type DC = LIO DCLabel
-- | DCLabel privileges are expressed as a CNF of the
-- principals whose authority is being exercised.
type DCPriv = Priv CNF
-- | An alias for Labeled values labeled with a DCLabel.
type DCLabeled = Labeled DCLabel
-- | A common default starting state, where lioLabel =
-- dcPublic and lioClearance = False %%
-- True (i.e., the highest possible clearance).
dcDefaultState :: LIOState DCLabel
-- | Wrapper function for running LIO DCLabel
-- computations.
--
--
-- evalDC dc = evalLIO dc dcDefaultState
--
evalDC :: DC a -> IO a
-- | DCLabel wrapper for tryLIO:
--
--
-- tryDC dc = tryLIO dc dcDefaultState
--
tryDC :: DC a -> IO (Either SomeException a, LIOState DCLabel)
-- | A Principal is a primitive source of authority, represented
-- as a string. The interpretation of principal strings is up to the
-- application. Reasonable schemes include encoding user names, domain
-- names, and/or URLs in the Principal type.
data Principal
-- | Create a principal from a strict ByteString.
principalBS :: ByteString -> Principal
-- | Create a principal from a String. The String is packed
-- into a ByteString using fromString, which will almost
-- certainly give unexpected results for non-ASCII unicode code points.
principal :: String -> Principal
-- | Main DCLabel type. DCLabels use CNF boolean formulas
-- over principals to express authority exercised by a combination of
-- principals. A DCLabel contains two CNFs. One,
-- dcSecrecy, specifies the minimum authority required to make
-- data with the label completely public. The second, dcIntegrity,
-- expresses the minimum authority that was used to endorse data with the
-- label, or, for mutable objects, the minimum authority required to
-- modify the object.
--
-- DCLabels are more conveniently expressed using the %%
-- operator, with dcSecrecy on the left and dcIntegrity on
-- the right, i.e.: (dcSecrecyValue %%
-- dcIntegrityValue).
--
-- DCLabels enforce the following relations:
--
--
-- - If cnf1 and cnf2 are CNFs describing
-- authority, then cnf1 `speaksFor` cnf2 if and only if
-- cnf1 logically implies cnf2 (often written cnf1
-- ⟹ cnf2). For example, ("A" /\ "B") `speaksFor`
-- toCNF "A", while toCNF "A" `speaksFor`
-- ("A" \/ "C").
-- - Given two DCLabels dc1 = (s1 %% i1) and
-- dc2 = (s2 %% i2), dc1 `canFlowTo` dc2
-- (often written dc1 ⊑ dc2) if and only if s2
-- `speaksFor` s1 && i1 `speaksFor` i2. In
-- other words, data can flow in the direction of requiring more
-- authority to make it public or removing integrity endorsements.
-- - Given two DCLabels dc1 = (s1 %% i1) and
-- dc2 = (s2 %% i2), and a p::CNF
-- representing privileges, canFlowToP p dc1 dc2 (often
-- written dc1 ⊑ₚ dc2) if and only if (p /\
-- s2) `speaksFor` s2 && (p /\ i1)
-- `speaksFor` i2.
--
data DCLabel
DCLabel :: !CNF -> !CNF -> DCLabel
-- | Describes the authority required to make the data public.
dcSecrecy :: DCLabel -> !CNF
-- | Describes the authority with which immutable data was endorsed, or the
-- authority required to modify mutable data.
dcIntegrity :: DCLabel -> !CNF
-- |
-- dcPublic = True %% True
--
--
-- This label corresponds to public data with no integrity guarantees.
-- For instance, an unrestricted Internet socket should be labeled
-- dcPublic. The significance of dcPublic is that given
-- data labeled (s %% i), s is the exact minimum
-- authority such that (s %% i) ⊑ₛ dcPublic, while i is
-- the exact minimum authority such that dcPublic ⊑ᵢ (s %% i).
dcPublic :: DCLabel
-- | The primary way of creating a DCLabel. The secrecy component
-- goes on the left, while the integrity component goes on the right,
-- e.g.:
--
--
-- label = secrecyCNF %% integrityCNF
--
--
-- Unlike the DCLabel constructor, the arguments can be any
-- instance of ToCNF. %% has fixity:
--
--
-- infix 6 %%
--
(%%) :: (ToCNF a, ToCNF b) => a -> b -> DCLabel
-- | Compute a conjunction of two CNFs or ToCNF instances.
--
-- Has fixity:
--
--
-- infixr 7 /\
--
(/\) :: (ToCNF a, ToCNF b) => a -> b -> CNF
-- | Compute a disjunction of two CNFs or ToCNF instances.
-- Note that this can be an expensive operation if the inputs have many
-- conjunctions.
--
-- The fixity is specifically chosen so that \/ and /\
-- cannot be mixed in the same expression without parentheses:
--
--
-- infixl 7 \/
--
(\/) :: (ToCNF a, ToCNF b) => a -> b -> CNF
-- | A boolean formula in Conjunctive Normal Form. CNF is used to
-- describe DCLabel privileges, as well to provide each of the two
-- halves of a DCLabel.
data CNF
-- | As a type, a CNF is always a conjunction of Disjunctions
-- of Principals. However, mathematically speaking, a single
-- Principal or single Disjunction is also a degenerate
-- example of conjunctive normal form. Class ToCNF abstracts over
-- the differences between these types, promoting them all to CNF.
class ToCNF c
toCNF :: ToCNF c => c -> CNF
-- | Extract the name of a principal as a strict ByteString. (Use
-- show to get it as a regular String.)
principalName :: Principal -> ByteString
-- | Represents a disjunction of Principals, or one clause of a
-- CNF. There is generally not much need to work directly with
-- Disjunctions unless you need to serialize and de-serialize
-- them (by means of dToSet and dFromList).
data Disjunction
-- | Expose the set of Principals being ORed together in a
-- Disjunction.
dToSet :: Disjunction -> Set Principal
-- | Convert a list of Principals into a Disjunction.
dFromList :: [Principal] -> Disjunction
-- | A CNF that is always True--i.e., trivially
-- satisfiable. When dcSecrecy = cTrue, it means data is
-- public. When dcIntegrity = cTrue, it means data
-- carries no integrity guarantees. As a description of privileges,
-- cTrue conveys no privileges; canFlowToP cTrue l1
-- l2 is equivalent to canFlowTo l1 l2.
--
-- Note that toCNF True = cTrue. Hence
-- dcPublic = DCLabel cTrue cTrue.
cTrue :: CNF
-- | A CNF that is always False. If dcSecrecy =
-- cFalse, then no combination of principals is powerful enough to
-- make the data public. For that reason, cFalse generally
-- shouldn't appear in a data label. However, it is convenient to include
-- as the dcSecrecy component of lioClearance to indicate a
-- thread may arbitrarily raise its label.
--
-- dcIntegrity = cFalse indicates impossibly much
-- integrity--i.e., data that no combination of principals is powerful
-- enough to modify or have created. Generally this is not a useful
-- concept.
--
-- As a privilege description, cFalse indicates impossibly high
-- privileges (i.e., higher than could be achieved through any
-- combination of Principals). cFalse `speaksFor`
-- p for any CNF p. This can be a useful concept for
-- bootstrapping privileges within the DC monad itself. For
-- instance, the result of privInit cFalse can be passed
-- to fully-trusted DC code, which can in turn use
-- delegate to create arbitrary finite privileges to pass to
-- less privileged code.
cFalse :: CNF
-- | Convert a CNF to a Set of Disjunctions. Mostly
-- useful if you wish to serialize a DCLabel.
cToSet :: CNF -> Set Disjunction
-- | Convert a list of Disjunctions into a CNF. Mostly useful
-- if you wish to de-serialize a CNF.
cFromList :: [Disjunction] -> CNF
instance Typeable Principal
instance Typeable Disjunction
instance Typeable CNF
instance Typeable DCLabel
instance Ord Principal
instance Eq CNF
instance Ord CNF
instance Eq DCLabel
instance Ord DCLabel
instance PrivDesc DCLabel CNF
instance SpeaksFor CNF
instance Label DCLabel
instance ToCNF Bool
instance ToCNF [Char]
instance ToCNF Principal
instance ToCNF Disjunction
instance ToCNF (Priv CNF)
instance ToCNF CNF
instance Read DCLabel
instance Show DCLabel
instance Monoid CNF
instance Read CNF
instance Show CNF
instance Monoid Disjunction
instance Read Disjunction
instance Show Disjunction
instance Ord Disjunction
instance Eq Disjunction
instance Eq Principal
instance Read Principal
instance Show Principal
-- | Helper routines for exposing IO operations on objects with
-- mutable labels. The mutable labels are implemented by type
-- MLabel, and have an immutable meta-label (or "label label")
-- protecting the mutable label.
--
-- It is reasonable to allow untrusted code to modify labels by exporting
-- a type-restricted version of modifyMLObjLabelP. When this
-- happens, asynchronous exceptions are sent to any other threads inside
-- mblessTCB or mblessPTCB if the new label revokes their
-- access.
module LIO.TCB.MLObj
-- | IO Object with a mutable label. By contrast with LObj, the
-- label on an MLObj can change over time. If this happens, the
-- internal MLabel ensures that threads accessing the object
-- receive an asynchronous exception.
data MLObj policy l object
MLObjTCB :: !(MLabel policy l) -> !object -> MLObj policy l object
-- | mlObjTCB ll l a creates an MLObj wrapping some
-- IO object a. Here ll is the label on the
-- label, which remains immutable over the lifetime of the MLObj.
-- l is the initial value of the mutable lable.
mlObjTCB :: MLabelPolicyDefault policy => l -> l -> a -> LIO l (MLObj policy l a)
-- | Like mlObjTCB, but create an MLObj with a particular
-- policy value. Note that you don't need to use this for
-- ExternalML and InternalML, as these don't have anything
-- interesting in the policy value, only the type matters. This might be
-- useful if, for instance, you wished to design a new policy type that
-- embeds a clearance.
mlPolicyObjTCB :: policy -> l -> l -> a -> LIO l (MLObj policy l a)
-- | Modify the MLabel within an MLObj.
modifyMLObjLabelP :: (PrivDesc l p, MLabelPolicy policy l) => Priv p -> MLObj policy l a -> (l -> LIO l l) -> LIO l ()
-- | The MLObj equivalent of blessTCB in
-- LIO.TCB.LObj#v:blessTCB. Use this for conveniently providing
-- LIO versions of standard IO functions.
mblessTCB :: (LabelIO l io lio, Label l) => String -> (a -> io) -> MLObj policy l a -> lio
-- | The MLObj equivalent of blessPTCB in
-- LIO.TCB.LObj#v:blessPTCB. Use this for conveniently providing
-- LIO versions of standard IO functions.
mblessPTCB :: (LabelIO l io lio, Label l, PrivDesc l p) => String -> (a -> io) -> Priv p -> MLObj policy l a -> lio
-- | A mutable label. Consists of a static label on the label, a mutable
-- label, and a list of threads currently accessing the label. This is
-- intended to be used by privileged code implementing IO
-- abstractions with mutable labels. Routines for accessing such an
-- IO abstraction should perform tne IO from within a
-- call to withMLabelP, to ensure an exception is raised if
-- another thread revokes access with modifyMLabelP.
data MLabel policy l
MLabelTCB :: !l -> !(IORef l) -> !(MVar (Map Unique (l -> IO Bool))) -> policy -> MLabel policy l
mlLabelLabel :: MLabel policy l -> !l
mlLabel :: MLabel policy l -> !(IORef l)
mlUsers :: MLabel policy l -> !(MVar (Map Unique (l -> IO Bool)))
mlPolicy :: MLabel policy l -> policy
-- | Create an MLabel, performing access control checks to ensure
-- that the labels are within the range allowed given the current label
-- and clearance, and the supplied privileges.
newMLabelP :: PrivDesc l p => Priv p -> policy -> l -> l -> LIO l (MLabel policy l)
-- | Returns the immutable label that controls access to the mutable label
-- value of an MLabel.
labelOfMlabel :: MLabel policy l -> l
-- | Retreive a snapshot of the value of a mutable label. Of course, it may
-- already have changed by the time you process it.
readMLabelP :: PrivDesc l p => Priv p -> MLabel policy l -> LIO l l
-- | Run an action that should be protected by a mutable label. An
-- exception is thrown if the invoking thread cannot write to the mutable
-- label given the privileges. No attempt is made to adjust the current
-- label, even if doing so would make the permissions acceptable.
--
-- Note that if the label changes after this function has been invoked,
-- an exception may be raised in the middle of the protected action.
withMLabelP :: PrivDesc l p => Priv p -> MLabel policy l -> LIO l a -> LIO l a
-- | Change the mutable label in an MLabel. Raises asynchronous
-- exceptions in other threads that are inside withMLabelP if the
-- new label revokes their access.
modifyMLabelP :: (PrivDesc l p, MLabelPolicy policy l) => Priv p -> MLabel policy l -> (l -> LIO l l) -> LIO l ()
-- | Class of objects with mutable labels.
class MLabelOf t
mLabelOf :: MLabelOf t => t policy l a -> MLabel policy l
-- | Class for MLabelPolicys that don't encode any interesting
-- values. This allows mlObjTCB to create an MLObj without
-- requiring a policy argument.
class MLabelPolicyDefault policy
mlabelPolicyDefault :: MLabelPolicyDefault policy => policy
-- | Class of policies for when it is permissible to update an
-- MLabel.
class MLabelPolicy policy l
mlabelPolicy :: (MLabelPolicy policy l, PrivDesc l p) => policy -> p -> l -> l -> LIO l ()
-- | InternalML is for objects contained entirely within Haskell,
-- such as a variable. Raising the label can't cause data to leak.
data InternalML
InternalML :: InternalML
-- | ExternalML is for objects that communicate to the outside
-- world, where extra privileges are required since once data gets out,
-- so as to vouch for the fact that the other end of a socket won't
-- arbitrarily downgrade data.
data ExternalML
ExternalML :: ExternalML
-- | Takes a liftIO-like function and an IO
-- function of an arbitrary number of arguments (up to 10). Applies the
-- arguments to the IO function, then passed the result to its
-- argument funciton to transform it into an LIO function.
class LabelIO l io lio | l io -> lio
labelIO :: LabelIO l io lio => (forall r. IO r -> LIO l r) -> io -> lio
instance Typeable InternalML
instance Typeable ExternalML
instance Typeable2 MLabel
instance Typeable3 MLObj
instance Show InternalML
instance Show ExternalML
instance LabelIO 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 LabelIO 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 LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r)
instance LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r)
instance LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r)
instance LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r)
instance LabelIO l (a1 -> a2 -> a3 -> a4 -> IO r) (a1 -> a2 -> a3 -> a4 -> LIO l r)
instance LabelIO l (a1 -> a2 -> a3 -> IO r) (a1 -> a2 -> a3 -> LIO l r)
instance LabelIO l (a1 -> a2 -> IO r) (a1 -> a2 -> LIO l r)
instance LabelIO l (a1 -> IO r) (a1 -> LIO l r)
instance LabelIO l (IO r) (LIO l r)
instance MLabelOf MLObj
instance MLabelPolicyDefault ExternalML
instance MLabelPolicy ExternalML l
instance MLabelPolicyDefault InternalML
instance MLabelPolicy InternalML l
-- | 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 labels and privileges (documented
-- in LIO.Label) and labeled values (documented in
-- LIO.Labeled).
--
-- 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 consisting
-- mostly of IO code that simply need to run LIO code
-- should import LIO.Run (or LIO.DCLabel) to avoid
-- polluting their namespaces.
--
-- Most code will need to use a particular label format, which needs to
-- be imported separately. Hence, a typical set of imports for an
-- untrusted LIO module is:
--
--
-- import LIO
-- import LIO.DCLabel
--
module LIO