-- 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.
--
-- The paper that describes the core of LIO, including motivation and
-- formal modeling/proofs, is available here:
-- http://arxiv.org/abs/1207.1457
@package lio
@version 0.9.1.2
-- | This module exports the class PrivTCB which all privilege types
-- must be an instance of. This class is in the TCB since privileges can
-- be used to bypass label restrictions and untrusted code should not be
-- allowed to do do arbitrarily. See LIO.Privs for an additional
-- description of privileges and their role within LIO.
--
-- In addition to PrivTCB this module exports the class
-- PrivDesc which provides a function from privileges to
-- privilege descriptions. A privilege description is a meaningful
-- and safe interpretation of a coresponding privilege (note that the
-- function must be one-to-on). Privilege descriptions are used in
-- LIO.Gate as "proof" of privilege ownership. Additionally,
-- privilege descriptions can be used by TCB code to mint new privileges
-- using the MintTCB class.
module LIO.Privs.TCB
-- | Zero-method class that imposes a restriction on what code (namely
-- trusted) can make a "privilege type".
class PrivTCB p
-- | Class used to convert a privilege to a privilege description. This is
-- particularly useful when one piece of code wishes to prove ownership
-- of certain privileges without granting the privilege. NOTE: it
-- (almost) always a security violation if the privilege is also the
-- privilege description.
--
-- Although this class is not part of the TCB there are some security
-- implications that should be considered when making a type an instance
-- of this class. Specifically, if the value constructor for the
-- privilege description type d is exported then some trusted
-- code must be used when "proving" ownership of a certain privilege.
-- This is generally a good idea even if the constructor is not made
-- available, since code can (usually) cache such privilege descriptions.
-- An alternative is to use phantom types to enforce a linear-type-like
-- behavior.
class (PrivTCB p, Show d) => PrivDesc p d | p -> d, d -> p
privDesc :: PrivDesc p d => p -> d
-- | The dual of PrivDesc. This class provides mintTCB
-- which may be used to convert, or mint, a privilege descriptions
-- into a privilege. Of course, mintTCB must be restricted to
-- the TCB.
class PrivDesc p d => MintTCB p d
mintTCB :: MintTCB p d => d -> p
-- | 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 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, Typeable l) => Label l
bottom :: Label l => l
top :: Label l => l
lub :: Label l => l -> l -> l
glb :: Label l => l -> l -> l
canFlowTo :: Label l => l -> l -> Bool
-- | A more meaningful name for lub. Note that since the name does
-- not imply least upper bound it is not a method of Label.
upperBound :: Label l => l -> l -> l
-- | A more meaningful name for glb. Note that since the name does
-- not imply greatest lower bound it is not a method of
-- Label.
lowerBound :: Label l => l -> l -> l
-- | 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, Label l) => t l a -> l
-- | Privileges are instances of the class called Priv. They
-- represent the ability to bypass the protection of certain labels.
-- Specifically, privilege allows you to behave as if L_1
-- `canFlowTo` L_2 even when that is not the case. The
-- process of making data labeled L_1 affect data labeled
-- L_2 when not (L_1 `canFlowTo` L_2) is called
-- downgrading.
--
-- The basic method of the Priv class is canFlowToP, which
-- performs a more permissive can-flow-to check by exercising particular
-- privileges (in literature this relation is a pre-order, commonly
-- written as ⊑ₚ). Almost all LIO operations have variants
-- ending ...P that take a privilege argument to act in a more
-- permissive way.
--
-- All Priv types are Monoids, and so privileges can be
-- combined with mappend. The creation of Priv values is
-- specific to the particular label type in use; the method used is
-- mintTCB, but the arguments depend on the particular label type.
module LIO.Privs
-- | Class used to convert a privilege to a privilege description. This is
-- particularly useful when one piece of code wishes to prove ownership
-- of certain privileges without granting the privilege. NOTE: it
-- (almost) always a security violation if the privilege is also the
-- privilege description.
--
-- Although this class is not part of the TCB there are some security
-- implications that should be considered when making a type an instance
-- of this class. Specifically, if the value constructor for the
-- privilege description type d is exported then some trusted
-- code must be used when "proving" ownership of a certain privilege.
-- This is generally a good idea even if the constructor is not made
-- available, since code can (usually) cache such privilege descriptions.
-- An alternative is to use phantom types to enforce a linear-type-like
-- behavior.
class (PrivTCB p, Show d) => PrivDesc p d | p -> d, d -> p
privDesc :: PrivDesc p d => p -> d
-- | This class defines privileges and the more-permissive relation
-- (canFlowToP) on labels using privileges. Additionally, it
-- defines partDowngradeP which is used to downgrage a label up to
-- a limit, given a set of privilege.
class (Label l, PrivTCB p, Monoid p) => Priv l p where canFlowToP p a b = partDowngradeP p a b `canFlowTo` b
canFlowToP :: Priv l p => p -> l -> l -> Bool
partDowngradeP :: Priv l p => p -> l -> l -> l
-- | Generic privilege type used to denote the lack of privileges.
data NoPrivs
NoPrivs :: NoPrivs
instance Show NoPrivs
instance Read NoPrivs
instance Label l => Priv l NoPrivs
instance Monoid NoPrivs
instance MintTCB NoPrivs NoPrivs
instance PrivDesc NoPrivs NoPrivs
instance PrivTCB NoPrivs
-- | LIO provides a basic implementation of gates, useful in
-- providing controlled RPC-like services where the client and service
-- provider are in mutual distrust.
--
-- A service provider uses gate to create a gate data type
-- Gate d a given a computation of type d ->
-- a. Here, d is a privilege description (type variable for
-- an instance of PrivDesc). Gates are invoked with
-- callGate, and as such the service provider has the guarantee
-- that the client (the caller) owns the privileges corresponding to the
-- privilege description d. In effect, this allows a client to
-- "prove" to the service provider that they own certain privileges
-- without entrusting the service with its privileges. The gate
-- computation can analyze this privilege description before performing
-- the "actual" computation. The client and server solely need to trust
-- the implementation of callGate.
module LIO.Gate
-- | 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 :: PrivDesc p d => (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 :: PrivDesc p d => Gate d a -> p -> a
-- | This module exports
--
--
-- - The definition of the LIO monad and relevant trusted state
-- access/modifying functions.
-- - Labeled exceptions that are use throughout LIO and
-- low-level, unsafe, throw and catch primitives.
-- - Combinators for executing IO actions.
--
--
-- The documentation and external, safe LIO interface is provided
-- in LIO.Core.
module LIO.TCB
-- | 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 :: StateT (LIOState l) IO a -> LIO l a
unLIOTCB :: LIO l a -> StateT (LIOState l) IO 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
-- | Get internal state. This function is not actually unsafe, but to avoid
-- future security bugs we leave all direct access to the internal state
-- to trusted code.
getLIOStateTCB :: Label l => LIO l (LIOState l)
-- | Set internal state.
putLIOStateTCB :: Label l => LIOState l -> LIO l ()
-- | Update the internal state given some function.
updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()
-- | A labeled exception is simply an exception associated with a label.
data LabeledException l
LabeledExceptionTCB :: !l -> SomeException -> LabeledException l
-- | Throw an arbitrary exception. Note that the exception being thrown is
-- not labeled.
unlabeledThrowTCB :: (Exception e, Label l) => e -> LIO l a
-- | Catch an exception. Note that all exceptions thrown by LIO are labeled
-- and thus this trusted function can be used to handle any exception.
-- Note that the label of the exception must be considered in the handler
-- (i.e., handler must raise the current label) to preserve security.
catchTCB :: Label l => LIO l a -> (LabeledException l -> LIO l a) -> LIO l a
-- | Lifts an IO computation into the LIO monad. Note that
-- exceptions thrown within the IO computation cannot directly be
-- caught within the LIO computation. Thus, you will generally
-- want to use rtioTCB exported by LIO.Exception.TCB
-- instead of ioTCB.
ioTCB :: Label l => IO a -> LIO l a
-- | Lifts an IO computation into the LIO monad. If the
-- IO computation throws an exception, it labels the exception
-- with the current label so that the exception can be caught with
-- catchLIO.
rethrowIoTCB :: Label l => IO a -> LIO l a
-- | 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 Typeable1 LabeledException
instance Eq l => Eq (LIOState l)
instance Show l => Show (LIOState l)
instance Read l => Read (LIOState l)
instance Functor (LIO l)
instance Applicative (LIO l)
instance Monad (LIO l)
instance Show l => Show (LabeledException l)
instance Label l => Exception (LabeledException l)
instance Label l => MonadLIO l (LIO l)
-- | This module implements the core of the Labeled IO (LIO) library for
-- information flow control (IFC) in Haskell. It provides a monad,
-- LIO, that is intended to be used as a replacement for the
-- IO monad in untrusted code. The idea is for untrusted code to
-- provide a computation in the LIO monad, which trusted code can
-- then safely execute through using evalLIO-like functions.
-- Though, usually a wrapper function is employed depending on the type
-- of labels used by an application. For example, with
-- LIO.DCLabel trusted code would evalDC to execute an
-- untrusted computation.
--
-- Labels are a way of describing who can observe and modify data. (A
-- detailed consideration of labels is given in LIO.Label.) LIO
-- associates a current label with every LIO computation.
-- The current label effectively tracks the sensitivity of all the data
-- that the computation has observed. For example, if the computation has
-- read a "secret" mutable refernce (see LIO.LIORef) and then the
-- result of a "top-secret" thread (see LIO.Concurrent) then the
-- current label will be at least "top-secret". The role of the current
-- label is two-fold. First, the current label protects all the data in
-- scope -- it is the label associated with any unlabeled data.
-- For example, the current label is the label on contants such as
-- 3 or "tis a string". More interestingly, consider
-- reading a "secret" file:
--
--
-- bs <- readFile "/secret/file.txt"
--
--
-- Though the label in the file store may be "secret", bs has
-- type ByteString, which is not explicitly labeled. Hence, to
-- protect the contents (bs) the current label must be at least
-- "secret" before executing readFile. More generally, if the
-- current label is L_cur, then it is only permissible to read
-- data labeled L_r if L_r `canFlowTo` L_cur.
-- Note that, rather than throw an exception, reading data will often
-- just increase the current label to ensure that L_r
-- `canFlowTo` L_cur using taint.
--
-- Second, the current label prevents inforation leaks into public
-- channels. Specifically, it is only permissible to modify, or write to,
-- data labeled L_w when L_cur`canFlowTo` L_w.
-- Thus, it the following attempt to leak the secret bs would
-- fail:
--
--
-- writeFile "/public/file.txt" bs
--
--
-- In addition to the current label, the LIO monad keeps a second label,
-- the current clearance (accessible via the getClearance
-- function). The clearance can be used to enforce a "need-to-know"
-- policy since it represents the highest value the current label can be
-- raised to. In other words, if the current clearance is
-- L_clear then the computation cannot create, read or write to
-- objects labeled L such that L `canFlowTo`
-- L_clear does not hold.
--
-- This module exports the LIO monad, functions to access the
-- internal state (e.g., getLabel and getClearance),
-- functions for raising and catching exceptions, and IFC guards.
-- Exceptions are core to LIO since they provide a way to deal with
-- potentially-misbehaving untrusted code. Specifically, when a
-- computation is about to violate IFC (as writeFile above), an
-- exception is raised. Guards provide a useful abstraction for dealing
-- with labeled objects; they should be used before performing a
-- read-only, write-only, or read-write operation on a labeled object.
-- The remaining core, but not all, abstractions are exported by
-- LIO.
module LIO.Core
-- | 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
-- | Given an LIO computation and some initial state, return an IO
-- action which when executed will perform the IFC-safe LIO computation.
--
-- Because untrusted code cannot execute IO computations, this
-- function should only be useful within trusted code. No harm is done
-- from exposing the evalLIO symbol to untrusted code. (In
-- general, untrusted code is free to produce IO computations, but
-- it cannot execute them.)
evalLIO :: Label l => LIO l a -> LIOState l -> IO a
-- | Execute an LIO action, returning the final state. See
-- evalLIO.
runLIO :: Label l => LIO l a -> LIOState l -> IO (a, LIOState l)
-- | Similar to evalLIO, but catches all exceptions exceptions
-- thrown with throwLIO.
tryLIO :: Label l => LIO l a -> LIOState l -> IO (Either (LabeledException l) a, LIOState l)
-- | Similar to evalLIO, but catches all exceptions, including
-- language level exceptions.
paranoidLIO :: Label l => LIO l a -> LIOState l -> IO (Either SomeException (a, LIOState l))
-- | 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
-- | Returns the current value of the thread's label.
getLabel :: MonadLIO l m => m l
-- | Raise the current label to the provided label, which must be between
-- the current label and clearance. See taint.
setLabel :: MonadLIO l m => l -> m ()
-- | If the current label is oldLabel and the current clearance is
-- clearance, this function allows code to raise the current
-- label to any value newLabel such that oldLabel
-- `canFlowTo` newLabel && newLabel `canFlowTo`
-- clearance.
setLabelP :: (MonadLIO l m, Priv l p) => p -> l -> m ()
-- | Returns the current value of the thread's clearance.
getClearance :: MonadLIO l m => m 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 :: MonadLIO l m => l -> m ()
-- | Raise the current clearance (undoing the effects of
-- setClearance) by exercising privileges. If the current label is
-- l and current clearance is c, then setClearanceP
-- p cnew succeeds only if the new clearance is can flow to the
-- current clearance (modulo privileges), i.e., canFlowToP p
-- cnew c must hold. Additionally, the current label must flow to
-- the new clearance, i.e., l `canFlowTo` cnew must hold.
setClearanceP :: (MonadLIO l m, Priv l p) => p -> l -> m ()
-- | 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 :: Priv l p => p -> l -> LIO l a -> LIO l a
-- | A labeled exception is simply an exception associated with a label.
data LabeledException l
-- | Throw an exception. The label on the exception is the current label.
throwLIO :: (Exception e, MonadLIO l m) => e -> m a
-- | Catches an exception, so long as the label at the point where the
-- exception was thrown can flow to the clearance at which
-- catchLIO is invoked. Note that the handler raises the current
-- label to the join (upperBound) of the current label and
-- exception label.
catchLIO :: (Exception e, Label l) => LIO l a -> (e -> LIO l a) -> LIO l a
-- | Same as catchLIO but does not use privileges when raising the
-- current label to the join of the current label and exception label.
catchLIOP :: (Exception e, Priv l p) => p -> LIO l a -> (e -> LIO l a) -> LIO l a
-- | Performs an action only if there was an exception raised by the
-- computation. Note that the exception is rethrown after the final
-- computation is executed.
onException :: Label l => LIO l a -> LIO l b -> LIO l a
-- | Privileged version of onExceptionP. onException cannot
-- run its handler if the label was raised in the computation that threw
-- the exception. This variant allows privileges to be supplied, so as to
-- catch exceptions thrown with a "higher" label.
onExceptionP :: Priv l p => p -> LIO l a -> LIO l b -> LIO l a
-- | Execute a computation and a finalizer, which is executed even if an
-- exception is raised in the first computation.
finally :: Label l => LIO l a -> LIO l b -> LIO l a
-- | Version of finally that uses privileges when handling
-- exceptions thrown in the first computation.
finallyP :: Priv l p => p -> LIO l a -> LIO l b -> LIO l a
-- | The bracket function is used in patterns where you acquire a
-- resource, perform a computation on it, and then release the resource.
-- The function releases the resource even if an exception is raised in
-- the computation. An example of its use case is file handling:
--
--
-- bracket
-- (openFile ... {- open file -} )
-- (\handle -> {- close file -} )
-- (\handle -> {- computation on handle -})
--
--
-- Note: bracket does not use mask and thus asynchronous
-- may leave the resource unreleased if the thread is killed in during
-- release. An interface for arbitrarily killing threads is not provided
-- by LIO.
bracket :: Label l => LIO l a -> (a -> LIO l c) -> (a -> LIO l b) -> LIO l b
-- | Like bracket, but uses privileges to downgrade the label of any
-- raised exception.
bracketP :: Priv l p => p -> 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. This is simply a wrapper for
-- Control.Exception's evaluate.
evaluate :: MonadLIO l m => a -> m 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
-- | 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 :: MonadLIO l m => l -> m ()
-- | Like guardAlloc, but takes privilege argument to be more
-- permissive. Note: privileges are only used when checking that
-- the current label can flow to the given label.
guardAllocP :: (MonadLIO l m, Priv l p) => p -> l -> m ()
-- | Use taint l in trusted code before observing an object
-- labeled l. This will raise the current label to a value
-- l' such that l `canFlowTo` l', or throw
-- ClearanceViolation if l' would have to be higher than
-- the current clearance.
taint :: MonadLIO l m => l -> m ()
-- | Like taint, but use privileges to reduce the amount of taint
-- required. Note that taintP will never lower the current
-- label. It simply uses privileges to avoid raising the label as high as
-- taint would raise it.
taintP :: (MonadLIO l m, Priv l p) => p -> l -> m ()
-- | Use guardWrite l in any (trusted) code before modifying an
-- object labeled l, for which a the modification can be
-- observed, i.e., the write implies a read.
--
-- The implementation of guardWrite is straight forward:
--
--
-- guardWrite l = taint l >> guardAlloc l
--
--
-- This guarantees that l `canFlowTo` the current label
-- (and clearance), and that the current label `canFlowTo`
-- l.
guardWrite :: MonadLIO l m => l -> m ()
-- | Like guardWrite, but takes privilege argument to be more
-- permissive.
guardWriteP :: (MonadLIO l m, Priv l p) => p -> l -> m ()
instance Typeable MonitorFailure
instance Typeable VMonitorFailure
instance Show MonitorFailure
instance Exception VMonitorFailure
instance Show VMonitorFailure
instance Exception MonitorFailure
-- | This is the TCB-restricted version of LIO.Labeled, which
-- documents the implementation of Labeled values and their use.
-- It provides functions for labeling (labelTCB) and unlabeling
-- (unlabelTCB) labeled values without imposing any information
-- flow restrictions.
module LIO.Labeled.TCB
-- | Labeled 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
-- | Label of Labeled valued
labelOfLabeled :: Labeled l t -> !l
-- | Extracts the value from an Labeled, discarding the label and
-- any protection.
unlabelTCB :: Labeled l t -> !t
-- | Trusted constructor that creates labeled values.
labelTCB :: Label l => l -> a -> Labeled l a
instance Typeable2 Labeled
instance (Label l, Read l, Read a) => ReadTCB (Labeled l a)
instance (Label l, Show a) => ShowTCB (Labeled l a)
-- | 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 :: MonadLIO l m => l -> a -> m (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 :: (MonadLIO l m, Priv l p) => p -> l -> a -> m (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 :: MonadLIO l m => Labeled l a -> m 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 :: (MonadLIO l m, Priv l p) => p -> Labeled l a -> m a
-- | Relabels a Labeled value to the supplied label if the given
-- privilege privileges permits it. It must be that the original label
-- and new label are equal, modulo the supplied privileges. In other
-- words the label remains in the same congruence class.
--
-- Consequently relabelP p l lv throws an
-- InsufficientPrivs exception if
--
--
-- canFlowToP p l (labelOf lv) && canFlowToP p (labelOf lv) l
--
--
-- does not hold.
relabelLabeledP :: (MonadLIO l m, Priv l p) => p -> l -> Labeled l a -> m (Labeled l a)
-- | Raises the label of a Labeled to the upperBound of it's
-- current label and the value supplied. The label supplied must be
-- bounded by the current label and clearance, though the resulting label
-- may not be if the Labeled is already above the current thread's
-- clearance. If the supplied label is not bounded then
-- taintLabeled will throw an exception (see guardAlloc).
taintLabeled :: MonadLIO l m => l -> Labeled l a -> m (Labeled l a)
-- | Same as taintLabeled, but uses privileges when comparing the
-- current label to the supplied label. In other words, this function can
-- be used to lower the label of the labeled value by leveraging the
-- supplied privileges.
taintLabeledP :: (MonadLIO l m, Priv l p) => p -> l -> Labeled l a -> m (Labeled l a)
-- | Downgrades the label of a Labeled as much as possible given the
-- current privilege.
untaintLabeled :: MonadLIO l m => l -> Labeled l a -> m (Labeled l a)
-- | Same as untaintLabeled but uses the supplied privileges when
-- downgrading the label of the labeled value.
untaintLabeledP :: (MonadLIO l m, Priv l p) => p -> l -> Labeled l a -> m (Labeled l a)
-- | IFC-aware functor instance. Since certain label formats may contain
-- integrity information, this is provided as a class rather than a
-- function. Such label formats will likely wish to drop endorsements in
-- the new labeled valued.
class Label l => LabeledFunctor l
lFmap :: (LabeledFunctor l, MonadLIO l m) => Labeled l a -> (a -> b) -> m (Labeled l b)
instance LabelOf Labeled
-- | This module implements the core of labeled MVarss in the 'LIO
-- ad. to Control.Concurrent.MVar, but the operations take place
-- in the LIO monad. The types and functions exported by this
-- module are strictly TCB and do not perform any information flow
-- checks. The external, safe interface is provided and documented in
-- LIO.Concurrent.LMVar.
module LIO.Concurrent.LMVar.TCB
-- | An LMVar is a labeled synchronization variable (an
-- MVar) that can be used by concurrent threads to communicate.
data LMVar l a
LMVarTCB :: !l -> MVar a -> LMVar l a
-- | Label of MVar.
labelOfLMVar :: LMVar l a -> !l
-- | Access the underlying MVar, ignoring IFC.
unlabelLMVarTCB :: LMVar l a -> MVar a
-- | Trusted function used to create an empty LMVar, ignoring IFC.
newEmptyLMVarTCB :: MonadLIO l m => l -> m (LMVar l a)
-- | Trusted function used to create an LMVar with the supplied
-- value, ignoring IFC.
newLMVarTCB :: MonadLIO l m => l -> a -> m (LMVar l a)
-- | Read the contents of an LMVar, ignoring IFC.
takeLMVarTCB :: MonadLIO l m => LMVar l a -> m a
-- | Same as tryTakeLMVar, but ignorses IFC.
tryTakeLMVarTCB :: MonadLIO l m => LMVar l a -> m (Maybe a)
-- | Put a value into an LMVar, ignoring IFC.
putLMVarTCB :: MonadLIO l m => LMVar l a -> a -> m ()
-- | Same as tryPutLMVar, but ignorses IFC.
tryPutLMVarTCB :: MonadLIO l m => LMVar l a -> a -> m Bool
-- | Trusted function used to read (take and put) an LMVar, ignoring
-- IFC.
readLMVarTCB :: MonadLIO l m => LMVar l a -> m a
-- | Trusted function that swaps value of LMVar, ignoring IFC.
swapLMVarTCB :: MonadLIO l m => LMVar l a -> a -> m a
-- | Same as isEmptyLMVar, but ignorses IFC.
isEmptyLMVarTCB :: MonadLIO l m => LMVar l a -> m Bool
instance LabelOf LMVar
-- | 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.
data LMVar l 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 :: MonadLIO l m => l -> m (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 :: (MonadLIO l m, Priv l p) => p -> l -> m (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 :: (MonadLIO l m, Priv l p) => p -> l -> a -> m (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 :: MonadLIO l m => LMVar l a -> m a
-- | Same as takeLMVar except takeLMVarP takes a privilege
-- object which is used when the current label is raised.
takeLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> m a
-- | Non-blocking version of takeLMVar. It returns Nothing
-- if the LMVar is empty, otherwise it returns Just
-- value, emptying the LMVar.
tryTakeLMVar :: MonadLIO l m => LMVar l a -> m (Maybe a)
-- | Same as tryTakeLMVar, but uses priviliges when raising current
-- label.
tryTakeLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> m (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 :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> a -> m ()
-- | Non-blocking version of putLMVar. It returns True if
-- the LMVar was empty and the put succeeded, otherwise it returns
-- False.
tryPutLMVar :: MonadLIO l m => LMVar l a -> a -> m Bool
-- | Same as tryPutLMVar, but uses privileges when raising current
-- label.
tryPutLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> a -> m Bool
-- | Combination of takeLMVar and putLMVar. Read the value,
-- and just put it back. As specified for readMVar, this
-- operation is atomic iff there is no other thread calling
-- putLMVar for this LMVar.
readLMVar :: MonadLIO l m => LMVar l a -> m a
-- | Same as readLMVar except readLMVarP takes a privilege
-- object which is used when the current label is raised.
readLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> m a
-- | 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 :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> a -> m 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 :: MonadLIO l m => LMVar l a -> m Bool
-- | Same as isEmptyLMVar, but uses privileges when raising current
-- label.
isEmptyLMVarP :: (MonadLIO l m, Priv l p) => p -> LMVar l a -> m 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.Concurrent.TCB
-- | A labeled thread result is simply a wrapper for a LMVar. A
-- thread can observe the result of another thread, only after raising
-- its label to the label of the result.
data LabeledResult l a
LabeledResultTCB :: ThreadId -> LMVar l (Either (LabeledException l) a) -> LabeledResult l a
-- | Thread executing the computation
lresThreadIdTCB :: LabeledResult l a -> ThreadId
-- | Plecement of computation result
lresResultTCB :: LabeledResult l a -> LMVar l (Either (LabeledException l) a)
-- | A ThreadId is an abstract type representing a handle to a
-- thread. ThreadId is an instance of Eq, Ord and
-- Show, where the Ord instance implements an arbitrary
-- total ordering over ThreadIds. The Show instance lets
-- you convert an arbitrary-valued ThreadId to string form;
-- showing a ThreadId value is occasionally useful when debugging
-- or diagnosing the behaviour of a concurrent program.
--
-- Note: in GHC, if you have a ThreadId, you essentially
-- have a pointer to the thread itself. This means the thread itself
-- can't be garbage collected until you drop the ThreadId. This
-- misfeature will hopefully be corrected at a later date.
--
-- Note: Hugs does not provide any operations on other threads; it
-- defines ThreadId as a synonym for ().
data ThreadId :: *
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 labeled thread result is simply a wrapper for a LMVar. A
-- thread can observe the result of another thread, only after raising
-- its label to the label of the result.
data LabeledResult l a
-- | A ThreadId is an abstract type representing a handle to a
-- thread. ThreadId is an instance of Eq, Ord and
-- Show, where the Ord instance implements an arbitrary
-- total ordering over ThreadIds. The Show instance lets
-- you convert an arbitrary-valued ThreadId to string form;
-- showing a ThreadId value is occasionally useful when debugging
-- or diagnosing the behaviour of a concurrent program.
--
-- Note: in GHC, if you have a ThreadId, you essentially
-- have a pointer to the thread itself. This means the thread itself
-- can't be garbage collected until you drop the ThreadId. This
-- misfeature will hopefully be corrected at a later date.
--
-- Note: Hugs does not provide any operations on other threads; it
-- defines ThreadId as a synonym for ().
data ThreadId :: *
-- | Get the ThreadId of the calling thread.
myThreadId :: MonadLIO l m => m ThreadId
-- | Execute an LIO computation in a new lightweight thread. The
-- ThreadId of the newly created thread is returned.
forkLIO :: Label l => LIO l () -> LIO l ThreadId
-- | Same as lFork, but the supplied set of priviliges are accounted
-- for when performing label comparisons.
lForkP :: Priv l p => p -> l -> LIO l a -> LIO l (LabeledResult l a)
-- | 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 require that this label is above the current label, and
-- below the current clearance as enforced by the underlying
-- guardAlloc. Moreover, the supplied computation must not read
-- anything more sensitive (i.e., with a label above the supplied label)
-- --- doing so will result in an exception (whose label will reflect
-- this observation) being thrown.
--
-- If an exception is thrown in the inner computation, the exception
-- label will be raised to the join of the result label and original
-- exception label.
--
-- 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 lWait, but uses priviliges in label checks and raises.
lWaitP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m 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 :: MonadLIO l m => LabeledResult l a -> m a
-- | Same as trylWait, but uses priviliges in label checks and
-- raises.
trylWaitP :: (MonadLIO l m, Priv l p) => p -> LabeledResult l a -> m (Maybe a)
-- | Same as lWait, but does not block waiting for result.
trylWait :: MonadLIO l m => LabeledResult l a -> m (Maybe a)
-- | Suspend current thread for a given number of microseconds.
threadDelay :: MonadLIO l m => Int -> m ()
-- | Asynchronous exceptions.
data AsyncException :: *
-- | The current thread's stack exceeded its limit. Since an exception has
-- been raised, the thread's stack will certainly be below its limit
-- again, but the programmer should take remedial action immediately.
StackOverflow :: AsyncException
-- | The program's heap is reaching its limit, and the program should take
-- action to reduce the amount of live data it has. Notes:
--
--
-- - It is undefined which thread receives this exception.
-- - GHC currently does not throw HeapOverflow exceptions.
--
HeapOverflow :: AsyncException
-- | This exception is raised by another thread calling killThread,
-- or by the system if it needs to terminate the thread for some reason.
ThreadKilled :: AsyncException
-- | This exception is raised by default in the main thread of the program
-- when the user requests to terminate the program via the usual
-- mechanism(s) (e.g. Control-C in the console).
UserInterrupt :: AsyncException
-- | Though in most cases using a LabeledResult is sufficient, in
-- certain scenarios it is desirable to produce a pure Labeled
-- value that is the result of other potentially sensitive values. As
-- such, we provide lBracket.
--
-- lBracket is like lFork, but rather than returning a
-- LabeledResult, it returns a Labeled value. The key
-- difference between the two is that lBracket takes an
-- additional parameter specifying the number of microseconds the inner
-- computation will take. As such, lBracket will block for the
-- specified duration and the result of the inner computation be
-- forced. That is, if the computation terminated cleanly,
-- i.e., it did not throw an exception and it finished in the time
-- specified, then Just the result is returned, otherwise
-- Nothing is returned.
--
-- Note that the original LIO (before version 0.9) included a similar
-- "primitive" called toLabeled. We have chosen to call this
-- lBracket in part because it is a more descriptive name and to
-- avoid confusion with the previous toLabeled where time was
-- not considered.
lBracket :: MonadLIO l m => l -> Int -> LIO l a -> m (Labeled l (Maybe a))
-- | Same as lBracket, but uses privileges when forking the new
-- thread.
lBracketP :: (MonadLIO l m, Priv l p) => p -> l -> Int -> LIO l a -> m (Labeled l (Maybe 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 :: S8 -> Principal
-- | Get the principal name.
principalName :: Principal -> S8
-- | Principal constructor.
principal :: S8 -> 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
-- | Label constructor. Note that each component is first reduced 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
-- | 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] Show DCLabel
instance [safe] Show Component
instance [safe] Show Clause
instance [safe] Ord Clause
instance [safe] Show Principal
-- | This module provides instances for binary serialization of
-- DCLabels. Specifically, we provide insgtances for
-- cereal's Data.Serialize.
module LIO.DCLabel.Serialize
instance Serialize Clause
instance Serialize Principal
instance Serialize DCLabel
instance Serialize Component
-- | This module implements the trusted compoenet of DCLabel privileges,
-- documented in LIO.DCLabel.Privs. Since privilege objects may be
-- used unsafely, this module is marked -XUnsafe. Untrusted code
-- may access privileges using the interface provided by
-- LIO.DCLabel.Privs.
module LIO.DCLabel.Privs.TCB
-- | A privilege description is simply a conjunction of disjunctions.
-- Unlike (actually minted) privileges (see DCPriv), privilege
-- descriptions may be created by untrusted code.
type DCPrivDesc = Component
-- | A privilege is a minted and protected privilege description
-- (DCPrivDesc) that may only be created by trusted code or
-- delegated from an existing DCPriv.
newtype DCPriv
DCPrivTCB :: DCPrivDesc -> DCPriv
unDCPriv :: DCPriv -> DCPrivDesc
-- | The all privilege corresponds to logical False
allPrivTCB :: DCPriv
instance Typeable DCPriv
instance Eq DCPriv
instance Show DCPriv
instance MintTCB DCPriv DCPrivDesc
instance PrivDesc DCPriv DCPrivDesc
instance PrivTCB DCPriv
-- | This module exports the basic interface for creating and using the
-- labeled file system, implemented as a file store. Trusted code should
-- use initFSTCB to set the root of the labeled file system.
-- Moreover, trusted code should implement all the IO functions in terms
-- of createFileTCB, createDirectoryTCB, and
-- getPathLabelTCB and setPathLabelTCB.
module LIO.FS.TCB
-- | Initialize filesystem at the given path. The supplied path must be
-- absolute, otherwise initFSTCB throw FSRootInvalid. If
-- the FS has already been created then initFSTCB solely
-- verifies that the root directory is not corrupt (see setFSTCB).
-- Otherwise, a new FS is created with the supplied label (see
-- mkFSTCB).
--
-- This function performs several checks that setFSTCB and
-- mkFSTCB perform, so when considering performance they should be
-- called directly.
initFSTCB :: SLabel l => FilePath -> Maybe l -> LIO l ()
-- | Create a the file store (i.e., labeled file system) with a given label
-- and root file path. The path must be an absolute path, otherwise
-- initFSTCB throws FSRootInvalid.
mkFSTCB :: SLabel l => FilePath -> l -> LIO l ()
-- | Set the given file path as the root of the labeled filesystem. This
-- function throws a FSLabelCorrupt if the directory does not
-- contain a valid label, and a FSRootCorrupt if the
-- magicAttr attribute is missing.
setFSTCB :: SLabel l => FilePath -> LIO l ()
-- | Get the root directory.
getRootDirTCB :: SLabel l => LIO l FilePath
-- | Set the label of a given path. This function sets the labelAttr
-- attribute to the encoded label, and the hash to labelHashAttr.
setPathLabelTCB :: SLabel l => FilePath -> l -> LIO l ()
-- | Get the label of a given path. If the object does not have an
-- associated label or the hash of the label and stored-hash are not
-- equal, this function throws FSLabelCorrupt.
getPathLabelTCB :: SLabel l => FilePath -> LIO l l
-- | Create a file object with the given label and return a handle to the
-- new file.
createFileTCB :: SLabel l => l -> FilePath -> IOMode -> LIO l Handle
-- | Create a directory object with the given label.
createDirectoryTCB :: SLabel l => l -> FilePath -> LIO l ()
data LFilePath l
LFilePathTCB :: l -> FilePath -> LFilePath l
-- | Label of file path
labelOfFilePath :: LFilePath l -> l
-- | Unlabel a filepath, ignoring IFC.
unlabelFilePathTCB :: LFilePath l -> FilePath
-- | Filesystem errors
data FSError
-- | Root structure is corrupt.
FSRootCorrupt :: FSError
-- | Root is invalid (must be absolute).
FSRootInvalid :: FSError
-- | Root already exists.
FSRootExists :: FSError
-- | Root does not exists.
FSRootNoExist :: FSError
-- | Cannot create root, missing label.
FSRootNeedLabel :: FSError
-- | FSobjectcannot be created without a label.
FSObjNeedLabel :: FSError
-- | Object label is corrupt.
FSLabelCorrupt :: FilePath -> FSError
-- | Supplied file name is illegal.
FSIllegalFileName :: FSError
-- | Constraintfor serializable labels
type SLabel l = (Label l, Serialize l)
-- | Encode a label into an attribute value.
lazyEncodeLabel :: SLabel l => l -> L8
-- | Encode a label into an attribute value.
encodeLabel :: SLabel l => l -> AttrValue
-- | Descode label from an attribute value.
decodeLabel :: SLabel l => AttrValue -> Either String l
instance Typeable FSError
instance Show FSError
instance Exception FSError
-- | This is the main module to be included by code using the Labeled IO
-- (LIO) library. This module exports the core library (documented in
-- LIO.Core), with support for labeled values (documented in
-- LIO.Labeled), privileges (documented in LIO.Privs), and
-- gates (documented in LIO.Gate).
--
-- Certain symbols in the LIO library supersede variants in the standard
-- Haskell libraries. Thus, depending on the modules imported and
-- functions used, you may wish to import LIO with commands like these:
--
--
-- import Control.Exception hiding ( onException
-- , finally
-- , bracket)
-- 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
-- | This module implements the core of labeled IORefs in the 'LIO
-- ad. to Data.IORef, but the operations take place in the
-- LIO monad. The types and functions exported by this module are
-- strictly TCB and do not perform any information flow checks. The
-- external, safe interface is provided and documented in
-- LIO.LIORef.
--
-- Different from many labeled objects (e.g., files or MVars), references
-- are uni-directional. This means that reading from a reference can be
-- done without being able to write to it; and writing to a refernece can
-- be done without raising the current label, as if also performing a
-- read.
module LIO.LIORef.TCB
-- | An LIORef is an IORef with an associated, fixed
-- label. The restriction to an immutable label come from the fact that
-- it is possible to leak information through the label itself, if we
-- wish to allow LIORef to be an instance of LabelOf. Of
-- course, you can create an LIORef of Labeled to get a
-- limited form of flow-sensitivity.
data LIORef l a
LIORefTCB :: !l -> (IORef a) -> LIORef l a
-- | Label of the labeled IORef.
labelOfLIORef :: LIORef l a -> !l
-- | Access the underlying IORef, ignoring IFC.
unlabelLIORefTCB :: LIORef l a -> (IORef a)
-- | Trusted constructor that creates labeled references with the given
-- label without any IFC checks.
newLIORefTCB :: MonadLIO l m => l -> a -> m (LIORef l a)
-- | Trusted function used to read the value of a reference without raising
-- the current label.
readLIORefTCB :: MonadLIO l m => LIORef l a -> m a
-- | Trusted function used to write a new value into a labeled reference,
-- ignoring IFC.
writeLIORefTCB :: MonadLIO l m => LIORef l a -> a -> m ()
-- | Trusted function that mutates the contents on an LIORef,
-- ignoring IFC.
modifyLIORefTCB :: MonadLIO l m => LIORef l a -> (a -> a) -> m ()
-- | Trusted function used to atomically modify the contents of a labeled
-- reference, ignoring IFC.
atomicModifyLIORefTCB :: MonadLIO l m => LIORef l a -> (a -> (a, b)) -> m b
instance LabelOf LIORef
-- | 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 solely 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.
data LIORef l a
-- | To create a new reference the label of the reference must be below the
-- thread's current clearance and above the current label. If this is the
-- case, the reference is built. Otherwise an exception will be thrown by
-- the underlying guardAlloc guard.
newLIORef :: MonadLIO l m => l -> a -> m (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 :: (MonadLIO l m, Priv l p) => p -> l -> a -> m (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 :: MonadLIO l m => LIORef l a -> m a
-- | Same as readLIORef except readLIORefP takes a
-- privilege object which is used when the current label is raised.
readLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> m a
-- | Write a new value into a labeled reference. A write succeeds if the
-- current label can-flow-to the label of the reference, and the label of
-- the reference can-flow-to the current clearance. Otherwise, an
-- exception is raised by the underlying guardAlloc guard.
writeLIORef :: MonadLIO l m => LIORef l a -> a -> m ()
-- | Same as writeLIORef except writeLIORefP takes a set of
-- privileges which are accounted for in comparing the label of the
-- reference to the current label and clearance.
writeLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> a -> m ()
-- | 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 :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> (a -> a) -> m ()
-- | Atomically modifies the contents of an LIORef. It is required
-- that the label of the reference be above the current label, but below
-- the current clearance. Moreover, since this function can be used to
-- directly read the value of the stored reference, the computation is
-- "tainted" by the reference label (i.e., the current label is raised to
-- the join of the current and reference labels). These checks
-- and label raise are done by guardWrite, which will raise an
-- exception if any of the IFC conditions cannot be satisfied.
atomicModifyLIORef :: MonadLIO l m => LIORef l a -> (a -> (a, b)) -> m b
-- | Same as atomicModifyLIORef except atomicModifyLIORefP
-- takes a set of privileges which are accounted for in label
-- comparisons.
atomicModifyLIORefP :: (MonadLIO l m, Priv l p) => p -> LIORef l a -> (a -> (a, b)) -> m b
-- | This module re-exports Data.Time wrapped in LIO.
--
-- WARNING: The time functions can be used to carry out
-- external-timing attacks with less effort than using threads and
-- synchronization. It is therefore advised that computations that
-- operate on sensitive data take the same amount of time regardless of
-- the input.
module LIO.Data.Time
-- | Get the current UTC time from the system clock.
getCurrentTime :: MonadLIO l m => m UTCTime
-- | Get the local time together with a TimeZone.
getZonedTime :: MonadLIO l m => m ZonedTime
-- | Convert UTC time to local time with TimeZone.
utcToLocalZonedTime :: MonadLIO l m => UTCTime -> m ZonedTime
-- | 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.
data DCPriv
-- | 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
instance Priv DCLabel DCPriv
instance Monoid DCPriv
-- | This module implements a `nano`, very simple, embedded domain
-- specific language to create Components and privilage
-- descriptions from conjunctions of principal disjunctions.
--
-- A Component or DCPrivDesc is created using the
-- (\/) and (/\) operators. The disjunction operator
-- (\/) is used to create a Clause from 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 = dcPrivTCB . dcPrivDesc $ "Alice" /\ "Carla"
--
--
-- where
--
--
-- dc1 = <{["Alice" ⋁ "Bob"] ⋀ ["Carla"]} , {["Alice"] ⋀
-- ["Carla"]}> dc2 = <{["Djon"]} , {["Alice"]}> canFlowTo dc1 dc2 = False
canFlowToP pr dc1 dc2 = True
module LIO.DCLabel.DSL
-- | 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 where dcPrivDesc = toComponent
toComponent :: ToComponent a => a -> Component
dcPrivDesc :: ToComponent a => a -> DCPrivDesc
-- | 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 Nothing.
toList :: Component -> [[Principal]]
-- | Logical falsehood can be thought of as the component containing every
-- possible principal:
--
--
-- everybody = dcFalse
--
everybody :: Component
-- | Logical truth can be thought of as the component containing no
-- specific principal:
--
--
-- anybody = dcTrue
--
anybody :: Component
instance [safe] ToComponent String
instance [safe] ToComponent S8
instance [safe] ToComponent Principal
instance [safe] ToComponent Clause
instance [safe] ToComponent Component
-- | 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.
data Principal
-- | Get the principal name.
principalName :: Principal -> S8
-- | Principal constructor.
principal :: S8 -> 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
-- | Label constructor. Note that each component is first reduced 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
-- | 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 DCLabeledException a, DCState)
-- | Similar to evalLIO, but catches all exceptions.
paranoidDC :: DC a -> IO (Either SomeException (a, DCState))
-- | Type synonym for MonadLIO.
type MonadDC m = MonadLIO DCLabel m
-- | DC Labeled exceptions.
type DCLabeledException = LabeledException DCLabel
-- | DC Labeled values.
type DCLabeled = Labeled DCLabel
-- | DC Labeled LIORefs.
type DCRef = LIORef DCLabel
-- | DC Gate.
type DCGate = Gate DCPrivDesc
instance LabeledFunctor DCLabel
-- | This module abstracts the basic file Handle methods provided by
-- the system library, and provides a LabeledHandle type that can
-- be manipulated from within the LIO Monad. A
-- LabeledHandle is imply a file Handle with an associated
-- label that is used to track and control the information flowing from
-- and to the file. The API exposed by this module is analogous to
-- System.IO, and the functions mainly differ in taking an
-- additional label and enforcing IFC.
--
-- The actual storage of labeled files is handled by the LIO.FS
-- module. The filesystem is implemented as a file store in which labels
-- are associated with files and directories (using extended attributes).
--
-- IMPORTANT: To use the labeled filesystem you must use
-- evalWithRootFS (or other initializers from LIO.FS.TCB),
-- otherwise any actions built using the combinators of this module will
-- crash.
--
-- An example use case shown below:
--
--
-- main = dcEvalWithRoot "/tmp/lioFS" $ do
-- createDirectoryP p lsecrets "secrets"
-- writeFileP p ("secrets" </> "alice" ) "I like Bob!"
-- where p = ...
-- lsecrets = ....
--
--
-- The file store for the labeled filesystem (see LIO.FS) will be
-- created in /tmp/lioFS, but this is transparent and the user
-- can think of the filesystem as having root /. Note that for
-- this to work the filesystem must be mounted with the
-- user_xattr option. For example, on GNU/Linux:
--
--
-- mount -o rw,noauto,user,sync,noexec,user_xattr /dev/sdb1 /tmp/lioFS
--
--
-- In the current version of the filesystem, there is no notion of
-- changeable current working directory in the LIO Monad, nor
-- symbolic links.
module LIO.Handle
-- | Same as evalLIO, but takes two additional parameters
-- corresponding to the path of the labeled filesystem store and the
-- label of the root. If the labeled filesystem store does not exist, it
-- is created at the specified path with the root having the supplied
-- label. If the filesystem does exist, the supplied label is ignored and
-- thus unnecessary. However, if the root label is not provided and the
-- filesystem has not been initialized, a FSRootNeedLabel
-- exception will be thrown.
evalWithRootFS :: SLabel l => FilePath -> Maybe l -> LIO l a -> LIOState l -> IO a
-- | Constraintfor serializable labels
type SLabel l = (Label l, Serialize l)
-- | Serialize MonadLIO
type SMonadLIO l m = (SLabel l, MonadLIO l m)
type LabeledHandle l = Labeled l Handle
-- | Haskell defines operations to read and write characters from and to
-- files, represented by values of type Handle. Each value of
-- this type is a handle: a record used by the Haskell run-time
-- system to manage I/O with file system objects. A handle has at
-- least the following properties:
--
--
-- - whether it manages input or output or both;
-- - whether it is open, closed or
-- semi-closed;
-- - whether the object is seekable;
-- - whether buffering is disabled, or enabled on a line or block
-- basis;
-- - a buffer (whose length may be zero).
--
--
-- Most handles will also have a current I/O position indicating where
-- the next input or output operation will occur. A handle is
-- readable if it manages only input or both input and output;
-- likewise, it is writable if it manages only output or both
-- input and output. A handle is open when first allocated. Once
-- it is closed it can no longer be used for either input or output,
-- though an implementation cannot re-use its storage while references
-- remain to it. Handles are in the Show and Eq classes.
-- The string produced by showing a handle is system dependent; it should
-- include enough information to identify the handle for debugging. A
-- handle is equal according to == only to itself; no attempt is
-- made to compare the internal state of different handles for equality.
data Handle :: *
-- | See openFile
data IOMode :: *
ReadMode :: IOMode
WriteMode :: IOMode
AppendMode :: IOMode
ReadWriteMode :: IOMode
-- | Three kinds of buffering are supported: line-buffering,
-- block-buffering or no-buffering. These modes have the following
-- effects. For output, items are written out, or flushed, from
-- the internal buffer according to the buffer mode:
--
--
-- - line-buffering: the entire output buffer is flushed
-- whenever a newline is output, the buffer overflows, a hFlush is
-- issued, or the handle is closed.
-- - block-buffering: the entire buffer is written out whenever
-- it overflows, a hFlush is issued, or the handle is closed.
-- - no-buffering: output is written immediately, and never
-- stored in the buffer.
--
--
-- An implementation is free to flush the buffer more frequently, but not
-- less frequently, than specified above. The output buffer is emptied as
-- soon as it has been written out.
--
-- Similarly, input occurs according to the buffer mode for the handle:
--
--
-- - line-buffering: when the buffer for the handle is not
-- empty, the next item is obtained from the buffer; otherwise, when the
-- buffer is empty, characters up to and including the next newline
-- character are read into the buffer. No characters are available until
-- the newline character is available or the buffer is full.
-- - block-buffering: when the buffer for the handle becomes
-- empty, the next block of data is read into the buffer.
-- - no-buffering: the next input item is read and returned. The
-- hLookAhead operation implies that even a no-buffered handle may
-- require a one-character buffer.
--
--
-- The default buffering mode when a handle is opened is
-- implementation-dependent and may depend on the file system object
-- which is attached to that handle. For most implementations, physical
-- files will normally be block-buffered and terminals will normally be
-- line-buffered.
data BufferMode :: *
-- | buffering is disabled if possible.
NoBuffering :: BufferMode
-- | line-buffering should be enabled if possible.
LineBuffering :: BufferMode
-- | block-buffering should be enabled if possible. The size of the buffer
-- is n items if the argument is Just n and is
-- otherwise implementation-dependent.
BlockBuffering :: Maybe Int -> BufferMode
-- | Given a set of privileges, a (maybe) new label of a file, a filepath,
-- and the IO mode, open (and possibly create) the file. If the file
-- exists, the supplied label is not necessary; otherwise it must be
-- supplied. The current label is raised to reflect all the traversed
-- directories. Additionally the label of the file (new or existing) must
-- be between the current label and clearance, as imposed by
-- guardAlloc. If the file is created, it is further required that
-- the current computation be able to write to the containing directory,
-- as imposed by guardWrite.
openFile :: SMonadLIO l m => Maybe l -> FilePath -> IOMode -> m (LabeledHandle l)
-- | Same as openFile, but uses privileges when traversing
-- directories and performing IFC checks.
openFileP :: (SMonadLIO l m, Priv l p) => p -> Maybe l -> FilePath -> IOMode -> m (LabeledHandle l)
-- | Close a file handle. Must be able to write to the the labeled handle,
-- as checkd by guardWrite.
hClose :: SMonadLIO l m => LabeledHandle l -> m ()
-- | Close a labeled file handle.
hCloseP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m ()
-- | Flush a file handle. Must be able to write to the the labeled handle,
-- as checkd by guardWrite.
hFlush :: SMonadLIO l m => LabeledHandle l -> m ()
-- | Flush a labeled file handle.
hFlushP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m ()
-- | Class used to abstract reading and writing from and to handles,
-- respectively.
class Monad m => HandleOps h b m where hPutStr = hPut
hGet :: HandleOps h b m => h -> Int -> m b
hGetNonBlocking :: HandleOps h b m => h -> Int -> m b
hGetContents :: HandleOps h b m => h -> m b
hGetLine :: HandleOps h b m => h -> m b
hPut :: HandleOps h b m => h -> b -> m ()
hPutStr :: HandleOps h b m => h -> b -> m ()
hPutStrLn :: HandleOps h b m => h -> b -> m ()
-- | Read n bytes from the labeled handle, using privileges when
-- performing label comparisons and tainting.
hGetP :: (Priv l p, Serialize l, HandleOps Handle b IO) => p -> LabeledHandle l -> Int -> LIO l b
-- | Same as hGetP, but will not block waiting for data to become
-- available. Instead, it returns whatever data is available. Privileges
-- are used in the label comparisons and when raising the current label.
hGetNonBlockingP :: (Priv l p, Serialize l, HandleOps Handle b IO) => p -> LabeledHandle l -> Int -> LIO l b
-- | Read the entire labeled handle contents and close handle upon reading
-- EOF. Privileges are used in the label comparisons and when
-- raising the current label.
hGetContentsP :: (Priv l p, Serialize l, HandleOps Handle b IO) => p -> LabeledHandle l -> LIO l b
-- | Read the a line from a labeled handle.
hGetLineP :: (Priv l p, Serialize l, HandleOps Handle b IO) => p -> LabeledHandle l -> LIO l b
-- | Output the given (Byte)String to the specified labeled handle.
-- Privileges are used in the label comparisons and when raising the
-- current label.
hPutP :: (Priv l p, Serialize l, HandleOps Handle b IO) => p -> LabeledHandle l -> b -> LIO l ()
-- | Synonym for hPutP.
hPutStrP :: (Priv l p, Serialize l, HandleOps Handle b IO) => p -> LabeledHandle l -> b -> LIO l ()
-- | Output the given (Byte)String with an appended newline to the
-- specified labeled handle. Privileges are used in the label comparisons
-- and when raising the current label.
hPutStrLnP :: (Priv l p, Serialize l, HandleOps Handle b IO) => p -> LabeledHandle l -> b -> LIO l ()
-- | Reads a file and returns the contents of the file as a ByteString.
readFile :: (HandleOps Handle b IO, SLabel l) => FilePath -> LIO l b
-- | Same as readFile but uses privilege in opening the file.
readFileP :: (HandleOps Handle b IO, Priv l p, Serialize l) => p -> FilePath -> LIO l b
-- | Write a ByteString to the given filepath with the supplied label.
writeFile :: (HandleOps Handle b IO, SLabel l) => l -> FilePath -> b -> LIO l ()
-- | Same as writeFile but uses privilege when opening, writing and
-- closing the file.
writeFileP :: (HandleOps Handle b IO, Priv l p, Serialize l) => p -> l -> FilePath -> b -> LIO l ()
-- | Get the contents of a directory. The current label is raised to the
-- join of the current label and that of all the directories traversed to
-- the leaf directory. Note that, unlike the standard Haskell
-- getDirectoryContents, we first normalise the path by collapsing
-- all the ..'s. The function uses unlabelFilePath when
-- raising the current label and thus may throw an exception if the
-- clearance is too low. Note: The current LIO filesystem does not
-- support links.
getDirectoryContents :: SMonadLIO l m => FilePath -> m [FilePath]
-- | Same as getDirectoryContents, but uses privileges when raising
-- the current label.
getDirectoryContentsP :: (SMonadLIO l m, Priv l p) => p -> FilePath -> m [FilePath]
-- | Create a directory at the supplied path with the given label. The
-- given label must be bounded by the the current label and clearance, as
-- checked by guardAlloc. The current label (after traversing the
-- filesystem to the directory path) must flow to the supplied label,
-- which must, in turn, flow to the current label as required by
-- guardWrite.
createDirectory :: SMonadLIO l m => l -> FilePath -> m ()
-- | Same as createDirectory, but uses privileges when raising the
-- current label and checking IFC restrictions.
createDirectoryP :: (SMonadLIO l m, Priv l p) => p -> l -> FilePath -> m ()
-- | Set the buffering mode
hSetBuffering :: SMonadLIO l m => LabeledHandle l -> BufferMode -> m ()
-- | Set the buffering mode
hSetBufferingP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> BufferMode -> m ()
-- | Get the buffering mode
hGetBuffering :: SMonadLIO l m => LabeledHandle l -> m BufferMode
-- | Get the buffering mode
hGetBufferingP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m BufferMode
-- | Select binary mode (True) or text mode (False)
hSetBinaryMode :: SMonadLIO l m => LabeledHandle l -> Bool -> m ()
-- | Select binary mode (True) or text mode (False)
hSetBinaryModeP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> Bool -> m ()
-- | End of file.
hIsEOF :: SMonadLIO l m => LabeledHandle l -> m Bool
-- | End of file.
hIsEOFP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool
-- | Is handle open.
hIsOpen :: SMonadLIO l m => LabeledHandle l -> m Bool
-- | Is handle open.
hIsOpenP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool
-- | Is handle closed.
hIsClosed :: SMonadLIO l m => LabeledHandle l -> m Bool
-- | Is handle closed.
hIsClosedP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool
-- | Is handle readable.
hIsReadable :: SMonadLIO l m => LabeledHandle l -> m Bool
-- | Is handle readable.
hIsReadableP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool
-- | Is handle writable.
hIsWritable :: SMonadLIO l m => LabeledHandle l -> m Bool
-- | Is handle writable.
hIsWritableP :: (SMonadLIO l m, Priv l p) => p -> LabeledHandle l -> m Bool
instance (SLabel l, HandleOps Handle b IO) => HandleOps (LabeledHandle l) b (LIO l)
instance HandleOps Handle ByteString IO
instance HandleOps Handle ByteString IO