Safe Haskell | Unsafe |
---|
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.)
- class (Eq a, Show a, Read a, Typeable a) => Label a where
- class (Label l, Monoid p, PrivTCB p) => Priv l p where
- noPrivs :: Monoid p => p
- getPrivileges :: LabelState l p s => LIO l p s p
- withPrivileges :: LabelState l p s => p -> LIO l p s a -> LIO l p s a
- withCombinedPrivs :: LabelState l p s => p -> (p -> LIO l p s a) -> LIO l p s a
- newtype LIO l p s a = LIO (StateT (LIOstate l p s) IO a)
- class (Priv l p, Label l) => LabelState l p s | l -> s, l -> p
- evalLIO :: LabelState l p s => LIO l p s a -> s -> IO (a, l)
- 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)
- newState :: LabelState l p s => s -> LIOstate l p s
- getLabel :: LabelState l p s => LIO l p s l
- setLabelP :: LabelState l p s => p -> l -> LIO l p s ()
- getClearance :: LabelState l p s => LIO l p s l
- lowerClr :: LabelState l p s => l -> LIO l p s ()
- lowerClrP :: LabelState l p s => p -> l -> LIO l p s ()
- withClearance :: LabelState l p s => l -> LIO l p s a -> LIO l p s a
- data Labeled l t
- labelOf :: Label l => Labeled l a -> l
- label :: LabelState l p s => l -> a -> LIO l p s (Labeled l a)
- labelP :: LabelState l p s => p -> l -> a -> LIO l p s (Labeled l a)
- unlabel :: LabelState l p s => Labeled l a -> LIO l p s a
- unlabelP :: LabelState l p s => p -> Labeled l a -> LIO l p s a
- taintLabeled :: LabelState l p s => l -> Labeled l a -> LIO l p s (Labeled l a)
- toLabeled :: LabelState l p s => l -> LIO l p s a -> LIO l p s (Labeled l a)
- toLabeledP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s (Labeled l a)
- discard :: LabelState l p s => l -> LIO l p s a -> LIO l p s ()
- discardP :: LabelState l p s => p -> l -> LIO l p s a -> LIO l p s ()
- taint :: LabelState l p s => l -> LIO l p s ()
- taintP :: LabelState l p s => p -> l -> LIO l p s ()
- wguard :: LabelState l p s => l -> LIO l p s ()
- wguardP :: LabelState l p s => p -> l -> LIO l p s ()
- aguard :: LabelState l p s => l -> LIO l p s ()
- aguardP :: LabelState l p s => p -> l -> LIO l p s ()
- data LabelFault
- data LabeledException l = LabeledExceptionTCB l SomeException
- class Monad m => MonadCatch m where
- mask :: ((forall a. m a -> m a) -> m b) -> m b
- mask_ :: m a -> m a
- throwIO :: Exception e => e -> m a
- catch :: Exception e => m a -> (e -> m a) -> m a
- handle :: Exception e => (e -> m a) -> m a -> m a
- onException :: m a -> m b -> m a
- bracket :: m b -> (b -> m c) -> (b -> m a) -> m a
- bracket_ :: m a -> m b -> m c -> m c
- finally :: m a -> m b -> m a
- catchP :: (Exception e, LabelState l p s) => p -> LIO l p s a -> (e -> LIO l p s a) -> LIO l p s a
- handleP :: (Exception e, LabelState l p s) => p -> (e -> LIO l p s a) -> LIO l p s a -> LIO l p s a
- onExceptionP :: LabelState l p s => p -> LIO l p s a -> LIO l p s b -> LIO l p s a
- bracketP :: LabelState l p s => p -> LIO l p s a -> (a -> LIO l p s c) -> (a -> LIO l p s b) -> LIO l p s b
- evaluate :: LabelState l p s => a -> LIO l p s a
- class PrivTCB t
- class MintTCB t i where
- mintTCB :: i -> t
- data LIOstate l p s = LIOstate {
- labelState :: s
- lioL :: l
- lioC :: l
- lioP :: p
- getTCB :: LabelState l p s => LIO l p s (LIOstate l p s)
- putTCB :: LabelState l p s => LIOstate l p s -> LIO l p s ()
- getLabelStateTCB :: LabelState l p s => LIO l p s s
- putLabelStateTCB :: LabelState l p s => s -> LIO l p s ()
- setLabelTCB :: LabelState l p s => l -> LIO l p s ()
- lowerClrTCB :: LabelState l p s => l -> LIO l p s ()
- class ShowTCB a where
- class ReadTCB a where
- readsPrecTCB :: Int -> ReadS a
- readTCB :: String -> a
- labelTCB :: Label l => l -> a -> Labeled l a
- unlabelTCB :: Label l => Labeled l a -> a
- catchTCB :: LabelState l p s => LIO l p s a -> (LabeledException l -> LIO l p s a) -> LIO l p s a
- class MonadCatch m => OnExceptionTCB m where
- onExceptionTCB :: m a -> m b -> m a
- bracketTCB :: m a -> (a -> m c) -> (a -> m b) -> m b
- ioTCB :: LabelState l p s => IO a -> LIO l p s a
- rtioTCB :: LabelState l p s => IO a -> LIO l p s a
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 `
. This is sometimes
termed "no read up" in the literature; however, because the partial
order allows for incomparable labels (i.e., two labels leq
` L_curL_1
and
L_2
such that not (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
leq
` L_2) && not (L_2 `leq
` L_1)L_r `
. The LIO monad keeps a second label, called
the clearance (see leq
` L_curgetClearance
), 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`
, 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 leq
` L_wL_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
`
, then the current thread can
neither read nor write the data, at least without invoking some
privilege.
leq
` L_d || L_d `leq
` C_cur)
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 ⊑).
Bottom
Top
Least upper bound (join) of two labels
Greatest lower bound (meet) of two labels
Can-flow-to relation
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 `
even when
that is not the case. The process of making data labeled leq
` L_2L_1
affect data labeled L_2
when not (L_1 `
is called
downgrading.
leq
` L_2)
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.
leqp :: p -> l -> l -> BoolSource
The "can-flow-to given privileges" pre-order used to
compare two labels in the presence of privileges.
If
holds, then privileges leqp
p L_1 L_2p
are sufficient to
downgrade data from L_1
to L_2
. Note that
implies leq
L_1 L_2
for all leq
p L_1 L_2p
, but for some labels and
privileges, leqp
will hold even where leq
does not.
:: 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 ==
, the resulting
label noPrivs
L_r == L `
. If lub
`L_gp
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:
-
L_g ⊑ L_l
, and -
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)
getPrivileges :: LabelState l p s => LIO l p s pSource
Returns the current privileges.
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.
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.
LIO monad is a State monad transformer with IO as the underlying monad.
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.
:: 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
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 `
.
Note that there is no leq
` newLabel && newLabel `leq
` clearancesetLabel
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
Priv
s, it may still be able to raise its clearance above the
supplied argument using lowerClrP
.
Labeled Values
Labeled
is a type representing labeled data.
label :: LabelState l p s => l -> a -> LIO l p s (Labeled l a)Source
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 `
.
Note that privilege is not used to bypass the clearance. You must
use leq
` ccurrentlowerClrP
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
:: 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 a a toLabeled
block, the join of
the exception label and supplied label will be used as the new
label. If the current label of the inner computation is above
the supplied label, an exception (whose label will reflect this
observatoin) is throw by toLabeled
.
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.
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 thatldata `
. This check is performed by theleq
` lcurrenttaint
function, so named becuase it "taints" the current LIO context by raisinglcurrent
untilldata `
. (Specifically, it does this by computing the least upper bound of the two labels with theleq
` lcurrentlub
method of theLabel
class.) However, if after doing this it would be the case thatnot (lcurrent `
, thenleq
` ccurrent)taint
throws exceptionLerrClearance
rather than raising the current label. - When writing an object, it should be the case that
ldata `
. (As stated, this is the same as sayingleq
` lcurrent && lcurrent `leq
` ldataldata == lcurrent
, but the two are different when usingleqp
instead ofleq
.) This is ensured by thewguard
(write guard) function, which does the equivalent oftaint
to ensure the target labelldata
can flow to the current label, then throws an exception iflcurrent
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 `
. This is ensured by theleq
` ldata && ldata `leq
` ccurrentaguard
(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 `
, or throw leq
` l'
if LerrClearance
l'
would have to be
higher than the current clearance.
:: LabelState l p s | |
=> p | Privileges to invoke |
-> l | Label to taint to if no privileges |
-> LIO l p s () |
wguard :: LabelState l p s => l -> LIO l p s ()Source
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.
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.
Typeable1 LabeledException | |
Label l => Show (LabeledException l) | |
Label l => Exception (LabeledException l) |
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
.
:: ((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.
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.
:: 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.
:: 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.
:: 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.
:: m a | Computation to run first |
-> m b | Computation to run after |
-> m a |
Performs an action and a subsequent action.
MonadCatch IO | |
LabelState l p s => MonadCatch (LIO l p s) |
:: (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.
:: (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.
:: 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.
:: 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
.
Unsafe (TCB) Operations
Basic Label Functions
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.
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)
Internal state of an LIO
computation.
LIOstate | |
|
getTCB :: LabelState l p s => LIO l p s (LIOstate l p s)Source
Get internal state.
getLabelStateTCB :: LabelState l p s => LIO l p s sSource
putLabelStateTCB :: LabelState l p s => s -> LIO l p s ()Source
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
unlabelTCB :: Label l => Labeled l a -> aSource
Extracts the value from an Labeled
, discarding the label and any
protection.
Labeled Exceptions
:: 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.
onExceptionTCB :: m a -> m b -> m aSource
bracketTCB :: m a -> (a -> m c) -> (a -> m b) -> m bSource
OnExceptionTCB IO | |
LabelState l p s => OnExceptionTCB (LIO l p s) |
ioTCB :: LabelState l p s => IO a -> LIO l p s aSource