lio-0.1.3: Labeled IO Information Flow Control Library

Safe HaskellUnsafe

LIO.TCB

Contents

Description

This module implements the core of the Labeled IO library for information flow control in Haskell. 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 the evalLIO function. (Though usually a wrapper function is employed depending on the type of labels used by an application. For example, with LIO.DCLabel, you would use evalDC to execute an untrusted computation. There are also abbreviations for the LIO monad type of a particular label--for instance DC.)

A data structure Labeled (labeled value) protects access to pure values. Without the appropriate privileges, one cannot produce a pure value that depends on a secret Labeled, or conversely produce a high-integrity Labeled based on pure data. The function toLabeled allows one to seal off the results of an LIO computation inside an Labeled without tainting the current flow of execution. unlabel conversely allows one to use the value stored within a Labeled.

We note that using toLabeled is not safe with respect to the termination covert channel. Specifically, LIO with toLabeled is only termination-insensitive non-interfering. For a termination-sensitive toLabeled-like function, see LIO.Concurrent.

Any code that imports this module is part of the Trusted Computing Base (TCB) of the system. Hence, untrusted code must be prevented from importing this module. The exported symbols ending ...TCB can be used to violate label protections even from within pure code or the LIO Monad. A safe subset of these symbols is exported by the LIO.Safe module, which is how untrusted code should access the core label functionality. (LIO.Safe is also re-exported by LIO, the main gateway to this library.)

Synopsis

Basic Label Functions

Labels are a way of describing who can observe and modify data. There is a partial order, generally pronounced "can flow to" on labels. In Haskell we write this partial order `leq` (in the literature it is usually written as ⊑).

The idea is that data labeled L_1 should affect data labeled L_2 only if L_1 `leq` L_2, (i.e., L_1 can flow to L_2). The LIO monad keeps track of the current label of the executing code (accessible via the getLabel function). Code may attempt to perform various IO or memory operations on labeled data. Touching data may change the current label (or throw an exception if an operation would violate can-flow-to restrictions).

If the current label is L_cur, then it is only permissible to read data labeled L_r if L_r `leq` L_cur. This is sometimes termed "no read up" in the literature; however, because the partial order allows for incomparable labels (i.e., two labels L_1 and L_2 such that not (L_1 `leq` L_2) && not (L_2 `leq` L_1)), a more appropriate phrasing would be "read only what can flow to your label". Note that, rather than throw an exception, reading data will often just increase the current label to ensure that L_r `leq` L_cur. The LIO monad keeps a second label, called the clearance (see getClearance), that represents the highest value the current thread can raise its label to. The purpose of clearance is to enforce of discretionary access control: you can set the clearance to a label L_clear as to prevent a piece of LIO code from reading anything above L_clear.

Conversely, it is only permissible to modify data labeled L_w when L_cur`leq` L_w, a property often cited as "no write down", but more accurately characterized as "write only what you can flow to". In practice, there are very few IO abstractions (namely, mutable references) in which it is possible to do a pure write that doesn't also involve observing some state. For instance, writing to a file handle and not getting an exception tells you that the handle is not closed. Thus, in practice, the requirement for modifying data labeled L_w is almost always that L_cur == L_w.

Note that higher labels are neither more nor less privileged than lower ones. Simply, the higher one's label is, the more things one can read. Conversely, the lower one's label, the more things one can write. But, because labels are a partial and not a total order, some data may be completely inaccessible to a particular computation; for instance, if the current label is L_cur, the current clearance is C_cur, and some data is labeled Ld_, such that not (L_cur `leq` L_d || L_d `leq` C_cur), then the current thread can neither read nor write the data, at least without invoking some privilege.

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

Basic Privilige Functions

Privilege comes from a separate class called Priv, representing the ability to bypass the protection of certain labels. Essentially, privilege allows you to behave as if L_1 `leq` L_2 even when that is not the case. The process of making data labeled L_1 affect data labeled L_2 when not (L_1 `leq` L_2) is called downgrading.

The basic method of the Priv object is leqp, which performs the more permissive can-flow-to check in the presence of particular privileges (in literature this relation is a pre-order, commonly written as ⊑ₚ). Many LIO operations have variants ending ...P that take a privilege argument to act in a more permissive way. It is also possible to execute an LIO action with a set of privileges (without explicitly using the ...P combinators) using the withPrivileges combinator. Practicing the /principle of least privilege/, it is recommended that withPrivileges only be used in small blocks of code in which many operations require the same privileges. It is safer to use ...P operators and privileges explicitly.

All Priv types are monoids, and so can be combined with mappend. How to create Priv objects is specific to the particular label type in use. The method used is mintTCB, but the arguments depend on the particular label type. (Of course, the symbol mintTCB must not be available to untrusted code.)

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

noPrivs :: Monoid p => pSource

Alias for mempty.

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

Returns the current privileges.

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

