Safe Haskell  Safe 

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 Component
s
(sometimes called category sets). Each Component
(or formula) is a
conjunction (implemented in terms of Set
s) of Clause
s (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 Principal
s,
, where a Principal
is a source of authority of type ByteString
,
whose meaning is applicationspecific (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 "canflowto" 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 canflowto 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 = Principal {
 principalName :: S8
 principal :: S8 > Principal
 newtype Clause = Clause {}
 clause :: Set Principal > Clause
 data Component
 = DCFalse
  DCFormula {
 unDCFormula :: !(Set Clause)
 dcTrue :: Component
 dcFalse :: Component
 dcFormula :: Set Clause > Component
 isTrue :: Component > Bool
 isFalse :: Component > Bool
 data DCLabel = DCLabel {
 dcSecrecy :: !Component
 dcIntegrity :: !Component
 dcLabel :: Component > Component > DCLabel
 dcLabelNoReduce :: Component > Component > DCLabel
 dcPub :: DCLabel
 dcReduce :: Component > Component
 dcImplies :: Component > Component > Bool
 dcAnd :: Component > Component > Component
 dcOr :: Component > Component > Component
Principals
A Principal
is a simple string representing a source of
authority. Any piece of code can create principals, regardless of how
untrusted it is.
Principal  

Clauses
A clause or disjunction category is a set of Principal
s.
Logically the set corresponds to a disjunction of the principals.
Components
A Component
is a conjunction of disjunctions of Principal
s. A
DCLabel
is simply a pair of such Component
s. Hence, we define
almost all operations in terms of this construct, from which the
DCLabel
implementation follows almost trivially.
A component is a set of clauses, i.e., a formula (conjunction of
disjunction of Principal
s). DCFalse
corresponds to logical
False
, while DCFormula Set.empty
corresponds to logical True
.
DCFalse  Logical 
DCFormula  Conjunction of disjunction categories 

Labels
A DCLabel
is a pair of secrecy and integrity Component
s.
DCLabel  

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