Browse Theses

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 challenge in the verification is that machine code, unlike high-level languages, contains unstructured control flow (due to arbitrary jumps). A piece of machine code can contain multiple entry points that jump instructions might jump to, and multiple exit points. Traditional Hoare logic and its variants 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.

The major contribution of this dissertation is a program logic, L _c , which modularly verifies properties of machine-code fragments. Unlike previous program logics, the basic reasoning units in L _c are multiple-entry and multiple-exit code fragments. L _c provides composition rules to combine code fragments and to eliminate intermediate entries/exits in the combined fragment. L _c is not only useful for reasoning about properties of machine code with unstructured control flow, but also useful for deriving rules for common control-flow structures such as while-loops, repeat-until-loops, among others. We also present a semantics for L _c and prove that L _c is both sound and complete.

As an application to the FPCC project, I have implemented L _c on top of the SPARC machine language and used L _c 's rules to verify the soundness of the instruction rules of a full-fledged low-level typed assembly language—LTAL. This demonstrates L _c 's applicability of verifying properties of machine-language programs.