SecLib.TCB.Sec

It provides a family of security monads for pure values.

Documentation

newtype Sec l a

This monad denotes computations which produce values at security level l.

Constructors

MkSec a

Instances

Monad (Sec l)

Functor (Sec l)

Applicative (Sec l)

unsec :: Sec l a -> a

This function unlabels data (to be used only by trusted modules)

up :: Less l l' => Sec l a -> Sec l' a

It raises the security level of a value based on order-relationship expressed by the security lattice.

This is the only operation which connects members of the Sec l monad family.