Lattice Models

Lattice Model
subjects
objects
security classes (SC)

(object x is in security class x)

Flow Policy:

(SC, -->)

--> is a reflexive, antisymmetric, transitive relation over SC

Information is allowed to flow from object x to object y iff x --> y.

Lattice Flow Policy:

A flow policy is a lattice if there exists least upper bound and greatest lower bounds on SC

An Example Lattice

Certification of Information Flow


For:
       b := f(a1,...,an)

verify that:
       a1 + ... + an --> b


For:
       if e then S1 else S2

verify that:
       e --> S1 x S2

where:
       S1 = x { b | b is a target of an assignment in S1}
       S2 = x { b | b is a target of an assignment in S2}

Go Back to the Operating Systems page.