Safe Haskell | Trustworthy |
---|
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 Monoid
s, 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.
canFlowToP :: p -> l -> l -> BoolSource
The "can-flow-to given privileges" pre-order used to compare
two labels in the presence of privileges. If
holds, then privileges canFlowToP
p L_1
L_2p
are sufficient to downgrade data
from L_1
to L_2
. Note that
implies
canFlowTo
L_1 L_2
for all canFlowToP
p L_1 L_2p
, but for some labels and
privileges, canFlowToP
will hold even where canFlowTo
does
not.
:: 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 NoPrivs
L_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.
(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.