DCLabel.Core

Contents

Description

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

Synopsis

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.

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
Serialize Disj
Owns Disj
PrettyShow Disj
ConjunctionOf String Disj
ConjunctionOf Principal Disj
ConjunctionOf Component Disj
ConjunctionOf Disj String
ConjunctionOf Disj Principal
ConjunctionOf Disj Component
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 ⋁ ...]} Logically '[]' = True.

Constructors

MkConj
Fields conj :: [Disj]

Instances

Eq Conj
Ord Conj
Read Conj
Show Conj
Serialize Conj
PrettyShow Conj

data Component Source

A components is a conjunction of disjunctions, where MkComponentAll is the constructor that is associated with the logical False.

Constructors

MkComponentAll
MkComponent
Fields component :: Conj

Instances

Eq Component	Components have a unique LNF (see `ToLNF`) form, and equality testing is perfomed on labels of this form.
Read Component
Show Component
Serialize Component
Owns Component
ToLNF Component	Reduce a `Component` to LNF. First it applies `cleanComponent` 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 component that implies it.
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 :: Component Source

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 :: Component Source

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.

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:

```
⊥ = <emptyComponent, allComponent>
```
```
⊤ = <allComponent, emptyComponent>
```

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

Methods

toLNF :: a -> aSource

Instances

ToLNF DCLabel	Each `DCLabel` can be reduced a unique label representation in LNF, using the `toLNF` function.
ToLNF Component	Reduce a `Component` to LNF. First it applies `cleanComponent` 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 component that implies it.
ToLNF SLabel
ToLNF ILabel

DC Components

data DCLabel Source

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

Constructors

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

Instances

Eq DCLabel
Read DCLabel
Show DCLabel
Serialize 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: ⊥ = <`emptyComponent`, `allComponent`> ⊤ = <`allComponent`, `emptyComponent`> <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 components or be ignoerd a corresponding privilege (TCBPriv) must be created (by trusted code) or delegated.

Constructors

MkPrincipal
Fields name :: ByteString

Instances

Eq Principal
Ord Principal
Read Principal
Show Principal
Serialize Principal
DisjToFromList Principal	To/from `Principal`s and `Disj`unction categories.
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 -> 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 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 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., Component. A trusted privileged object must be introduced by trusted code, after which trusted privileged objects can be created by delegation.

Constructors

MkTCBPriv
Fields priv :: Component

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 = Component 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 Component
Owns Disj

Component/internal operations

and_component :: Component -> Component -> Component Source

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

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

cleanComponent :: Component -> Component Source

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

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.

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

listToComponent Source

Arguments

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

Given a list of categories, return a component.

componentToList Source

Arguments

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

Given a component return a list of categories.