Our results establish that our system ensures that well-typed programs do not leak confidential information under the security policy prescribed by the assumed security lattice.
data does not flow from a security compartment to another if they are unrelated or if it is a down-flow in the security lattice.