MAC.Effects

It provides functions which map read and write effects into security checks.

Documentation

create :: Less l l' => IO (d a) -> MAC l (Res l' (d a))

It lifts functions which create resources into secure functions which create labeled resources

writeup :: Less l l' => (d a -> IO ()) -> Res l' (d a) -> MAC l ()

It lifts an IO-action which writes into a data type d a into a secure function which writes into a labeled resource

readdown :: Less l' l => (d a -> IO a) -> Res l' (d a) -> MAC l a

It lifts an IO-action which reads from a data type d a into a secure function which reads from a labeled resource

fix :: l -> MAC l ()

Proxy function to set the index of the family member MAC

read_and_fix :: Less l l => (d a -> IO a) -> Res l (d a) -> MAC l a

Auxiliary function. A combination of fix and readdown.

write_and_fix :: Less l' l' => (d a -> IO ()) -> Res l' (d a) -> MAC l' ()

Auxiliary function. A combination of fix and readdown.

rw_read :: (Less l l', Less l' l) => (d a -> IO a) -> Res l' (d a) -> MAC l a

It lifts an operation which perform a read on data type d a, but it also performs a write on it as side-effect

rw_write :: (Less l l', Less l' l) => (d a -> IO ()) -> Res l' (d a) -> MAC l ()

It lifts an operation which perform a write on data type d a, but it also performs a read on it as side-effect