This module implements Disjunction Category labels.
A DCLabel is a pair of secrecy
and integrity
category sets (of type Label
).
A category set (of type Conj
) is a conjunction of categories (of type Disj
).
Each category, in turn, is a disjunction of Principal
s, where a Principal
is just a String
whose meaning is up to the application.
A category imposes an information flow restriction. In the case of secrecy, a category restricts who can read, receive, or propagate the information, while in the case of integrity it restricts who can modify a piece of data. The principals constructing a category are said to own the category.
For information to flow from a source labeled L_1
to a sink L_2
, the
restrictions imposed by the categories of L_2
must at least as restrictive as
all the restrictions imposed by the categories of L_1
(hence the conjunction)
in the case of secrecy, and at least as permissive in the case of integrity.
More specifically, for information to flow from L_1
to L_2
,
the labels must satisfy the "canflowto" relation: L_1 ⊑ L_2
.
The ⊑ label check is implemented by the canflowto
function.
For labels L_1=<S_1, I_1>
, L_2=<S_2, I_2>
the canflowto relation is
satisfied if the secrecy category set S_2
implies
S_1
and I_1
implies
I_2
(recall that a category set is a conjunction of
disjunctions of principals).
For example, <{[P_1 ⋁ P_2]},{}> ⊑ <{[P_1]},{}>
because data
that can be read by P_1
is more restricting than that readable by P_1
or
P_2
. Conversely, <{{},[P_1]}> ⊑ <{},[P_1 ⋁ P_2]},{}>
because
data vouched for by P_1
or P_2
is more permissive than just P_1
(note
the same idea holds when writing to sinks with such labeling).
A piece of a code running with a privilege object (of type TCBPriv
), i.e.,
owning a Principal
confers the right to modify
labels by removing any secrecy
categories containing that Principal
and
adding any integrity
categories containing the Principal
(hence the name disjunction categories: the category [P1 ⋁ P2]
can be
downgraded by either Principal
P1
or P2
).
More specifically, privileges can be used to bypass information flow restrictions
by using the more permissive "canflowto given permission"
relation:⊑ᵨ. The label check function implementing this restriction
is canflowto_p
, taking an additional argument (of type TCBPriv
). For
example, if
L_1=<{[P_1 ⋁ P_2] ⋀ [P_3]},{}>
, and L_2=<{[P_1]},{}>
, then
L_1 ⋢ L_2
, but given a privilege object corresponding to [P_3]
the
L_1 ⊑ᵨ L_2
holds.
To construct DC labels and privilege objects the constructors exported by this module may be used, but we strongly suggest using DCLabel.NanoEDSL as exported by DCLabel.TCB and DCLabel.Safe. The former is to be used by trusted code only, while the latter module should be imported by untrusted code as it prevents the creation of arbitrary privileges.
 newtype Disj = MkDisj {}
 newtype Conj = MkConj {}
 data Label
 = MkLabelAll
  MkLabel { }
 emptyLabel :: Label
 allLabel :: Label
 class Eq a => Lattice a where
 class ToLNF a where
 toLNF :: a > a
 data DCLabel = MkDCLabel {}
 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 CanDelegate a b where
 canDelegate :: a > b > Bool
 class Owns a where
 and_label :: Label > Label > Label
 or_label :: Label > Label > Label
 cleanLabel :: Label > Label
 implies :: Label > Label > Bool
 class DisjToFromList a where
 listToDisj :: [a] > Disj
 disjToList :: Disj > [a]
 listToLabel :: [Disj] > Label
 labelToList :: Label > [Disj]
