LIO.Labeled

A data type Labeled protects access to pure values (hence, we refer to values of type Label a 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, Labeled 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.

Documentation

data Labeled l t

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.

Instances

Typeable2 Labeled

LabelOf Labeled

(Show l, Show a) => ShowTCB (Labeled l a)

Trusted Show instance.

class LabelOf t where

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 LVals but not necessarily the actual value. To do so, simply provide an instance for LabelOf:

 instance LabelOf LVal where
   labelOf (LValTCB l a) = l

Methods

labelOf :: t l a -> l

Get the label of a labeled value or object. Note the label must be the second to last type constructor argument.

Instances

LabelOf LabeledResult

LabelOf Labeled

LabelOf LObj

Label values

label :: Label l => l -> a -> LIO l (Labeled l a)

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 `canFlowTo` l && l `canFlowTo` ccurrent. Otherwise an exception is thrown (see guardAlloc).

labelP :: PrivDesc l p => Priv p -> l -> a -> LIO l (Labeled l a)

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 `canFlowTo` ccurrent. Note that privilege is not used to bypass the clearance. You must use setClearanceP 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

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 unlabeling 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

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)

Relabels a Labeled value to the supplied label if the given privileges permit it. An exception is thrown unless the following two conditions hold:

1. The new label must be below the current clearance.
2. 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)

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)

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)

A function similar to fmap for Labeled values. Applies a function to a Labeled value without unlabeling 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 unlabels the result.

lAp :: Label l => Labeled l (a -> b) -> Labeled l a -> LIO l (Labeled l b)

Similar to ap, apply function (wrapped by Labeled) to the labeld value. The label of the returned value is the lub of the thread's current label, the label of the supplied function, and the label of the supplied value.