lio- Labeled IO Information Flow Control Library

Safe HaskellTrustworthy




Disjunction Category Labels (DCLabels) are a label format that encodes authority, secrecy restrictions, and integrity properties using propositional logic.

A DCLabel consists of two boolean formulas over Principals. Each formula is in conjunctive normal form, represented by type CNF. The first CNF (dcSecrecy) specifies what combinations of principals are allowed to make data public. The second CNF (dcIntegrity) specifies which combinations of principals have endorsed the integrity of the data.

The %% operator allows one to construct a DCLabel by joining a secrecy CNF on the left with an integrity CNF on the right. A DCLabel can also be directly constructed with the constructor DCLabel. However, %% has the added convenience of accepting any argument types that are instances of ToCNF.

For example, the following expresses data that can be exported by the principal "Alice" and may have been written by anybody: "Alice" %% True. (toCNF True indicates a trivially satisfiable label component, which in this case means a label conveying no integrity properties.)

A CNF is created using the (\/) and (/\) operators. The disjunction operator (\/) is used to compute a CNF equivalent to the disjunciton of two Principals, Strings, or CNFs. For example:

p1 = principal "p1"
p2 = principal "p2"
p3 = principal "p3"
e1 = p1 \/ p2
e2 = e1 \/ "p4"

Similarly, the conjunction operator (/\) creates CNF as a conjunction of Principals, Strings, Disjunctions, or CNFs.

e3 = p1 \/ p2
e4 = e1 /\ "p4" /\ p3

Note that because a CNF formula is stored as a conjunction of Disjunctions, it is much more efficient to apply /\ to the result of \/ than vice versa. It would be logical for /\ to have higher fixity than \/. Unfortunately, this makes formulas harder to read (given the convention of AND binding more tightly than OR). Hence \/ and /\ have been given the same fixity but different associativities, preventing the two from being mixed in the same expression without explicit parentheses.

Consider the following, example:

cnf1 = ("Alice" \/ "Bob") /\ "Carla"
cnf2 = "Alice" /\ "Carla"
dc1 = cnf1 %% cnf2
dc2 = "Djon" %% "Alice"
pr = PrivTCB $ "Alice" /\ "Carla"

This will result in the following:

>>> dc1
"Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla"
>>> dc2
"Djon" %% "Alice"
>>> canFlowTo dc1 dc2
>>> canFlowToP pr dc1 dc2


Top-level aliases and functions

type DC = LIO DCLabelSource

The main monad type alias to use for LIO computations that are specific to DCLabels.

type DCPriv = Priv CNFSource

DCLabel privileges are expressed as a CNF of the principals whose authority is being exercised.

type DCLabeled = Labeled DCLabelSource

An alias for Labeled values labeled with a DCLabel.

dcDefaultState :: LIOState DCLabelSource

A common default starting state, where lioLabel = dcPublic and lioClearance = False %% True (i.e., the highest possible clearance).

evalDC :: DC a -> IO aSource

Wrapper function for running LIO DCLabel computations.

 evalDC dc = evalLIO dc dcDefaultState

Main types and functions

data Principal Source

A Principal is a primitive source of authority, represented as a string. The interpretation of principal strings is up to the application. Reasonable schemes include encoding user names, domain names, and/or URLs in the Principal type.

principalBS :: ByteString -> PrincipalSource

Create a principal from a strict ByteString.

principal :: String -> PrincipalSource

Create a principal from a String. The String is packed into a ByteString using fromString, which will almost certainly give unexpected results for non-ASCII unicode code points.

data DCLabel Source

Main DCLabel type. DCLabels use CNF boolean formulas over principals to express authority exercised by a combination of principals. A DCLabel contains two CNFs. One, dcSecrecy, specifies the minimum authority required to make data with the label completely public. The second, dcIntegrity, expresses the minimum authority that was used to endorse data with the label, or, for mutable objects, the minimum authority required to modify the object.

DCLabels are more conveniently expressed using the %% operator, with dcSecrecy on the left and dcIntegrity on the right, i.e.: (dcSecrecyValue %% dcIntegrityValue).

DCLabels enforce the following relations:

  • If cnf1 and cnf2 are CNFs describing authority, then cnf1 `speaksFor` cnf2 if and only if cnf1 logically implies cnf2 (often written cnf1 ⟹ cnf2). For example, ("A" /\ "B") `speaksFor` toCNF "A", while toCNF "A" `speaksFor` ("A" \/ "C").
  • Given two DCLabels dc1 = (s1 %% i1) and dc2 = (s2 %% i2), dc1 `canFlowTo` dc2 (often written dc1dc2) if and only if s2 `speaksFor` s1 && i1 `speaksFor` i2. In other words, data can flow in the direction of requiring more authority to make it public or removing integrity endorsements.
  • Given two DCLabels dc1 = (s1 %% i1) and dc 2 = (s2 %% i2), and a p::CNF representing privileges, canFlowToPrivDesc p dc1 dc2 (often written dc1 ⊑ₚ dc2) if and only if (p /\ s2) `speaksFor` s2 && (p /\ i1) `speaksFor` i2.




