Safe Haskell  Trustworthy 

Labels
Labels are a way of describing who can observe and modify data.
Labels are governed by a partial order, generally pronounced "can
flow to." In LIO, we write this relation `canFlowTo
`. In the
literature, it is usually written ⊑.
At a high level, the purpose of this whole library is to ensure that
data labeled l1
may affect data labeled l2
only if l1
`
. The canFlowTo
` l2LIO
monad (see LIO.Core) ensures this by
keeping track of a current label of the executing thread (accessible
via the getLabel
function). Code may attempt to perform various IO
or memory operations on labeled data. Touching data may change the
current label and will throw an exception in the event that an
operation would violate information flow restrictions.
The specific invariant maintained by LIO
is, first, that labels on
all previously observed data must flow to a thread's current label.
Second, the current label must flow to the labels of any future
objects the thread will be allowed to modify. Hence, after a thread
with current label lcur
observes data labeled l1
, it must hold
that l1 `
. If the thread is later permitted to
modify an object labeled canFlowTo
` lcurl2
, it must hold that lcur `
. By transitifity of the `canFlowTo
`
l2canFlowTo
` relation, it holds that l1
`
.
canFlowTo
l2
class (Eq l, Show l, Typeable l) => Label l whereSource
This class defines the operations necessary to make a label into
a lattice (see http://en.wikipedia.org/wiki/Lattice_(order)).
canFlowTo
partially orders labels.
lub
and glb
compute the least upper bound and greatest lower
bound of two labels, respectively.
Compute the least upper bound, or join, of two labels. When
data carrying two different labels is mixed together in a
document, the lub
of the two labels is the lowest safe value
with which to label the result.
More formally, for any two labels l1
and l2
, if ljoin = l1
`lub` l2
, it must be that:

L_1 `
,canFlowTo
` ljoin 
L_2 `
, andcanFlowTo
` ljoin  There is no label
l /= ljoin
such thatl1 `
,canFlowTo
` ll2 `
, andcanFlowTo
` ll `
. In other wordscanFlowTo
` ljoinljoin
is the least element to which bothl1
andl2
can flow.
When used infix, has fixity:
infixl 5 `lub`
Greatest lower bound, or meet, of two labels. For any two
labels l1
and l2
, if lmeet = l1 `glb` l2
, it must be
that:

lmeet `
,canFlowTo
` l1 
lmeet `
, andcanFlowTo
` l2  There is no label
l /= lmeet
such thatl `
,canFlowTo
` l1l `
, andcanFlowTo
` l2lmeet `
. In other wordscanFlowTo
` llmeet
is the greatest element flowing to bothl1
andl2
.
When used infix, has fixity:
infixl 5 `glb`
canFlowTo :: l > l > BoolSource
Canflowto relation (⊑). An entity labeled l1
should
be allowed to affect an entity l2
only if l1 `canFlowTo`
l2
. This relation on labels is at least a partial order (see
https://en.wikipedia.org/wiki/Partially_ordered_set), and must
satisfy the following laws:
 Reflexivity:
l1 `canFlowTo` l1
for anyl1
.  Antisymmetry: If
l1 `canFlowTo` l2
andl2 `canFlowTo` l1
thenl1 = l2
.  Transitivity: If
l1 `canFlowTo` l2
andl2 `canFlowTo` l3
thenl1 `canFlowTo` l3
.
When used infix, has fixity:
infix 4 `canFlowTo`
Privileges
Privileges are objects the possesion of which allows code to bypass
certain label protections. An instance of class PrivDesc
describes
a preorder (see http://en.wikipedia.org/wiki/Preorder) among labels
in which certain unequal labels become equivalent. A Priv
object
containing a PrivDesc
instance allows code to make those unequal
labels equivalent for the purposes of many library functions.
Effectively, a PrivDesc
instance describes privileges, while a
Priv
object embodies them.
Any code is free to construct PrivDesc
values describing arbitrarily
powerful privileges. Security is enforced by preventing safe code
from accessing the constructor for Priv
(called PrivTCB
). Safe
code can construct arbitrary privileges from the IO
monad (using
privInit
in LIO.Run), but cannot do so from the LIO
monad. Starting from existing privileges, safe code can also
delegate
lesser privileges (see LIO.Delegate).
Privileges allow you to behave as if l1 `
even when
that is not the case, but only for certain pairs of labels canFlowTo
` l2l1
and
l2
; which pairs depends on the specific privileges. The process of
allowing data labeled l1
to infulence data labeled l2
when (l1
`
is known as downgrading.
canFlowTo
` l2) == False
The core privilege function is canFlowToP
, which performs a
more permissive canflowto check by exercising particular privileges
(in literature this relation is commonly written ⊑ₚ
for
privileges p
). Most core LIO
function have variants ending ...P
that take a privilege argument to act in a more permissive way.
By convention, all PrivDesc
instances should also be instances of
Monoid
, allowing privileges to be combined with mappend
, though
this is not enforced with superclasses.
class (Typeable p, Show p) => SpeaksFor p whereSource
Every privilege type must be an instance of SpeaksFor
, which
specifies when one privilege value is more powerful than another.
If you do not wish to allow delegation, you can simply define
.
speaksFor
_ _ = False
class (Label l, SpeaksFor p) => PrivDesc l p whereSource
This class represents privilege descriptions, which define a
preorder on labels in which distinct labels become equivalent.
The preoder implied by a privilege description is specified by the
method canFlowToP
. In addition, this this class defines a method
downgradeP
, which is important for finding least labels
satisfying a privilege equivalence.
Minimal complete definition: downgradeP
.
(The downgradeP
requirement represents the fact that a generic
canFlowToP
can be implemented efficiently in terms of
downgradeP
, but not viceversa.)
:: p  Privilege description 
> l  Label to downgrade 
> l  Lowest label equivelent to input 
Privileges are described in terms of a preorder on labels in
which sets of distinct labels become equivalent. downgradeP p
l
returns the lowest of all labels equivalent to l
under
privilege description p
.
Less formally, downgradeP p l
returns a label representing
the furthest you can downgrade data labeled l
given
privileges described by p
.
Yet another way to view this function is that downgradeP p l
returns the greatest lower bound (under canFlowTo
) of the set
of all labels l'
such that
.
canFlowToP
p l' l
canFlowToP :: p > l > l > BoolSource
canFlowToP p l1 l2
determines whether p
describes
sufficient privileges to observe data labeled l1
and
subsequently write it to an object labeled l2
. The function
returns True
if and only if either canFlowTo l1 l2
or l1
and l2
are equivalent under p
.
The default definition is:
canFlowToP p l1 l2 = downgradeP p l1 `canFlowTo` l2
canFlowToP
is a method rather than a function so that it can
be optimized in labelspecific ways. However, custom
definitions should behave identically to the default.
A newtype wrapper that can be used by trusted code to transform a
powerless description of privileges into actual privileges. The
constructor, PrivTCB
, is dangerous as it allows creation of
arbitrary privileges. Hence it is only exported by the unsafe
module LIO.TCB. A safe way to create arbitrary privileges is to
call privInit
(see LIO.Run) from the IO
monad
before running your LIO
computation.
Turns privileges into a powerless description of the privileges
by unwrapping the Priv
newtype.