Gang Tan, Department of Computer Science & Engineering- Lehigh University

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.

Publications

A Compositional Logic for Control Flow. Gang Tan and Andrew W. Appel. In Seventh International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 06), LNCS 3855, pages 80-94, Springer, January 2006.
Construction of a Semantic Model for a Typed Assembly Language. Gang Tan, Andrew W. Appel, Kedar Swadi and Dinghao Wu. In Fifth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI 04), LNCS 2937, pages 30-43, Springer, January 2004.

Ph.D. Thesis

A Compositional Logic for Control Flow and its Application in Foundational Proof-Carrying Code, Princeton University, July 2005. Advised by Prof. Andrew W. Appel

Last updated: Sep. 2007