Proof-Carrying Code (PCC) is a general framework for the mechanical verification of safety properties of machine-language programs. It allows a code producer to provide an executable program to a code consumer, along with a machine-checkable proof of safety such that the code consumer can check the proof before running the program. PCC has the advantage of a small Trusted Computing Base (TCB), since the proof checking can be a simple mechanical procedure. A weakness of previous PCC systems is that the proof-checking infrastructure is based on some complicated logic or type system that is not necessarily sound.
Foundational Proof-Carrying Code (FPCC) aims to further reduce the TCB size by an order of magnitude by building the safety proof based on the simple and trustworthy foundations of mathematical logic. There are three major components in an FPCC system: a compiler, a proof checker, and the safety proof of an input machine-language program. The compiler should produce machine code accompanied by a proof of safety. The proof checker verifies, sometimes also reconstructs, the safety proof before the program gets executed.
We have built a prototype system. Our prototype is the first end-to-end FPCC system, including a type-preserving compiler from core ML to SPARC (based on SML/NJ), a low-level typed assembly language LTAL, a foundational proof-checker Flit, and a nearly complete machine-checkable soundness proof. The system compiles Core ML programs to SPARC code, accompanied with programs in a low-level typed assembly language; these typed assembly programs serve as the proof witnesses of safety of the corresponding SPARC machine code. Our Flit proof checker includes a simple logic programming engine enabling efficient proof-checking.
In this thesis, I'll explain the design of interfaces between these components and show how to build an end-to-end FPCC system. We have come to the following conclusion: a type system (a low-level typed assembly language) should be designed to check machine code; and the proof-checking should be factored into two stages, namely typechecking of the input machine code and verification of soundness of the type system. Since a type checker can be efficiently interpreted as a logic program, Flit's logic programming engine enables efficient proof-checking.
Cited By
- Ahmed A, Appel A, Richards C, Swadi K, Tan G and Wang D (2010). Semantic foundations for typed assembly languages, ACM Transactions on Programming Languages and Systems (TOPLAS), 32:3, (1-67), Online publication date: 1-Mar-2010.
- Appel A, Melliès P, Richards C and Vouillon J (2007). A very modal model of a modern, major, general type system, ACM SIGPLAN Notices, 42:1, (109-122), Online publication date: 17-Jan-2007.
- Appel A, Melliès P, Richards C and Vouillon J A very modal model of a modern, major, general type system Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, (109-122)
Index Terms
- Interfacing compilers, proof checkers, and proofs for foundational proof-carrying code
Recommendations
A Syntactic Approach to Foundational Proof-Carrying Code
Proof-carrying code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules; they certify safety but only if there is no bug in ...
Foundational proof certificates: making proof universal and permanent
LFMTP '13: Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practiceConsider a world where exporting proof evidence into a declarative, universal, and permanent format is taken as ``feature zero'' for computational logic systems. In such a world, provers will be able to communicate and share theorems and proofs; ...
A Syntactic Approach to Foundational Proof-Carrying Code
LICS '02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer ScienceProof-Carrying Code (PCC) is a general framework for verifying the safety properties of machine-language programs. PCC proofs are usually written in a logic extended with language-specific typing rules. In Foundational Proof-Carrying Code (FPCC), on the ...