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.

Synopsis

DC Labels with EDSL

join Source

Arguments

:: Lattice a
=> a
-> a
-> a	Join of two elements, ⊔

meet Source

Arguments

:: Lattice a
=> a
-> a
-> a	Meet of two elements, ⊓

top Source

Arguments

:: Lattice a
=> a	Top of lattice, ⊤

bottom Source

Arguments

:: Lattice a
=> a	Bottom of lattice, ⊥

canflowto Source

Arguments

:: Lattice a
=> a
-> a
-> Bool	Partial order relation, ⊑

data Label Source

A label is a conjunction of disjunctions, where MkLabelAll is the constructor that is associated with the conjunction of all possible disjunctions.

Instances

Eq Label	Labels have a unique LNF (see `ToLNF`) form, and equality testing is perfomed on labels of this form.
Read Label
Show Label
Owns Label
ToLNF Label	Reduce a `Label` to LNF. First it applies `cleanLabel` to remove duplicate principals and categories. Following, it removes extraneous/redundant categories. A category is said to be extraneous if there is another category in the label that implies it.
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

data DCLabel Source

A DCLabel is a pair of secrecy and integrity category sets, i.e., a pair of Labels.

Instances

Eq DCLabel
Read DCLabel
Show DCLabel
RelaxedLattice DCLabel
ToLNF DCLabel	Each `DCLabel` can be reduced a unique label representation in LNF, using the `toLNF` function.
Lattice DCLabel	Elements of `DCLabel` form a bounded lattice, where: ⊥ = <`emptyLabel`, `allLabel`> ⊤ = <`allLabel`, `emptyLabel`> <S_1, I_1> ⊔ <S_2, I_2> = <S_1 ⋀ S_2, I_1 ⋁ I_2> <S_1, I_1> ⊓ <S_2, I_2> = <S_1 ⋁ S_2, I_1 ⋀ I_2> <S_1, I_1> ⊑ <S_2, I_2> = S_2 => S_1 ⋀ I_1 => I_2
PrettyShow DCLabel

secrecy :: DCLabel -> Label Source

Integrity category set.

integrity :: DCLabel -> Label Source

Secrecy category set.

principal :: String -> Principal Source

Generates a principal from an string.

listToDisj Source

Arguments

:: DisjToFromList a
=> [a]
-> Disj	Given list return category.

disjToList Source

Arguments

:: DisjToFromList a
=> Disj
-> [a]	Given category return list.

listToLabel Source

Arguments

:: [Disj]
-> Label	Given list return category.

Given a list of categories, return a label.

labelToList Source

Arguments

:: Label
-> [Disj]	Given category return list.

Given a label return a list of categories.

(.\/.)Source

Arguments

:: DisjunctionOf a b
=> a
-> b
-> Label	Given two elements it joins them with ⋁

(./\.)Source

Arguments

:: ConjunctionOf a b
=> a
-> b
-> Label	Given two elements it joins them with ⋀

(<>) :: Label Source

Empty label.

(><) :: Label Source

All label.

newDC Source

Arguments

:: NewDC a b
=> a
-> b
-> DCLabel	Given two elements create label.

Privilegies

data TCBPriv Source

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	`TCBPriv` is an instance of `Monoid`.
PrettyShow TCBPriv
CanDelegate Priv TCBPriv
CanDelegate TCBPriv Priv
CanDelegate TCBPriv TCBPriv

type Priv = Label Source

Untrusted privileged object, which can be converted to a TCBPriv with delegatePriv.

canflowto_p :: RelaxedLattice a => TCBPriv -> a -> a -> Bool Source

Relaxed partial-order relation

delegatePriv :: TCBPriv -> Priv -> Maybe TCBPriv Source

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 -> Bool Source

Can use first privilege in place of second.

owns :: Owns a => TCBPriv -> a -> Bool Source

Checks if category restriction can be bypassed given the privilege.

newPriv :: NewPriv a => a -> Priv Source

Given element create privilege.

newTCBPriv :: NewPriv a => TCBPriv -> a -> Maybe TCBPriv Source

Given privilege and new element, create (maybe) trusted privileged object.