Set the underlying privileges. Although this function is not unsafe, it is not exported by LIO.Safe as it provides a higher security risk. Users are encouraged to use withPrivileges.

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

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 aSource

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

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

Labeled IO Monad (LIO)

The LIO monad is a wrapper around IO that keeps track of the current label and clearance. It is possible to raise one's label or lower one's clearance without privilege, but moving in the other direction requires appropriate privilege. The LIO monad also keeps track of a set of privileges, used within a withPrivileges block.

LIO is parameterized by three types. The first is the particular label type. The second type is the type of underlying privileges. The third type is state specific to and functionally determined by the label type. Trusted label implementation code can use getTCB and putTCB to get and set the label state.

newtype LIO l p s a Source

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

Constructors

LIO (StateT (LIOstate l p s) IO a) 

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

runLIO :: forall l p s a. LabelState l p s => LIO l p s a -> LIOstate l p s -> IO (a, LIOstate l p s)Source

Execute an LIO action. The label on exceptions are removed. See evalLIO.

newState :: LabelState l p s => s -> LIOstate l p sSource

Generate a fresh state to pass runLIO when invoking it for the first time. The current label is set to lbot, the current clearance is set to ltop, and the current privileges are set to none.

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.

Labeled Values

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) 

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.

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

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

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

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

toLabeledSource

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

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

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

LIO Guards

Guards are used by 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 `leq` lcurrent. This check is performed by the taint function, so named becuase it "taints" the current LIO context by raising lcurrent until ldata `leq` lcurrent. (Specifically, it does this by computing the least upper bound of the two labels with the lub method of the Label class.) However, if after doing this it would be the case that not (lcurrent `leq` ccurrent), then taint throws exception LerrClearance rather than raising the current label.
  • When writing an object, it should be the case that ldata `leq` lcurrent && lcurrent `leq` ldata. (As stated, this is the same as saying ldata == lcurrent, but the two are different when using leqp instead of leq.) This is ensured by the wguard (write guard) 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.
  • When creating or allocating objects, it is permissible for them to be higher than the current label, so long as they are bellow the current clearance. In other words, it must be the case that lcurrent `leq` ldata && ldata `leq` ccurrent. This is ensured by the aguard (allocation guard) function.

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

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.

Labeled Exceptions

LIO throws LabelFault exceptions when an information flow violation is to occur. In general, such exceptions are handled in the outer, trusted IO code block that executes untrusted LIO code. However, it is sometimes desirable for untrusted code to throw exceptions. To this end we provide an implementation of labeled exceptions, as "normal" exceptions are unsafe and can be used to leak information. We describe the interface below.

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

Throwing and Catching Labeled Exceptions

We must re-define the throwIO and catch functions to work in the LIO monad. A complication is that exceptions could potentially leak information. For instance, within a block of code wrapped by discard, one might examine a secret bit, and throw an exception when the bit is 1 but not 0. Allowing untrusted code to catch the exception leaks the bit.

The solution is to wrap exceptions up with a label. The exception may be caught, but only if the label of the exception can flow to the label at the point the catch statement began execution. For compatibility, the throwIO, catch, and onException functions are now methods that work in both the IO or LIO monad.

If an exception is uncaught in the LIO monad, the evalLIO function will unlabel and re-throw the exception, so that it is okay to throw exceptions from within the LIO monad and catch them within the IO monad. (Of course, code in the IO monad must be careful not to let the LIO code exploit it to exfiltrate information.)

Wherever possible, however, code should use the catchP and onExceptionP variants that use whatever privilege is available to downgrade the exception. Privileged code that must always run some cleanup function can use the onExceptionTCB and bracketTCB functions to run the cleanup code on all exceptions.

Note: Do not use throw (as opposed to throwIO) within the LIO monad. Because throw can be invoked from pure code, it has no notion of current label and so cannot assign an appropriate label to the exception. As a result, the exception will not be catchable within the LIO monad and will propagate all the way out of the evalLIO function. Similarly, asynchronous exceptions (such as divide by zero or undefined values in lazily evaluated expressions) cannot be caught within the LIO monad.

data LabeledException l Source

A labeled exception is simply an exception associated with a label.

class Monad m => MonadCatch m whereSource

MonadCatch is the class used to generalize the standard IO catch and throwIO functions to methods that can be defined in multiple monads. Minimal definition requires: mask, throwIO, catch, and onException.

Methods

maskSource

Arguments

:: ((forall a. m a -> m a) -> m b)

Function that takes a mask-restoring function as argument and returns an action to execute.

-> m b 

Executes a computation with asynchronous exceptions masked. See Control.Exception for more details.

mask_ :: m a -> m aSource

Like mask, but does not pass a restore action to the argument.

throwIO :: Exception e => e -> m aSource

A variant of throwIO that can be used within the monad.

catchSource

Arguments

:: Exception e 
=> m a

Computation to run

-> (e -> m a)

Handler

-> m a 

Simplest exception-catching function.

handle :: Exception e => (e -> m a) -> m a -> m aSource

