Models for Security Policies in Proof-Carrying Code
|Authors:||Appel, Andrew W., Felten, Edward W.|
|Download Formats:||[Postscript] [PDF]|
When an untrusted machine-language program runs on a host with resources that must be protected, the security policy specifies how the program may interact with the host. Proof-carrying code is a framework for automatically verifying that a program complies with a security policy. We show how to specify a wide variety of security policies, how to ensure that these specifications are consistent, how to develop compilers that produce compliant machine code and proofs of compliance, and how to reason about whether the host environment correctly implements its side of the policy.