Outline for January 26, 2007

1. Greetings and Felicitations!
2. Security policies and mechanisms
   1. Policy vs. mechanism
   2. Secure, precise
   3. Observability postulate
   4. 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
   5. Theorem: There is no effective procedure that determines a maximally precise, secure mechanism for any policy and program
3. Bell-LaPadula Model: intuitive, security classifications only
   1. Security clearance, classification
   2. Simple security condition (no reads up), *-property (no writes down), discretionary security property
   3. Basic Security Theorem: if it is secure and transformations follow these rules, it will remain secure
4. Bell-LaPadula Model: full model
   1. Show categories, refefine 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 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 it is secure and transformations follow these rules, it will remain secure
   6. Maximum, current security level
5. 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:
      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₁.