Outline for January 26, 1999 1. Greetings and felicitations! a. Please get your project proposals in as soon as possible, so you can get started 2. Bell-LaPadula Model a. Go through security levels, categories, compartments b. Describe simple security property (no reads up) and *-property (no writes down) c. State Basic Security Theorem: if it's secure and transformations follow these rules, it's still secure d. Add in discretionary security policy 3. BLP: formally a. Elements of system: si subjects, oi objects, b. State space V = BÄMÄF 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 c. Set of requests is R d. Set of decisions is D e. W ¼ RÄDÄVÄV is motion from one state to another. f. System S(R, D, W, z0) ¼ XÄYÄZ such that (x, y, z) ? S(R, D, W, z0) iff (xt, yt, zt, zt-1) ? W for each i ? T; lat- ter is an action of system g. Theorem: S(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'), (b, M, f)): (i) 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) (ii) if (s, o, x) ? b does not satisfy the simple security condition relative to f', then (s, o, x) ? b' h. Theorem: S(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 action (Ri, Di, (b', M', f'), (b, M, f)): (i) for each s ? S', any (s, o, x) ? b' - b satisfies the *-property with respect to f' (ii) for each s ? S', if (s, o, x) ? b does not satisfy the *-property with respect to f', then (s, o, x) ? b' i. Theorem: S(R, D, W, z0) satisfies the ds-property iff the initial state z0 satisfies the ds-property and W satis- fies the following conditions for each action (Ri, Di, (b', M', f'), (b, M, f)): (i) if (sk, oi, x) ? b' - b, then x ? M'[k, i]; (ii) if (sk, oi, x) ? b and x ? M'[k, i] then (sk, oi, x) ? b' j. Basic Security Theorem: A system S(R, D, W, z0) is secure iff z0 is a secure state and W satisfies the condi- tions of the above three theorems for each action. 4. Biba a. Integrity levels and trust b. No reads down c. No writes up