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

SME.Trustworthy

Synopsis

Documentation

class Eq a => Lattice a whereSource

Type class to encode security lattices.

Methods

meet :: a -> a -> Maybe aSource

The greatest lower bound between two security levels.

join :: a -> a -> Maybe aSource

The lowest upper bound between two security levels.

Instances

class Lattice a => FiniteLattice a whereSource

Type class to encode finite security lattices.

Methods

universe :: [a]Source

All the elements in the lattice.

upset :: a -> [a]Source

It returns all the elements in the lattice that are strictly above the security level given as argument.

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.

Constructors

L

Security level to represent public (low) information.

H

Security level to represent secret (high) information.

Instances

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

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

Methods

level :: a -> lSource

It defines the security level assigned to an input or output of type a.

defvalue :: a -> bSource

It assigns a default value (of type b) to an input of type a.

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.