| Safe Haskell | Unsafe |
|---|
LIO.TCB
Contents
Description
This module exports
- The definition of the
LIOmonad and relevant trusted state access/modifying functions. - Labeled exceptions that are use throughout
LIOand low-level, unsafe, throw and catch primitives. - Combinators for executing
IOactions.
The documentation and external, safe LIO interface is provided in
LIO.Core.
- newtype LIO l a = LIOTCB {}
- class (Monad m, Label l) => MonadLIO l m | m -> l where
- data LIOState l = LIOState {
- lioLabel :: !l
- lioClearance :: !l
- getLIOStateTCB :: Label l => LIO l (LIOState l)
- putLIOStateTCB :: Label l => LIOState l -> LIO l ()
- updateLIOStateTCB :: Label l => (LIOState l -> LIOState l) -> LIO l ()
- data LabeledException l = LabeledExceptionTCB !l SomeException
- unlabeledThrowTCB :: (Exception e, Label l) => e -> LIO l a
- catchTCB :: Label l => LIO l a -> (LabeledException l -> LIO l a) -> LIO l a
- ioTCB :: Label l => IO a -> LIO l a
- rethrowIoTCB :: Label l => IO a -> LIO l a
- class ShowTCB a where
- class ReadTCB a where
- readsPrecTCB :: Int -> ReadS a
- readTCB :: String -> a
LIO monad
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.
class (Monad m, Label l) => MonadLIO l m | m -> l whereSource
Synonym for monad in which LIO is the base monad.
Internal state
Internal state of an LIO computation.
Constructors
| LIOState | |
Fields
| |
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.
Exceptions
data LabeledException l Source
A labeled exception is simply an exception associated with a label.
Constructors
| LabeledExceptionTCB !l SomeException |
Instances
| Typeable1 LabeledException | |
| Show l => Show (LabeledException l) | |
| Label l => Exception (LabeledException l) |
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
rethrowIoTCB :: Label l => IO a -> LIO l aSource