| Safe Haskell | Safe |
|---|---|
| Language | Haskell2010 |
LIO
Description
This is the main module to be included by code using the Labeled IO (LIO) library. This module exports the core library (documented in LIO.Core), with support for labels and privileges (documented in LIO.Label) and labeled values (documented in LIO.Labeled).
Certain symbols in the LIO library, particularly those in
LIO.Exception, use the same names as their IO equivalents in the
system libraries. Hence main modules consisting mostly of IO code
that simply need to run LIO code should import LIO.Run (or
LIO.DCLabel) to avoid polluting their namespaces.
Most code will need to use a particular label format, which needs to be imported separately. Hence, a typical set of imports for an untrusted LIO module is:
import LIO import LIO.DCLabel
Synopsis
- module LIO.Core
- module LIO.Delegate
- module LIO.Exception
- data Priv a
- data NoPrivs = NoPrivs
- class (Label l, SpeaksFor p) => PrivDesc l p where
- downgradeP :: p -> l -> l
- canFlowToP :: p -> l -> l -> Bool
- class (Typeable p, Show p) => SpeaksFor p where
- class (Eq l, Show l, Read l, Typeable l) => Label l where
- privDesc :: Priv a -> a
- noPrivs :: Priv NoPrivs
- module LIO.Labeled
Documentation
module LIO.Core
module LIO.Delegate
module LIO.Exception
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#v:privInit") from the IO monad
before running your LIO computation.
Generic PrivDesc used to denote the lack of privileges. Works
with any Label type. This is only a privilege description; a
more useful symbol is noPrivs, which actually embodies the
NoPrivs privilege.
Constructors
| NoPrivs |
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.)
Minimal complete definition
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.
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.
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 canFlowToP p1 l1 l2p2
, then it should also be true that speaksFor p1canFlowToP 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
speaksFor _ _ = False
Methods
speaksFor :: p -> p -> Bool infix 4 Source #
speaksFor p1 p2 returns True iff p1 subsumes all the
privileges of p2. In other words, it is safe for delegate to
hand out p2 to a caller who already has p1.
Has fixity:
infix 4 `speaksFor`
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.
Methods
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` ljoinL_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`
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` l1lmeet `, 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 -> 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` 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`
privDesc :: Priv a -> a Source #
Turns privileges into a powerless description of the privileges
by unwrapping the Priv newtype.
module LIO.Labeled