# Outline for April 24, 2003

1. Apply lattice work
1. Set of classes SC is a partially ordered set under relation ≤ with GLB (greatest lower bound), LUB (least upper bound) operators
2. Note: is reflexive, transitive, antisymmetric
3. Examples: (A, C) ≤ (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´)
2. Describe simple security condition (no reads up), *-property (no writes down), discretionary security property
3. State Basic Security Theorem: if it's secure and transformations follow these rules, it's still secure
4. Maximum, current security level
2. Example: DG/UX UNIX
1. Labels and regions
2. Multilevel directories
3. File object labels
4. MAC tuples
3. 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:O->P(O) with two properties:
If oi <> oj, then h(oi) ∩ h(oj) = Ø
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 statez0 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' (ie, x is not read, or x is read and fs(s) dominates 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. Σ(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'
10. Basic Security Theorem: A system Σ(R, D, W, z0) is secure iff z0 is a secure state and W satisfies the conditions of the above three theorems for each action.

This document is also available in Postscript and PDF.