Computer Science Department
School of Computer Science, Carnegie Mellon University
Enforcing Formal Security Properties
Andrew Bernard, Peter Lee
Keywords: Security-policy specification, security-policy enforcement,
first-order logic, temporal logic, verification-condition generation,
We define the formal semantics of expressive security-property language.
The language distinguishes safe from unsafe programs and can be enforced
systematically using proof-carrying code. The soundness of an
enforcement algorithm is shown with respect to the language semantics.