- Bell-LaPadula: formal model
- 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*t*∈*T*; latter is an action of system - Theorem: Σ(
*R*,*D*,*W*,*z*_{0}) satisfies the simple security condition for any initial state*z*_{0}that satisfies the simple security condition 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*′ (i.e.,*x*is not read, or*x*is read and*f*(_{s}*s*) dom*f*(_{o}*o*); and - 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*′; and - 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
- Theorem: Σ(
*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 (*r*,_{i}*d*, (_{i}*b*′,*m*′,*f*′,*h*′), (*b*,*m*,*f*,*h*)):- if (
*s*,*o*,*x*) ∈*b*′−*b*, then*x*∈*m*′[*s*,*o*]; and - 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.

- Set of requests is
- Using the model
- 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

You can also obtain a PDF version of this. | Version of April 23, 2013 at 7:06PM |