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
dom is reflexive, transitive, antisymmetric
(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′
Simple security condition (no reads up), *-property (no writes down), discretionary security property
Basic Security Theorem: if system is secure and transformations follow these rules, system will remain secure