Safe Haskell	Unsafe
Language	Haskell98

SecLib.TCB.SecIO

Description

Provide security for computations involving side-effects.

Synopsis

Documentation

newtype SecIO l a Source

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 Source

Lift pure sensitive values into secure side-effectful computations.

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

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) Source

Secure coupling of side-effectul computations.

ioTCB :: IO a -> SecIO l a Source