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.
- join :: Lattice a => a -> a -> a
- meet :: Lattice a => a -> a -> a
- top :: Lattice a => a
- bottom :: Lattice a => a
- canflowto :: Lattice a => a -> a -> Bool
- data Label
- data DCLabel
- secrecy :: DCLabel -> Label
- integrity :: DCLabel -> Label
- principal :: String -> Principal
- (.\/.) :: DisjunctionOf a b => a -> b -> Label
- (./\.) :: ConjunctionOf a b => a -> b -> Label
- (<>) :: Label
- (><) :: Label
- newDC :: NewDC a b => a -> b -> DCLabel
- data TCBPriv
- type Priv = Label
- canflowto_p :: RelaxedLattice a => TCBPriv -> a -> a -> Bool
- delegatePriv :: TCBPriv -> Priv -> Maybe TCBPriv
- canActFor :: CanActFor a b => a -> b -> Bool
- newPriv :: NewPriv a => a -> Priv
- newTCBPriv :: NewPriv a => TCBPriv -> a -> Maybe TCBPriv
DC Labels with EDSL
A label is a conjunction of disjunctions, where
the constructor that is associated with the conjunction of all
Reduce a label to LNF.
First it applies
|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|
A DC label for secrecy and integrity.
Privilege object is just a conjunction of disjunctions, i.e., a
A trusted privileged object must be introduced by trusted code, after which
trusted privileged objects can be created by delegation.
Given trusted privilige and a "desired" untrusted privilege, return a trusted version of the untrusted privilige, if the provided (trusted) privilige implies it.
Given element create privilege.
Given element create (maybe) trusted privileged object.