lio- Labeled IO Information Flow Control Library

Safe HaskellTrustworthy




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.



data Labeled l t Source

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.


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

Trusted Show instance.

class LabelOf t whereSource

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


labelOf :: t l a -> lSource

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 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)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 `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 aSource

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 aSource

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:

  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)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 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)Source

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.