SecLib.Ref

It provides a secure interface for manipulation of references.

Secure references

data Ref l a

Secure references

tcbRef :: IORef a -> Ref l a

Only use by trusted code

Operations

newRefSecIO :: a -> SecIO l (Ref l' a)

It creates a new reference. There is no relation between l and l' since creating a reference is not an observable event inside the SecIO monad.

readRefSecIO :: Ref l a -> SecIO l' (Sec l a)

As above, there is no relation between l and l'. Bare in mind that reading a reference is not an observable event inside the SecIO monad.

writeRefSecIO :: Ref l a -> a -> SecIO l ()

It writes references only at the security level indicated by the argument of the SecIO monad.