dclabel-0.0.6: The Disjunction Category Label Format

Safe HaskellTrustworthy




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

A 'Component'/'Priv' is created using the (.\/.) and (./\.) operators. The disjunction operator (.\/.) is used to create a category from Principals, Strings, 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, Strings, and conjunctive or disjunctive sub-expressions. For example:

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

Note that because a category consists of a disjunction of principals, and a category set 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 newDC. And, similarly, given a TCBPriv and Priv you can create a new minted privilege with newTCBPriv.

Consider the following, example:

     l1 = "Alice" .\/. "Bob" ./\. "Carla" 
     l2 = "Alice" ./\. "Carla" 
     dc1 = newDC l1 l2
     dc2 = newDC "Deian" "Alice"
     pr = createPrivTCB $ newPriv ("Alice" ./\. "Carla")


  •  dc1 = <{["Alice" ⋁ "Bob"] ⋀ ["Carla"]} , {["Alice"] ⋀ ["Carla"]}>
  •  dc2 = <{["Deian"]} , {["Alice"]}>
  •  canflowto dc1 dc2 = False
  •  canflowto_p pr dc1 dc2 = True





:: DisjunctionOf a b 
=> a 
-> b 
-> Component

Given two elements it joins them with ⋁



:: ConjunctionOf a b 
=> a 
-> b 
-> Component

Given two elements it joins them with ⋀

(<>) :: ComponentSource

Empty component (logically this is True).

(><) :: ComponentSource

All component (logically this is False).



:: Singleton a 
=> a 
-> Component

Creates a singleton component.

DCLabel creation



:: NewDC a b 
=> a 
-> b 
-> DCLabel

Given two elements create label.

Privilege object creation

class NewPriv a whereSource

Class used to create Privs and TCBPrivs.


newPriv :: a -> PrivSource

Given element create privilege.

newTCBPriv :: TCBPriv -> a -> Maybe TCBPrivSource

Given privilege and new element, create (maybe) trusted privileged object.