**Reading:** §4.6–4.7, [LT05], 5.2.1–5.2.2

- English policy
- Authorized Use Policy
- Electronic Mail Policy

- Secure, precise
- Observability postulate
- 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* - Theorem: There is no effective procedure that determines a maximally precise, secure mechanism for any policy and program

- Bell-LaPadula Model: intuitive, security classifications only
- Show level, categories, define clearance and classification
- Lattice: poset with ≤ relation reflexive, antisymmetric, transitive; greatest lower bound, least upper bound
- Apply lattice
- Set of classes
*SC*is a partially ordered set under relation*dom*with*glb*(greatest lower bound),*lub*(least upper bound) operators - Note:
*dom*is reflexive, transitive, antisymmetric - Example: (
*A*,*C*)*dom*(*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*′)

- Set of classes
- Simple security condition (no reads up), *-property (no writes down), discretionary security property
- Basic Security Theorem: if it is secure and transformations follow these rules, it will remain secure
- Maximum, current security level

A PDF version is available here.

ECS 235B, Foundations of Computer and Information Security Winter Quarter 2012 |