LIO.DCLabel.DSL

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

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 = dcPrivTCB . dcPrivDesc $ "Alice" /\ "Carla"

where

•  dc1 = <{["Alice" ⋁ "Bob"] ⋀ ["Carla"]} , {["Alice"] ⋀ ["Carla"]}>

•  dc2 = <{["Djon"]} , {["Alice"]}>

•  canFlowTo dc1 dc2 = False

•  canFlowToP pr dc1 dc2 = True

Operators

(\/) :: (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

dcPrivDesc :: a -> DCPrivDesc

Trivial synonym for toComponent. Convert to a DCPrivDesc.

Instances

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.

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

Aliases

everybody :: Component

Logical falsehood can be thought of as the component containing every possible principal:

 everybody = dcFalse

anybody :: Component

Logical truth can be thought of as the component containing no specific principal:

 anybody = dcTrue