Safe Haskell | Safe |
---|

This module implements a ``nano`

`, very simple, embedded domain
specific language to create `Component`

s 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 `Principal`

s, 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 `Principal`

s, 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 `Component`

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

- (\/) :: (ToComponent a, ToComponent b) => a -> b -> Component
- (/\) :: (ToComponent a, ToComponent b) => a -> b -> Component
- class ToComponent a where
- toComponent :: a -> Component
- dcPrivDesc :: a -> DCPrivDesc

- fromList :: [[Principal]] -> Component
- toList :: Component -> [[Principal]]
- everybody :: Component
- anybody :: Component

# Operators

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

Disjunction of two `Principal`

-based elements.

infixl 7 \/

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

Conjunction of two `Principal`

-based elements.

infixl 6 /\

class ToComponent a whereSource

toComponent :: a -> ComponentSource

Convert to `Component`

dcPrivDesc :: a -> DCPrivDescSource

Trivial synonym for `toComponent`

. Convert to a `DCPrivDesc`

.

ToComponent String | Convert singleton |

ToComponent Component | Identity of |

ToComponent Clause | |

ToComponent Principal | |

ToComponent S8 | Convert singleton |

# Aliases

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

everybody = dcFalse