Outline for January 26, 2007

Greetings and Felicitations!

Security policies and mechanisms

Policy vs. mechanism

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

BellLaPadula Model: intuitive, security classifications only

Security clearance, classification

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

BellLaPadula Model: full model

Show categories, refefine 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′)

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

BLP: formally

Elements of system: s_{i} subjects, o_{i} objects

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: f_{s} is security level associated with each subject, f_{o} security level associated with each object, and f_{c} current security level for each subject;
H hierarchy of system objects, functions h: O→P(O) with two properties:

If o_{i} o_{j}, then h(o_{i}) ∩ h(o_{j}) = ∅

There is no set { o_{1}, ..., o_{k} } ⊆ O such that for each i, o_{i}_{+1} ∈ h(o_{i}) and o_{k}_{+1} = o_{1}.
Here is a PDF version of this document.