Internal state of an LIO computation.

The LIO monad is a state monad, with IO as the underlying monad, that carries along a current label (lioLabel) and current clearance (lioClearance). The current label imposes restrictions on what the current computation may read and write (e.g., no writes to public channels after reading sensitive data). Since the current label can be raised to be permissive in what a computation observes, we need a way to prevent certain computations from reading overly sensitive data. This is the role of the current clearance: it imposes an upper bound on the current label.

Get internal state. This function is not actually unsafe, but to avoid future security bugs we leave all direct access to the internal state to trusted code.

Set internal state.

Update the internal state given some function.

Lifts an IO computation into the LIO monad. Note that exceptions thrown within the IO computation cannot directly be caught within the LIO computation. Thus, you will generally want to use rethrowIoTCB.

A newtype wrapper that can be used by trusted code to bless privileges. Privilege-related functions are defined in LIO.Privs, but the constructor, PrivTCB, allows one to mint arbitrary privileges and hence must be located in this file.

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

An uncatchable exception hierarchy use to terminate an untrusted thread. Wrap the uncatchable exception in UncatchableTCB before throwing it to the thread. runLIO will subsequently unwrap the UncatchableTCB constructor.

Note this can be circumvented by mapException, which should be made unsafe.

Simple utility function that strips UncatchableTCB from around an exception.

It would be a security issue to make certain objects a member of the Show class, but nonetheless it is useful to be able to examine such objects when debugging. The showTCB method can be used to examine such objects.

It is useful to have the dual of ShowTCB, ReadTCB, that allows for the reading of strings that were created using showTCB. Only readTCB (corresponding to read) and readsPrecTCB (corresponding to readsPrec) are implemented.