Outline for January 29, 2007

Greetings and Felicitations!

BellLaPadula Model: full model

Show categories, refefine 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′), glb((A, C), (A′, C′)) = (min(A, A′), C ∩ C′)

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

BLP: formally

Elements of system: s_{i} subjects, o_{i} 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_{s} is security level associated with each subject, f_{o} security level associated with each object, and f_{c} current security level for each subject;
H hierarchy of system objects, functions h: O→P(O) with two properties:

If o_{i} o_{j}, then 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_{i}) and 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} , zt, 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′ (i.e., x is not read, or x is read and f_{s}(s) dom f_{o}(o))

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′ 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′
Here is a PDF version of this document.