lio-0.1.1: Labeled IO Information Flow Control Library

LIO.Safe

Description

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.

Synopsis

Documentation

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

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 :: 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

leq :: a -> a -> BoolSource

Can-flow-to relation

Instances

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

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 -> BoolSource

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.

lostarSource

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

data NoPrivs Source

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

Constructors

NoPrivs 

data LIO l p s a Source

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 -> pSource

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

evalLIOSource

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 lSource

Returns the current value of the thread's label.

setLabelP :: LabelState l p s => p -> l -> LIO l p 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 :: LabelState l p s => LIO l p s lSource

Returns the current value of the thread's clearance.

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

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 ()Source

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

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

Returns label of a Labeled type.

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

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)Source

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 aSource

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

taintLabeled :: LabelState l p s => l -> Labeled l a -> LIO l p 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 clearance, though the resulting label may not be if the Labeled is already above the current thread's clearance.

toLabeled :: LabelState l p s => l -> LIO l p s a -> LIO l p 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 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.

WARNING: 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)Source

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

WARNING: toLabeledP is susceptible to termination attacks.

discard :: LabelState l p s => l -> LIO l p s a -> LIO l p 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.)

WARNING: discard is susceptible to termination attacks.

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

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 ()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.

taintPSource

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

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

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

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

data Labeled l t Source

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 Source

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

catchPSource

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 receives an extra first argument (before the exception), which is the label when the exception was thrown.

handlePSource

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.

onExceptionPSource

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.

bracketPSource

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 aSource

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.