Sponsors: NSF, IBM
Proof-carrying code enables a host to verify that its security policies are satisfied by code from untrusted sources. This provides an approach to safe mobile code, safe active networks, etc. The idea is to let software be accompanied by a proof that the software satisfies the security policies. Since proofs are easier to check than to produce, this puts the burden of proof on the code producer instead of the code consumer. Experiments have shown that proofs can be produced by a certifying compiler. Our project is aimed at building a certifying compiler for a subset of Java.