Version of catch with the arguments swapped around.

onExceptionSource

Arguments

:: m a

Computation to run first

-> m b

Computation to run after, if an exception was raised.

-> m a 

Performs an action and a subsequent action if an exceptino is raised.

bracketSource

Arguments

:: m b

Computation to run first

-> (b -> m c)

Computation to run last

-> (b -> m a)

Computation to run in-between

-> m a 

This function allows you to execute an action with an initial "acquire resource" and final "release resource" as bracket of Control.Exception.

bracket_ :: m a -> m b -> m c -> m cSource

Variant of bracket where the return value from the first computation is not required.

finallySource

Arguments

:: m a

Computation to run first

-> m b

Computation to run after

-> m a 

Performs an action and a subsequent action.

Instances

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

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 raises the current label to the joint of the current label and exception label.

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.

Gates

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

Class used to describe privileges in a meaningful manner.

Methods

privDesc :: p -> dSource

Get privilege description

newtype Gate l d a Source

A Gate is a wrapper for a Labeled type.

Constructors

Gate (Labeled l (d -> a)) 

Instances

mkGateSource

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.

mkGatePSource

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.

callGateSource

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.

Unsafe (TCB) Operations

Basic Label Functions

class PrivTCB t Source

PrivTCB is a method-less class whose only purpose is to be unavailable to unprivileged code. Since (PrivTCB t) => is in the context of class Priv and unprivileged code cannot create new instances of the PrivTCB class, this ensures unprivileged code cannot create new instances of the Priv class either, even though the symbol Priv is exported by LIO.Base and visible to untrusted code.

Instances

class MintTCB t i whereSource

Methods

mintTCB :: i -> tSource

A function that mints new objects (such as instances of Priv) in a way that only privileged code should be allowed to do. Because the MintTCB method is only available to priviledged code, other modules imported by unpriviledged code can define instances of mintTCB.

Labeled IO Monad (LIO)

data LIOstate l p s Source

Internal state of an LIO computation.

Constructors

LIOstate 

Fields

labelState :: s

label-specific state

lioL :: l

current label

lioC :: l

current clearance

lioP :: p

current privileges

getTCB :: LabelState l p s => LIO l p s (LIOstate l p s)Source

Get internal state.

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

Put internal state.

getLabelStateTCB :: LabelState l p s => LIO l p s sSource

Returns label-specific state of the LIO monad. This is the data specified as the second argument of evalLIO, whose type is s in the monad LIO l s.

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

Sets the label-specific state of the LIO monad. See getTCB.

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

Set the current label to anything, with no security check.

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

Set the current clearance to anything, with no security check.

Labeled Values

class ShowTCB a whereSource

It would be a security issue to make certain objects a member of the Show class, but nonetheless it is useful to be able to examine such objects when debugging. The showTCB method can be used to examine such objects.

Methods

showTCB :: a -> StringSource

Instances

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

class ReadTCB a whereSource

It is useful to have the dual of ShowTCB, ReadTCB, that allows for the reading of Labeleds that were written using showTCB. Only readTCB (corresponding to read) and readsPrecTCB (corresponding to readsPrec) are implemented.

Instances

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

labelTCB :: Label l => l -> a -> Labeled l aSource

Trusted constructor that creates labeled values.

unlabelTCB :: Label l => Labeled l a -> aSource

Extracts the value from an Labeled, discarding the label and any protection.

Labeled Exceptions

catchTCBSource

Arguments

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

Computation to run

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

Exception handler

-> LIO l p s a

Result of computation or handler

Trusted catch functin.

class MonadCatch m => OnExceptionTCB m whereSource

For privileged code that needs to catch all exceptions in some cleanup function. Note that for the LIO monad, these methods do not label the exceptions. It is assumed that you will use rtioTCB instead of ioTCB for IO within the computation arguments of these methods.

Methods

onExceptionTCB :: m a -> m b -> m aSource

finallyTCB :: m a -> m b -> m aSource

bracketTCB :: m a -> (a -> m c) -> (a -> m b) -> m bSource

Instances

ioTCB :: LabelState l p s => IO a -> LIO l p s aSource

Lifts an IO computation into the LIO monad. Note that exceptions thrown within the IO computation cannot directly be caught within the LIO computation. Thus, you will generally want to use rtioTCB instead of ioTCB.

rtioTCB :: LabelState l p s => IO a -> LIO l p s aSource

Lifts an IO computation into the LIO monad. If the IO computation throws an exception, it labels the exception with the current label so that the exception can be caught with catch or catchP. This function's name stands for "re-throw io".

Gates

mkGateTCBSource

Arguments

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

Label of gate

-> (d -> a)

Gate action

-> Gate l d a 

Same as mkGate, but ignores IFC.

callGateTCBSource

Arguments

:: (LabelState l p s, PrivDesc p d) 
=> Gate l d a

Gate

-> p

Privilege used to unlabel gate action

-> a 

Same as callGate, but does not raise label in accessing the gate computation.