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