lio- Labeled IO Information Flow Control Library

Safe HaskellTrustworthy




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.



data Principal Source

A Principal is a simple string representing a source of authority. Any piece of code can create principals, regardless of how untrusted it is.

principal :: S8 -> PrincipalSource

Principal constructor.


data Clause Source

A clause or disjunction category is a set of Principals. Logically the set corresponds to a disjunction of the principals.

clause :: Set Principal -> ClauseSource

Clause constructor


data Component Source

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.


dcTrue :: ComponentSource

Logical True.

dcFalse :: ComponentSource

Logical False.

dcFormula :: Set Clause -> ComponentSource

Arbitrary formula from a clause.

isTrue :: Component -> BoolSource

Is the component True.

isFalse :: Component -> BoolSource

Is the component False.


data DCLabel Source

A DCLabel is a pair of secrecy and integrity Components.


Eq DCLabel 
Show DCLabel 
Typeable DCLabel 
Serialize DCLabel

Serialize labels by converting them to pairs of components.

Label DCLabel 
LabeledFunctor DCLabel 
Priv DCLabel DCPriv 

dcSecrecy :: DCLabel -> ComponentSource

Extract secrecy component of a label

dcIntegrity :: DCLabel -> ComponentSource

Extract integrity component of a label

dcLabel :: Component -> Component -> DCLabelSource

Label constructor. Note that each component is first reduced to CNF.

dcPub :: DCLabelSource

Element in the DCLabel lattice corresponding to public data. dcPub = < True, True > . This corresponds to data that is not secret nor trustworthy.



Synonyms for LIO

The DC monad is LIO with using DCLabels as the label format. Most application should be written in terms of this monad, while most libraries should remain polymorphic in the label type. It is important that any *real* application set the initial current label and clearance to values other than bottom and top as set by defaultState, respectively. In most cases the initial current label should be public, i.e., dcPub.

type DCState = LIOState DCLabelSource

LIOState with underlying label being DCLabel

defaultState :: DCStateSource

Default, starting state for a DC computation. The current label is public (i.e., dcPub) and the current clearance is top.

type DC = LIO DCLabelSource

The monad for LIO computations using DCLabel as the label.

evalDC :: DC a -> IO aSource

Evaluate computation in the DC monad.

runDC :: DC a -> IO (a, DCState)Source

Evaluate computation in the DC monad.

tryDC :: DC a -> IO (Either DCLabeledException a, DCState)Source

Similar to evalLIO, but catches any exceptions thrown by untrusted code with throwLIO.

paranoidDC :: DC a -> IO (Either SomeException (a, DCState))Source

Similar to evalLIO, but catches all exceptions.

type MonadDC m = MonadLIO DCLabel mSource

Type synonym for MonadLIO.


type DCLabeledException = LabeledException DCLabelSource

DC Labeled exceptions.

Labeled values

Labeled references

type DCRef = LIORef DCLabelSource

DC Labeled LIORefs.