LIO.Core

This module implements the core of the Labeled IO (LIO) information flow control (IFC) library. It provides a monad, LIO, that is intended to be used as a replacement for the IO monad in untrusted code. The idea is for untrusted code to provide a computation in the LIO monad, which trusted code can then safely execute through evalLIO and similar functions (e.g., evalDC in LIO.DCLabel).

Unlike IO, the LIO monad keeps track of a current label (accessible via the getLabel function) during each computation. The current label effectively tracks the sensitivity of all the data that the computation has observed. For example, if the computation has read a "secret" mutable reference (see LIO.LIORef) and then the result of a "top-secret" thread (see LIO.Concurrent) then the current label will be at least "top-secret". Labels are described in more detail in the documentation for LIO.Label, as well as the documentation for particular label formats (such as LIO.DCLabel).

The role of the current label is two-fold: First, the current label protects all pure values currently in scope. For example, the current label is the label on constants (such as 3 and "tis a string") as well as function arguments. More interestingly, consider reading a secret reference:

 val <- readLIORef secret

Though the label of secret may be "secret", val is not explicitly labeled. Hence, to protect the contents of the LIORef that has been read into val, the current label must be at least "secret" before returning from readLIORef. More generally, if the current label is l_cur, then it is only permissible to read data labeled l_r if l_r `canFlowTo` l_cur. Note that, instead of throwing an exception, reading data often just increases the current label to ensure that l_r `canFlowTo` l_cur. This is acomplished using a function such as taint.

The second purpose of the current label is to prevent inforation leaks into public channels. Specifically, it is only permissible to modify or write to data labeled l_w when l_cur`canFlowTo` l_w. Thus, the following attempt to leak the val after reading it from a secret LIORef would fail:

 writeLIORef public val

In addition to the current label, the LIO monad keeps a second label, the current clearance (accessible via the getClearance function). The clearance can be used to enforce a "need-to-know" policy, since it represents the highest value the current label can be raised to. In other words, if the current clearance is l_clear then the computation cannot create, read or write to objects labeled l such that (l `canFlowTo` l_clear) == False.

LIO monad

data LIO l a

The LIO monad is a wrapper around IO that keeps track of a current label and current clearance. Safe code cannot execute arbitrary IO actions from the LIO monad. However, trusted runtime functions can use ioTCB to perform IO actions (which they should only do after appropriately checking labels).

Instances

Typeable2 LIO

Label l => MonadLIO l (LIO l)

GuardIO l (IO r) (LIO l r)

LabelIO l (IO r) (LIO l r)

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r)

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r)

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r)

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r)

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r)

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r)

GuardIO l (a1 -> a2 -> a3 -> a4 -> IO r) (a1 -> a2 -> a3 -> a4 -> LIO l r)

GuardIO l (a1 -> a2 -> a3 -> IO r) (a1 -> a2 -> a3 -> LIO l r)

GuardIO l (a1 -> a2 -> IO r) (a1 -> a2 -> LIO l r)

GuardIO l (a1 -> IO r) (a1 -> LIO l r)

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r)

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r)

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r)

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r)

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r)

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r)

LabelIO l (a1 -> a2 -> a3 -> a4 -> IO r) (a1 -> a2 -> a3 -> a4 -> LIO l r)

LabelIO l (a1 -> a2 -> a3 -> IO r) (a1 -> a2 -> a3 -> LIO l r)

LabelIO l (a1 -> a2 -> IO r) (a1 -> a2 -> LIO l r)

LabelIO l (a1 -> IO r) (a1 -> LIO l r)

Monad (LIO l)

Functor (LIO l)

Applicative (LIO l)

class (Label l, Monad m) => MonadLIO l m | m -> l where

Synonym for monad in which LIO is the base monad.

Methods

liftLIO :: LIO l a -> m a

Lift an LIO computation.

Instances

Label l => MonadLIO l (LIO l)

Execute LIO actions

data LIOState l

Internal state of an LIO computation.

Constructors

LIOState

Fields

lioLabel :: !l

Current label.

lioClearance :: !l

Current clearance.

Instances

Eq l => Eq (LIOState l)

Read l => Read (LIOState l)

Show l => Show (LIOState l)

evalLIO :: LIO l a -> LIOState l -> IO 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.)

Unlike runLIO, this function throws an exception if the underlying LIO action terminates with an exception.

runLIO :: LIO l a -> LIOState l -> IO (a, LIOState l)

Execute an LIO action, returning its result and the final label state as a pair. Note that it returns a pair whether or not the LIO action throws an exception. Forcing the result value will re-throw the exception, but the label state will always be valid.

See also evalLIO.

Manipulating label state

getLabel :: Label l => LIO l l

Returns the value of the thread's current label.

setLabel :: Label l => l -> LIO l ()

Raises the current label to the provided label, which must be between the current label and clearance. See taint.

setLabelP :: PrivDesc l p => Priv p -> l -> LIO l ()

If the current label is oldLabel and the current clearance is clearance, this function allows code to raise the current label to any value newLabel such that canFlowToP priv oldLabel newLabel && canFlowTo newLabel clearance. (Note the privilege argument affects the label check, not the clearance check; call setClearanceP first to raise the clearance.)

Manipulating clearance

getClearance :: Label l => LIO l l

Returns the thread's current clearance.

setClearance :: Label l => l -> LIO l ()

Lowers the current clearance. The new clerance must be between the current label and previous current clerance. One cannot raise the current label or create object with labels higher than the current clearance.

setClearanceP :: PrivDesc l p => Priv p -> l -> LIO l ()

