Privileges are objects the possesion of which allows code to bypass
some label protections. An in instance of class
a pre-order among labels in which certain unequal labels become
equivalent. When wrapped in a
Priv type (whose constructor is
PrivDesc allows code to treat those labels as equivalent.
Put another way, privileges 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
L_1 affect data labeled
not (L_1 ` is called downgrading.
The basic method of the
PrivDesc class is
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
...P that take a privilege argument to act in a more
By convention, all
PrivDesc instances are also be instances of
Monoid, allowing privileges to be combined with
PrivDesc values is specific to the particular label type
in use; the method used is
mintTCB, but the arguments depend on the
particular label type.
- class Label l => PrivDesc l p where
- canFlowToP :: PrivDesc l p => Priv p -> l -> l -> Bool
- partDowngradeP :: PrivDesc l p => Priv p -> l -> l -> l
- data Priv a
- privDesc :: Priv a -> a
- data NoPrivs
- noPrivs :: Priv NoPrivs
- data Gate d a
- gate :: (d -> a) -> Gate d a
- callGate :: Gate p a -> Priv p -> a
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.
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
p are sufficient to downgrade data
L_2. Note that
canFlowTo L_1 L_2
canFlowToP p L_1 L_2
p, but for some labels and
canFlowToP will hold even where
Label from which data must flow
L_r = partDowngradeP p L L_g computes how
close one can come to downgrading data labeled
L to the goal
L_g, given privileges
p == , the
L_r == L `. If
p contains all
possible privileges, then
L_r == L_g.
L_r is the greatest lower bound of the
set of all labels
L_g ⊑ L_l, and
L ⊑ₚ L_l.
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
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.
A newtype wrapper that can be used by trusted code to bless
privileges. Privilege-related functions are defined in
LIO.Privs, but the constructor,
PrivTCB, allows one to mint
arbitrary privileges and hence must be located in this file.
Generic privilege type used to denote the lack of privileges.
LIO provides a basic implementation of gates, useful in providing controlled RPC-like services where the client and service provider are in mutual distrust.
A service provider uses
gate to create a gate data type
given a computation of type
Gate d a
d -> a. Here,
d is a privilege
description (type variable for an instance of
PrivDesc). Gates are
callGate, and as such the service provider has the
guarantee that the client (the caller) owns the privileges
corresponding to the privilege description
d. In effect, this
allows a client to "prove" to the service provider that they own
certain privileges without entrusting the service with its privileges.
The gate computation can analyze this privilege description before
performing the "actual" computation. The client and server solely
need to trust the implementation of
A Gate is a lambda abstraction from a privilege description to an
a. Applying the gate is accomplished with
which takes a privilege argument that is converted to a description
before invoking the gate computation.
|:: (d -> a)|
|-> Gate d a|
Create a gate given a computation from a privilege description.
Note that because of currying type
a may itself be a function
type and thus gates can take arguments in addition to the privilege
Given a gate and privilege, execute the gate computation. It is
important to note that
callGate invokes the gate computation with
the privilege description and NOT the privilege itself.
Note that, in general, code should not provide privileges to
functions other than
callGate when wishing to call a gate. This
function is provided by LIO since it can be easily inspected by
both the gate creator and caller to be doing the "right" thing:
provide the privilege description corresponding to the supplied
privilege as "proof" without explicitly passing in the privilege.
This example uses LIO.DCLabel to demonstrate the use of gates. The
service provider provides
addGate which adds two integers if the
gate is called by a piece of code that owns the "Alice" or "Bob"
principals. Otherwise, it simply returns
import LIO import LIO.DCLabel import LIO.Privs.TCB (mintTCB) -- | Add two numbers if the computation is invoked by Alice or Bob. addGate :: DCGate (Int -> Int -> Maybe Int) addGate = gate $ \pd a b -> if pd `elem` (dcPrivDesc `map` ["Alice", "Bob"]) then Just $ a + b else Nothing alice, bob, clark :: DCPriv alice = PrivTCB . dcPrivDesc $ "Alice" bob = PrivTCB . dcPrivDesc $ "Bob" clark = PrivTCB . dcPrivDesc $ "Clark" main = putStrLn . show $ [ callGate addGate alice 1 2 -- Just 3 , callGate addGate bob 3 4 -- Just 7 , callGate addGate clark 5 6 -- Nothing ]