LIO.Safe

This module exports the subset of symbols in the LIO.TCB module that are safe for untrusted code to access. See the LIO.TCB module for documentation.

Documentation

class (Eq a, Show a, Read a, Typeable a) => Label a where

This class defines a label format, corresponding to a bounded lattice. Specifically, it is necessary to define a bottom element lbot (in literature, written as ⊥), a top element ltop (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 leq (in literature, written as ⊑).

Methods

lbot :: a

Bottom

ltop :: a

Top

lub :: a -> a -> a

Least upper bound (join) of two labels

glb :: a -> a -> a

Greatest lower bound (meet) of two labels

leq :: a -> a -> Bool

Can-flow-to relation

Instances

Label DCLabel

class (Label l, Monoid p, PrivTCB p) => Priv l p where

This class defines privileges and the more-permissive relation (leqp) on labels using privileges. Additionally, it defines lostar which is used to compute the smallest difference between two labels given a set of privilege.

Methods

leqp :: p -> l -> l -> Bool

The "can-flow-to given privileges" pre-order used to compare two labels in the presence of privileges. If leqp p L_1 L_2 holds, then privileges p are sufficient to downgrade data from L_1 to L_2. Note that leq L_1 L_2 implies leq p L_1 L_2 for all p, but for some labels and privileges, leqp will hold even where leq does not.

lostar

Arguments

:: p

Privileges

-> l

Label from which data must flow

-> l

Goal label

-> l

Result

Roughly speaking, L_r = lostar p L L_g computes how close one can come to downgrading data labeled L to the goal label L_g, given privileges p. When p == noPrivs, the resulting label L_r == L `lub`L_g. If p contains all possible privileges, then L_r == L_g.

More specifically, L_r is the greatest lower bound of the set of all labels L_l satisfying:

1. L_g ⊑ L_l, and
2. L ⊑ₚ L_l.

Operationally, lostar captures the minimum change required to the current label when viewing data labeled L_l. A common pattern is to use the result of getLabel as L_g (i.e., the goal is to use privileges p to avoid changing the label at all), and then compute L_r based on the label of data the code is about to observe. For example, taintP could be implemented as:

    taintP p l = do lcurrent <- getLabel
                    taint (lostar p l lcurrent)

Instances

Priv DCLabel TCBPriv

noPrivs :: Monoid p => p

Alias for mempty.

getPrivileges :: LabelState l p s => LIO l p s p

Returns the current privileges.

withPrivileges :: LabelState l p s => p -> LIO l p s a -> LIO l p s a

Execute an LIO action with a set of underlying privileges. Within a withPrivileges block, the supplied privileges are used in every even (non ...P) operation. For instance,

  unlabelP p x

can instead be written as:

  withPrivileges p $ unlabel x

The original privileges of the thread are restored after the action is executed within the withPrivileges block. The withPrivileges combinator provides a middle-ground between a fully explicit, but safe, privilege use (...P combinators), and an implicit, but less safe, interface (provide getter/setter, and always use underlying privileges). It allows for the use of implicit privileges by explicitly enclosing the code with a withPrivileges block.

withCombinedPrivs :: LabelState l p s => p -> (p -> LIO l p s a) -> LIO l p s a

Execute an LIO action with the combination of the supplied privileges (usually passed to ...P functions) and current privileges.

dropPrivileges :: LabelState l p s => LIO l p s ()

Drop all privileges. It is useful to remove all privileges when executing some untrusted code withing a withPrivileges block.

data LIO l p s a

LIO monad is a State monad transformer with IO as the underlying monad.

Instances

LabelState l p s => MonadError IOException (LIO l p s)

(LabelState l p s, CloseOps (LHandle l) (LIO l p s), HandleOps Handle b IO) => HandleOps (LHandle l) b (LIO l p s)

LabelState l p s => CloseOps (LHandle l) (LIO l p s)

(Serialize l, LabelState l p s) => DirectoryOps (LHandle l) (LIO l p s)

Monad (LIO l p s)

Functor (LIO l p s)

Applicative (LIO l p s)

LabelState l p s => MonadCatch (LIO l p s)

LabelState l p s => OnExceptionTCB (LIO l p s)

LabelState l p s => MonadLIO (LIO l p s) l p s

class (Priv l p, Label l) => LabelState l p s | l -> s, l -> p

Empty class used to specify the functional dependency between a label and it state.

Instances

LabelState DCLabel DCPrivTCB ()

evalLIO

Arguments

:: LabelState l p s

=> LIO l p s a

The LIO computation to execute

-> s

Initial value of label-specific state

-> IO (a, l)

IO computation that will execute first argument

Produces an IO computation that will execute a particular 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--it just can't execute them without access to ioTCB.)

getLabel :: LabelState l p s => LIO l p s l

Returns the current value of the thread's label.

setLabelP :: LabelState l p s => p -> l -> LIO l p s ()

If the current label is oldLabel and the current clearance is clearance, this function allows code to raise the label to any value newLabel such that oldLabel `leq` newLabel && newLabel `leq` clearance. Note that there is no setLabel variant without the ...P because the taint function provides essentially the same functionality that setLabel would.

getClearance :: LabelState l p s => LIO l p s l

Returns the current value of the thread's clearance.

lowerClr :: LabelState l p s => l -> LIO l p s ()

Reduce the current clearance. One cannot raise the current label or create object with labels higher than the current clearance.

lowerClrP :: LabelState l p s => p -> l -> LIO l p s ()

Raise the current clearance (undoing the effects of lowerClr). This requires privileges.

withClearance :: LabelState l p s => l -> LIO l p s a -> LIO l p s a

Lowers the clearance of a computation, then restores the clearance to its previous value. Useful to wrap around a computation if you want to be sure you can catch exceptions thrown by it. Also useful to wrap around toLabeled to ensure that the computation does not access data exceeding a particular label. If withClearance is given a label that can't flow to the current clearance, then the clearance is lowered to the greatest lower bound of the label supplied and the current clearance.

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

labelOf :: Label l => Labeled l a -> l

Returns label of a Labeled type.

label :: LabelState l p s => l -> a -> LIO l p s (Labeled l a)

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 `leq` l && l `leq` ccurrent.

labelP :: LabelState l p s => p -> l -> a -> LIO l p s (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 (leqp p lcurrent l) && l `leq` ccurrent. Note that privilege is not used to bypass the clearance. You must use lowerClrP to raise the clearance first if you wish to create an Labeled at a higher label than the current clearance.

unlabel :: LabelState l p s => Labeled l a -> LIO l p s a

Within the LIO monad, this function takes a Labeled and returns the 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, 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 LerrClearance. However, you can use labelOf to check if unlabel will succeed without throwing an exception.

unlabelP :: LabelState l p s => p -> Labeled l a -> LIO l p s 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. Will still throw LerrClearance under the same circumstances as unlabel.

taintLabeled :: LabelState l p s => l -> Labeled l a -> LIO l p s (Labeled l a)

Raises the label of a Labeled to the lub of it's current label and the value supplied. The label supplied must be less than the current clearance, though the resulting label may not be if the Labeled is already above the current thread's clearance.

untaintLabeled :: LabelState l p s => l -> Labeled l a -> LIO l p s (Labeled l a)

Downgrades the label of a Labeled as much as possible given the current privilege.

untaintLabeledP :: LabelState l p s => p -> l -> Labeled l a -> LIO l p s (Labeled l a)

Same as untaintLabeled but combines the current privilege with the supplied privilege when downgrading the label.

relabelP :: LabelState l p s => p -> l -> Labeled l a -> LIO l p s (Labeled l a)

Relabeles a Labeled value if the given privilege combined with the current privileges permits it.

toLabeled

Arguments

:: LabelState l p s

=> l

Label of result and upper bound on inner-computations' observation

-> LIO l p s a

Inner computation

-> LIO l p s (Labeled l a)

toLabeled is the dual of unlabel. It allows one to invoke computations that would raise the current label, but without actually raising the label. Instead, the result of the computation is packaged into a Labeled with a supplied label. (Of couse, the computation executed by toLabeled must most observe any data whose label exceeds the supplied label.)

To get at the result of the computation one will have to call unlabel and raise the label, but this can be postponed, or done inside some other call to toLabeled. This suggests that the provided label must be above the current label and below the current clearance.

Note that toLabeled always restores the clearance to whatever it was when it was invoked, regardless of what occurred in the computation producing the value of the Labeled. This highlights one main use of clearance: to ensure that a Labeled computed does not exceed a particular label.

If an exception is thrown within a toLabeled block, such that the outer context is withing a catch, which is futher within a toLabeled block, infromation can be leaked. Consider the following program that uses DCLabels. (Note that discard is simply toLabeled that throws throws the result away.)

 main = evalDC' $ do
   lRef <- newLIORef lbot ""
   hRef <- newLIORef ltop "secret" 
   -- brute force:
   forM_ ["fun", "secret"] $ \guess -> do
     stash <- readLIORef lRef
     writeLIORef lRef $ stash ++ "\n" ++ guess ++ ":"
     discard ltop $ do 
       catch ( discard ltop $ do
                 secret <- readLIORef hRef
                 when (secret == guess) $ throwIO . userError $ "got it!"
             ) (\(e :: IOError) -> return ())
       l <- getLabel
       when (l == lbot) $ do stash <- readLIORef lRef
                             writeLIORef lRef $ stash ++ "no!"
   readLIORef lRef
     where evalDC' act = do (r,l) <- evalDC act
                            putStrLn r
                            putStrLn $ "label = " ++ prettyShow l

The output of the program is:

 $ ./new
 
 fun:no!
 secret:
 label = <True , False>

Note that the current label is lbot (which in DCLabels is True , False), and the secret is leaked. The fundamental issue is that the outer discard allows for the current label to remain low even though the catch raised the current label when the secret was found (and thus exception was throw). As a consequence, toLabeled catches all exceptions, and returns a Labeled value that may have a labeled exception as wrapped by throw. All exceptions within the outer computation, including IFC violation attempts, are essentially rethrown when performing an unlabel.

DEPRECATED: toLabeled is susceptible to termination attacks.

toLabeledP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s (Labeled l a)

Same as toLabeled but allows one to supply a privilege object when comparing the initial and final label of the computation.

DEPRECATED: toLabeledP is susceptible to termination attacks.

discard :: LabelState l p s => l -> LIO l p s a -> LIO l p s ()

Executes a computation that would raise the current label, but discards the result so as to keep the label the same. Used when one only cares about the side effects of a computation. For instance, if log_handle is an LHandle with a high label, one can execute

   discard ltop $ hputStrLn log_handle "Log message"

to create a log message without affecting the current label.

DEPRECATED: discard is susceptible to termination attacks.

discardP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s ()

Same as discard, but uses privileges when comparing initial and final label of the computation.

taint :: LabelState l p s => l -> LIO l p s ()

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 `leq` l', or throw LerrClearance if l' would have to be higher than the current clearance.

taintP

Arguments

:: LabelState l p s

=> p

Privileges to invoke

-> l

Label to taint to if no privileges

-> LIO l p s ()

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

wguard :: LabelState l p s => l -> LIO l p s ()

Use wguard l in trusted code before modifying an object labeled l. If l' is the current label, then this function ensures that l' `leq` l before doing the same thing as taint l. Throws LerrHigh if the current label l' is too high.

wguardP :: LabelState l p s => p -> l -> LIO l p s ()

Like wguard, but takes privilege argument to be more permissive.

aguard :: LabelState l p s => l -> LIO l p s ()

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 aguard l does not throw an exception.

aguardP :: LabelState l p s => p -> l -> LIO l p s ()

Like aguardP, but takes privilege argument to be more permissive.

data Labeled l t

Labeled is a type representing labeled data.

Instances

Typeable2 Labeled

(Label l, Read l, Read a) => ReadTCB (Labeled l a)

(Label l, Show a) => ShowTCB (Labeled l a)

data LabelFault

Violation of information flow conditions, or label checks should throw exceptions of type LabelFault. The LerrInval constructor takes a string parameter -- it is important that trusted code use this carefully and aovid leaking information through it.

Constructors

LerrLow

Requested label too low

LerrHigh

Current label too high

LerrClearance

Label would exceed clearance

LerrPriv

Insufficient privileges

LerrInval String

Invalid request

Instances

Show LabelFault

Typeable LabelFault

Exception LabelFault

catchP

Arguments

:: (Exception e, LabelState l p s)

=> p

Privileges with which to downgrade exception

-> LIO l p s a

Computation to run

-> (e -> LIO l p s a)

Exception handler

-> LIO l p s a

Result of computation or handler

Catches an exception, so long as the label at the point where the exception was thrown can flow to the label at which catchP is invoked, modulo the privileges specified. Note that the handler raises the current label to the joint of the current label and exception label.

handleP

Arguments

:: (Exception e, LabelState l p s)

=> p

Privileges with which to downgrade exception

-> (e -> LIO l p s a)

Exception handler

-> LIO l p s a

Computation to run

-> LIO l p s a

Result of computation or handler

Version of catchP with arguments swapped.

onExceptionP

Arguments

:: LabelState l p s

=> p

Privileges to downgrade exception

-> LIO l p s a

The computation to run

-> LIO l p s b

Handler to run on exception

-> LIO l p s a

Result if no exception thrown

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 raised label.

bracketP

Arguments

:: LabelState l p s

=> p

Priviliges used to downgrade

-> LIO l p s a

Computation to run first

-> (a -> LIO l p s c)

Computation to run last

-> (a -> LIO l p s b)

Computation to run in-between

-> LIO l p s b

Like standard bracket, but with privileges to downgrade exception.

evaluate :: LabelState l p s => a -> LIO l p s a

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.

class (PrivTCB p, Show d) => PrivDesc p d | p -> d

Class used to describe privileges in a meaningful manner.

Instances

PrivDesc DCPrivTCB DCPriv

data Gate l d a

A Gate is a wrapper for a Labeled type.

Instances

Typeable3 Gate

mkGate

Arguments

:: (LabelState l p s, PrivDesc p d)

=> l

Label of gate

-> (d -> a)

Gate omputation

-> LIO l p s (Gate l d a)

Create a gate given a gate label and computation. The label of the gate must be bounded by the current label and clearance.

mkGateP

Arguments

:: (LabelState l p s, PrivDesc p d)

=> p

Privileges

-> l

Label of gate

-> (d -> a)

Gate computation

-> LIO l p s (Gate l d a)

Same as mkGate, but uses privileges when making the gate.

callGate

Arguments

:: (LabelState l p s, PrivDesc p d)

=> Gate l d a

Gate

-> p

Privilege used to unlabel gate action

-> LIO l p s a

Given a labeled gate and privilege, execute the gate computation. The current label is raised to the join of the gate and current label, clearance permitting. It is important to note that callGate invokes the gate computation with the privilege description and not the actual privilege.