Outline for April 27, 2004

1. BLP: formally
   1. Elements of system: si subjects, oi objects,
   2. 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₁, ..., o_k } ⊆ O such that for each i, o_i+1 ∈ h(o_i) and o_i+1 = o₁.
   3. Set of requests is R
   4. Set of decisions is D
   5. W ⊆ R × D × V × V is motion from one state to another.
   6. System Σ(R, D, W, z₀) ⊆ X × Y × Z such that (x, y, z) ∈ Σ(R, D, W, z₀) iff (x_t, y_t, z_t, z_t-1) ∈ W for each i ∈ T; latter is an action of system
   7. Theorem: Σ(R, D, W, z₀) satisfies the simple security property for any initial state z₀ 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)):
      (i) 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))
      (ii) if (s, o, x) ∈ b does not satisfy the simple security condition relative to f´, then (s, o, x) ∉ b´
   8. Theorem: Σ(R, D, W, z₀) satisfies the *-property relative to S´ ⊆ S for any initial state z₀ that satisfies the *-property relative to S´ ⊆ S iff W satisfies the following conditions for each action (r_i, d_i, (b´, m´, f´, h´), (b, m, f, h)):
      (i) for each s ∈ S´, any (s, o, x) ∈ b´ - b satisfies the *-property with respect to f´ (ii) for each s ∈ S´, if (s, o, x) ∈ b does not satisfy the *-property with respect to f´, then (s, o, x) ∉ b´
   9. Theorem: Σ(R, D, W, z₀) satisfies the ds-property for any initial state z₀ that satisfies the ds-property iff W satisfies the following conditions for each action (r_i, d_i, (b´, m´, f´, h´), (b, m, f, h)):
      (i) if (s, o, x) ∈ b´ - b, then x ∈ m´[s, o];
      (ii) if (s, o, x) ∈ b and x ∉ m´[s, o], then (s, o, x) ∉ b´
   10. 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.
2. 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
3. Tranquility
   1. Strong tranquility
   2. Weak tranquility
4. System Z and the controversy
5. Goals of integrity policies