- Bell-LaPadula Model: intuitive, security classifications only
- Show level, categories, define clearance and classification
- Lattice: poset with ≤ relation reflexive, antisymmetric, transitive; greatest lower bound, least upper bound
- Apply lattice
- Set of classes
*SC*is a partially ordered set under relation*dom*with glb (greatest lower bound), lub (least upper bound) operators - Note:
*dom*is reflexive, transitive, antisymmetric - Example: (
*A*,*C*)*dom*(*A*′,*C*′) iff*A*≤*A*′ and*C*⊆*C*′;

lub((*A*,*C*), (*A*′,*C*′)) = max(*A*,*A*′),*C*∪*C*′); and

glb((*A*,*C*), (*A*′,*C*′)) = min(*A*,*A*′),*C*∪*C*′)

- Set of classes
- Simple security condition (no reads up), *-property (no writes down), discretionary security property
- Basic Security Theorem: if it is secure and transformations follow these rules, it will remain secure
- Maximum, current security level

- 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:
- 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

You can also obtain a PDF version of this. | Version of January 22, 2014 at 9:11PM |