CMU-CS-01-121
Computer Science Department
School of Computer Science, Carnegie Mellon University


CMU-CS-01-121

Enforcing Formal Security Properties

Andrew Bernard, Peter Lee

April 2001

CMU-CS-01-121.ps
CMU-CS-01-121.pdf


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 reports@cs.cmu.edu