dclabel-eci11-0.3: The Disjunction Category Label Format.

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]
 

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 :: LabelSource

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 :: LabelSource

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

bottomSource

Arguments

:: a

Bottom of lattice, ⊥

topSource

Arguments

:: a

Top of lattice, ⊤

joinSource

Arguments

:: a 
-> a 
-> a

Join of two elements, ⊔

meetSource

Arguments

:: a 
-> a 
-> a

Meet of two elements, ⊓

canflowtoSource

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 Principals and Disjunction 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 -> 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 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
 

type Priv = LabelSource

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

Relaxed partial-order relation

noPriv :: TCBPrivSource

Privilege object corresponding to no privileges.

rootPrivTCB :: TCBPrivSource

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

Methods

canDelegate :: a -> b -> BoolSource

Can use first privilege in place of second.

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

Checks if category restriction can be bypassed given the privilege.

Instances

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:

class DisjToFromList a whereSource

Class used to convert list of principals to a disjunction category and vice versa.

Methods

listToDisjSource

Arguments

:: [a] 
-> Disj

Given list return category.

disjToListSource

Arguments

:: Disj 
-> [a]

Given category return list.

Instances

DisjToFromList String

To/from Strings and Disjunction categories.

DisjToFromList Principal

To/from Principals and Disjunction categories.

listToLabelSource

Arguments

:: [Disj] 
-> Label

Given list return category.

Given a list of categories, return a label.

labelToListSource

Arguments

:: Label 
-> [Disj]

Given category return list.

Given a label return a list of categories.