Outline for April 22, 2013

1. Secure, precise
   1. Observability postulate
   2. Theorem: for any program p and policy c, there is a secure, precise mechanism m^* such that, for all security mechanisms m associated with p and c, m^* ≈ m
   3. Theorem: There is no effective procedure that determines a maximally precise, secure mechanism for any policy and program
2. Bell-LaPadula Model: intuitive, security classifications only
   1. Show level, categories, define clearance and classification
   2. Lattice: poset with ≤ relation reflexive, antisymmetric, transitive; greatest lower bound, least upper bound
   3. Apply lattice
      1. Set of classes SC is a partially ordered set under relation dom with glb (greatest lower bound), lub (least upper bound) operators
      2. dom is reflexive, transitive, antisymmetric
      3. (A, C) dom (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′
   4. Simple security condition (no reads up), *-property (no writes down), discretionary security property
   5. Basic Security Theorem: if system is secure and transformations follow these rules, system will remain secure
   6. Maximum, current security level
3. Bell-LaPadula: formal model
   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:
      1. If o_i ≠ o_j, then h(o_i) ∩ h(o_j) = ∅
      2. 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 t ∈ T; latter is an action of system
   7. Theorem: Σ(R, D, W, z₀) satisfies the simple security condition for any initial state z₀ that satisfies the simple security condition 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′ (i.e., x is not read, or x is read and f_s(s) dom f_o(o); and
      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′; and
      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. Theorem: Σ(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 (r_i, d_i, (b′, m′, f′, h′), (b, m, f, h)):
      1. if (s, o, x) ∈ b′−b, then x ∈ m′[s, o]; and
      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.