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
 dropPrivileges :: LabelState l p s => LIO l p s ()
 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)
 untaintLabeled :: LabelState l p s => l > Labeled l a > LIO l p s (Labeled l a)
 untaintLabeledP :: LabelState l p s => p > l > Labeled l a > LIO l p s (Labeled l a)
 relabelP :: LabelState l p s => p > 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
 class (PrivTCB p, Show d) => PrivDesc p d  p > d
 data Gate l d a
 mkGate :: (LabelState l p s, PrivDesc p d) => l > (d > a) > LIO l p s (Gate l d a)
 mkGateP :: (LabelState l p s, PrivDesc p d) => p > l > (d > a) > LIO l p s (Gate l d a)
 callGate :: (LabelState l p s, PrivDesc p d) => Gate l d a > p > 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
canflowto partialorder leq
(in literature, written as ⊑).
Bottom
Top
Least upper bound (join) of two labels
Greatest lower bound (meet) of two labels
Canflowto relation
class (Label l, Monoid p, PrivTCB p) => Priv l p whereSource
This class defines privileges and the morepermissive 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 "canflowto given privileges" preorder 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 middleground 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.
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 labelspecific 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
computationsit 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
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.
:: LabelState l p s  
=> l  Label of result and upper bound on innercomputations' 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 DCLabel
s. (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.
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
objectsuntrusted 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
raises the current label to the joint of the current label and
exception label.
:: (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 inbetween 
> 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
.
class (PrivTCB p, Show d) => PrivDesc p d  p > dSource
Class used to describe privileges in a meaningful manner.
:: (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.
:: (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.
:: (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.