LIO.DCLabel

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 a 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
False
>>> canFlowToP pr dc1 dc2
True

Because the \/ and /\ operators accept strings and Principals as well as CNFs, it is sometimes easy to forget that strings and Principals are not actually CNFs. For example:

>>> "Alice" /\ "Bob" `speaksFor` "Alice" \/ "Bob"
True
>>> "Alice" `speaksFor` "Alice" \/ "Bob"
<interactive>:12:21:
    Couldn't match expected type `[Char]' with actual type `CNF'

To convert a single string or Principal to a CNF, you must use the toCNF method:

>>> toCNF "Alice" `speaksFor` "Alice" \/ "Bob"
True

Top-level aliases and functions

type DC = LIO DCLabel

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

type DCPriv = Priv CNF

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

type DCLabeled = Labeled DCLabel

An alias for Labeled values labeled with a DCLabel.

dcDefaultState :: LIOState DCLabel

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

evalDC :: DC a -> IO a

Wrapper function for running LIO DCLabel computations.

 evalDC dc = evalLIO dc dcDefaultState

tryDC :: DC a -> IO (Either SomeException a, LIOState DCLabel)

DCLabel wrapper for tryLIO:

 tryDC dc = tryLIO dc dcDefaultState

Main types and functions

data Principal

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.

Instances

Eq Principal

Ord Principal

Read Principal

Show Principal

Typeable Principal

ToCNF Principal

principalBS :: ByteString -> Principal

Create a principal from a strict ByteString.

principal :: String -> Principal

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

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.

Constructors

DCLabel

Fields

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.

Instances

Eq DCLabel

Ord DCLabel

Read DCLabel

Show DCLabel

Typeable DCLabel

Label DCLabel

PrivDesc DCLabel CNF

dcPublic :: DCLabel

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

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

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

Compute a conjunction of two CNFs or ToCNF instances.

Has fixity:

 infixr 7 /\

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

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

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.

Instances

Eq CNF

Ord CNF

Read CNF

Show CNF

Typeable CNF

Monoid CNF

SpeaksFor CNF

ToCNF CNF

PrivDesc DCLabel CNF

ToCNF (Priv CNF)

class ToCNF c where

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.

Methods

toCNF :: c -> CNF

Instances

ToCNF Bool

ToCNF CNF

ToCNF Disjunction

ToCNF Principal

ToCNF [Char]

ToCNF (Priv CNF)

Lower-level functions

principalName :: Principal -> ByteString

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

data Disjunction

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

Instances

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 Principal

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

dFromList :: [Principal] -> Disjunction

Convert a list of Principals into a Disjunction.

cTrue :: CNF

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.

cFalse :: CNF

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 Disjunction

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

cFromList :: [Disjunction] -> CNF

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