dclabel-eci11-0.2: Dynamic labels to assign confidentiality and integrity levels in scenarios of mutual distrust




This module exports a safe-subset of DCLabel.Core, implementing Disjunction Category Labels. The exported functions and constructors may be used by untrusted code, guaranteeing that they cannot perform anything unsafe.


DC Labels with EDSL



:: Lattice a 
=> a 
-> a 
-> a

Join of two elements



:: Lattice a 
=> a 
-> a 
-> a

Meet of two elements



:: Lattice a 
=> a

Top of lattice



:: Lattice a 
=> a

Bottom of lattice



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

Partial order relation

data Label Source

A label is a conjunction of disjunctions, where MkLabelAll is the constructor that is associated with the conjunction of all possible disjunctions.


Eq Label 
Read Label 
Show Label 
ToLNF Label

Reduce a label to LNF. First it applies cleanLabel to remove duplicate principals and categories. Following, it removes extraneous/redundant categories. A category is said to be extraneous if there is another category in the label that implies it.

NewPriv Label 
PrettyShow Label 
CanActFor Priv Priv 
CanActFor Priv TCBPriv 
CanActFor TCBPriv Priv 
NewDC String Label 
NewDC Principal Label 
NewDC Label String 
NewDC Label Principal 
NewDC Label Label 
ConjunctionOf String Label 
ConjunctionOf Principal Label 
ConjunctionOf Label String 
ConjunctionOf Label Principal 
ConjunctionOf Label Label 
DisjunctionOf String Label 
DisjunctionOf Principal Label 
DisjunctionOf Label String 
DisjunctionOf Label Principal 
DisjunctionOf Label Label 

data DCLabel Source

A DC label for secrecy and integrity.

principal :: String -> PrincipalSource

Generates a principal from an string.

(.\/.) :: DisjunctionOf a b => a -> b -> LabelSource

(./\.) :: ConjunctionOf a b => a -> b -> LabelSource

(<>) :: LabelSource

Empty label.

(><) :: LabelSource

All label.



:: NewDC a b 
=> a 
-> b 
-> DCLabel

Given two elements create label.


data TCBPriv Source

Privilege object is just a conjunction of disjunctions, i.e., a Label. A trusted privileged object must be introduced by trusted code, after which trusted privileged objects can be created by delegation.

type Priv = LabelSource

Untrusted privileged object, which can be converted to a TCBPriv with delegatePriv.

canflowto_p :: RelaxedLattice a => TCBPriv -> a -> a -> BoolSource

Relaxed partial-order relation

delegatePriv :: TCBPriv -> Priv -> Maybe TCBPrivSource

Given trusted privilige and a "desired" untrusted privilege, return a trusted version of the untrusted privilige, if the provided (trusted) privilige implies it.

canActFor :: CanActFor a b => a -> b -> BoolSource

Can use first privilige in place of second.

newPriv :: NewPriv a => a -> PrivSource

Given element create privilege.

Given element create (maybe) trusted privileged object.

newTCBPriv :: NewPriv a => TCBPriv -> a -> Maybe TCBPrivSource