Models for Security Policies in Proof-Carrying Code

Abstract:

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.