| Safe Haskell | Trustworthy |
|---|
LIO.Label
Contents
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.
Methods
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 /= ljoinsuch thatl1 `,canFlowTo` ll2 `, andcanFlowTo` ll `. In other wordscanFlowTo` ljoinljoinis the least element to which bothl1andl2can 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 /= lmeetsuch thatl `,canFlowTo` l1l `, andcanFlowTo` l2lmeet `. In other wordscanFlowTo` llmeetis the greatest element flowing to bothl1andl2.
When used infix, has fixity:
infixl 5 `glb`
canFlowTo :: l -> l -> BoolSource
Can-flow-to 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` l1for anyl1. - Antisymmetry: If
l1 `canFlowTo` l2andl2 `canFlowTo` l1thenl1 = l2. - Transitivity: If
l1 `canFlowTo` l2andl2 `canFlowTo` l3thenl1 `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 pre-order (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 can-flow-to 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
pre-order on labels in which distinct labels become equivalent.
The pre-oder 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 vice-versa.)
Methods
Arguments
| :: p | Privilege description |
| -> l | Label to downgrade |
| -> l | Lowest label equivelent to input |
Privileges are described in terms of a pre-order 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 label-specific 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.