Open Problems With Certifying Compilation presented at 14th USENIX Security Symposium 2005

by Greg Morrisett,

Tags: Security Monitoring

Summary : Proof-carrying code was introduced by Necula and Lee as a technique for minimizing trusted code: instead of monitoring or analyzing code to see if it is trustworthy, we require that the code comes with a machine-checkable, mathematical proof that the code respects a desired security policy. In practice, checking the proof is easy when compared to constructing one, so the framework shifts the hard work from the code consumer to the code producer. Unfortunately, it doesn't eliminate the hard problem: how does a code producer construct the proof?
Certifying compilers provide part of the answer: A certifying compiler takes as input high-level source code and a proof that the source code respects the policy, and then transforms the code and proof in parallel. In this fashion, it is able to automatically output the required proof at the machine-code level. For simple policies, such as memory-safety and type-safety, the proof can be automatically constructed at the source level, assuming we start with a type-safe source language.
Unfortunately,most of the code that needs to be trustworthy is written in type-unsafe languages such as C or C++, so we need some way to realize proofs for these languages. Furthermore, we need support for security policies that go well beyond type-safety. I will survey some of the research that has been done, and that needs to be done to achieve these goals, so that we may one day realize the full potential of proof-carrying code.