Proof-carrying code

TLDR

This paper introduces proof‑carrying code (PCC) and demonstrates its application to creating safe assembly‑language extensions of ML programs and high‑performance network packet filters. PCC works by having the code producer attach a safety proof to the code, which the host can quickly validate without cryptography or external agents, as shown in several case studies. The authors prove the adequacy of the safety policy representations and show that PCC‑based packet filters outperform comparable filters while being formally guaranteed safe.

Abstract

This paper describes proof-carrying code (PCC), a mechanism by which a host system can determine with certainty that it is safe to execute a program supplied (possibly in binary form) by an untrusted source. For this to be possible, the untrusted code producer must supply with the code a safety proof that attests to the code's adherence to a previously defined safety policy. The host can then easily and quickly validate the proof without using cryptography and without consulting any external agents.In order to gain preliminary experience with PCC, we have performed several case studies. We show in this paper how proof-carrying code might be used to develop safe assembly-language extensions of ML programs. In the context of this case study, we present and prove the adequacy of concrete representations for the safety policy, the safety proofs, and the proof validation. Finally, we briefly discuss how we use proof-carrying code to develop network packet filters that are faster than similar filters developed using other techniques and are formally guaranteed to be safe with respect to a given operating system safety policy.