Safe Haskell | Trustworthy |
---|---|

Language | Haskell98 |

# 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`

` l2`LIO`

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`

` lcur`l2`

, it must hold that `lcur ``

. By transitivity of the ``canFlowTo`

`
l2`canFlowTo`

` relation, it holds that ```
l1
`
```

.`canFlowTo`

` l2

class (Eq l, Show l, Read l, Typeable l) => Label l where Source #

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.

lub :: l -> l -> l infixl 5 Source #

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 ``

, and`canFlowTo`

` ljoin- There is no label
`l /= ljoin`

such that`l1 ``

,`canFlowTo`

` l`l2 ``

, and`canFlowTo`

` l`l ``

. In other words`canFlowTo`

` ljoin`ljoin`

is the least element to which both`l1`

and`l2`

can flow.

When used infix, has fixity:

infixl 5 `lub`

glb :: l -> l -> l infixl 5 Source #

*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 ``

, and`canFlowTo`

` l2- There is no label
`l /= lmeet`

such that`l ``

,`canFlowTo`

` l1`l ``

, and`canFlowTo`

` l2`lmeet ``

. In other words`canFlowTo`

` l`lmeet`

is the greatest element flowing to both`l1`

and`l2`

.

When used infix, has fixity:

infixl 5 `glb`

canFlowTo :: l -> l -> Bool infix 4 Source #

*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` l1`

for any`l1`

. - Antisymmetry: If
`l1 `canFlowTo` l2`

and`l2 `canFlowTo` l1`

then`l1 = l2`

. - Transitivity: If
`l1 `canFlowTo` l2`

and`l2 `canFlowTo` l3`

then`l1 `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`

` l2`l1`

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 `canFlowTo`

` l2) == False*downgrading*.

The core privilege function is `canFlowToP`

, which performs a more
permissive can-flow-to check by exercising particular privileges (in
the literature this relation is commonly written `⊑ₚ`

for
privileges `p`

). Most core `LIO`

functions 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
there is no superclass to enforce this.

class (Typeable p, Show p) => SpeaksFor p where Source #

Every privilege type must be an instance of `SpeaksFor`

, which is
a partial order specifying when one privilege value is at least as
powerful as another. If

and `canFlowToP`

p1 l1 l2```
p2
```

, then it should also be true that `speaksFor`

p1

.`canFlowToP`

p2
l1 l2

As a partial order, `SpeaksFor`

should obey the reflexivity,
antisymmetry and transitivity laws. However, if you do not wish to
allow delegation of a particular privilege type, you can define

(which violates the reflexivity law, but
is reasonable when you don't want the partial order).`speaksFor`

_ _ = False

class (Label l, SpeaksFor p) => PrivDesc l p where Source #

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.)

downgradeP :: p -> l -> l Source #

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`

.

canFlowToP :: p -> l -> l -> Bool Source #

`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.

privDesc :: Priv a -> a Source #

Turns privileges into a powerless description of the privileges
by unwrapping the `Priv`

newtype.