Foundational Proof-Carrying Code

Proof-Carrying Code (PCC) is a static mechanism that mechanically verifies type safety of machine-language programs. But the problem in conventional PCC is, who will verify the verifier (the type checker) itself? The Foundational Proof-Carrying Code (FPCC) project at Princeton verifies the soundness of the type checker from the smallest possible set of axioms --- logic plus machine semantics. One of the challenges in the verification is that machine code, unlike high-level languages, contains unstructured control flows (due to arbitrary jumps). A piece of machine code contains multiple entry points that jump instructions might jump to, and multiple exit points. Traditional Hoare logics either verify the partial correctness of programs with only one entry and one exit, or need the whole program to verify jump instructions, which is not modular.

In my Ph.D. thesis work, I designed a logic that modularly verifies properties of program fragments. The logic works directly on program fragments with multiple entries and multiple exits. It provides inference rules to combine fragments together and eliminate intermediate entries and exits. I showed this logic to be both sound and (relatively) complete with respect to a small-step machine semantics. In the FPCC project, I used this logic to construct a soundness proof for a full-fledged Typed Assembly Language (TAL). All proofs were formally developed in a theorem prover and rigorously checked.


Ph.D. Thesis

Last updated: Sep. 2007