DCLabel.NanoEDSL

Contents

Description

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

A 'Label'/'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 Labels, 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")

where

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

```
 dc2 = <{["Deian"]} , {["Alice"]}>
```
```
 canflowto dc1 dc2 = False
```
```
 canflowto_p pr dc1 dc2 = True
```

Synopsis

Operators

(.\/.)Source

Arguments

:: DisjunctionOf a b
=> a
-> b
-> Label	Given two elements it joins them with ⋁

(./\.)Source

Arguments

:: ConjunctionOf a b
=> a
-> b
-> Label	Given two elements it joins them with ⋀

(<>) :: Label Source

Empty label.

(><) :: Label Source

All label.

singleton Source

Arguments

:: Singleton a
=> a
-> Label	Creates a singleton label.

DCLabel creation

newDC Source

Arguments

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

Methods

newPriv :: a -> Priv Source

Given element create privilege.

newTCBPriv :: TCBPriv -> a -> Maybe TCBPriv Source

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

Instances

NewPriv String
NewPriv Principal
NewPriv Label