Outline for January 31, 2007

Greetings and Felicitations!

BLP: formally, continued

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

Using the model

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.