| Safe Haskell | Trustworthy |
|---|
LIO.Privs
Contents
Description
Privileges are instances of the class called Priv. They represent
the ability to bypass the protection of certain labels. Specifically,
privilege allows you to behave as if L_1 ` even when
that is not the case. The process of making data labeled canFlowTo` L_2L_1 affect
data labeled L_2 when not (L_1 ` is called
downgrading.
canFlowTo` L_2)
The basic method of the Priv class is canFlowToP, which performs a
more permissive can-flow-to check by exercising particular privileges
(in literature this relation is a pre-order, commonly written as
⊑ₚ). Almost all LIO operations have variants ending
...P that take a privilege argument to act in a more permissive way.
All Priv types are Monoids, and so privileges can be combined with
mappend. The creation of Priv values is specific to the
particular label type in use; the method used is mintTCB, but the
arguments depend on the particular label type.
Privilege descriptions
class (PrivTCB p, Show d) => PrivDesc p d | p -> d, d -> p whereSource
Class used to convert a privilege to a privilege description. This is particularly useful when one piece of code wishes to prove ownership of certain privileges without granting the privilege. NOTE: it (almost) always a security violation if the privilege is also the privilege description.
Although this class is not part of the TCB there are some security
implications that should be considered when making a type an
instance of this class. Specifically, if the value constructor for
the privilege description type d is exported then some
trusted code must be used when "proving" ownership of a certain
privilege. This is generally a good idea even if the constructor is
not made available, since code can (usually) cache such privilege
descriptions. An alternative is to use phantom types to enforce a
linear-type-like behavior.
Privileges
class (Label l, PrivTCB p, Monoid p) => Priv l p whereSource
This class defines privileges and the more-permissive relation
(canFlowToP) on labels using privileges. Additionally, it defines
partDowngradeP which is used to downgrage a label up to a limit,
given a set of privilege.
Methods
canFlowToP :: p -> l -> l -> BoolSource
The "can-flow-to given privileges" pre-order used to compare
two labels in the presence of privileges. If canFlowToP p L_1
L_2p are sufficient to downgrade data
from L_1 to L_2. Note that canFlowTo L_1 L_2canFlowToP p L_1 L_2p, but for some labels and
privileges, canFlowToP will hold even where canFlowTo does
not.
Arguments
| :: p | Privileges |
| -> l | Label from which data must flow |
| -> l | Goal label |
| -> l | Result |
Roughly speaking, L_r = partDowngradeP p L L_g computes how
close one can come to downgrading data labeled L to the goal label
L_g, given privileges p. When p == , the resulting
label NoPrivsL_r == L `. If upperBound` L_gp contains all
possible privileges, then L_r == L_g.
More specifically, L_r is the greatest lower bound of the
set of all labels L_l satisfying:
-
L_g ⊑ L_l, and -
L ⊑ₚ L_l.
Operationally, partDowngradeP captures the minimum change required
to the current label when viewing data labeled L_l. A common
pattern is to use the result of getLabel as L_g (i.e., the
goal is to use privileges p to avoid changing the label at all),
and then compute L_r based on the label of data the code is
about to observe.
Instances
| (PrivTCB NoPrivs, Monoid NoPrivs, Label l) => Priv l NoPrivs | With lack of privileges, |
| Priv DCLabel DCPriv |
Generic privilege type used to denote the lack of privileges.
Constructors
| NoPrivs |