This module should be imported by untrustworthy code. Generally speaking, untrustworhty code's import list should look like
import SME.Untrustworthy import MyLattice
MyLattice implements the security lattice under consideration.
- class Eq a => Lattice a
- class Lattice a => FiniteLattice a
- less :: Lattice a => a -> a -> Bool
- sless :: Lattice a => a -> a -> Bool
- data Level
- class FiniteLattice l => Policy l a b | a -> l b
- 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 finite security lattices.
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.
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.