LIO.DCLabel.DSL

This module implements a simple, embedded domain specific language to create Components, privilage descriptions and labels from conjunctions of principal disjunctions.

A DCLabel consists of a secrecy Component and an integrity Component. The %% operator allows one to construct a DCLabel by joining a secrecy Component (on the left) with an integrity Component on the right. This is similar to dcLabel, except that the arguments can also be instances of ToComponent. For example, the following expresses data that can be exported by the principal "Alice" and written by anybody: "Alice" %% True. (The component True or dcTrue indicates a trivially satisfiable label component, which in this case means a label with no integrity guarantees.)

A Component or DCPrivDesc is created using the (\/) and (/\) operators. The disjunction operator (\/) is used to create a Clause from Principals, ByteStrings, or a disjunctive sub-expression. For example:

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

Similarly, the conjunction operator (/\) is used to create category-sets from Principals, ByteStrings, and conjunctive or disjunctive sub-expressions. For example:

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

Note that because a clause consists of a disjunction of principals, and a component is composed of the conjunction of categories, (\/) binds more tightly than (/\).

Given two Components, one for secrecy and one for integrity, you can create a DCLabel with dcLabel. Given a DCPriv and DCPrivDesc you can create a new minted privilege with dcDelegatePriv.

Consider the following, example:

l1 = "Alice" \/ "Bob" /\ "Carla"
l2 = "Alice" /\ "Carla"
dc1 = dcLabel l1 l2
dc2 = dcLabel (toComponent "Djon") (toComponent "Alice")
pr = PrivTCB $ toComponent $ "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

Operators

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

Create a DCLabel from a secrecy ToComponent and integrity ToComponent. E.g.:

   "secrecy" %% "integrity"

 infix 5 %%

(\/) :: (ToComponent a, ToComponent b) => a -> b -> Component

Disjunction of two Principal-based elements.

 infixl 7 \/

(/\) :: (ToComponent a, ToComponent b) => a -> b -> Component

Conjunction of two Principal-based elements.

 infixl 6 /\

class ToComponent a where

Convert a type (e.g., Clause, Principal) to a label component.

Methods

toComponent :: a -> Component

Convert to Component

Instances

ToComponent Bool

ToComponent String

Convert singleton Principal (in the form of a String)to Component.

ToComponent Component

Identity of Component.

ToComponent Clause

Convert singleton Clause to Component.

ToComponent Principal

Convert singleton Principal to Component.

ToComponent (Priv Component)

fromList :: [[Principal]] -> Component

Convert a list of list of Principals to a Component. Each inner list is considered to correspond to a Clause.

toList :: Component -> [[Principal]]

Convert a Component to a list of list of Principals if the Component does not have the value DCFalse. In the latter case the function returns an exception.

Aliases

impossible :: Component

Logical falsehood can be thought of as the component containing every possible principal, hence impossible to express:

 impossible = dcFalse

unrestricted :: Component

Logical truth can be thought of as the component containing no specific principal, hence imposing no restrictions:

 unrestricted = dcTrue