DCLabel.Core
- newtype Disj = MkDisj {}
- newtype Conj = MkConj {}
- data Label
- = MkLabelAll
- | MkLabel { }
- class Eq a => Lattice a where
- data DCLabel = MkDCLabel {}
- emptyLabel :: Label
- allLabel :: Label
- newtype Principal = MkPrincipal {}
- principal :: String -> Principal
- data TCBPriv = MkTCBPriv {}
- type Priv = Label
- class Lattice a => RelaxedLattice a where
- canflowto_p :: TCBPriv -> a -> a -> Bool
- noPriv :: TCBPriv
- rootPrivTCB :: TCBPriv
- delegatePriv :: TCBPriv -> Priv -> Maybe TCBPriv
- createPrivTCB :: Priv -> TCBPriv
- class CanActFor a b where
- and_label :: Label -> Label -> Label
- or_label :: Label -> Label -> Label
- class ToLNF a where
- toLNF :: a -> a
- cleanLabel :: Label -> Label
- implies :: Label -> Label -> Bool
Constructors
A disjunction of ordered elements.
The empty list '[]' corresponds to the disjunction of all principals.
In other words, conceptually, [] = [P_1 / P_2 / ...]
A conjunction of ordered elements.
The empty list '[]' corresponds to the single disjunction of all principals.
In other words, conceptually, [] = {[P_1 / P_2 / ...]}
A label is a conjunction of disjunctions, where MkLabelAll is
the constructor that is associated with the conjunction of all
possible disjunctions.
Constructors
| MkLabelAll | |
| MkLabel | |
Instances
| Eq Label | |
| Read Label | |
| Show Label | |
| ToLNF Label | Reduce a label to LNF.
First it applies |
| 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 |
DC Labels
class Eq a => Lattice a whereSource
(Bounded) Lattice definition
Methods
Arguments
| :: a | Bottom of lattice |
Arguments
| :: a | Top of lattice |
Arguments
| :: a | |
| -> a | |
| -> a | Join of two elements |
Arguments
| :: a | |
| -> a | |
| -> a | Meet of two elements |
Arguments
| :: a | |
| -> a | |
| -> Bool | Partial order relation |
A DC label for secrecy and integrity.
A label without any disjunctions or conjunctions. This label, conceptually
corresponds to the label consisting of a single category containing all
principals.
In other words, conceptually, emptyLabel = {[P_1 \/ P_2 \/ ...]}
The dual of emptyLabel, allLabel consists of the conjunction of
all possible disjunctions, i.e., it is the label that implies all
other labels.
In other words, conceptually, allLabel = {[P_1] /\ [P_2] /\ ...}
Principals
Principal is a simple string.
Constructors
| MkPrincipal | |
Instances
| Eq Principal | |
| Ord Principal | |
| Read Principal | |
| Show Principal | |
| NewPriv Principal | |
| Singleton Principal | |
| PrettyShow Principal | |
| NewDC Principal Principal | |
| NewDC Principal Label | |
| NewDC Label Principal | |
| ConjunctionOf Principal Principal | |
| ConjunctionOf Principal Label | |
| ConjunctionOf Label Principal | |
| DisjunctionOf Principal Principal | |
| DisjunctionOf Principal Label | |
| DisjunctionOf Label Principal |
Priviliges
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.
Untrusted privileged object, which can be converted to a TCBPriv with
delegatePriv.
class Lattice a => RelaxedLattice a whereSource
Class extending Lattice, by allowing for the more relaxed label
comparison canflowto_p.
Privilege object corresponding to the "root", or all privileges. Any other privilige may be delegated using this privilege object and it must therefore not be exported to untrusted code.
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.
createPrivTCB :: Priv -> TCBPrivSource
This function creates any privilege object given an untrusted
privilege Priv. Note that this function should not be exported
to untrusted code.
class CanActFor a b whereSource
Class used for checking if a computation can use a privilege in place of the other. This notion corresponds to the DLM "can-act-for".
Label/internal operations
and_label :: Label -> Label -> LabelSource
Given two labels, take the union of the disjunctions, i.e., simply perform an "and". Note the new label is not necessarily in LNF.
or_label :: Label -> Label -> LabelSource
Given two labels, perform an "or". Note that the new label is not necessarily in LNF.
Class used to reduce labels to LNF.
It is used to overload the reduce function used by the Label, SLabel,
ILabel, and DCLabel.
Instances
cleanLabel :: Label -> LabelSource
Removes any duplicate principals from categories, and any duplicate categories from the label. To return a clean label, it sorts the label and removes empty disjunctions.