dcSecrecy :: !CNF

Describes the authority required to make the data public.

dcIntegrity :: !CNF

Describes the authority with which immutable data was endorsed, or the authority required to modify mutable data.

dcPublic :: DCLabelSource

 dcPublic = True %% True

This label corresponds to public data with no integrity guarantees. For instance, an unrestricted Internet socket should be labeled dcPublic. The significance of dcPublic is that given data labeled (s %% i), s is the exact minimum authority required to transition the data to dcPublic. Conversely, given data labeled dcPublic, i is the exact authority required to transition the data to (s %% i) (assuming sufficient clearance).

(%%) :: (ToCNF a, ToCNF b) => a -> b -> DCLabelSource

The primary way of creating a DCLabel. The secrecy component goes on the left, while the integrity component goes on the right, e.g.:

 label = secrecyCNF %% integrityCNF

Unlike the DCLabel constructor, the arguments can be any instance of ToCNF. %% has fixity:

 infix 6 %%

(/\) :: (ToCNF a, ToCNF b) => a -> b -> CNFSource

Compute a conjunction of two CNFs or ToCNF instances.

Has fixity:

 infixr 7 /\

(\/) :: (ToCNF a, ToCNF b) => a -> b -> CNFSource

Compute a disjunction of two CNFs or ToCNF instances. Note that this can be an expensive operation if the inputs have many conjunctions.

The fixity is specifically chosen so that \/ and /\ cannot be mixed in the same expression without parentheses:

 infixl 7 \/

data CNF Source

A boolean formula in Conjunctive Normal Form. CNF is used to describe DCLabel privileges, as well to provide each of the two halves of a DCLabel.

class ToCNF c whereSource

As a type, a CNF is always a conjunction of Disjunctions of Principals. However, mathematically speaking, a single Principal or single Disjunction is also a degenerate example of conjunctive normal form. Class ToCNF abstracts over the differences between these types, promoting them all to CNF.


toCNF :: c -> CNFSource

Lower-level functions

principalName :: Principal -> ByteStringSource

Extract the name of a principal as a strict ByteString. (Use show to get it as a regular String.)

data Disjunction Source

Represents a disjunction of Principals, or one clause of a CNF. There is generally not much need to work directly with Disjunctions unless you need to serialize and de-serialize them (by means of dToSet and dFromList).


Eq Disjunction 
Ord Disjunction 
Read Disjunction

Note that a disjunction containing more than one element must be surrounded by parentheses to parse correctly.

Show Disjunction 
Typeable Disjunction 
Monoid Disjunction 
ToCNF Disjunction 

dToSet :: Disjunction -> Set PrincipalSource

Expose the set of Principals being ORed together in a Disjunction.

dFromList :: [Principal] -> DisjunctionSource

Convert a list of Principals into a Disjunction.

cTrue :: CNFSource

A CNF that is always True--i.e., trivially satisfiable. When dcSecrecy = cTrue, it means data is public. When dcIntegrity = cTrue, it means data carries no integrity guarantees. As a description of privileges, cTrue conveys no privileges; canFlowToPrivDesc cTrue l1 l2 is equivalent to canFlowTo l1 l2.

Note that toCNF True = cTrue. Hence dcPublic = DCLabel cTrue cTrue.

cFalse :: CNFSource

A CNF that is always False. If dcSecrecy = cFalse, then no combination of principals is powerful enough to make the data public. For that reason, cFalse generally shouldn't appear in a data label. However, it is convenient to include as the dcSecrecy component of lioClearance to indicate a thread may arbitrarily raise its label.

dcIntegrity = cFalse indicates impossibly much integrity--i.e., data that no combination of principals is powerful enough to modify or have created. Generally this is not a useful concept.

As a privilege description, cFalse indicates impossibly high privileges (i.e., higher than could be achieved through any combination of Principals). cFalse `speaksFor` p for any CNF p. This can be a useful concept for bootstrapping privileges within the DC monad itself. For instance, the result of privInit cFalse can be passed to fully-trusted DC code, which can in turn use delegate to create arbitrary finite privileges to pass to less privileged code.

cToSet :: CNF -> Set DisjunctionSource

Convert a CNF to a Set of Disjunctions. Mostly useful if you wish to serialize a DCLabel.

cFromList :: [Disjunction] -> CNFSource

Convert a list of Disjunctions into a CNF. Mostly useful if you wish to de-serialize a CNF.