# Outline for May 3, 2005

1. BLP: formally
1. Review:
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:
If oi oj, then h(oi) h(oj) = Ø
There is no set { o1, ..., ok } O such that for each i, oi+1 h(oi) and ok+1 = o1.
3. Set of requests is R
4. Set of decisions is D
5. W R×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 i T; latter is an action of system
2. 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) dominates fo(o))
2. if (s, o, x) b does not satisfy the simple security condition relative to f´, then (s, o, x) b´
3. 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 s S´, any (s, o, x) b´ - b satisfies the *-property with respect to f´
2. for each s S´, if (s, o, x) b does not satisfy the *-property with respect to f´, then (s, o, x) b´
4. 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 x m´[s, o];
2. if (s, o, x) b and x m´[s, o] then (s, o, x) b´
5. 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.
2. BLP: formally
1. Define ssc-preserving, *-property-preserving, ds-property-preserving
2. Define relation W(ω)
3. Show conditions under which rules are ssc-preserving, *-property-preserving, ds-property-preserving
4. Show when adding a state preserves those properties
5. Example instantiation: get-read for Multics
3. Tranquility
1. Strong tranquility
2. Weak tranquility
4. System Z and the controversy