This module should be ** only ** imported by trustworthy for:
- define the security levels of files and their default values
- define a security lattice
- class Eq a => Lattice a where
- class Lattice a => FiniteLattice a where
- less :: Lattice a => a -> a -> Bool
- sless :: Lattice a => a -> a -> Bool
- data Level
- class FiniteLattice l => Policy l a b | a -> l b where
- data ME a
- data SetLevel l = SetLevel
- readFile :: FilePath -> ME String
- writeFile :: FilePath -> String -> ME ()
- sme :: Policy l FilePath String => SetLevel l -> ME a -> IO ()
- sme' :: Policy Level FilePath String => ME a -> IO ()
Type class to encode security lattices.
The greatest lower bound between two security levels.
The lowest upper bound between two security levels.
Type class to encode finite security lattices.
All the elements in the lattice.
It returns all the elements in the lattice that are strictly above the security level given as argument.
Implementation of the order relationship between elements of the lattice.
Implementation of the strict order relationship between security levels of the lattice.
Data type encoding two security levels.
Security level to represent public (low) information.
Security level to represent secret (high) information.
Type class to specify security policies for programs run under secure multi-execution.
Function to perform secure multi-execution. The first argument is only there for type-checking purposes.