Interfacing Compilers, Proof Checkers, and Proofs for Foundational Proof-Carrying Code
Computer Science Departmental Seminar series features Dinghao Wu of Princeton University.
Faculty Host: Lori Clarke
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. A weakness of previous PCC systems is that the proof-checking infrastructure is based on some complicated logic that is not necessarily sound.
Foundational Proof-Carrying Code (FPCC) aims to build 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 discovers, the safety proof before the program gets executed. We have built an end-to-end FPCC system. Our prototype 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 talk, I'll present the design of interfaces between these components and show how to build an end-to-end FPCC system. We have come to the conclusion that: (1) a type system (a low-level typed assembly language) should be designed to check machine code; (2) 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.
I'll also briefly present my research on software model checking and program verification.
Refreshments at 3:30 p.m. in the atrium outside the presentation room.
Please visit our departmental calendar at for information on upcoming events.
