Safe Haskell | Unsafe |
---|
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 "can-flow-to" 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 can-flow-to 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 "can-flow-to 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
- class CreatePrincipal s where
- 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 secrecy-only and integrity-only 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
closed-world 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 closed-world 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 | |
IsString 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 |
class CreatePrincipal s whereSource
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
privilege-hierarchy. 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 un-minted 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 partial-order 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 "can-act-for".
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.