Outline for January 31, 2007

1. Greetings and Felicitations!
2. BLP: formally, continued
1. Theorem: Σ(R, D, W, z0) satisfies the simple security property for any initial state z0 that satisfies the simple security property iff W satisfies the following conditions for each action (ri, di, (b′, m′, f′ , h′), (b, m, f, h)):
1. 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 fs(s) dom fo(o))
2. if (s, o, x) ∈ b does not satisfy the simple security condition relative to f′, then (s, o, x) ∉ b
2. Theorem: Σ(R, D, W, z0) satisfies the *-property relative to S′ ⊆ S, for any initial state z0 that satisfies the *-property relative to S′ iff W satisfies the following conditions for each (ri, di, (b′, m′, f′ , h′), (b, m, f, h)):
1. for each sS′, any (s, o, x) ∈ b′-b satisfies the *-property with respect to f
2. for each sS′, if (s, o, x) ∈ b does not satisfy the *-property with respect to f′, then (s, o, x) ∉ b
3. Theorem: Σ(R, D, W, z0) satisfies the ds-property iff the initial state z0 satisfies the ds-property and W satisfies the following conditions for each action (ri, di, (b′, m′, f′ , h′), (b, m, f, h)):
1. if (s, o, x) ∈ b′-b, then xm′[s, o];
2. if (s, o, x) ∈ b and xm′[s, o] then (s, o, x) ∉ b
4. Basic Security Theorem: A system Σ(R, D, W, z0) is secure iff z0 is a secure state and W satisfies the conditions of the above three theorems for each action.
3. Using the model
1. Define ssc-preserving, *-property-preserving, ds-property-preserving
2. Define relation W(ω)
3. Show conditions under which rules are ssc-preserving, *-property-preserving, ds-property-preserving
4. Show when adding a state preserves those properties
5. Example instantiation: get-read for Multics
4. Tranquility
1. Strong tranquility
2. Weak tranquility
5. System Z and the controversy

Here is a PDF version of this document.