Outline for April 19, 2006

Reading: text, §5.2—5.4

1. Greetings and felicitations!
2. BLP: formally
   1. Basic Security Theorem: A system Σ(R, D, W, z₀) is secure iff z₀ is a secure state and W satisfies the conditions of the above three theorems for each action.
3. BLP: formally
   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