Invited talk: what's the future for proof-carrying code?

ABSTRACT

Proof-carrying code (PCC) was introduced by George Necula and Peter Lee in 1996. The principle is simple: we can eliminate the need to trust code by forcing the producer to give us a formal, machine-checkable proof that the code won't exhibit some "bad behavior" when executed. Thus, instead of having to perform a complicated (and thus un-trustworthy) analysis to determine whether or not code is bad, we can instead use a simple (and thus trustworthy) proof checker.The attraction to systems people was that the PCC framework placed no inherent limits on good code. As long as you could manufacture a proof that the code wasn't bad, then the code would be accepted. So, at least in principle, you wouldn't have to pay a performance penalty for safety. Over the past eight years, many researchers have worked to make PCC a reality. But I would argue that we are still very far from reaping the benefits that the framework promises. Good progress has been made in some areas, but there are a number of hard problems that remain. The hardest conceptual questions are (a) "What policies should we enforce?" and (b) "How does the code producer generate a proof?