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



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.



class Eq a => Lattice a Source

Type class to encode security lattices.


class Lattice a => FiniteLattice a Source

Type class to encode finite security lattices.


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.


data SetLevel l Source

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



readFile :: FilePath -> ME StringSource

Secure operation for reading files.

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

Secure operation for writing files.

sme :: Policy l FilePath String => SetLevel 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.