SME.Untrustworthy

This module should be imported by untrustworthy code. Generally speaking, untrustworhty code's import list should look like

     import SME.Untrustworthy 
     import MyLattice

where module MyLattice implements the security lattice under consideration.

Documentation

class Eq a => Lattice a

Type class to encode security lattices.

Instances

Lattice Level

class Lattice a => FiniteLattice a

Type class to encode finite security lattices.

Instances

FiniteLattice Level

less :: Lattice a => a -> a -> Bool

Implementation of the order relationship between elements of the lattice.

sless :: Lattice a => a -> a -> Bool

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

data Level

Data type encoding two security levels.

Instances

Enum Level

Eq Level

Show Level

FiniteLattice Level

Lattice Level

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

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

data ME a

The multi-execution monad.

Instances

Monad ME

data SetLevel l

Data type to set the security lattice to be used by function sme.

Constructors

SetLevel

readFile :: FilePath -> ME String

Secure operation for reading files.

writeFile :: FilePath -> String -> ME ()

Secure operation for writing files.

sme :: Policy l FilePath String => SetLevel l -> ME a -> IO ()

Function to perform secure multi-execution. The first argument is only there for type-checking purposes.

sme' :: Policy Level FilePath String => ME a -> IO ()

Function to perform secure multi-execution considering the two-point security lattice encoded by Level.