lio- Labeled IO Information Flow Control Library

Safe HaskellUnsafe




This module exports

  • The definition of the LIO monad and relevant trusted state access/modifying functions.
  • Labeled exceptions that are use throughout LIO and low-level, unsafe, throw and catch primitives.
  • Combinators for executing IO actions.

The documentation and external, safe LIO interface is provided in LIO.Core.


LIO monad

newtype LIO l a Source

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.




unLIOTCB :: StateT (LIOState l) IO a


Label l => MonadLIO l (LIO l) 
Monad (LIO l) 
Functor (LIO l) 
Applicative (LIO l) 
(SLabel l, HandleOps Handle b IO) => HandleOps (LabeledHandle l) b (LIO l) 

class (Monad m, Label l) => MonadLIO l m | m -> l whereSource

Synonym for monad in which LIO is the base monad.


liftLIO :: LIO l a -> m aSource

Lift an LIO computation.


Label l => MonadLIO l (LIO l) 

Internal state

data LIOState l Source

Internal state of an LIO computation.




lioLabel :: !l

Current label.

lioClearance :: !l

Current clearance.


Eq l => Eq (LIOState l) 
Read l => Read (LIOState l) 
Show l => Show (LIOState l) 

getLIOStateTCB :: Label l => LIO l (LIOState l)Source

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.

putLIOStateTCB :: Label l => LIOState l -> LIO l ()Source

Set internal state.

updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()Source

Update the internal state given some function.


data LabeledException l Source

A labeled exception is simply an exception associated with a label.

Throw and catch

unlabeledThrowTCB :: (Exception e, Label l) => e -> LIO l aSource

Throw an arbitrary exception. Note that the exception being thrown is not labeled.

catchTCB :: Label l => LIO l a -> (LabeledException l -> LIO l a) -> LIO l aSource

Catch an exception. Note that all exceptions thrown by LIO are labeled and thus this trusted function can be used to handle any exception. Note that the label of the exception must be considered in the handler (i.e., handler must raise the current label) to preserve security.

Executing IO actions

ioTCB :: Label l => IO a -> LIO l aSource

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 rtioTCB exported by LIO.Exception.TCB instead of ioTCB.

rethrowIoTCB :: Label l => IO a -> LIO l aSource

Lifts an IO computation into the LIO monad. If the IO computation throws an exception, it labels the exception with the current label so that the exception can be caught with catchLIO.

Trusted Show and Read

class ShowTCB a whereSource

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.


showTCB :: a -> StringSource


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

Trusted Show instance.

class ReadTCB a whereSource

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.


readsPrecTCB :: Int -> ReadS aSource

Trusted readsPrec

readTCB :: String -> aSource

Trusted read


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

Trusted Read instance.