LIO.DCLabel.Core

This module implements Disjunction Category Labels (DCLabels). DCLabels is a label format for information flow control (IFC) systems. This library exports relevant data types and operations that may be used by dynamic IFC systems such as the LIO library.

A DCLabel is a pair of secrecy and integrity Components (sometimes called category sets). Each Component (or formula) is a conjunction (implemented in terms of Sets) of Clauses (or category) in propositional logic (without negation) specifying a restriction on the flow of information labeled as such. Alternatively, a Component can take on the value DCFalse corresponding to falsehood. Each Clause, in turn, is a disjunction of Principals, , where a Principal is a source of authority of type ByteString, whose meaning is application-specific (e.g., a Principal can be a user name, a URL, etc.).

A clause imposes an information flow restriction. In the case of secrecy, a clause 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 composing a clause are said to own the clause or category.

For information to flow from a source labeled L_1 to a sink L_2, the restrictions imposed by the clauses of L_2 must at least as restrictive as all the restrictions imposed by the clauses 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 component 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, True> ⊑ <P_1, True> because data that can be read by P_1 is more restricting than that readable by P_1 or P_2. Conversely, <True,P_1> ⊑ <True,P_1 ⋁ P_2> because data vouched for by P_1 or P_2 is more permissive than just P_1 (note the same principle holds when writing to sinks with such labeling).

Principals

newtype Principal

A Principal is a simple string representing a source of authority. Any piece of code can create principals, regardless of how untrusted it is.

Constructors

Principal

Fields

principalName :: S8

Get the principal name.

Instances

Eq Principal

Ord Principal

Show Principal

Typeable Principal

Serialize Principal

ToComponent Principal

Convert singleton Principal to Component.

principal :: S8 -> Principal

Principal constructor.

Clauses

newtype Clause

A clause or disjunction category is a set of Principals. Logically the set corresponds to a disjunction of the principals.

Constructors

Clause

Fields

unClause :: Set Principal

Get underlying principal-set.

Instances

Eq Clause

Ord Clause

Show Clause

Typeable Clause

Serialize Clause

ToComponent Clause

Convert singleton Clause to Component.

clause :: Set Principal -> Clause

Clause constructor

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.

data Component

A component is a set of clauses, i.e., a formula (conjunction of disjunction of Principals). DCFalse corresponds to logical False, while DCFormula Set.empty corresponds to logical True.

Constructors

DCFalse

Logical False

DCFormula

Conjunction of disjunction categories

Fields

unDCFormula :: !(Set Clause)

Get underlying clause-set.

Instances

Eq Component

Show Component

Typeable Component

Serialize Component

Serialize components by converting them to maybe's

ToComponent Component

Identity of Component.

MintTCB DCPriv DCPrivDesc

PrivDesc DCPriv DCPrivDesc

dcTrue :: Component

Logical True.

dcFalse :: Component

Logical False.

dcFormula :: Set Clause -> Component

Arbitrary formula from a clause.

isTrue :: Component -> Bool

Is the component True.

isFalse :: Component -> Bool

Is the component False.

Labels

data DCLabel

A DCLabel is a pair of secrecy and integrity Components.

Constructors

DCLabel

Fields

dcSecrecy :: !Component

Extract secrecy component of a label

dcIntegrity :: !Component

Extract integrity component of a label

Instances

Eq DCLabel

Show DCLabel

Typeable DCLabel

Serialize DCLabel

Serialize labels by converting them to pairs of components.

Label DCLabel

LabeledFunctor DCLabel

Priv DCLabel DCPriv

dcLabel :: Component -> Component -> DCLabel

Label constructor. Note that each component is first reduced to CNF.

dcLabelNoReduce :: Component -> Component -> DCLabel

Label contstructor. Note: the components should already be reduced.

dcPub :: DCLabel

Element in the DCLabel lattice corresponding to public data. dcPub = < True, True > . This corresponds to data that is not secret nor trustworthy.

Internal

dcReduce :: Component -> Component

Reduce component to conjunction normal form by removing clauses implied by other.

dcImplies :: Component -> Component -> Bool

Logical implication.

dcAnd :: Component -> Component -> Component

Logical conjunction

dcOr :: Component -> Component -> Component

Logical disjunction