January 28, 2014 Outline

Reading: text, §5
Assignment due: Project progress report, due February 4, 2014; Homework #2, due February 11, 2014


  1. 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. Note: dom is reflexive, transitive, antisymmetric
      3. Example: (A, C) dom (A′, C′) iff AA′ and CC′;
        lub((A, C), (A′, C′)) = max(A, A′), CC′); and
        glb((A, C), (A′, C′)) = min(A, A′), CC′)
    4. Simple security condition (no reads up), *-property (no writes down), discretionary security property
    5. Basic Security Theorem: if it is secure and transformations follow these rules, it will remain secure
    6. Maximum, current security level
  2. Bell-LaPadula: formal model
    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: OP(O) with two properties:
      1. If oioj, then h(oi) ∩ h(oi) = ∅
      2. There is no set { o1, …, ok } ⊆ O such that for each i, oi+1h(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 tT; latter is an action of system
    7. Theorem: Σ(R, D, W, z0) satisfies the simple security condition for any initial state z0 that satisfies the simple security condition iff W satisfies the following conditions for each action (r, d, (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) dom fo(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, 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 (r, d, (b′, m′, f′, h′), (b, m, f, h)):
      1. for each sS′, any (s, o, x) ∈ b′ − b satisfies the *-property with respect to f′; and
      2. for each sS′, 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 (r, d, (b′, m′, f′, h′), (b, m, f, h)):
      1. if (s, o, x) ∈ b′ − b, then xm′[s, o]; and
      2. if (s, o, x) ∈ b and xm′[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.
  3. Using the model
    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


You can also obtain a PDF version of this. Version of January 22, 2014 at 9:11PM