LIO.Labeled.TCB

This is the TCB-restricted version of LIO.Labeled, which documents the implementation of Labeled values and their use. It provides functions for labeling (labelTCB) and unlabeling (unlabelTCB) labeled values without imposing any information flow restrictions.

Documentation

data Labeled l t

Labeled l a is a value that associates a label of type l with a value of type a. Labeled values allow users to label data with a label other than the current label. In an embedded setting this is akin to having first class labeled values. Note that Labeled is an instance of LabelOf, which effectively means that the label of a Labeled value is usually just protected by the current label. (Of course if you have a nested labeled value then the label on the inner labeled value's label is the outer label.)

Constructors

LabeledTCB

Fields

labelOfLabeled :: !l

Label of Labeled valued

unlabelTCB :: !t

Extracts the value from an Labeled, discarding the label and any protection.

Instances

Typeable2 Labeled

LabelOf Labeled

Returns label of a Labeled type.

(Monad (LIO l), SLabel l, HandleOps Handle b IO) => HandleOps (LabeledHandle l) b (LIO l)

(Label l, Read l, Read a) => ReadTCB (Labeled l a)

Trusted Read instance.

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

Trusted Show instance.

labelTCB :: Label l => l -> a -> Labeled l a

Trusted constructor that creates labeled values.