SME.Trustworthy

This module should be ** only ** imported by trustworthy for:

• define the security levels of files and their default values
• define a security lattice

Documentation

class Eq a => Lattice a where

Type class to encode security lattices.

Methods

meet :: a -> a -> Maybe a

The greatest lower bound between two security levels.

join :: a -> a -> Maybe a

The lowest upper bound between two security levels.

Instances

Lattice Level

class Lattice a => FiniteLattice a where

Type class to encode finite security lattices.

Methods

universe :: [a]

All the elements in the lattice.

upset :: a -> [a]

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

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.

Constructors

L

Security level to represent public (low) information.

H

Security level to represent secret (high) information.

Instances

Enum Level

Eq Level

Show Level

FiniteLattice Level

Lattice Level

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

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

Methods

level :: a -> l

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

defvalue :: a -> b

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

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.