Safe Haskell | Trustworthy |
---|---|
Language | Haskell98 |
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
).
Two Applicative
Functor
-like operations are also defined for
Labeled
data, namely lFmap
and lAp
.
- data Labeled l t
- class LabelOf t where
- 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.
class LabelOf t where Source #
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:
data 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 l a) = l
Label values
label :: Label l => l -> a -> LIO l (Labeled l a) Source #
Function to construct a Labeled
value from a label and a 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
value using privilege to allow the value'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 a Labeled
value
at a higher label than the current clearance.
Unlabel values
unlabel :: Label l => Labeled l a -> LIO l a Source #
Within the LIO
monad, this function takes a Labeled
value and
returns it as an unprotected value of the inner type. For
instance, in the LIO
monad one can say:
x <- unlabel (lx :: Labeled SomeLabelType Int)
And now it is possible to use the pure value x :: Int
, which was
previously protected by a label in lx
.
unlabel
raises the current label as needed to reflect the fact
that the thread's behavior can now depend on the contents of lx
.
If unlabel
ing a value would require raising the current label
above the current clearance, then unlabel
throws an exception of
type LabelError
. You can use labelOf
to check beforehand
whether unlabel
will succeed.
unlabelP :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a Source #
Extracts the contents of a Labeled
value just like unlabel
,
but takes a privilege argument to minimize the amount the current
label must be raised. The privilege is used to raise the current
label less than might be required otherwise, but this function does
not change the current clarance and still throws a LabelError
if
the privileges supplied are insufficient to save the current label
from needing to exceed the current clearance.
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
privileges permit it. An exception is thrown unless the following
two conditions hold:
- The new label must be below the current clearance.
- The old label and new label must be equal (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
value to the lub
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
value's label 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.
lFmap :: Label l => Labeled l a -> (a -> b) -> LIO l (Labeled l b) Source #
A function similar to fmap
for Labeled
values. Applies a
function to a Labeled
value without unlabel
ing the value or
changing the thread's current label. The label of the result is the
lub
of the current label and that of the supplied Labeled
value. Because of laziness, the actual computation on the value of
type a
will be deferred until a thread with a higher label
actually unlabel
s the result.