This module implements the core of the Labeled IO (LIO) library for information flow control (IFC) in Haskell. It provides a monad, LIO, that is intended to be used as a replacement for the IO monad in untrusted code. The idea is for untrusted code to provide a computation in the LIO monad, which trusted code can then safely execute through using evalLIO-like functions. Though, usually a wrapper function is employed depending on the type of labels used by an application. For example, with LIO.DCLabel trusted code would evalDC to execute an untrusted computation.

Labels are a way of describing who can observe and modify data. (A detailed consideration of labels is given in LIO.Label.) LIO associates a current label with every LIO computation. The current label effectively tracks the sensitivity of all the data that the computation has observed. For example, if the computation has read a "secret" mutable refernce (see LIO.LIORef) and then the result of a "top-secret" thread (see LIO.Concurrent) then the current label will be at least "top-secret". The role of the current label is two-fold. First, the current label protects all the data in scope -- it is the label associated with any unlabeled data. For example, the current label is the label on constants such as 3 or "tis a string". More interestingly, consider reading a "secret" file:

 bs <- readFile "/secret/file.txt"

Though the label in the file store may be "secret", bs has type ByteString, which is not explicitly labeled. Hence, to protect the contents (bs) the current label must be at least "secret" before executing readFile. More generally, if the current label is L_cur, then it is only permissible to read data labeled L_r if L_r `canFlowTo` L_cur. Note that, rather than throw an exception, reading data will often just increase the current label to ensure that L_r `canFlowTo` L_cur using taint.

Second, the current label prevents inforation leaks into public channels. Specifically, it is only permissible to modify, or write to, data labeled L_w when L_cur`canFlowTo` L_w. Thus, it the following attempt to leak the secret bs would fail:

 writeFile "/public/file.txt" bs

In addition to the current label, the LIO monad keeps a second label, the current clearance (accessible via the getClearance function). The clearance can be used to enforce a "need-to-know" policy since it represents the highest value the current label can be raised to. In other words, if the current clearance is L_clear then the computation cannot create, read or write to objects labeled L such that L `canFlowTo` L_clear does not hold.

This module exports the LIO monad, functions to access the internal state (e.g., getLabel and getClearance), functions for raising and catching exceptions, and IFC guards. Exceptions are core to LIO since they provide a way to deal with potentially-misbehaving untrusted code. Specifically, when a computation is about to violate IFC (as writeFile above), an exception is raised. Guards provide a useful abstraction for dealing with labeled objects; they should be used before performing a read-only, write-only, or read-write operation on a labeled object. The remaining core, but not all, abstractions are exported by LIO.

Library functions throw an exceptions before an IFC violation can take place. MonitorFailure should be used when the reason for failure is sufficiently described by the type. Otherwise, VMonitorFailure (i.e., "Verbose"-MonitorFailure) should be used to further describe the error.

Guards are used by (usually privileged) code to check that the invoking, unprivileged code has access to particular data. If the current label is lcurrent and the current clearance is ccurrent, then the following checks should be performed when accessing data labeled ldata:

• When reading an object labeled ldata, it must be the case that ldata `canFlowTo` lcurrent. This check is performed by the taint function, so named because it "taints" the current LIO context by raising lcurrent until ldata `canFlowTo` lcurrent. (Specifically, it does this by computing the least upperBound of the two labels.) However, this is done only if the new lcurrent `canFlowTo` ccurrent.
• When creating or allocating objects, it is permissible for them to be higher than the current label, so long as they are below the current clearance. In other words, it must be the case that lcurrent `canFlowTo` ldata && ldata `canFlowTo` ccurrent. This is ensured by the guardAlloc function.
• When writing an object, it should be the case that lcurrent `canFlowTo` ldata && ldata `canFlowTo` lcurrent. (As stated, this is the same as saying ldata == lcurrent, but the two are different when using canFlowToP instead of canFlowTo.) This is ensured by the guardWrite function, which does the equivalent of taint to ensure the target label ldata can flow to the current label, then throws an exception if lcurrent cannot flow back to the target label.

Note that in this case a write always implies a read. Hence, when writing to an object for which you can observe the result, you must use guardWrite. However, when performing a write for which there is no observable side-effects to the writer, i.e., you cannot observe the success or failure of the write, then it is safe to solely use guardAlloc.

The taintP, guardAllocP, and guardWriteP functions are variants of the above that take privilege to be more permissive and raise the current label less.