Safe Haskell	Trustworthy

LIO.DCLabel

Contents

Principals
Clauses
Components
Labels
Privileges
DSL
Synonyms for LIO

Description

Disjunction Category Labels (DCLabels) are a label format that encode secrecy and integrity using propositional logic. This exports label operators and instances for the LIO. The label format is documented in LIO.DCLabel.Core, privileges are described in LIO.DCLabel.Privs, and a domain specific language for constructing labels is presented in LIO.DCLabel.DSL.

Synopsis

Principals

newtype Principal Source

A Principal is a simple string representing a source of authority. Any piece of code can create principals, regardless of how untrusted it is.

Constructors

Principal
Fields principalName :: ByteString Get the principal name.

Instances

Eq Principal
Ord Principal
Show Principal
Typeable Principal
ToComponent Principal	Convert singleton `Principal` to `Component`.

principal :: String -> Principal Source

Generate a principal from a String. (To create one from a ByteString, just use the Principal constructor directly.)

Clauses

data Clause Source

A clause or disjunction category is a set of Principals. Logically the set corresponds to a disjunction of the principals.

Instances

Eq Clause
Ord Clause
Show Clause
Typeable Clause
ToComponent Clause	Convert singleton `Clause` to `Component`.

clause :: Set Principal -> Clause Source

Clause constructor

Components

data Component Source

A component is a set of clauses, i.e., a formula (conjunction of disjunction of Principals). DCFalse corresponds to logical False, while DCFormula Set.empty corresponds to logical True.

Instances

Eq Component
Show Component
Typeable Component
Monoid Component	Privileges can be combined using `mappend`
ToComponent Component	Identity of `Component`.
PrivDesc DCLabel Component
ToComponent (Priv Component)

dcTrue :: Component Source

Logical True.

dcFalse :: Component Source

Logical False.

dcFormula :: Set Clause -> Component Source

Arbitrary formula from a clause.

isTrue :: Component -> Bool Source

Is the component True.

isFalse :: Component -> Bool Source

Is the component False.

Labels

data DCLabel Source

A DCLabel is a pair of secrecy and integrity Components.

Instances

Bounded DCLabel
Eq DCLabel
Show DCLabel
Typeable DCLabel
Label DCLabel
PrivDesc DCLabel Component

dcSecrecy :: DCLabel -> Component Source

Extract secrecy component of a label

dcIntegrity :: DCLabel -> Component Source

Extract integrity component of a label

dcLabel :: Component -> Component -> DCLabel Source

dcLabel secrecyComponent integrityComponent creates a label, reducing each component to CNF.

dcPub :: DCLabel Source

Element in the DCLabel lattice corresponding to public data. dcPub = < True, True > . This corresponds to data that is not secret nor trustworthy.

dcTop :: DCLabel Source

Element in the DCLabel lattice corresponding to the most secret and least trustworthy data. dcTop = < False, True > .

dcBottom :: DCLabel Source

Element in the DCLabel lattice corresponding to the least secret and most trustworthy data. dcTop = < True, False > .

Privileges

module LIO.DCLabel.Privs

DSL

module LIO.DCLabel.DSL

Synonyms for LIO

The DC monad is LIO with using DCLabels as the label format. Most application should be written in terms of this monad, while most libraries should remain polymorphic in the label type. It is important that any *real* application set the initial current label and clearance to values other than bottom and top as set by defaultState, respectively. In most cases the initial current label should be public, i.e., dcPub.

type DCState = LIOState DCLabel Source

LIOState with underlying label being DCLabel

defaultState :: DCState Source

Default, starting state for a DC computation. The current label is public (i.e., dcPub) and the current clearance is top.

type DC = LIO DCLabel Source

The monad for LIO computations using DCLabel as the label.

evalDC :: DC a -> IO aSource

Evaluate computation in the DC monad.

runDC :: DC a -> IO (a, DCState)Source

Evaluate computation in the DC monad.

tryDC :: DC a -> IO (Either SomeException a, DCState)Source

Similar to evalLIO, but catches any exceptions thrown by untrusted code with throwLIO.