lio- Labeled IO Information Flow Control Library

Safe HaskellTrustworthy




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


privDesc :: p -> dSource

Retrive privilege description from a privilege.


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



:: p


-> l

Label from which data must flow

-> l

Goal label

-> l


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 `upperBound` 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.


Label l => Priv l NoPrivs

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

Priv DCLabel DCPriv 

data NoPrivs Source

Generic privilege type used to denote the lack of privileges.