LIO.Base

Description

This file 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.

Synopsis

Documentation

data POrdering Source

Constructors

PEQ	Equal
PLT	Less than
PGT	Greater than
PNE	Incomparable (neither less than nor greater than)

Instances

Eq POrdering
Ord POrdering
Show POrdering
Monoid POrdering

class Eq a => POrd a whereSource

Methods

pcompare :: a -> a -> POrdering Source

leq :: a -> a -> Bool Source

Instances

POrd DCLabel
POrd HSLabel
POrd HSLevel

o2po :: Ordering -> POrdering Source

class (POrd a, Show a, Read a, Typeable a) => Label a whereSource

Methods

lbot :: aSource

bottom

ltop :: aSource

top

lub :: a -> a -> aSource

least upper bound (join) of two labels

glb :: a -> a -> aSource

greatest lower bound (meet) of two labels

Instances

Label DCLabel
Label HSLabel

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

Methods

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

leqp p l1 l2 means that privileges p are sufficient to downgrade data from l1 to l2. Note that leq l1 l2 implies leq p l1 l2 for all p, but for some labels and privileges, leqp will hold even where leq does not.

lostar Source

Arguments

:: p	Privileges
-> l	Label from which data must flow
-> l	Goal label
-> l	Result

Roughly speaking, the function

 result = lostar p label goal

computes how close one can come to downgrading data labeled label to goal given privileges p. When p == NoPrivs, result == lub label goal. If p contains all possible privileges, then result == goal.

More specifically, result is the greatest lower bound of the set of all labels r satisfying:

leq goal r, and
```
leqp p label r
```

Operationally, lostar captures the minimum change required to the current label when viewing data labeled label. A common pattern is to use the result of getLabel as goal (i.e., the goal is to use privileges p to avoid changing the label at all), and then compute result 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

Label l => Priv l NoPrivs
Priv DCLabel TCBPriv
Priv HSLabel HSPrivs

data NoPrivs Source

A generic Priv instance that works for all Labels and confers no downgrading privileges.

Constructors

NoPrivs

Instances

Monoid NoPrivs
PrivTCB NoPrivs
Label l => Priv l NoPrivs

data Label l => LIO l s a Source

Instances

Label l => MonadError IOException (LIO l s)
Monad (LIO l s)
Functor (LIO l s)
MonadFix (LIO l s)
Label l => MonadCatch (LIO l s)
Label l => OnExceptionTCB (LIO l s)
Label l => MonadLIO (LIO l s) l s
(Label l, CloseOps (LHandle l h) (LIO l s), HandleOps h b IO) => HandleOps (LHandle l h) b (LIO l s)
Label l => CloseOps (LHandle l Handle) (LIO l s)
Label l => DirectoryOps (LHandle l Handle) (LIO l s)

getLabel :: Label l => LIO l s lSource

Returns the current value of the thread's label.

setLabelP :: Priv l p => p -> l -> LIO l s ()Source

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 :: Label l => LIO l s lSource

Returns the current value of the thread's clearance.

lowerClr :: Label l => l -> LIO l s ()Source

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

lowerClrP :: Priv l p => p -> l -> LIO l s ()Source

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

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

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.

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

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 Source

Arguments

:: Priv l p
=> p	Privileges to invoke
-> l	Label to taint to if no privileges
-> LIO l 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 :: Label l => l -> LIO l s ()Source

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 :: Priv l p => p -> l -> LIO l s ()Source

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

aguard :: Label l => l -> LIO l s ()Source

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 :: Priv l p => p -> l -> LIO l s ()Source

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

data Label l => Labeled l t Source

Labeled is a type representing labeled data.

Instances

Label l => Functor (Labeled l)	To make programming easier with labeled values, we provide a functor instance definition.
(Label l, Read l, Read a) => ReadTCB (Labeled l a)
(Label l, Show a) => ShowTCB (Labeled l a)

label :: Label l => l -> a -> LIO l s (Labeled l a)Source

Function to construct an 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 :: Priv l p => p -> l -> a -> LIO l s (Labeled l a)Source

Constructs an 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 :: Label l => Labeled l a -> LIO l s aSource

Within the LIO monad, this function takes an 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 suceed without throwing an exception.

unlabelP :: Priv l p => p -> Labeled l a -> LIO l s aSource

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.

toLabeled :: Label l => l -> LIO l s a -> LIO l s (Labeled l a)Source

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. Thus, 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 suggestst 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 occured in the computation producing the value of the Labeled. This higlights one main use of clearance: to ensure that a Labeled computed does not exceed a particular label.

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

discard :: Label l => l -> LIO l s a -> LIO l s ()Source

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. (Of course, if log_handle is closed and this throws an exception, it may not be possible to catch the exception within the LIO monad without sufficient privileges--see catchP.)

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

Returns label of a Label type.

taintLabeled :: Label l => l -> Labeled l a -> LIO l s (Labeled l a)Source

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 clarance, though the resulting label may not be if the Labeled is already above the current thread's clearance.

data LabelFault Source

Constructors

LerrLow	Requested label too low
LerrHigh	Current label too high
LerrClearance	Label would exceed clearance
LerrPriv	Insufficient privileges
LerrInval	Invalid request

Instances

Show LabelFault
Typeable LabelFault
Exception LabelFault

catchP Source

Arguments

:: (Label l, Exception e, Priv l p)
=> p	Privileges with which to downgrade exception
-> LIO l s a	Computation to run
-> (l -> e -> LIO l s a)	Exception handler
-> LIO l 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 receives an an extra first argument (before the exception), which is the label when the exception was thrown.

onExceptionP Source

Arguments

:: Priv l p
=> p	Privileges to downgrade exception
-> LIO l s a	The computation to run
-> LIO l s b	Handler to run on exception
-> LIO l 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 :: Priv l p => p -> LIO l s a -> (a -> LIO l s c) -> (a -> LIO l s b) -> LIO l s bSource

Like standard bracket, but with privileges to downgrade exception.

handleP Source

Arguments

:: (Label l, Exception e, Priv l p)
=> p	Privileges with which to downgrade exception
-> (l -> e -> LIO l s a)	Exception handler
-> LIO l s a	Computation to run
-> LIO l s a	Result of computation or handler

Version of catchP with arguments swapped.

evaluate :: Label l => a -> LIO l s aSource

Evaluate in LIO.

evalLIO Source

Arguments

:: Label l
=> LIO l 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.)