Post date: Mar 25, 2009 3:19:42 PM
Proof-carrying code is a mechanism by which an operating system kernel can determine with certainty that it is safe to execute a binary supplied by an untrusted source. The kernel first defines a safety policy and makes it public. Then, using this policy, an application can provide binaries in a special form called proof-carrying code, or simply PCC. Each PCC binary contains, in addition to the native code, a formal proof that the code obeys the safety policy. The kernel can easily validate the proof and if it succeeds, the code is guaranteed to respect the safety policy without relying on run-time checks. The main practical difficulty lies in the automatic generation of safety proofs, which can be done off-line.
I will show the architecture of PCC, give an example of how it works, and discuss a case study of safe, hand-written network packet filters operating in kernel space.
This talk is based on a paper by George Necula and Peter Lee of the same title.
Date: Mar 25, 2009
Presented by: Matthew Danish