Labels
A label is a conjunction of disjunctions of principals. A DCLabel
is simply a
pair of such labels. Hence, we define almost all operations in terms of this
construct, from which the DCLabel
implementation follows almost trivially.
Moreover, we note that secrecyonly and integrityonly labels are implemented
in DCLabel.Secrecy and DCLabel.Integrity, respectively.
A category, i.e., disjunction, of Principal
s.
The empty list '[]' corresponds to the disjunction of all principals.
Conceptually, [] = [P_1 ⋁ P_2 ⋁ ...]
A category set, i.e., a conjunction of disjunctions.
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.
Eq Label  Labels have a unique LNF (see 
Read Label  
Show Label  
Owns Label  
ToLNF Label  Reduce a 
NewPriv Label  
PrettyShow Label  
CanDelegate Priv Priv  
CanDelegate Priv TCBPriv  
CanDelegate 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  
ConjunctionOf Label Disj  
ConjunctionOf Disj Label  
DisjunctionOf String Label  
DisjunctionOf Principal Label  
DisjunctionOf Label String  
DisjunctionOf Label Principal  
DisjunctionOf Label Label 
A label without any disjunctions or conjunctions. This label, conceptually
corresponds to the label consisting of a single category containing all
principals. 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. Conceptually,
allLabel = <{[P_1] ⋀ [P_2] ⋀ ...}>
class Eq a => Lattice a whereSource
Labels forma a partial order according to the ⊑ relation.
Specifically, this means that for any two labels L_1
and L_2
there is a
unique label L_3 = L_1 ⊔ L_2
, known as the join, such that
L_1 ⊑ L_3
and L_2 ⊑ L_3
. Similarly, there is a unique label
L_3' = L_1 ⊓ L_2
, known as the meet, such that
L_3 ⊑ L_1
and L_3 ⊑ L_2
. This class defines a bounded
lattice, which further requires the definition of the bottom ⊥ and
top ⊤ elements of the lattice, such that ⊥ ⊑ L
and
L ⊑ ⊤
for any label L
.
:: a  Bottom of lattice, ⊥ 
:: a  Top of lattice, ⊤ 
:: a  
> a  
> a  Join of two elements, ⊔ 
:: a  
> a  
> a  Meet of two elements, ⊓ 
:: a  
> a  
> Bool  Partial order relation, ⊑ 
Class used to reduce labels to a unique label normal form (LNF), which
corresponds to conjunctive normal form of principals. We use this class
to overload the reduce function used by the Label
, DCLabel
, etc.
ToLNF DCLabel  Each 
ToLNF Label  Reduce a 
ToLNF SLabel  
ToLNF ILabel 
DC Labels
A DCLabel
is a pair of secrecy and integrity category sets, i.e.,
a pair of Label
s.
Eq DCLabel  
Read DCLabel  
Show DCLabel  
RelaxedLattice DCLabel  
ToLNF DCLabel  Each 
Lattice DCLabel  Elements of

PrettyShow DCLabel 
Principals
Principal is a simple string representing a source of authority. Any piece
of code can create principals, regarless of how untrusted it is. However,
for principals to be used in integrity labels or be ignoerd a corresponding
privilege (TCBPriv
) must be created (by trusted code) or delegated.
Eq Principal  
Ord Principal  
Read Principal  
Show Principal  
DisjToFromList Principal  
NewPriv Principal  
Singleton Principal  
PrettyShow Principal  
NewDC Principal Principal  
NewDC Principal Label  
NewDC Label Principal  
ConjunctionOf Principal Principal  
ConjunctionOf Principal Label  
ConjunctionOf Principal Disj  
ConjunctionOf Label Principal  
ConjunctionOf Disj Principal  
DisjunctionOf Principal Principal  
DisjunctionOf Principal Label  
DisjunctionOf Label Principal 
Privileges
As previously mentioned privileges allow a piece of code to bypass certain
information flow restrictions. Like principals, privileges of type Priv
may be created by any piece of code. A privilege is simply a conjunction of
disjunctions, i.e., a Label
where a category consisting of a single principal
corresponds to the notion of owning that principal. We, however, allow for
the more general notion of ownership of a category as to create a
privilegehierarchy. Specifically, a piece of code exercising a privilege P
can always exercise privilege P'
(instead), if P' => P
. This is similar to
the DLM notion of "can act for", and, as such, we provide a function which
tests if one privilege may be use in pace of another: canDelegate
.
Note that the privileges form a partial order over =>
, such that
and rootPrivTCB
=> PP =>
for any privilege noPriv
P
.
As such we have a privilege hierarchy which can be concretely built through
delegation, with rootPrivTCB
corresponding to the root, or all, privileges
from which all others may be created. More specifically, given a minted privilege
P'
of type TCBPriv
, and an unminted privilege P
of type Priv
, any
piece of code can use delegatePriv
to mint P
, assuming P' => P
.
Finally, given a set of privileges a piece of code can check if it owns a
category using the owns
function.
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.
Eq TCBPriv  
Show TCBPriv  
Monoid TCBPriv 

PrettyShow TCBPriv  
CanDelegate Priv TCBPriv  
CanDelegate TCBPriv Priv  
CanDelegate TCBPriv TCBPriv 
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
.
canflowto_p :: TCBPriv > a > a > BoolSource
Relaxed partialorder relation
Privilege object corresponding to the "root", or all privileges. Any other privilege may be delegated using this privilege object and it must therefore not be exported to untrusted code.
delegatePriv :: TCBPriv > Priv > Maybe TCBPrivSource
Given trusted privilege and a "desired" untrusted privilege, return a trusted version of the untrusted privilege, if the provided (trusted) privilege 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 CanDelegate a b whereSource
Class used for checking if a computation can use a privilege in place of the other. This notion is similar to the DLM "canactfor".
canDelegate :: a > b > BoolSource
Can use first privilege in place of second.
We say a TCBPriv
privilege object owns a category when the privileges
allow code to bypass restrictions implied by the category. This is the
case if and only if the TCBPriv
object contains one of the Principal
s
in the Disj
. This class is used to check ownership
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.
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.
implies :: Label > Label > BoolSource
Determines if a label implies (in the logical sense) another label. In other words, d_1 ⋀ ... ⋀ d_n => d_1' ⋀ ... ⋀ d_n'.
Properties:
 ∀ X,
allLabel
`implies
` X := True  ∀ X≠
allLabel
, X `implies
`allLabel
:= False  ∀ X, X `
implies
`emptyLabel
:= True  ∀ X≠
emptyLabel
,emptyLabel
`implies
` X := False
class DisjToFromList a whereSource
Class used to convert list of principals to a disjunction category and vice versa.
Given a list of categories, return a label.
Given a label return a list of categories.