# Outline for April 17, 2006

1. Greetings and felicitations!
2. Lattice models
1. Poset, ≤ the relation
2. Reflexive, antisymmetric, transitive
3. Greatest lower bound, least upper bound
4. Example with complex numbers
1. Security clearance, categories, levels
2. Simple security condition (no reads up)
3. *-property (no writes down)
4. Discretionary security property
5. Basic Security Theorem: if it is secure and transformations follow these rules, it will remain secure
1. Apply lattice work
1. Set of classes SC is a partially ordered set under relation dom with glb (greatest lower bound), lub (least upper bound) operators
2. Note: dom is reflexive, transitive, antisymmetric
3. Example: (A, C) dom (A′, C′) iff AA′ and CC′; lub((A, C), (A′, C′)) = (max(A, A′), CC′), glb((A, C), (A′, C′)) = (min(A, A′), CC′)
2. Simple security condition (no reads up)
3. *-property (no writes down)
4. Discretionary security property
5. Basic Security Theorem: if it is secure and transformations follow these rules, it will remain secure
6. Maximum, current security level
5. BLP: formally
1. Elements of system: si subjects, oi objects
2. 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: fs is security level associated with each subject, fo security level associated with each object, and fc current security level for each subject
H hierarchy of system objects, functions h: OP(O) with two properties:
1. If oioj, then h(oi) ∩ h(oj) = ∅
2. There is no set { o1, ..., ok } ⊆ O such that for each i, oi+1h(oi) and ok+1 = o1.
3. Set of requests is R
4. Set of decisions is D
5. WR×D×V×V is motion from one state to another.
6. System Σ(R, D, W, z0) ⊆ X×Y×Z such that (x, y, z) ∈ Σ(R, D, W, z0) iff (xt, yt, zt, zt-1) ∈ W for each iT; latter is an action of system
7. Theorem: Σ(R, D, W, z0) satisfies the simple security property for any initial state z0 that satisfies the simple security property iff W satisfies the following conditions for each action (ri, di, (b′, m′, f′, h′), (b, m, f, h)):
1. 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 fs(s) dom fo(o))
2. if (s, o, x) ∈ b does not satisfy the simple security condition relative to f′, then (s, o, x) ∉ b′
8. Theorem: Σ(R, D, W, z0) satisfies the *-property relative to S′S, for any initial state z0 that satisfies the *-property relative to S′ iff W satisfies the following conditions for each (ri, di, (b′, m′, f′, h′), (b, m, f, h)):
1. for each sS′, any (s, o, x) ∈ b′b satisfies the *-property with respect to f′
2. for each sS′, if (s, o, x) ∈ b does not satisfy the *-property with respect to f′, then (s, o, x) ∉ b′
9. Theorem: Σ(R, D, W, z0) satisfies the ds-property iff the initial state z0 satisfies the ds-property and W satisfies the following conditions for each action (ri, di, (b′, m′, f′, h′), (b, m, f, h)):
1. if (s, o, x) ∈ b′b, then xm′[s, o];
2. if (s, o, x) ∈ b and xm′[s, o] then (s, o, x) ∉ b′

Version of April 17, 2006 at 12:25 PM