LIO.TCB

This module exports symbols that must be accessible only to trusted code. By convention, the names of such symbols always end "...TCB" (short for "trusted computing base"). In many cases, a type is safe to export while its constructor is not. Hence, only the constructor ends "TCB", while the type is re-exported to safe code (without constructors) from LIO.Core.

Security rests on the fact that untrusted code must be compiled with -XSafe. Because this module is flagged unsafe, it cannot be imported from safe modules.

LIO monad

data LIOState l

Internal state of an LIO computation.

Constructors

LIOState

Fields

• lioLabel :: !l

  Current label.

• lioClearance :: !l

  Current clearance.

Instances

Eq l => Eq (LIOState l)

Defined in LIO.TCB

Methods

(==) :: LIOState l -> LIOState l -> Bool

(/=) :: LIOState l -> LIOState l -> Bool

Read l => Read (LIOState l)

Defined in LIO.TCB

Methods

readsPrec :: Int -> ReadS (LIOState l)

readList :: ReadS [LIOState l]

readPrec :: ReadPrec (LIOState l)

readListPrec :: ReadPrec [LIOState l]

Show l => Show (LIOState l)

Defined in LIO.TCB

Methods

showsPrec :: Int -> LIOState l -> ShowS

show :: LIOState l -> String

showList :: [LIOState l] -> ShowS

newtype LIO l a

The LIO monad is a wrapper around IO that keeps track of a current label and current clearance. Safe code cannot execute arbitrary IO actions from the LIO monad. However, trusted runtime functions can use ioTCB to perform IO actions (which they should only do after appropriately checking labels).

Constructors

LIOTCB (IORef (LIOState l) -> IO a)

Instances

Label l => MonadLIO l (LIO l)

Defined in LIO.Monad

Methods

liftLIO :: LIO l a -> LIO l a

