Computer Science Department
School of Computer Science, Carnegie Mellon University


Enforcing Formal Security Properties

Andrew Bernard, Peter Lee

April 2001

Keywords: Security-policy specification, security-policy enforcement, first-order logic, temporal logic, verification-condition generation, proof-carrying code

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.

96 pages

Return to: SCS Technical Report Collection
School of Computer Science homepage

This page maintained by