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

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

An alias for Labeled values labeled with a DCLabel.

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

Wrapper function for running LIO DCLabel computations.

evalDC dc = evalLIO dc dcDefaultState

DCLabel wrapper for tryLIO:

tryDC dc = tryLIO dc dcDefaultState

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.

Create a principal from a strict ByteString.

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.

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 dc1 ⊑ dc2) 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 dc2 = (s2 %% i2), and a p::CNF representing privileges, canFlowToP p dc1 dc2 (often written dc1 ⊑ₚ dc2) if and only if (p /\ s2) `speaksFor` s2 && (p /\ i1) `speaksFor` i2.

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 such that (s %% i) ⊑ₛ dcPublic, while i is the exact minimum authority such that dcPublic ⊑ᵢ (s %% i).

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

Compute a conjunction of two CNFs or ToCNF instances.

Has fixity:

infixr 7 /\

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 \/

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.

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.

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

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

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

Convert a list of Principals into a Disjunction.

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; canFlowToP cTrue l1 l2 is equivalent to canFlowTo l1 l2.

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

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.

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

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