GuardIO l (IO r) (LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> IO r -> LIO l r

LabelIO l (IO r) (LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> IO r -> LIO l r

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r

GuardIO l (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r

GuardIO l (a1 -> a2 -> a3 -> a4 -> IO r) (a1 -> a2 -> a3 -> a4 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> a3 -> a4 -> IO r) -> a1 -> a2 -> a3 -> a4 -> LIO l r

GuardIO l (a1 -> a2 -> a3 -> IO r) (a1 -> a2 -> a3 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> a3 -> IO r) -> a1 -> a2 -> a3 -> LIO l r

GuardIO l (a1 -> a2 -> IO r) (a1 -> a2 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> a2 -> IO r) -> a1 -> a2 -> LIO l r

GuardIO l (a1 -> IO r) (a1 -> LIO l r)

Defined in LIO.TCB.LObj

Methods

guardIOTCB :: LIO l () -> (a1 -> IO r) -> a1 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> a10 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> a9 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> a8 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> a7 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> a6 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) (a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> a3 -> a4 -> a5 -> IO r) -> a1 -> a2 -> a3 -> a4 -> a5 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> a4 -> IO r) (a1 -> a2 -> a3 -> a4 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> a3 -> a4 -> IO r) -> a1 -> a2 -> a3 -> a4 -> LIO l r

LabelIO l (a1 -> a2 -> a3 -> IO r) (a1 -> a2 -> a3 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> a3 -> IO r) -> a1 -> a2 -> a3 -> LIO l r

LabelIO l (a1 -> a2 -> IO r) (a1 -> a2 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> a2 -> IO r) -> a1 -> a2 -> LIO l r

LabelIO l (a1 -> IO r) (a1 -> LIO l r)

Defined in LIO.TCB.MLObj

Methods

labelIO :: (forall r0. IO r0 -> LIO l r0) -> (a1 -> IO r) -> a1 -> LIO l r

Monad (LIO l)

Defined in LIO.TCB

Methods

(>>=) :: LIO l a -> (a -> LIO l b) -> LIO l b

(>>) :: LIO l a -> LIO l b -> LIO l b

return :: a -> LIO l a

fail :: String -> LIO l a

Functor (LIO l)

Defined in LIO.TCB

Methods

fmap :: (a -> b) -> LIO l a -> LIO l b

(<$) :: a -> LIO l b -> LIO l a

Applicative (LIO l)

Defined in LIO.TCB

Methods

pure :: a -> LIO l a

(<*>) :: LIO l (a -> b) -> LIO l a -> LIO l b

liftA2 :: (a -> b -> c) -> LIO l a -> LIO l b -> LIO l c

(*>) :: LIO l a -> LIO l b -> LIO l b

(<*) :: LIO l a -> LIO l b -> LIO l a

Accessing internal state

getLIOStateTCB :: LIO l (LIOState l)

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 :: LIOState l -> LIO l ()

Set internal state.

modifyLIOStateTCB :: (LIOState l -> LIOState l) -> LIO l ()

Update the internal state given some function.

Executing IO actions

ioTCB :: IO a -> LIO l a

Lifts an IO computation into the LIO monad. This function is dangerous and should only be called after appropriate checks ensure the IO computation will not violate IFC policy.

Privileged constructors

newtype Priv a

A newtype wrapper that can be used by trusted code to transform a powerless description of privileges into actual privileges. The constructor, PrivTCB, is dangerous as it allows creation of arbitrary privileges. Hence it is only exported by the unsafe module LIO.TCB. A safe way to create arbitrary privileges is to call privInit (see "LIO.Run#v:privInit") from the IO monad before running your LIO computation.

Constructors

PrivTCB a

Instances

PrivDesc l p => PrivDesc l (Priv p)

Defined in LIO.Label

Methods

downgradeP :: Priv p -> l -> l

canFlowToP :: Priv p -> l -> l -> Bool

Eq a => Eq (Priv a)

Defined in LIO.TCB

Methods

(==) :: Priv a -> Priv a -> Bool

(/=) :: Priv a -> Priv a -> Bool

Show a => Show (Priv a)

Defined in LIO.TCB

Methods

showsPrec :: Int -> Priv a -> ShowS

show :: Priv a -> String

showList :: [Priv a] -> ShowS

Semigroup p => Semigroup (Priv p)

Defined in LIO.TCB

Methods

(<>) :: Priv p -> Priv p -> Priv p

sconcat :: NonEmpty (Priv p) -> Priv p

stimes :: Integral b => b -> Priv p -> Priv p

Monoid p => Monoid (Priv p)

Defined in LIO.TCB

Methods

mempty :: Priv p

mappend :: Priv p -> Priv p -> Priv p

mconcat :: [Priv p] -> Priv p

SpeaksFor p => SpeaksFor (Priv p)

Defined in LIO.Label

Methods

speaksFor :: Priv p -> Priv p -> Bool

ToCNF (Priv CNF)

Defined in LIO.DCLabel

Methods

toCNF :: Priv CNF -> CNF

data Labeled l t

Labeled l a is a value that associates a label of type l with a pure value of type a. Labeled values allow users to label data with a label other than the current label. Note that Labeled is an instance of LabelOf, which means that only the contents of a labeled value (the type t) is kept secret, not the label. Of course, if you have a Labeled within a Labeled, then the label on the inner value will be protected by the outer label.

Constructors

LabeledTCB !l t

Instances

LabelOf Labeled

Defined in LIO.TCB

Methods

labelOf :: Labeled l a -> l

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

Trusted Show instance.

Defined in LIO.TCB

Methods

showTCB :: Labeled l a -> String

class LabelOf t where

Generic class used to get the type of labeled objects. For, instance, if you wish to associate a label with a pure value (as in LIO.Labeled), you may create a data type:

data LVal l a = LValTCB l a

Then, you may wish to allow untrusted code to read the label of any LVals but not necessarily the actual value. To do so, simply provide an instance for LabelOf:

instance LabelOf LVal where
  labelOf (LValTCB l a) = l

Methods

labelOf :: t l a -> l

Get the label of a labeled value or object. Note the label must be the second to last type constructor argument.

Instances

LabelOf LabeledResult

Defined in LIO.TCB

Methods

labelOf :: LabeledResult l a -> l

LabelOf Labeled

Defined in LIO.TCB

Methods

labelOf :: Labeled l a -> l

LabelOf LObj

Defined in LIO.TCB.LObj

Methods

labelOf :: LObj l a -> l

Uncatchable exception type

data UncatchableTCB

An uncatchable exception hierarchy is used 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. In the interim, auditing untrusted code for this is necessary.

Constructors

Exception e => UncatchableTCB e

Instances

Show UncatchableTCB

Defined in LIO.TCB

Methods

showsPrec :: Int -> UncatchableTCB -> ShowS

show :: UncatchableTCB -> String

showList :: [UncatchableTCB] -> ShowS

Exception UncatchableTCB

Defined in LIO.TCB

Methods

toException :: UncatchableTCB -> SomeException

fromException :: SomeException -> Maybe UncatchableTCB

displayException :: UncatchableTCB -> String

makeCatchable :: SomeException -> SomeException

Simple utility function that strips UncatchableTCB from around an exception.

Trusted Show

class ShowTCB a where

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

Methods

showTCB :: a -> String

Instances

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

Trusted Show instance.

Defined in LIO.TCB

Methods

showTCB :: Labeled l a -> String

(Label l, Show t) => ShowTCB (LObj l t)

Defined in LIO.TCB.LObj

Methods

showTCB :: LObj l t -> String

LabeledResults

data LabeledResult l a

A LabeledResult encapsulates a future result from a computation spawned by lFork or lForkP. See LIO.Concurrent for a description of the concurrency abstractions of LIO.

Constructors

LabeledResultTCB

Fields

• lresThreadIdTCB :: !ThreadId

  Thread executing the computation

• lresLabelTCB :: !l

  Label of the tresult

• lresBlockTCB :: !(MVar ())

  This MVar is empty until such point as lresStatusTCB is no longer LResEmpty. Hence, calling readMVar on this field allows one to wait for the thread to terminate.

• lresStatusTCB :: !(IORef (LResStatus l a))

  Result (when it is ready), or the label at which the thread terminated, if that label could not flow to lresLabelTCB.

Instances

LabelOf LabeledResult

Defined in LIO.TCB

Methods

labelOf :: LabeledResult l a -> l

data LResStatus l a

Status of a LabeledResult.

Constructors

LResEmpty

LResLabelTooHigh !l

LResResult a

Instances

(Show l, Show a) => Show (LResStatus l a)

Defined in LIO.TCB

Methods

showsPrec :: Int -> LResStatus l a -> ShowS

show :: LResStatus l a -> String

showList :: [LResStatus l a] -> ShowS