DCLabel.Safe

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.

DC Labels with EDSL

join

Arguments

:: Lattice a

=> a

-> a

-> a

Join of two elements, ⊔

meet

Arguments

:: Lattice a

=> a

-> a

-> a

Meet of two elements, ⊓

top

Arguments

:: Lattice a

=> a

Top of lattice, ⊤

bottom

Arguments

:: Lattice a

=> a

Bottom of lattice, ⊥

canflowto

Arguments

:: Lattice a

=> a

-> a

-> Bool

Partial order relation, ⊑

data Label

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

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

Integrity category set.

integrity :: DCLabel -> Label

Secrecy category set.

principal :: String -> Principal

Generates a principal from an string.

listToDisj

Arguments

:: DisjToFromList a

=> [a]

-> Disj

Given list return category.

disjToList

Arguments

:: DisjToFromList a

=> Disj

-> [a]

Given category return list.

listToLabel

Arguments

:: [Disj]

-> Label

Given list return category.

Given a list of categories, return a label.

labelToList

Arguments

:: Label

-> [Disj]

Given category return list.

Given a label return a list of categories.

(.\/.)

Arguments

:: DisjunctionOf a b

=> a

-> b

-> Label

Given two elements it joins them with ⋁

(./\.)

Arguments

:: ConjunctionOf a b

=> a

-> b

-> Label

Given two elements it joins them with ⋀

(<>) :: Label

Empty label.

(><) :: Label

All label.

newDC

Arguments

:: NewDC a b

=> a

-> b

-> DCLabel

Given two elements create label.

Privilegies

data TCBPriv

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

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

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

Relaxed partial-order relation

delegatePriv :: TCBPriv -> Priv -> Maybe TCBPriv

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

Can use first privilege in place of second.

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

Checks if category restriction can be bypassed given the privilege.

newPriv :: NewPriv a => a -> Priv

Given element create privilege.

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

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