Safe Haskell | Trustworthy |
---|
A data type Labeled
protects access to pure values (hence, we refer
to values of type
as labeled values). The role of
labeled values is to allow users to associate heterogeneous labels (see
LIO.Label) with values. Although LIO's current label protects all
values in scope with the current label, Label
aLabeled
values allow for
more fine grained protection. Moreover, trusted code may easily
inspect Labeled
values, for instance, when inserting values into a
database.
Without the appropriate privileges, one cannot produce a pure
unlabeled value that depends on a secret Labeled
value, or
conversely produce a high-integrity Labeled
value based on pure
data. This module exports functions for creating labeled values
(label
), using the values protected by Labeled
by unlabeling them
(unlabel
), and changing the value of a labeled value without
inspection (relabelLabeledP
, taintLabeled
). A
Functor
-like class (LabeledFunctor
) on Labeled
is also defined
in this module.
- data Labeled l t
- class LabelOf t where
- labelOf :: t l a -> l
- label :: Label l => l -> a -> LIO l (Labeled l a)
- labelP :: PrivDesc l p => Priv p -> l -> a -> LIO l (Labeled l a)
- unlabel :: Label l => Labeled l a -> LIO l a
- unlabelP :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a
- relabelLabeledP :: PrivDesc l p => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)
- taintLabeled :: Label l => l -> Labeled l a -> LIO l (Labeled l a)
- taintLabeledP :: PrivDesc l p => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)
- lFmap :: Label l => Labeled l a -> (a -> b) -> LIO l (Labeled l b)
- lAp :: Label l => Labeled l (a -> b) -> Labeled l a -> LIO l (Labeled l b)
Documentation
Labeled l a
is a value that associates a label of type l
with
a pure value of type a
. Labeled values allow users to label data
with a label other than the current label. Note that Labeled
is
an instance of LabelOf
, which means that only the contents of a
labeled value (the type t
) is kept secret, not the label. Of
course, if you have a Labeled
within a Labeled
, then the label
on the inner value will be protected by the outer label.
Generic class used to get the type of labeled objects. For, instance, if you wish to associate a label with a pure value (as in LIO.Labeled), you may create a data type:
newtype LVal l a = LValTCB (l, a)
Then, you may wish to allow untrusted code to read the label of any
LVal
s but not necessarily the actual value. To do so, simply
provide an instance for LabelOf
:
instance LabelOf LVal where labelOf (LValTCB lv) = fst lv
Get the label of a labeled value or object. Note the label must be the second to last type constructor argument.
Label values
label :: Label l => l -> a -> LIO l (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
`
. Otherwise an
exception is thrown (see canFlowTo
` l && l `canFlowTo
` ccurrentguardAlloc
).
labelP :: PrivDesc l p => Priv p -> l -> a -> LIO l (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 canFlowTo p lcurrent l
and
l `
. Note that privilege is not used to bypass
the clearance. You must use canFlowTo
` ccurrentsetClearanceP
to raise the clearance
first if you wish to create an Labeled
at a higher label than the
current clearance.
Unlabel values
unlabel :: Label l => Labeled l a -> LIO l aSource
Within the LIO
monad, this function takes a Labeled
and returns
the underlying 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 :: Int
, 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 ClearanceViolation
.
However, you can use labelOf
to check if unlabel
will succeed
without throwing an exception.
Relabel values
relabelLabeledP :: PrivDesc l p => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)Source
Relabels a Labeled
value to the supplied label if the given
privilege privileges permits it. An exception is thrown unless the
following two conditions hold:
- The new label must be between the current label and clearance
(modulo privileges), as enforced by
guardAllocP
. - The old label must flow to the new label (again modulo
privileges), as enforced by
canFlowToP
.
taintLabeled :: Label l => l -> Labeled l a -> LIO l (Labeled l a)Source
Raises the label of a Labeled
to the upperBound
of it's current
label and the value supplied. The label supplied must be bounded by
the current label and clearance, though the resulting label may not be
if the Labeled
is already above the current thread's clearance. If
the supplied label is not bounded then taintLabeled
will throw an
exception (see guardAlloc
).
taintLabeledP :: PrivDesc l p => Priv p -> l -> Labeled l a -> LIO l (Labeled l a)Source
Same as taintLabeled
, but uses privileges when comparing the
current label to the supplied label. In other words, this function
can be used to lower the label of the labeled value by leveraging
the supplied privileges.