January 25, 2019 Outline

Reading: text, §5.1–5.3

1. Instantiation of Bell-LaPadula Model: Trusted Solaris
2. Bell-LaPadula: formal model
   1. Elements of system: s_i ∈ S subjects, o_i ∈ O 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_i) = ∅
      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

Matt Bishop Office: 2209 Watershed Science Phone: +1 (530) 752-8060 Email: mabishop@ucdavis.edu

You can also obtain a PDF version of this. Version of January 25, 2019 at 3:51PM