lio- Labeled IO Information Flow Control Library

Safe HaskellSafe




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



newtype Principal Source

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




principalName :: S8

Get the principal name.

principal :: S8 -> PrincipalSource

Principal constructor.


newtype Clause Source

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




unClause :: Set Principal

Get underlying principal-set.

clause :: Set Principal -> ClauseSource

Clause constructor


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 Source

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.



Logical False


Conjunction of disjunction categories


unDCFormula :: !(Set Clause)

Get underlying clause-set.


dcTrue :: ComponentSource

Logical True.

dcFalse :: ComponentSource

Logical False.

dcFormula :: Set Clause -> ComponentSource

Arbitrary formula from a clause.

isTrue :: Component -> BoolSource

Is the component True.

isFalse :: Component -> BoolSource

Is the component False.


data DCLabel Source

A DCLabel is a pair of secrecy and integrity Components.




dcSecrecy :: !Component

Extract secrecy component of a label

dcIntegrity :: !Component

Extract integrity component of a label


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

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

dcLabelNoReduce :: Component -> Component -> DCLabelSource

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

dcPub :: DCLabelSource

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


dcReduce :: Component -> ComponentSource

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

dcImplies :: Component -> Component -> BoolSource

Logical implication.

dcAnd :: Component -> Component -> ComponentSource

Logical conjunction

dcOr :: Component -> Component -> ComponentSource

Logical disjunction