# Outline for April 22, 2013

Due: Homework #2, due April 26, 2013

1. Secure, precise
1. Observability postulate
2. Theorem: for any program p and policy c, there is a secure, precise mechanism m* such that, for all security mechanisms m associated with p and c, m*m
3. Theorem: There is no effective procedure that determines a maximally precise, secure mechanism for any policy and program
2. Bell-LaPadula Model: intuitive, security classifications only
1. Show level, categories, define clearance and classification
2. Lattice: poset with ≤ relation reflexive, antisymmetric, transitive; greatest lower bound, least upper bound
3. Apply lattice
1. Set of classes SC is a partially ordered set under relation dom with glb (greatest lower bound), lub (least upper bound) operators
2. dom is reflexive, transitive, antisymmetric
3. (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
4. Simple security condition (no reads up), *-property (no writes down), discretionary security property
5. Basic Security Theorem: if system is secure and transformations follow these rules, system will remain secure
6. Maximum, current security level
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 tT; latter is an action of system
7. Theorem: Σ(R, D, W, z0) satisfies the simple security condition for any initial state z0 that satisfies the simple security condition 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); and
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′; and
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 (ri, di, (b′, m′, f′, h′), (b, m, f, h)):
1. if (s, o, x) ∈ b′−b, then xm′[s, o]; and
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.

 You can also obtain a PDF version of this. Version of April 20, 2013 at 10:36PM