Raises the current clearance (undoing the effects of setClearance) by exercising privileges. If the current label is l and current clearance is c, then setClearanceP p cnew succeeds only if the new clearance is can flow to the current clearance (modulo privileges), i.e., canFlowToP p cnew c == True. Additionally, the current label must flow to the new clearance, i.e., l `canFlowTo` cnew == True.

Since LIO guards that are used when reading/writing data (e.g., guardAllocP) do not use privileges when comparing labels with the current clearance, code must always raise the current clearance, to read/write data above the current clearance.

scopeClearance :: Label l => LIO l a -> LIO l a

Runs an LIO action and re-sets the current clearance to its previous value once the action returns. In particular, if the action lowers the current clearance, the clearance will be restored upon return.

Note that scopeClearance always restores the clearance. If that causes the clearance to drop below the current label, a ClearanceViolation exception is thrown. That exception can only be caught outside a second scopeClearance that restores the clearance to higher than the current label.

withClearance :: Label l => l -> LIO l a -> LIO l a

Temporarily lowers the clearance for a computation, then restores it. Equivalent to:

 withClearance c lio = scopeClearance $ setClearance c >> lio

Note that if the computation inside withClearance acquires any Privs, it may still be able to raise its clearance above the supplied argument using setClearanceP.

withClearanceP :: PrivDesc l p => Priv p -> l -> LIO l a -> LIO l a

A variant of withClearance that takes privileges. Equivalent to:

 withClearanceP p c lio = scopeClearance $ setClearanceP p c >> lio

Exceptions thrown by LIO

data AnyLabelError

Parent of all label-related exceptions.

Constructors

forall e . (Exception e, Annotatable e) => AnyLabelError e

Instances

Show AnyLabelError

Typeable AnyLabelError

Exception AnyLabelError

Annotatable AnyLabelError

data LabelError l

Main error type thrown by label failures in the LIO monad.

Constructors

LabelError

Fields

lerrContext :: [String]

Annotation of where the failure happened.

lerrFailure :: String

Actual function that failed.

lerrCurLabel :: l

Current label at time of error.

lerrCurClearance :: l

Current clearance at time of error.

lerrPrivs :: [GenericPrivDesc l]

Any privileges involved in error.

lerrLabels :: [l]

Any labels involved in error.

Instances

Typeable1 LabelError

Show l => Show (LabelError l)

Label l => Exception (LabelError l)

Annotatable (LabelError l)

data InsufficientPrivs

Error indicating insufficient privileges (independent of the current label). This exception is thrown by delegate, and should also be thrown by gates that receive insufficient privilege descriptions (see LIO.Delegate).

Constructors

forall p . SpeaksFor p => InsufficientPrivs

Fields

inspContext :: [String]

inspFailure :: String

inspSupplied :: p

inspNeeded :: p

Instances

Show InsufficientPrivs

Typeable InsufficientPrivs

Exception InsufficientPrivs

Annotatable InsufficientPrivs

Guards

Guards are used by (usually privileged) code to check that the invoking, unprivileged code has access to particular data. If the current label is lcurrent and the current clearance is ccurrent, then the following checks should be performed when accessing data labeled ldata:

• When reading an object labeled ldata, it must be the case that ldata `canFlowTo` lcurrent. This check is performed by the taint function, so named because it "taints" the current LIO context by raising lcurrent until ldata `canFlowTo` lcurrent. Specifically, it does this by computing the least upper bound or lub of the two labels. (Note taint will fail if the new label cannot flow to the current clearance.)
• When creating or allocating objects, it is permissible for them to be higher than the current label, so long as they are below the current clearance. In other words, it must be the case that lcurrent `canFlowTo` ldata && ldata `canFlowTo` ccurrent. This is ensured by the guardAlloc function.
• When writing an object, it should be the case that lcurrent `canFlowTo` ldata && ldata `canFlowTo` lcurrent. (As stated, this is the same as saying ldata == lcurrent, but the two are different when using canFlowToP instead of canFlowTo.) This is ensured by the guardWrite function, which does the equivalent of taint to ensure the target label ldata can flow to the current label, then throws an exception if lcurrent cannot flow back to the target label.

Note that a write always implies a read. Hence, when writing to an object for which you can observe the result (which is frequently the case), you must use guardWrite. However, when performing a write for which there are no observable side-effects to the writer, i.e., you cannot observe the success or failure of the write, then it is safe to use guardAlloc.

The taintP, guardAllocP, and guardWriteP functions are variants of the above that take privilege to be more permissive and raise the current label less.

Allocate/write-only guards

guardAlloc :: Label l => l -> LIO l ()

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.

guardAllocP :: PrivDesc l p => Priv p -> l -> LIO l ()

Like guardAlloc, but takes a privilege argument to be more permissive. Note: privileges are only used when checking that the current label can flow to the target label; guardAllocP still always throws an exception when the target label is higher than the current clearance.

Read-only guards

taint :: Label l => l -> LIO l ()

Use taint l in trusted code before observing an object labeled l. This will raise the current label to a value l' such that l `canFlowTo` l', or throw a LabelError exception if l' would have to be higher than the current clearance.

taintP :: PrivDesc l p => Priv p -> l -> LIO l ()

Like taint, but use privileges to reduce the amount of taint required. Note that taintP will never lower the current label. It simply uses privileges to avoid raising the label as high as taint would raise it.

Read-write guards

guardWrite :: Label l => l -> LIO l ()

Use guardWrite l in any (trusted) code before modifying an object labeled l, for which the modification can be observed, i.e., the write implies a read.

The implementation of guardWrite is straight forward:

 guardWrite l = guardAlloc l >> taint l

This guarantees that l `canFlowTo` the current label (and clearance), and that the current label `canFlowTo` l.

guardWriteP :: PrivDesc l p => Priv p -> l -> LIO l ()

Like guardWrite, but takes a privilege argument to be more permissive.