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 ()

# Documentation

class Eq a => Lattice a whereSource

Type class to encode security lattices.

class Lattice a => FiniteLattice a whereSource

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.

less :: Lattice a => a -> a -> BoolSource

Implementation of the order relationship between elements of the lattice.

sless :: Lattice a => a -> a -> BoolSource

Implementation of the strict order relationship between security levels of the lattice.

Data type encoding two security levels.

class FiniteLattice l => Policy l a b | a -> l b whereSource

Type class to specify security policies for programs run under secure multi-execution.