lio-0.11.6.0: Labeled IO Information Flow Control Library

LIO.Label

Synopsis

# Labels

Labels are a way of describing who can observe and modify data. Labels are governed by a partial order, generally pronounced "can flow to." In LIO, we write this relation canFlowTo. In the literature, it is usually written ⊑.

At a high level, the purpose of this whole library is to ensure that data labeled l1 may affect data labeled l2 only if l1 canFlowTo l2. The LIO monad (see LIO.Core) ensures this by keeping track of a current label of the executing thread (accessible via the getLabel function). Code may attempt to perform various IO or memory operations on labeled data. Touching data may change the current label and will throw an exception in the event that an operation would violate information flow restrictions.

The specific invariant maintained by LIO is, first, that labels on all previously observed data must flow to a thread's current label. Second, the current label must flow to the labels of any future objects the thread will be allowed to modify. Hence, after a thread with current label lcur observes data labeled l1, it must hold that l1 canFlowTo lcur. If the thread is later permitted to modify an object labeled l2, it must hold that lcur canFlowTo l2. By transitivity of the canFlowTo relation, it holds that l1 canFlowTo l2.

class (Eq l, Show l, Read l, Typeable l) => Label l where Source #

This class defines the operations necessary to make a label into a lattice (see http://en.wikipedia.org/wiki/Lattice_(order)). canFlowTo partially orders labels. lub and glb compute the least upper bound and greatest lower bound of two labels, respectively.

Minimal complete definition

Methods

lub :: l -> l -> l infixl 5 Source #

Compute the least upper bound, or join, of two labels. When data carrying two different labels is mixed together in a document, the lub of the two labels is the lowest safe value with which to label the result.

More formally, for any two labels l1 and l2, if ljoin = l1 lub l2, it must be that:

• L_1 canFlowTo ljoin,
• L_2 canFlowTo ljoin, and
• There is no label l /= ljoin such that l1 canFlowTo l, l2 canFlowTo l, and l canFlowTo ljoin. In other words ljoin is the least element to which both l1 and l2 can flow.

When used infix, has fixity:

infixl 5 lub

glb :: l -> l -> l infixl 5 Source #

Greatest lower bound, or meet, of two labels. For any two labels l1 and l2, if lmeet = l1 glb l2, it must be that:

• lmeet canFlowTo l1,
• lmeet canFlowTo l2, and
• There is no label l /= lmeet such that l canFlowTo l1, l canFlowTo l2, and lmeet canFlowTo l. In other words lmeet is the greatest element flowing to both l1 and l2.

When used infix, has fixity:

infixl 5 glb

canFlowTo :: l -> l -> Bool infix 4 Source #

Can-flow-to relation (⊑). An entity labeled l1 should be allowed to affect an entity l2 only if l1 canFlowTo l2. This relation on labels is at least a partial order (see https://en.wikipedia.org/wiki/Partially_ordered_set), and must satisfy the following laws:

• Reflexivity: l1 canFlowTo l1 for any l1.
• Antisymmetry: If l1 canFlowTo l2 and l2 canFlowTo l1 then l1 = l2.
• Transitivity: If l1 canFlowTo l2 and l2 canFlowTo l3 then l1 canFlowTo l3.

When used infix, has fixity:

infix 4 canFlowTo

Instances

 Source # Methods

# Privileges

Privileges are objects the possesion of which allows code to bypass certain label protections. An instance of class PrivDesc describes a pre-order (see http://en.wikipedia.org/wiki/Preorder) among labels in which certain unequal labels become equivalent. A Priv object containing a PrivDesc instance allows code to make those unequal labels equivalent for the purposes of many library functions. Effectively, a PrivDesc instance describes privileges, while a Priv object embodies them.

Any code is free to construct PrivDesc values describing arbitrarily powerful privileges. Security is enforced by preventing safe code from accessing the constructor for Priv (called PrivTCB). Safe code can construct arbitrary privileges from the IO monad (using privInit in LIO.Run), but cannot do so from the LIO monad. Starting from existing privileges, safe code can also delegate lesser privileges (see LIO.Delegate).

Privileges allow you to behave as if l1 canFlowTo l2 even when that is not the case, but only for certain pairs of labels l1 and l2; which pairs depends on the specific privileges. The process of allowing data labeled l1 to infulence data labeled l2 when (l1 canFlowTo l2) == False is known as downgrading.

The core privilege function is canFlowToP, which performs a more permissive can-flow-to check by exercising particular privileges (in the literature this relation is commonly written ⊑ₚ for privileges p). Most core LIO functions have variants ending ...P that take a privilege argument to act in a more permissive way.

By convention, all PrivDesc instances should also be instances of Monoid, allowing privileges to be combined with mappend, though there is no superclass to enforce this.

class (Typeable p, Show p) => SpeaksFor p where Source #

Every privilege type must be an instance of SpeaksFor, which is a partial order specifying when one privilege value is at least as powerful as another. If canFlowToP p1 l1 l2 and p2 speaksFor p1, then it should also be true that canFlowToP p2 l1 l2.

As a partial order, SpeaksFor should obey the reflexivity, antisymmetry and transitivity laws. However, if you do not wish to allow delegation of a particular privilege type, you can define speaksFor _ _ = False (which violates the reflexivity law, but is reasonable when you don't want the partial order).

Minimal complete definition

speaksFor

Methods

speaksFor :: p -> p -> Bool infix 4 Source #

speaksFor p1 p2 returns True iff p1 subsumes all the privileges of p2. In other words, it is safe for delegate to hand out p2 to a caller who already has p1.

Has fixity:

infix 4 speaksFor

Instances

 Source # Methods Source # Methods SpeaksFor p => SpeaksFor (Priv p) Source # MethodsspeaksFor :: Priv p -> Priv p -> Bool Source #

class (Label l, SpeaksFor p) => PrivDesc l p where Source #

This class represents privilege descriptions, which define a pre-order on labels in which distinct labels become equivalent. The pre-oder implied by a privilege description is specified by the method canFlowToP. In addition, this this class defines a method downgradeP, which is important for finding least labels satisfying a privilege equivalence.

Minimal complete definition: downgradeP.

(The downgradeP requirement represents the fact that a generic canFlowToP can be implemented efficiently in terms of downgradeP, but not vice-versa.)

Minimal complete definition

Methods

downgradeP :: p -> l -> l Source #

Privileges are described in terms of a pre-order on labels in which sets of distinct labels become equivalent. downgradeP p l returns the lowest of all labels equivalent to l under privilege description p.

Less formally, downgradeP p l returns a label representing the furthest you can downgrade data labeled l given privileges described by p.

canFlowToP :: p -> l -> l -> Bool Source #

canFlowToP p l1 l2 determines whether p describes sufficient privileges to observe data labeled l1 and subsequently write it to an object labeled l2. The function returns True if and only if either canFlowTo l1 l2 or l1 and l2 are equivalent under p.

The default definition is:

canFlowToP p l1 l2 = downgradeP p l1 canFlowTo l2

canFlowToP is a method rather than a function so that it can be optimized in label-specific ways. However, custom definitions should behave identically to the default.

Instances

 Label l => PrivDesc l NoPrivs Source # downgradeP NoPrivs is the identify function. Hence canFlowToP NoPrivs is the same as canFlowTo. MethodsdowngradeP :: NoPrivs -> l -> l Source #canFlowToP :: NoPrivs -> l -> l -> Bool Source # Source # Methods PrivDesc l p => PrivDesc l (Priv p) Source # MethodsdowngradeP :: Priv p -> l -> l Source #canFlowToP :: Priv p -> l -> l -> Bool Source #

data Priv a Source #

A newtype wrapper that can be used by trusted code to transform a powerless description of privileges into actual privileges. The constructor, PrivTCB, is dangerous as it allows creation of arbitrary privileges. Hence it is only exported by the unsafe module LIO.TCB. A safe way to create arbitrary privileges is to call privInit (see LIO.Run) from the IO monad before running your LIO computation.

Instances

 PrivDesc l p => PrivDesc l (Priv p) Source # MethodsdowngradeP :: Priv p -> l -> l Source #canFlowToP :: Priv p -> l -> l -> Bool Source # Eq a => Eq (Priv a) Source # Methods(==) :: Priv a -> Priv a -> Bool #(/=) :: Priv a -> Priv a -> Bool # Show a => Show (Priv a) Source # MethodsshowsPrec :: Int -> Priv a -> ShowS #show :: Priv a -> String #showList :: [Priv a] -> ShowS # Monoid p => Monoid (Priv p) Source # Methodsmempty :: Priv p #mappend :: Priv p -> Priv p -> Priv p #mconcat :: [Priv p] -> Priv p # SpeaksFor p => SpeaksFor (Priv p) Source # MethodsspeaksFor :: Priv p -> Priv p -> Bool Source # Source # Methods

privDesc :: Priv a -> a Source #

Turns privileges into a powerless description of the privileges by unwrapping the Priv newtype.

## Internal functions

isPriv :: Typeable p => p -> Bool Source #

Uses dynamic typing to return True iff the type of the argument is Priv a (for any a). Mostly useful to prevent users from accidentally wrapping Priv objects inside other Priv objects or accidentally including real privileges in an exception.

# Empty privileges

data NoPrivs Source #

Generic PrivDesc used to denote the lack of privileges. Works with any Label type. This is only a privilege description; a more useful symbol is noPrivs, which actually embodies the NoPrivs privilege.

Constructors

 NoPrivs

Instances

 Source # Methods Source # MethodsshowList :: [NoPrivs] -> ShowS # Source # Methodsmconcat :: [NoPrivs] -> NoPrivs # Source # Methods Label l => PrivDesc l NoPrivs Source # downgradeP NoPrivs is the identify function. Hence canFlowToP NoPrivs is the same as canFlowTo. MethodsdowngradeP :: NoPrivs -> l -> l Source #canFlowToP :: NoPrivs -> l -> l -> Bool Source #

Priv object corresponding to NoPrivs.