(object x is in security class x)
--> is a reflexive, antisymmetric, transitive relation over SC
Information is allowed to flow from object x to object y iff x --> y.

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.