Outline for April 24, 2003

1. Bell-LaPadula Model
   1. Apply lattice work
      1. Set of classes SC is a partially ordered set under relation ≤ with GLB (greatest lower bound), LUB (least upper bound) operators
      2. Note: is reflexive, transitive, antisymmetric
      3. Examples: (A, C) ≤ (A´, C´) iff A ≤ A´ and C ⊆ C´;
         LUB((A, C), (A´, C´)) = (max(A, A´), C ∪ C´), GLB((A, C), (A´, C´)) = (min(A, A´), C ∩ C´)
   2. Describe simple security condition (no reads up), *-property (no writes down), discretionary security property
   3. State Basic Security Theorem: if it's secure and transformations follow these rules, it's still secure
   4. Maximum, current security level
2. Example: DG/UX UNIX
   1. Labels and regions
   2. Multilevel directories
   3. File object labels
   4. MAC tuples
3. BLP: formally
   1. Elements of system: s_i subjects, o_i 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_k+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 statez₀ 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)):
      
      1. each (s, o, x) ∈ b' - b satisfies the simple security condition relative to f' (ie, x is not read, or x is read and f_s(s) dominates f_o(o)
         
      2. 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' iff W satisfies the following conditions for each (r_i, d_i, (b', m', f', h'), (b, m, f, h)):
      
      1. for each s ∈ S', any (s, o, x) ∈ b' - b satisfies the *-property with respect to f'
         
      2. for each s ∈ S', if (s, o, x) ∈ b does not satisfy the *-property with respect to f', then (s, o, x) ∉ b'
   9. Σ(R, D, W, z₀) satisfies the ds-property iff the initial state z₀ satisfies the ds-property and W satisfies the following conditions for each action (r_i, d_i, (b', m', f', h'), (b, m, f, h)):
      1. if (s, o, x) ∈ b' - b, then x ∈ m[s, o];
      2. 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.