Safe Haskell | Trustworthy |
---|
This module exports a safe-subset of DCLabel.Core, implementing Disjunction Category Components. The exported functions and constructors may be used by untrusted code, guaranteeing that they cannot perform anything unsafe.
- join :: Lattice a => a -> a -> a
- meet :: Lattice a => a -> a -> a
- top :: Lattice a => a
- bottom :: Lattice a => a
- canflowto :: Lattice a => a -> a -> Bool
- data Component
- = MkComponentAll
- | MkComponent { }
- data DCLabel = MkDCLabel {}
- newtype Disj = MkDisj {}
- newtype Conj = MkConj {}
- data Principal
- principal :: CreatePrincipal s => s -> Principal
- name :: Principal -> ByteString
- singleton :: Singleton a => a -> Component
- listToDisj :: DisjToFromList a => [a] -> Disj
- disjToList :: DisjToFromList a => Disj -> [a]
- listToComponent :: [Disj] -> Component
- componentToList :: Component -> [Disj]
- (.\/.) :: DisjunctionOf a b => a -> b -> Component
- (./\.) :: ConjunctionOf a b => a -> b -> Component
- (<>) :: Component
- (><) :: Component
- newDC :: NewDC a b => a -> b -> DCLabel
- data TCBPriv
- priv :: TCBPriv -> Component
- type Priv = Component
- canflowto_p :: RelaxedLattice a => TCBPriv -> a -> a -> Bool
- delegatePriv :: TCBPriv -> Priv -> Maybe TCBPriv
- canDelegate :: CanDelegate a b => a -> b -> Bool
- owns :: Owns a => TCBPriv -> a -> Bool
- class NewPriv a where
- noPriv :: TCBPriv
DC Components with EDSL
A components is a conjunction of disjunctions, where MkComponentAll
is
the constructor that is associated with the logical False
.
Eq Component | Components have a unique LNF (see |
Read Component | |
Show Component | |
Serialize Component | |
Owns Component | |
ToLNF Component | Reduce a |
NewPriv Component | |
PrettyShow Component | |
CanDelegate Priv Priv | |
CanDelegate Priv TCBPriv | |
CanDelegate TCBPriv Priv | |
NewDC String Component | |
NewDC Principal Component | |
NewDC Component String | |
NewDC Component Principal | |
NewDC Component Component | |
ConjunctionOf String Component | |
ConjunctionOf Principal Component | |
ConjunctionOf Component String | |
ConjunctionOf Component Principal | |
ConjunctionOf Component Component | |
ConjunctionOf Component Disj | |
ConjunctionOf Disj Component | |
DisjunctionOf String Component | |
DisjunctionOf Principal Component | |
DisjunctionOf Component String | |
DisjunctionOf Component Principal | |
DisjunctionOf Component Component |
A DCLabel
is a pair of secrecy and integrity category sets, i.e.,
a pair of Component
s.
Eq DCLabel | |
Read DCLabel | |
Show DCLabel | |
Serialize DCLabel | |
RelaxedLattice DCLabel | |
ToLNF DCLabel | Each |
Lattice DCLabel | Elements of
|
PrettyShow DCLabel |
A category, i.e., disjunction, of Principal
s.
The empty list '[]' corresponds to the disjunction of all principals.
Conceptually, [] = [P_1 ⋁ P_2 ⋁ ...]
A category set, i.e., a conjunction of disjunctions.
The empty list '[]' corresponds to the single disjunction of all principals.
In other words, conceptually, [] = {[P_1 ⋁ P_2 ⋁ ...]}
Logically '[]' = True
.
Principal is a simple string representing a source of authority. Any piece
of code can create principals, regarless of how untrusted it is. However,
for principals to be used in integrity components or be ignoerd a
corresponding privilege (TCBPriv
) must be created (by trusted code) or
delegated.
Eq Principal | |
Ord Principal | |
Read Principal | |
Show Principal | |
IsString Principal | |
Serialize Principal | |
DisjToFromList Principal | |
NewPriv Principal | |
Singleton Principal | |
PrettyShow Principal | |
NewDC Principal Principal | |
NewDC Principal Component | |
NewDC Component Principal | |
ConjunctionOf Principal Principal | |
ConjunctionOf Principal Component | |
ConjunctionOf Principal Disj | |
ConjunctionOf Component Principal | |
ConjunctionOf Disj Principal | |
DisjunctionOf Principal Principal | |
DisjunctionOf Principal Component | |
DisjunctionOf Component Principal |
principal :: CreatePrincipal s => s -> PrincipalSource
name :: Principal -> ByteStringSource
:: DisjToFromList a | |
=> [a] | |
-> Disj | Given list return category. |
:: DisjToFromList a | |
=> Disj | |
-> [a] | Given category return list. |
Given a list of categories, return a component.
Given a component return a list of categories.
Privilegies
Privilege object is just a conjunction of disjunctions, i.e., Component
.
A trusted privileged object must be introduced by trusted code, after which
trusted privileged objects can be created by delegation.
Eq TCBPriv | |
Show TCBPriv | |
Monoid TCBPriv |
|
PrettyShow TCBPriv | |
CanDelegate Priv TCBPriv | |
CanDelegate TCBPriv Priv | |
CanDelegate TCBPriv TCBPriv |
Untrusted privileged object, which can be converted to a TCBPriv
with
delegatePriv
.
canflowto_p :: RelaxedLattice a => TCBPriv -> a -> a -> BoolSource
Relaxed partial-order relation
delegatePriv :: TCBPriv -> Priv -> Maybe TCBPrivSource
Given trusted privilege and a "desired" untrusted privilege, return a trusted version of the untrusted privilege, if the provided (trusted) privilege implies it.
canDelegate :: CanDelegate a b => a -> b -> BoolSource
Can use first privilege in place of second.
owns :: Owns a => TCBPriv -> a -> BoolSource
Checks if category restriction can be bypassed given the privilege.
Given element create privilege.
newTCBPriv :: TCBPriv -> a -> Maybe TCBPrivSource
Given privilege and new element, create (maybe) trusted privileged object.