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

Read Label

Show 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

CanActFor Priv Priv

CanActFor Priv TCBPriv

CanActFor 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

DisjunctionOf String Label

DisjunctionOf Principal Label

DisjunctionOf Label String

DisjunctionOf Label Principal

DisjunctionOf Label Label

data DCLabel

A DC label for secrecy and integrity.

Instances

Eq DCLabel

Read DCLabel

Show DCLabel

RelaxedLattice DCLabel

ToLNF DCLabel

Lattice DCLabel

PrettyShow DCLabel

secrecy :: DCLabel -> Label

integrity :: DCLabel -> Label

principal :: String -> Principal

Generates a principal from an string.

(.\/.) :: DisjunctionOf a b => a -> b -> Label

(./\.) :: ConjunctionOf a b => a -> b -> Label

(<>) :: Label

Empty label.

(><) :: Label

All label.

newDC

Arguments

:: NewDC a b

=> a

-> b

-> DCLabel

Given two elements create label.

Priviligies

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

CanActFor Priv TCBPriv

CanActFor TCBPriv Priv

CanActFor 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 privilige and a "desired" untrusted privilege, return a trusted version of the untrusted privilige, if the provided (trusted) privilige implies it.

canActFor :: CanActFor a b => a -> b -> Bool

Can use first privilige in place of second.

newPriv :: NewPriv a => a -> Priv

Given element create privilege.

Given element create (maybe) trusted privileged object.

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