Modular Machine Code Verification
YALE UNIV NEW HAVEN CT DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
Formally establishing safety properties of software presents a grand challenge to the computer science community. Producing proof-carrying code, i.e., machine code with machine-checkable specifications and proofs, is particularly difficult for system softwares written in low-level languages. One central problem is the lack of verification theories that can handle the expressive power of low-level code in a modular fashion. In particular, traditional type- and logic-based verification approaches have restrictions on either expressive power or modularity. This dissertation presents XCAP, a logic-based proof-carrying code framework for modular machine code verification. In XCAP, program specifications are written as general logic predicates, in which syntactic constructs are used to modularly specify some crucial higher-order programming concepts for system code, including embedded code pointers, impredicative polymorphisms, recursive invariants, and general references, all in a logical setting. Thus, XCAP achieves the expressive power of logic-based approaches and the modularity of type-based approaches. Its meta theory has been completely mechanized and proved. XCAP can be used to directly certify system kernel code. This dissertation contains a mini certified thread library written in x86 assembly. Every single instruction in the library, including those for context switching and thread scheduling, has a formal XCAP specification and a proof. XCAP is also connected to existing certifying compiler a typepreserving translation from a typed assembly language to XCAP is included.
- Computer Programming and Software
- Structural Engineering and Building Technology