sme-0.1: A library for Secure Multi-Execution in Haskell

SME.Untrustworthy

Synopsis

Documentation

class Eq a => Lattice a Source

Type class to encode security lattices.

Instances

class Lattice a => FiniteLattice a Source

Type class to encode finite security lattices.

Instances

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 Level Source

Data type encoding two security levels.

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

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

data ME a Source

The multi-execution monad.

Instances

readFile :: FilePath -> ME StringSource

Secure operation for reading files.

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

Secure operation for writing files.

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

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

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

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