Safe Haskell | Trustworthy |
---|
Disjunction Category Labels (DCLabel
s) 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
Principals
A Principal
is a simple string representing a source of
authority. Any piece of code can create principals, regardless of how
untrusted it is.
principalName :: Principal -> S8Source
Get the principal name.
Clauses
A clause or disjunction category is a set of Principal
s.
Logically the set corresponds to a disjunction of the principals.
Components
A component is a set of clauses, i.e., a formula (conjunction of
disjunction of Principal
s). DCFalse
corresponds to logical
False
, while DCFormula Set.empty
corresponds to logical True
.
Labels
A DCLabel
is a pair of secrecy and integrity Component
s.
dcIntegrity :: DCLabel -> ComponentSource
Extract integrity component of a label
dcLabel :: Component -> Component -> DCLabelSource
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.
Privileges
module LIO.DCLabel.Privs
DSL
module LIO.DCLabel.DSL
Synonyms for LIO
The DC
monad is LIO
with using DCLabel
s 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
.
paranoidDC :: DC a -> IO (Either SomeException (a, DCState))Source
Similar to evalLIO
, but catches all exceptions.
Exceptions
type DCLabeledException = LabeledException DCLabelSource
DC Labeled exceptions.
Labeled values
Labeled references
Gates
type DCGate = Gate DCPrivDescSource
DC Gate
.