- Bell-LaPadula Model
- Apply lattice work
- Set of classes SC is a partially ordered set under relation ≤ with GLB (greatest lower bound), LUB (least upper bound) operators
- Note: is reflexive, transitive, antisymmetric
- 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´)

- Describe simple security condition (no reads up), *-property (no writes down), discretionary security property
- State Basic Security Theorem: if it's secure and transformations follow these rules, it's still secure
- Maximum, current security level

- Apply lattice work
- Example: DG/UX UNIX
- Labels and regions
- Multilevel directories
- File object labels
- MAC tuples

- BLP: formally
- Elements of system:
*s*subjects,_{i}*o*objects,_{i} - 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*is security level associated with each subject,_{s}*f*security level associated with each object, and_{o}*f*current security level for each subject_{c}

*H*hierarchy of system objects, functions*h*:*O*->*P*(*O*) with two properties:

If*o*<>_{i}*o*, then_{j}*h*(*o*) ∩_{i}*h*(*o*) = Ø_{j}

There is no set {*o*_{1}, ...,*o*} ⊆_{k}*O*such that for each*i*,*o*_{i+1}∈*h*(*o*) and_{i}*o*_{k+1}=*o*_{1}. - Set of requests is
*R* - Set of decisions is
*D* *W*⊆*R*×*D*×*V*×*V*is motion from one state to another.- System Σ(
*R*,*D*,*W*,*z*_{0}) ⊆*X*×*Y*×*Z*such that (*x*,*y*,*z*) ∈ Σ(*R*,*D*,*W*,*z*_{0}) iff (*x*,_{t}*y*,_{t}*z*,_{t}*z*_{t-1}) ∈*W*for each*i*∈*T*; latter is an action of system - Theorem:
Σ(
*R*,*D*,*W*,*z*_{0}) satisfies the simple security property for any initial state*z*_{0}that satisfies the simple security property iff*W*satisfies the following conditions for each action (*r*,_{i}*d*, (_{i}*b*',*m*',*f*',*h*'), (*b*,*m*,*f*,*h*)):

- each (
*s*,*o*,*x*) ∈*b*' -*b*satisfies the simple security condition relative to*f*' (ie,*x*is not read, or*x*is read and*f*(_{s}*s*) dominates*f*(_{o}*o*)

- if (
*s*,*o*,*x*) ∈*b*does not satisfy the simple security condition relative to*f*', then (*s*,*o*,*x*) ∉*b*'

- each (
- Theorem:
Σ(
*R*,*D*,*W*,*z*_{0}) satisfies the *-property relative to*S*' ⊆*S*, for any initial state*z*_{0}that satisfies the *-property relative to*S*' iff*W*satisfies the following conditions for each (*r*,_{i}*d*, (_{i}*b*',*m*',*f*',*h*'), (*b*,*m*,*f*,*h*)):

- for each
*s*∈*S*', any (*s*,*o*,*x*) ∈*b*' -*b*satisfies the *-property with respect to*f*'

- for each
*s*∈*S*', if (*s*,*o*,*x*) ∈*b*does not satisfy the *-property with respect to*f*', then (*s*,*o*,*x*) ∉*b*'

- for each
- Σ(
*R*,*D*,*W*,*z*_{0}) satisfies the ds-property iff the initial state*z*_{0}satisfies the ds-property and*W*satisfies the following conditions for each action (*r*,_{i}*d*, (_{i}*b*',*m*',*f*',*h*'), (*b*,*m*,*f*,*h*)):- if (
*s*,*o*,*x*) ∈*b*' -*b*, then*x*∈*m*[*s*,*o*]; - if (
*s*,*o*,*x*) ∈*b*and*x*∉*m*[*s*,*o*] then (*s*,*o*,*x*) ∉*b*'

- if (
- Basic Security Theorem: A system
Σ(
*R*,*D*,*W*,*z*_{0}) is secure iff*z*_{0}is a secure state and W satisfies the conditions of the above three theorems for each action.

- Elements of system:

This document is also available in Postscript and PDF.