LIO.Privs

Privileges are objects the possesion of which allows code to bypass some label protections. An in instance of class PrivDesc describes a pre-order among labels in which certain unequal labels become equivalent. When wrapped in a Priv type (whose constructor is private) a 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 `canFlowTo` L_2 even when that is not the case. The process of making data labeled L_1 affect data labeled L_2 when not (L_1 `canFlowTo` L_2) is called downgrading.

The basic method of the PrivDesc 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.

By convention, all PrivDesc instances are also be instances of Monoid, allowing privileges to be combined with mappend. The creation of 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.

Privilege descriptions

class Label l => PrivDesc l p where

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

canFlowToPrivDesc :: p -> l -> l -> Bool

The "can-flow-to given privileges" pre-order used to compare two labels in the presence of privileges. If canFlowToP p L_1 L_2 holds, then privileges p are sufficient to downgrade data from L_1 to L_2. Note that canFlowTo L_1 L_2 implies canFlowToP p L_1 L_2 for all p, but for some labels and privileges, canFlowToP will hold even where canFlowTo does not.

partDowngradePrivDesc

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 == NoPrivs, the resulting label L_r == L `lub` L_g. If p 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:

1. L_g ⊑ L_l, and
2. 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

Label l => PrivDesc l NoPrivs

With lack of privileges, canFlowToP is simply canFlowTo, and partDowngradeP is the least upperBound.

PrivDesc DCLabel Component

canFlowToP :: PrivDesc l p => Priv p -> l -> l -> Bool

TODO(dm): document

partDowngradeP :: PrivDesc l p => Priv p -> l -> l -> l

TODO(dm): document

Privileges

data Priv a

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.

Instances

Typeable1 Priv

Eq a => Eq (Priv a)

Show a => Show (Priv a)

Monoid p => Monoid (Priv p)

ToComponent (Priv Component)

privDesc :: Priv a -> a

data NoPrivs

Generic privilege type used to denote the lack of privileges.

Instances

Read NoPrivs

Show NoPrivs

Monoid NoPrivs

Label l => PrivDesc l NoPrivs

With lack of privileges, canFlowToP is simply canFlowTo, and partDowngradeP is the least upperBound.

noPrivs :: Priv NoPrivs

Gates

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 Gate d a given a computation of type d -> a. Here, d is a privilege description (type variable for an instance of PrivDesc). Gates are invoked with 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 callGate.

data Gate d a

A Gate is a lambda abstraction from a privilege description to an arbitrary type a. Applying the gate is accomplished with callGate which takes a privilege argument that is converted to a description before invoking the gate computation.

gate

Arguments

:: (d -> a)

Gate computation

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

callGate

Arguments

:: Gate p a

Gate

-> Priv p

Privilege used as proof-of-ownership

-> a

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.

Gate example

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

 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
   ]