# Outline for April 24, 2013

Reading: §5.2.3–5.2.4, 5.3, 5.4; handout
Due: Homework #2, due April 26, 2013
1. Bell-LaPadula: formal model
1. Set of requests is R
2. Set of decisions is D
3. WR × D × V × V is motion from one state to another.
4. System Σ(R, D, W, z0) ⊆ X × Y × Z such that (x, y, z) ∈ Σ(R, D, W, z0) iff (xt, yt, zt, zt−1) ∈ W for each tT; latter is an action of system
5. Theorem: Σ(R, D, W, z0) satisfies the simple security condition for any initial state z0 that satisfies the simple security condition 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); and
2. if (s, o, x) ∈ b does not satisfy the simple security condition relative to f′, then (s, o, x) ≠ b
6. 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′; and
2. for each sS′, if (s, o, x) ∈ b does not satisfy the *-property with respect to f′, then (s, o, x) ≠ b
7. 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 (ri, di, (b′, m′, f′, h′), (b, m, f, h)):
1. if (s, o, x) ∈ b′−b, then xm′[s, o]; and
2. if (s, o, x) ∈ b and xm′[s, o], then (s, o, x) ≠ b
8. 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.
2. 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
3. Tranquility
1. Strong tranquility
2. Weak tranquility
4. System Z and the controversy

 You can also obtain a PDF version of this. Version of April 23, 2013 at 7:06PM