SecLib.TCB.SecIO

Provide security for computations involving side-effects.

Documentation

newtype SecIO l a

This monad represents side-effectful computations with observable effects, and return values, at security level, at least, l.

Constructors

MkSecIO (IO (Sec l a))

Instances

Monad (SecIO l)

Functor (SecIO l)

SecIO cannot be a functor for security reasons. The member fmap is declared as undefined due to the Applicative-Monad Haskell 2014 proposal.

Applicative (SecIO l)

For the same reason as above, '(*)' is undefined.

toSecIO :: Sec l a -> SecIO l a

Lift pure sensitive values into secure side-effectful computations.

run :: SecIO l a -> IO (Sec l a)

Execute secure computations.

This function can be safely given to untrusted code. However, trusted code should not run an IO computation returned by untrusted code. After all, its origin cannot be determined, i.e., it could come from run or any other IO operation which could compromise confidentiality or integrity of data.

plug :: forall l l' a. Less l l' => SecIO l' a -> SecIO l (Sec l' a)

Secure coupling of side-effectul computations.

ioTCB :: IO a -> SecIO l a