This module implements Disjunction Category Labels.
A DCLabel is a pair of secrecy
and integrity
category sets or
components, of type Component
. Each component is simply a set of
clauses in propositional logic (without negation). A component
can either correspond to the term MkComponentAll
, representing
falsehood, or a set of categories (clauses): (of type Conj
)
corresponding to the conjunction of ategories (of type Disj
).
Each category, in turn, is a disjunction of Principal
s, where
a Principal
is just a ByteString
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 Component
 = MkComponentAll
  MkComponent { }
 emptyComponent :: Component
 allComponent :: Component
 class Eq a => Lattice a where
 class ToLNF a where
 toLNF :: a > a
 data DCLabel = MkDCLabel {}
 newtype Principal = MkPrincipal {
 name :: ByteString
 principal :: ByteString > Principal
 data TCBPriv = MkTCBPriv {}
 type Priv = Component
 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_component :: Component > Component > Component
 or_component :: Component > Component > Component
 cleanComponent :: Component > Component
 implies :: Component > Component > Bool
 class DisjToFromList a where
 listToDisj :: [a] > Disj
 disjToList :: Disj > [a]
 listToComponent :: [Disj] > Component
 componentToList :: Component > [Disj]
Components
A component is a conjunction of disjunctions of principals. A
DCLabel
is simply a pair of such components. 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 ⋁ ...]}
Logically '[]' = True
.
A components is a conjunction of disjunctions, where MkComponentAll
is
the constructor that is associated with the logical False
.
Eq Component  Components have a unique LNF (see 
Read Component  
Show Component  
Serialize Component  
Owns Component  
ToLNF Component  Reduce a 
NewPriv Component  
PrettyShow Component  
CanDelegate Priv Priv  
CanDelegate Priv TCBPriv  
CanDelegate TCBPriv Priv  
NewDC String Component  
NewDC Principal Component  
NewDC Component String  
NewDC Component Principal  
NewDC Component Component  
ConjunctionOf String Component  
ConjunctionOf Principal Component  
ConjunctionOf Component String  
ConjunctionOf Component Principal  
ConjunctionOf Component Component  
ConjunctionOf Component Disj  
ConjunctionOf Disj Component  
DisjunctionOf String Component  
DisjunctionOf Principal Component  
DisjunctionOf Component String  
DisjunctionOf Component Principal  
DisjunctionOf Component Component 
emptyComponent :: ComponentSource
A component without any disjunctions or conjunctions. This
component, conceptually corresponds to the label consisting of
a single category containing all principals. Conceptually (in a
closedworld system),
emptyComponent = <{[P_1 ⋁ P_2 ⋁ ...]}>
.
Logically, of course, this is equivalent to True
.
allComponent :: ComponentSource
The dual of emptyComponent
, allComponent
consists of the conjunction of
all possible disjunctions, i.e., it is the label that implies all
other labels. Conceptually (in a closedworld system),
allComponent = <{[P_1] ⋀ [P_2] ⋀ ...}>
Logically, of course, this is equivalent to False
.
class Eq a => Lattice a whereSource
Labels form 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, ⊑ 
Lattice DCLabel  Elements of

Lattice SLabel  
Lattice ILabel 
Class used to reduce labels and components to 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 Component
,
DCLabel
, etc.
ToLNF DCLabel  Each 
ToLNF Component  Reduce a 
ToLNF SLabel  
ToLNF ILabel 
DC Components
A DCLabel
is a pair of secrecy and integrity category sets, i.e.,
a pair of Component
s.
Eq DCLabel  
Read DCLabel  
Show DCLabel  
Serialize 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 components or be ignoerd a
corresponding privilege (TCBPriv
) must be created (by trusted code) or
delegated.
Eq Principal  
Ord Principal  
Read Principal  
Show Principal  
Serialize Principal  
DisjToFromList Principal  
NewPriv Principal  
Singleton Principal  
PrettyShow Principal  
NewDC Principal Principal  
NewDC Principal Component  
NewDC Component Principal  
ConjunctionOf Principal Principal  
ConjunctionOf Principal Component  
ConjunctionOf Principal Disj  
ConjunctionOf Component Principal  
ConjunctionOf Disj Principal  
DisjunctionOf Principal Principal  
DisjunctionOf Principal Component  
DisjunctionOf Component Principal 
principal :: ByteString > PrincipalSource
Generates a principal from an string.
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 Component
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., Component
.
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
Component/internal operations
and_component :: Component > Component > ComponentSource
Given two components, take the union of the disjunctions, i.e., simply perform an "and". Note the new component is not necessarily in LNF.
or_component :: Component > Component > ComponentSource
Given two components, perform an "or". Note that the new component is not necessarily in LNF.
cleanComponent :: Component > ComponentSource
Removes any duplicate principals from categories, and any duplicate categories from the component. To return a clean component, it sorts the component and removes empty disjunctions.
implies :: Component > Component > BoolSource
Determines if a component logically implies another component. In other words, d_1 ⋀ ... ⋀ d_n => d_1' ⋀ ... ⋀ d_n'.
Properties:
 ∀ X,
allComponent
`implies
` X := True  ∀ X≠
allComponent
, X `implies
`allComponent
:= False  ∀ X, X `
implies
`emptyComponent
:= True  ∀ X≠
emptyComponent
,emptyComponent
`implies
` X := False
class DisjToFromList a whereSource
Class used to convert list of principals to a disjunction category and vice versa.
DisjToFromList String  
DisjToFromList ByteString  To/from 
DisjToFromList Principal 
Given a list of categories, return a component.
Given a component return a list of categories.