|
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
|