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.
- data Principal
- principalName :: Principal -> S8
- principal :: S8 -> Principal
- data Clause
- clause :: Set Principal -> Clause
- data Component
- dcTrue :: Component
- dcFalse :: Component
- dcFormula :: Set Clause -> Component
- isTrue :: Component -> Bool
- isFalse :: Component -> Bool
- data DCLabel
- dcSecrecy :: DCLabel -> Component
- dcIntegrity :: DCLabel -> Component
- dcLabel :: Component -> Component -> DCLabel
- dcPub :: DCLabel
- module LIO.DCLabel.Privs
- module LIO.DCLabel.DSL
- type DCState = LIOState DCLabel
- defaultState :: DCState
- type DC = LIO DCLabel
- evalDC :: DC a -> IO a
- runDC :: DC a -> IO (a, DCState)
- tryDC :: DC a -> IO (Either DCLabeledException a, DCState)
- paranoidDC :: DC a -> IO (Either SomeException (a, DCState))
- type MonadDC m = MonadLIO DCLabel m
- type DCLabeledException = LabeledException DCLabel
- type DCLabeled = Labeled DCLabel
- type DCRef = LIORef DCLabel
- type DCGate = Gate DCPrivDesc
Principal is a simple string representing a source of
authority. Any piece of code can create principals, regardless of how
untrusted it is.
A clause or disjunction category is a set of
Logically the set corresponds to a disjunction of the principals.
A component is a set of clauses, i.e., a formula (conjunction of
DCFalse corresponds to logical
DCFormula Set.empty corresponds to logical
DCLabel is a pair of secrecy and integrity
Label constructor. Note that each component is first reduced to CNF.
Element in the DCLabel lattice corresponding to public data.
dcPub = < True, True > . This corresponds to data that is not
secret nor trustworthy.
Synonyms for LIO
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
top as set by
defaultState, respectively. In most cases the initial current label
should be public, i.e.,
evalLIO, but catches all exceptions.