Safe Haskell | Trustworthy |
---|
- 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
- data LIO l p s 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)
- 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
- 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 Labeled l t
- data LabelFault
- 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
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 ⊑).
Bottom
Top
Least upper bound (join) of two labels
Greatest lower bound (meet) of two labels
Can-flow-to relation
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.
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
.)
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
.
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.
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
is a type representing labeled data.
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.
:: (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
.