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
- 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. [paper]
- Tan, G. and Appel, A. (2006). A compositional logic for control flow. In International
Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), pages 80–94.
[paper]. [slides]
- Tan, G., Appel, A., Swadi, K., and Wu, D. (2004). Construction of a semantic model for
a typed assembly language. In International Conference on Verification, Model Checking, and
Abstract Interpretation (VMCAI), pages 30–43. [paper]. [slides]
Ph.D. Thesis
Last updated: Sep. 2007