Outline for April 21, 2005

  1. Policy
    1. Policy languages: high level, low level
  2. Bell-LaPadula Model (security classifications only)
    1. Go through security clearance, classification
    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
  3. Bell-LaPadula Model (security levels)
    1. Go through security clearance, categories, levels
  4. Lattice models
    1. Poset, ≤ the relation
    2. Reflexive, antisymmetric, transitive
    3. Greatest lower bound, least upper bound
    4. Example with complex numbers
  5. 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
  6. Example: DG/UX UNIX
    1. Labels and regions
    2. Multilevel directories
    3. File object labels
    4. MAC tuples
  7. 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: fs is security level associated with each subject, fo security level associated with each object, and fc current security level for each subject
      H hierarchy of system objects, functions h: O→P(O) with two properties:
      If oi oj, then h(oi) ∩ h(oj) = Ø
      There is no set { o1, ..., ok } ⊆ O such that for each i, oi+1 ∈ h(oi) and ok+1 = o1.
    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, z0) ⊆ X×Y×Z such that (x, y, z) ∈ Σ(R, D, W, z0) iff (xt, yt, zt, zt-1) ∈ W for each i ∈ T; latter is an action of system
    7. Theorem: Σ(R, D, W, z0) satisfies the simple security property for any initial state z0 that satisfies the simple security property 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) dominates fo(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, 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 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. 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 action (ri, di, (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, z0) is secure iff z0 is a secure state and W satisfies the conditions of the above three theorems for each action.
  8. 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
  9. Tranquility
    1. Strong tranquility
    2. Weak tranquility
  10. System Z and the controversy

Here is a PDF version of this document.