Proof-Carrying Code (PCC) is a static mechanism that mechanically verifies 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 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. This demonstrates L_c's applicability of verifying properties of machine-language programs.