Safe Haskell  Trustworthy 

Disjunction Category Labels (DCLabel
s) are a label format that
encodes authority, secrecy restrictions, and integrity properties
using propositional logic.
A DCLabel
consists of two boolean formulas over Principal
s. Each
formula is in conjunctive normal form, represented by type CNF
. The
first CNF
(dcSecrecy
) specifies what combinations of principals
are allowed to make data public. The second CNF
(dcIntegrity
)
specifies which combinations of principals have endorsed the integrity
of the data.
The %%
operator allows one to construct a DCLabel
by joining a
secrecy CNF
on the left with an integrity CNF
on the right. A
DCLabel
can also be directly constructed with the constructor
DCLabel
. However, %%
has the added convenience of accepting any
argument types that are instances of ToCNF
.
For example, the following expresses data that can be exported by the
principal "Alice" and may have been written by anybody: "Alice"
. (%%
True
indicates a trivially satisfiable
label component, which in this case means a label conveying no
integrity properties.)
toCNF
True
A CNF
is created using the (\/
) and (/\
) operators. The
disjunction operator (\/
) is used to compute a CNF
equivalent to
the disjunciton of two Principal
s, Strings
, or CNF
s. For
example:
p1 =principal
"p1" p2 =principal
"p2" p3 =principal
"p3" e1 = p1\/
p2 e2 = e1\/
"p4"
Similarly, the conjunction operator (/\
) creates a CNF
as a
conjunction of Principal
s, String
s, Disjunction
s, or CNF
s.
e3 = p1\/
p2 e4 = e1/\
"p4"/\
p3
Note that because a CNF
formula is stored as a conjunction of
Disjunction
s, it is much more efficient to apply /\
to the result
of \/
than vice versa. It would be logical for /\
to have higher
fixity than \/
. Unfortunately, this makes formulas harder to read
(given the convention of AND binding more tightly than OR). Hence
\/
and /\
have been given the same fixity but different
associativities, preventing the two from being mixed in the same
expression without explicit parentheses.
Consider the following, example:
cnf1 = ("Alice"\/
"Bob")/\
"Carla" cnf2 = "Alice"/\
"Carla" dc1 = cnf1%%
cnf2 dc2 = "Djon"%%
"Alice" pr = PrivTCB $ "Alice"/\
"Carla"
This will result in the following:
>>>
dc1
"Carla" /\ ("Alice" \/ "Bob") %% "Alice" /\ "Carla">>>
dc2
"Djon" %% "Alice">>>
canFlowTo dc1 dc2
False>>>
canFlowToP pr dc1 dc2
True
Because the \/
and /\
operators accept strings and Principal
s as
well as CNF
s, it is sometimes easy to forget that strings and
Principal
s are not actually CNF
s. For example:
>>>
"Alice" /\ "Bob" `speaksFor` "Alice" \/ "Bob"
True>>>
"Alice" `speaksFor` "Alice" \/ "Bob"
<interactive>:12:21: Couldn't match expected type `[Char]' with actual type `CNF'
To convert a single string or Principal
to a CNF
, you must use the
toCNF
method:
>>>
toCNF "Alice" `speaksFor` "Alice" \/ "Bob"
True
 type DC = LIO DCLabel
 type DCPriv = Priv CNF
 type DCLabeled = Labeled DCLabel
 dcDefaultState :: LIOState DCLabel
 evalDC :: DC a > IO a
 tryDC :: DC a > IO (Either SomeException a, LIOState DCLabel)
 data Principal
 principalBS :: ByteString > Principal
 principal :: String > Principal
 data DCLabel = DCLabel {
 dcSecrecy :: !CNF
 dcIntegrity :: !CNF
 dcPublic :: DCLabel
 (%%) :: (ToCNF a, ToCNF b) => a > b > DCLabel
 (/\) :: (ToCNF a, ToCNF b) => a > b > CNF
 (\/) :: (ToCNF a, ToCNF b) => a > b > CNF
 data CNF
 class ToCNF c where
 principalName :: Principal > ByteString
 data Disjunction
 dToSet :: Disjunction > Set Principal
 dFromList :: [Principal] > Disjunction
 cTrue :: CNF
 cFalse :: CNF
 cToSet :: CNF > Set Disjunction
 cFromList :: [Disjunction] > CNF
Toplevel aliases and functions
dcDefaultState :: LIOState DCLabelSource
A common default starting state, where
and lioLabel
= dcPublic
(i.e., the highest
possible clearance).
lioClearance
= False %%
True
Wrapper function for running
computations.
LIO
DCLabel
evalDC dc =evalLIO
dcdcDefaultState
tryDC :: DC a > IO (Either SomeException a, LIOState DCLabel)Source
tryDC dc =tryLIO
dcdcDefaultState
Main types and functions
A Principal
is a primitive source of authority, represented as
a string. The interpretation of principal strings is up to the
application. Reasonable schemes include encoding user names,
domain names, and/or URLs in the Principal
type.
principalBS :: ByteString > PrincipalSource
Create a principal from a strict ByteString
.
principal :: String > PrincipalSource
Create a principal from a String
. The String
is packed into
a ByteString
using fromString
, which will almost certainly
give unexpected results for nonASCII unicode code points.
Main DCLabel type. DCLabel
s use CNF
boolean formulas over
principals to express authority exercised by a combination of
principals. A DCLabel
contains two CNF
s. One, dcSecrecy
,
specifies the minimum authority required to make data with the
label completely public. The second, dcIntegrity
, expresses the
minimum authority that was used to endorse data with the label, or,
for mutable objects, the minimum authority required to modify the
object.
DCLabel
s are more conveniently expressed using the %%
operator,
with dcSecrecy
on the left and dcIntegrity
on the right, i.e.:
(
dcSecrecyValue %%
dcIntegrityValue)
.
DCLabel
s enforce the following relations:
 If
cnf1
andcnf2
areCNF
s describing authority, thencnf1 `
if and only ifspeaksFor
` cnf2cnf1
logically impliescnf2
(often writtencnf1 ⟹ cnf2
). For example,("A"
, while/\
"B") `speaksFor
`toCNF
"A"
.toCNF
"A" `speaksFor
` ("A"\/
"C")  Given two
DCLabel
sdc1 = (s1
and%%
i1)dc2 = (s2
,%%
i2)dc1 `
(often writtencanFlowTo
` dc2dc1
⊑dc2
) if and only ifs2 `
. In other words, data can flow in the direction of requiring more authority to make it public or removing integrity endorsements.speaksFor
` s1 && i1 `speaksFor
` i2  Given two
DCLabel
sdc1 = (s1
and%%
i1)dc2 = (s2
, and a%%
i2)p::
representing privileges,CNF
(often writtencanFlowToP
p dc1 dc2dc1
⊑ₚdc2
) if and only if(p
./\
s2) `speaksFor
` s2 && (p/\
i1) `speaksFor
` i2
DCLabel  

dcPublic = True %% True
This label corresponds to public data with no integrity guarantees.
For instance, an unrestricted Internet socket should be labeled
dcPublic
. The significance of dcPublic
is that given data
labeled (s %% i)
, s
is the exact minimum authority such that
(s %% i) ⊑ₛ dcPublic
, while i
is the exact
minimum authority such that dcPublic ⊑ᵢ (s %% i)
.
As a type, a CNF
is always a conjunction of Disjunction
s of
Principal
s. However, mathematically speaking, a single
Principal
or single Disjunction
is also a degenerate example of
conjunctive normal form. Class ToCNF
abstracts over the
differences between these types, promoting them all to CNF
.
Lowerlevel functions
principalName :: Principal > ByteStringSource
Extract the name of a principal as a strict ByteString
.
(Use show
to get it as a regular String
.)
data Disjunction Source
Represents a disjunction of Principal
s, or one clause of a
CNF
. There is generally not much need to work directly with
Disjunction
s unless you need to serialize and deserialize them
(by means of dToSet
and dFromList
).
Eq Disjunction  
Ord Disjunction  
Read Disjunction  Note that a disjunction containing more than one element must be surrounded by parentheses to parse correctly. 
Show Disjunction  
Typeable Disjunction  
Monoid Disjunction  
ToCNF Disjunction 
dToSet :: Disjunction > Set PrincipalSource
Expose the set of Principal
s being ORed together in a
Disjunction
.
dFromList :: [Principal] > DisjunctionSource
Convert a list of Principal
s into a Disjunction
.
A CNF
that is always True
i.e., trivially satisfiable. When
, it means data is public. When
dcSecrecy
= cTrue
, it means data carries no integrity
guarantees. As a description of privileges, dcIntegrity
= cTruecTrue
conveys no
privileges;
is equivalent to
canFlowToP
cTrue l1 l2
.
canFlowTo
l1 l2
Note that
. Hence toCNF
True
= cTrue
.
dcPublic
= DCLabel
cTrue cTrue
A CNF
that is always False
. If
, then
no combination of principals is powerful enough to make the data
public. For that reason, dcSecrecy
= cFalsecFalse
generally shouldn't appear in a
data label. However, it is convenient to include as the
dcSecrecy
component of lioClearance
to indicate a thread may
arbitrarily raise its label.
indicates impossibly much integrityi.e.,
data that no combination of principals is powerful enough to modify
or have created. Generally this is not a useful concept.
dcIntegrity
= cFalse
As a privilege description, cFalse
indicates impossibly high
privileges (i.e., higher than could be achieved through any
combination of Principal
s). cFalse `
for any
speaksFor
` pCNF
p
. This can be a useful concept for bootstrapping
privileges within the DC
monad itself. For instance, the result
of
can be passed to fullytrusted privInit
cFalseDC
code,
which can in turn use delegate
to create arbitrary finite
privileges to pass to less privileged code.
cToSet :: CNF > Set DisjunctionSource
Convert a CNF
to a Set
of Disjunction
s. Mostly useful if
you wish to serialize a DCLabel
.
cFromList :: [Disjunction] > CNFSource
Convert a list of Disjunction
s into a CNF
. Mostly useful if
you wish to deserialize a CNF
.