- BLP: formally
- Elements of system: si subjects, oi objects,
- 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*_{i+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*)):

(i) 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*f*(_{s}*s*) dominates*f*(_{o}*o*))

(ii) if (*s*,*o*,*x*) ∈*b*does not satisfy the simple security condition relative to*f´*, then (*s*,*o*,*x*) ∉*b´* - 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´*⊆*S*iff*W*satisfies the following conditions for each action (*r*,_{i}*d*, (_{i}*b´*,*m´*,*f´*,*h´*), (*b*,*m*,*f*,*h*)):

(i) for each*s*∈*S´*, any (*s*,*o*,*x*) ∈*b´*-*b*satisfies the *-property with respect to*f´*(ii) for each*s*∈*S´*, if (*s*,*o*,*x*) ∈*b*does not satisfy the *-property with respect to*f´*, then (*s*,*o*,*x*) ∉*b´* - Theorem: Σ(
*R*,*D*,*W*,*z*_{0}) satisfies the ds-property for any initial state*z*_{0}that satisfies the ds-property iff*W*satisfies the following conditions for each action (*r*,_{i}*d*, (_{i}*b´*,*m´*,*f´*,*h´*), (*b*,*m*,*f*,*h*)):

(i) if (*s*,*o*,*x*) ∈*b´*-*b*, then*x*∈*m´*[*s*,*o*];

(ii) if (*s*,*o*,*x*) ∈*b*and*x*∉*m´*[*s*,*o*], then (*s*,*o*,*x*) ∉*b´* - 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.

- BLP: formally
- Define ssc-preserving, *-property-preserving, ds-property-preserving
- Define relation
*W*(ω) - Show conditions under which rules are ssc-preserving, *-property-preserving, ds-property-preserving
- Show when adding a state preserves those properties
- Example instantiation:
*get-read*for Multics

- Tranquility
- Strong tranquility
- Weak tranquility

- System Z and the controversy
- Goals of integrity policies

Here is a PDF version of this document.