DCLabel.Core

Contents

Description

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 Principals, 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 "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.

Synopsis

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 secrecy-only and integrity-only labels are implemented in DCLabel.Secrecy and DCLabel.Integrity, respectively.

newtype Disj Source

A category, i.e., disjunction, of Principals. The empty list '[]' corresponds to the disjunction of all principals. Conceptually, [] = [P_1 ⋁ P_2 ⋁ ...]

Constructors

MkDisj
Fields disj :: [Principal]

Instances

Eq Disj
Ord Disj
Read Disj
Show Disj
Owns Disj
PrettyShow Disj
ConjunctionOf String Disj
ConjunctionOf Principal Disj
ConjunctionOf Label Disj
ConjunctionOf Disj String
ConjunctionOf Disj Principal
ConjunctionOf Disj Label
ConjunctionOf Disj Disj	Instances using disjunctions.

newtype Conj Source

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 ⋁ ...]}

Constructors

MkConj
Fields conj :: [Disj]

Instances

Eq Conj
Ord Conj
Read Conj
Show Conj
PrettyShow Conj

data Label Source

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
Fields label :: Conj

Instances

Eq Label	Labels have a unique LNF (see `ToLNF`) form, and equality testing is perfomed on labels of this form.
Read Label
Show Label
Owns Label
ToLNF Label	Reduce a `Label` to LNF. First it applies `cleanLabel` to remove duplicate principals and categories. Following, it removes extraneous/redundant categories. A category is said to be extraneous if there is another category in the label that implies it.
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

emptyLabel :: Label Source

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 ⋁ ...]}>

allLabel :: Label Source

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.

Methods

bottom Source

Arguments

:: a	Bottom of lattice, ⊥

top Source

Arguments

:: a	Top of lattice, ⊤

join Source

Arguments

:: a
-> a
-> a	Join of two elements, ⊔

meet Source

Arguments

:: a
-> a
-> a	Meet of two elements, ⊓

canflowto Source

Arguments

:: a
-> a
-> Bool	Partial order relation, ⊑

Instances

Lattice DCLabel

Elements of DCLabel form a bounded lattice, where:

```
⊥ = <emptyLabel, allLabel>
```
```
⊤ = <allLabel, emptyLabel>
```

 <S_1, I_1> ⊔ <S_2, I_2> = <S_1 ⋀ S_2, I_1 ⋁ I_2>

 <S_1, I_1> ⊓ <S_2, I_2> = <S_1 ⋁ S_2, I_1 ⋀ I_2>

 <S_1, I_1> ⊑ <S_2, I_2> = S_2 => S_1 ⋀ I_1 => I_2

Lattice SLabel

Lattice ILabel

class ToLNF a whereSource

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.

Methods

toLNF :: a -> aSource

Instances

ToLNF DCLabel	Each `DCLabel` can be reduced a unique label representation in LNF, using the `toLNF` function.
ToLNF Label	Reduce a `Label` to LNF. First it applies `cleanLabel` to remove duplicate principals and categories. Following, it removes extraneous/redundant categories. A category is said to be extraneous if there is another category in the label that implies it.
ToLNF SLabel
ToLNF ILabel

DC Labels

data DCLabel Source

A DCLabel is a pair of secrecy and integrity category sets, i.e., a pair of Labels.

Constructors

MkDCLabel
Fields secrecy :: Label Integrity category set. integrity :: Label Secrecy category set.

Instances

Eq DCLabel
Read DCLabel
Show DCLabel
RelaxedLattice DCLabel
ToLNF DCLabel	Each `DCLabel` can be reduced a unique label representation in LNF, using the `toLNF` function.
Lattice DCLabel	Elements of `DCLabel` form a bounded lattice, where: ⊥ = <`emptyLabel`, `allLabel`> ⊤ = <`allLabel`, `emptyLabel`> <S_1, I_1> ⊔ <S_2, I_2> = <S_1 ⋀ S_2, I_1 ⋁ I_2> <S_1, I_1> ⊓ <S_2, I_2> = <S_1 ⋁ S_2, I_1 ⋀ I_2> <S_1, I_1> ⊑ <S_2, I_2> = S_2 => S_1 ⋀ I_1 => I_2
PrettyShow DCLabel

Principals

newtype Principal Source

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.

Constructors

MkPrincipal
Fields name :: String

Instances

Eq Principal
Ord Principal
Read Principal
Show Principal
DisjToFromList Principal	To/from `Principal`s and `Disj`unction categories.
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

principal :: String -> Principal Source

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 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 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 rootPrivTCB => P and P => noPriv for any privilege 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.

data TCBPriv Source

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.

Constructors

MkTCBPriv
Fields priv :: Label

Instances

Eq TCBPriv
Show TCBPriv
Monoid TCBPriv	`TCBPriv` is an instance of `Monoid`.
PrettyShow TCBPriv
CanDelegate Priv TCBPriv
CanDelegate TCBPriv Priv
CanDelegate TCBPriv TCBPriv

type Priv = Label Source

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.

Methods

canflowto_p :: TCBPriv -> a -> a -> Bool Source

Relaxed partial-order relation

Instances

RelaxedLattice DCLabel
RelaxedLattice SLabel
RelaxedLattice ILabel

noPriv :: TCBPriv Source

Privilege object corresponding to no privileges.

rootPrivTCB :: TCBPriv Source

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 TCBPriv Source

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 -> TCBPriv Source

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".

Methods

canDelegate :: a -> b -> Bool Source

Can use first privilege in place of second.

Instances

CanDelegate Priv Priv
CanDelegate Priv TCBPriv
CanDelegate TCBPriv Priv
CanDelegate TCBPriv TCBPriv

class Owns a whereSource

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 Principals in the Disj. This class is used to check ownership

Methods

owns :: TCBPriv -> a -> Bool Source

Checks if category restriction can be bypassed given the privilege.

Instances

Owns Label
Owns Disj

Label/internal operations

and_label :: Label -> Label -> Label Source

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 -> Label Source

Given two labels, perform an "or". Note that the new label is not necessarily in LNF.

cleanLabel :: Label -> Label Source

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 -> Bool Source

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.

Methods

listToDisj Source

Arguments

:: [a]
-> Disj	Given list return category.

disjToList Source

Arguments

:: Disj
-> [a]	Given category return list.

Instances

DisjToFromList String	To/from `String`s and `Disj`unction categories.
DisjToFromList Principal	To/from `Principal`s and `Disj`unction categories.

listToLabel Source

Arguments

:: [Disj]
-> Label	Given list return category.

Given a list of categories, return a label.

labelToList Source

Arguments

:: Label
-> [Disj]	Given category return list.

Given a label return a list of categories.