**Reading:** §5.2.3–5.2.4

- Bell-LaPadula: formal model
- 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*) = ∅_{i} - 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}

- If
- 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*,*d*, (*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*,*d*, (*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*,*d*, (*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.

- Elements of system:

A PDF version is available here.

ECS 235B, Foundations of Computer and Information Security Winter Quarter 2012 |