April 17, 2017 Outline

Reading: Chapters from revised text §4, 5

  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, mm*
    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. 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
  3. Bell-LaPadula: formal model
    1. Elements of system: si subjects, oi objects

You can also obtain a PDF version of this. Version of April 18, 2017 at 2:25PM