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). A Functor-like class (LabeledFunctor) on Labeled is also defined in this module.

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:

 newtype 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 lv) = fst lv

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 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 `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 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 `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 an Labeled 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 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.

unlabelP :: PrivDesc l p => Priv p -> Labeled l a -> LIO l a

Extracts the value of an Labeled just like unlabel, but takes a privilege argument to minimize the amount the current label must be raised. Function will throw ClearanceViolation under the same circumstances as unlabel.

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 privilege privileges permits it. An exception is thrown unless the following two conditions hold:

1. The new label must be between the current label and clearance (modulo privileges), as enforced by guardAllocP.
2. 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)

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)

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)

Similar to fmap, apply function to the Labeled value. The label of the returned value is the least upper bound of the current label and label of the supplied labeled value.

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 least upper bound of the current label, label of the supplied labeled value, and label of the supplied function.