DCLabel.Safe
Contents
Description
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 :: ByteString -> 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
- 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.
Constructors
| MkComponentAll | |
| MkComponent | |
Instances
| 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 Components.
Constructors
| MkDCLabel | |
Instances
| 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 Principals.
The empty list '[]' corresponds to the disjunction of all principals.
Conceptually, [] = [P_1 ⋁ P_2 ⋁ ...]
Instances
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.
Instances
| Eq Principal | |
| Ord Principal | |
| Read Principal | |
| Show 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 :: ByteString -> PrincipalSource
Generates a principal from an string.
name :: Principal -> ByteStringSource
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 component.
Given a component return a list of categories.
Arguments
| :: DisjunctionOf a b | |
| => a | |
| -> b | |
| -> Component | Given two elements it joins them with ⋁ |
Arguments
| :: ConjunctionOf a b | |
| => a | |
| -> b | |
| -> Component | Given two elements it joins them with ⋀ |
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.
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.