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 = FalsecanFlowToP
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