DCLabel.Safe
Contents
Description
This module exports a safe-subset of DCLabel.Core, implementing Disjunction Category Labels. 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 Label
- = MkLabelAll
- | MkLabel { }
- data DCLabel = MkDCLabel {}
- newtype Disj = MkDisj {}
- newtype Conj = MkConj {}
- data Principal
- principal :: String -> Principal
- name :: Principal -> String
- singleton :: Singleton a => a -> Label
- listToDisj :: DisjToFromList a => [a] -> Disj
- disjToList :: DisjToFromList a => Disj -> [a]
- listToLabel :: [Disj] -> Label
- labelToList :: Label -> [Disj]
- (.\/.) :: DisjunctionOf a b => a -> b -> Label
- (./\.) :: ConjunctionOf a b => a -> b -> Label
- (<>) :: Label
- (><) :: Label
- newDC :: NewDC a b => a -> b -> DCLabel
- data TCBPriv
- type Priv = Label
- 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 Labels with EDSL
A label is a conjunction of disjunctions, where MkLabelAll is
the constructor that is associated with the conjunction of all
possible disjunctions.
Constructors
| MkLabelAll | |
| MkLabel | |
Instances
| Eq Label | Labels have a unique LNF (see |
| Read Label | |
| Show Label | |
| Owns Label | |
| ToLNF Label | Reduce a |
| NewPriv Label | |
| PrettyShow Label | |
| CanDelegate Priv Priv | |
| CanDelegate Priv TCBPriv | |
| CanDelegate TCBPriv Priv | |
| NewDC String Label | |
| NewDC Principal Label | |
| NewDC Label String | |
| NewDC Label Principal | |
| NewDC Label Label | |
| ConjunctionOf String Label | |
| ConjunctionOf Principal Label | |
| ConjunctionOf Label String | |
| ConjunctionOf Label Principal | |
| ConjunctionOf Label Label | |
| ConjunctionOf Label Disj | |
| ConjunctionOf Disj Label | |
| DisjunctionOf String Label | |
| DisjunctionOf Principal Label | |
| DisjunctionOf Label String | |
| DisjunctionOf Label Principal | |
| DisjunctionOf Label Label |
A DCLabel is a pair of secrecy and integrity category sets, i.e.,
a pair of Labels.
Constructors
| MkDCLabel | |
Instances
| Eq DCLabel | |
| Read DCLabel | |
| Show DCLabel | |
| RelaxedLattice DCLabel | |
| ToLNF DCLabel | Each |
| Lattice DCLabel | Elements of
|
| PrettyShow DCLabel |
A category, i.e., disjunction, of Principals.
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 ⋁ ...]}
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 labels or be ignoerd a corresponding
privilege (TCBPriv) must be created (by trusted code) or delegated.
Instances
| Eq Principal | |
| Ord Principal | |
| Read Principal | |
| Show Principal | |
| DisjToFromList Principal | |
| NewPriv Principal | |
| Singleton Principal | |
| PrettyShow Principal | |
| NewDC Principal Principal | |
| NewDC Principal Label | |
| NewDC Label Principal | |
| ConjunctionOf Principal Principal | |
| ConjunctionOf Principal Label | |
| ConjunctionOf Principal Disj | |
| ConjunctionOf Label Principal | |
| ConjunctionOf Disj Principal | |
| DisjunctionOf Principal Principal | |
| DisjunctionOf Principal Label | |
| DisjunctionOf Label Principal |
Arguments
| :: DisjToFromList a | |
| => [a] | |
| -> Disj | Given list return category. |
Arguments
| :: DisjToFromList a | |
| => Disj | |
| -> [a] | Given category return list. |
Given a list of categories, return a label.
Given a label return a list of categories.
Privilegies
Privilege object is just a conjunction of disjunctions, i.e., a Label.
A trusted privileged object must be introduced by trusted code, after which
trusted privileged objects can be created by delegation.
Instances
| 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.
Methods
Given element create privilege.
newTCBPriv :: TCBPriv -> a -> Maybe TCBPrivSource
Given privilege and new element, create (maybe) trusted privileged object.