SecLib.SecIO

Provide security for computations involving side-effects.

SecIO monad

data SecIO l a

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

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.

Lifting pure values

toSecIO :: Sec l a -> SecIO l a

Lift pure sensitive values into secure side-effectful computations.

Execution

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.

Composition

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

Secure coupling of side-effectul computations.