Outline for May 3, 2005

BLP: formally

Review:

Elements of system: s_{i} subjects, o_{i} objects

State space V = B×M×F×H where:
B set of current accesses (i.e., access modes each subject has currently to each object);
M access permission matrix;
F consists of 3 functions: f_{s} is security level associated with each subject, f_{o} security level associated with each object, and f_{c} current security level for each subject
H hierarchy of system objects, functions h: O→P(O) with two properties:
If o_{i} o_{j}, then h(o_{i}) ∩ h(o_{j}) = Ø
There is no set { o_{1}, ..., o_{k} } ⊆ O such that for each i, o_{i}_{+1} ∈ h(o_{i}) and o_{k}_{+1} = o_{1}.

Set of requests is R

Set of decisions is D

W ⊆ R×D×V×V is motion from one state to another.

System Σ(R, D, W, z_{0}) ⊆ X×Y×Z such that (x, y, z) ∈ Σ(R, D, W, z_{0}) iff (x_{t}, y_{t}, z_{t}, z_{t}_{1}) ∈ W for each i ∈ T; latter is an action of system

Theorem: Σ(R, D, W, z_{0}) satisfies the simple security property for any initial state z_{0} that satisfies the simple security property iff W satisfies the following conditions for each action (r_{i}, d_{i}, (b´, m´, f´, h´), (b, m, f, h)):

each (s, o, x) ∈ b´  b satisfies the simple security condition relative to f´ (i.e., x is not read, or x is read and f_{s}(s) dominates f_{o}(o))

if (s, o, x) ∈ b does not satisfy the simple security condition relative to f´, then (s, o, x) ∉ b´

Theorem: Σ(R, D, W, z_{0}) satisfies the *property relative to S´ ⊆ S, for any initial state z_{0} that satisfies the *property relative to S´ iff W satisfies the following conditions for each (r_{i}, d_{i}, (b´, m´, f´, h´), (b, m, f, h)):

for each s ∈ S´, any (s, o, x) ∈ b´  b satisfies the *property with respect to f´

for each s ∈ S´, if (s, o, x) ∈ b does not satisfy the *property with respect to f´, then (s, o, x) ∉ b´

Theorem: Σ(R, D, W, z_{0}) satisfies the dsproperty iff the initial state z_{0} satisfies the dsproperty and W satisfies the following conditions for each action (r_{i}, d_{i}, (b´, m´, f´, h´), (b, m, f, h)):

if (s, o, x) ∈ b´  b, then x ∈ m´[s, o];

if (s, o, x) ∈ b and x ∈ m´[s, o] then (s, o, x) ∉ b´

Basic Security Theorem: A system Σ(R, D, W, z_{0}) is secure iff z_{0} is a secure state and W satisfies the conditions of the above three theorems for each action.

BLP: formally

Define sscpreserving, *propertypreserving, dspropertypreserving

Define relation W(ω)

Show conditions under which rules are sscpreserving, *propertypreserving, dspropertypreserving

Show when adding a state preserves those properties

Example instantiation: getread for Multics

Tranquility

Strong tranquility

Weak tranquility

System Z and the controversy
Here is a PDF version of this document.