lio-0.11.6.0: Labeled IO Information Flow Control Library

Safe HaskellSafe
LanguageHaskell98

LIO.DCLabel

Contents

Description

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

Synopsis

Top-level aliases and functions

type DC = LIO DCLabel Source #

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

type DCPriv = Priv CNF Source #

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

type DCLabeled = Labeled DCLabel Source #

An alias for Labeled values labeled with a DCLabel.

dcDefaultState :: LIOState DCLabel Source #

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

evalDC :: DC a -> IO a Source #

Wrapper function for running LIO DCLabel computations.

evalDC dc = evalLIO dc dcDefaultState

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

DCLabel wrapper for tryLIO:

tryDC dc = tryLIO 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.

Instances

principalBS :: ByteString -> Principal Source #

Create a principal from a strict ByteString.

principal :: String -> Principal Source #

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

dcPublic :: DCLabel Source #

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 infix 6 Source #

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 infixr 7 Source #

Compute a conjunction of two CNFs or ToCNF instances.

Has fixity:

infixr 7 /\

(\/) :: (ToCNF a, ToCNF b) => a -> b -> CNF infixl 7 Source #

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.

Instances

Eq CNF Source # 

Methods

(==) :: CNF -> CNF -> Bool #

(/=) :: CNF -> CNF -> Bool #

Ord CNF Source # 

Methods

compare :: CNF -> CNF -> Ordering #

(<) :: CNF -> CNF -> Bool #

(<=) :: CNF -> CNF -> Bool #

(>) :: CNF -> CNF -> Bool #

(>=) :: CNF -> CNF -> Bool #

max :: CNF -> CNF -> CNF #

min :: CNF -> CNF -> CNF #

Read CNF Source # 
Show CNF Source # 

Methods

showsPrec :: Int -> CNF -> ShowS #

show :: CNF -> String #

showList :: [CNF] -> ShowS #

Monoid CNF Source # 

Methods

mempty :: CNF #

mappend :: CNF -> CNF -> CNF #

mconcat :: [CNF] -> CNF #

SpeaksFor CNF Source # 

Methods

speaksFor :: CNF -> CNF -> Bool Source #

ToCNF CNF Source # 

Methods

toCNF :: CNF -> CNF Source #

PrivDesc DCLabel CNF Source # 
ToCNF (Priv CNF) Source # 

Methods

toCNF :: Priv CNF -> CNF Source #

class ToCNF c where Source #

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.

Minimal complete definition

toCNF

Methods

toCNF :: c -> CNF Source #

Instances

Lower-level functions

principalName :: Principal -> ByteString Source #

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

Instances

dToSet :: Disjunction -> Set Principal Source #

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

dFromList :: [Principal] -> Disjunction Source #

Convert a list of Principals into a Disjunction.

cTrue :: CNF Source #

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 Source #

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 Source #

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

cFromList :: [Disjunction] -> CNF Source #

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