Verifying an x86 Supervisor-Mode Program that Interacts with the Paging Data Structures

Abstract:

We have verified a supervisor-mode, x86 binary-level zero-copy program. Instead of copying data byte-by-byte (or word-by-word, etc.), this zero-copy program alters the contents of privileged system data structures -- specifically, the memory-resident page tables. The binary code subjected to formal verification was created from a C program compiled by the Clang-LLVM tool suite. For this verification task, we used our formal, executable model of the x86 instruction-set architecture written in the ACL2 theorem-proving system. Programs that manage and update page tables are critical because these data structures are instrumental in x86 memory management, including providing the virtual memory abstraction.

Unsurprisingly, the x86 paging mechanism is complicated, and a number of updates, such as those to accessed and dirty flags, may be made to the page tables even during the execution of a single instruction. A key to reasoning about programs that interact with page tables is to precisely account for the effect of all such updates. Our verification framework makes this task tractable by providing lemma libraries that can automate large portions of the proof, thereby reducing the user overhead.

Our verification effort demonstrates the high fidelity of our x86 model, where all of the various memory accesses, including the accesses required for the page-walk mechanisms (i.e., traversal of the page tables done by the processor), have been modeled. In addition to presenting our proof of correctness of the zero-copy program, we present an overview of our x86 machine-code verification framework, and describe how it can be used to reason about both application and supervisor-mode programs effectively. Our effort demonstrates that it is possible to verify x86 supervisor-mode binary programs that directly involve the x86 memory-management system, and that it is possible to capture the semantics of commercial systems.

--

Warren A. Hunt, Jr. is Professor in the Department of Computer Sciences of the University of Texas at Austin. Dr. Hunt holds a BSEE from Rice University and a PhD in computer science from the University of Texas. His research interests include hardware verification, circuit design, SAT solving, and mechanized theorem proving. Hunt's dissertation, published in 1985, was the seminal example of a mechanized microprocessor correctness proof. He extended this verification work, to produce in 1991, the first and only fully verified microprocessor to be physically realized in hardware, the FM9001. Hunt's continuing refinement of verification technology and methodology continued with his participation on the FM9801 microprocessor verification effort, as well as industrial scale systems such as Motorola's Complex Arithmetic Processor DSP and his work on the VIA Nano family of X86 compatible processors. From 1997 to 2002, Hunt worked for IBM Research, where he initiated the PERCS project; this project culminated in a computer family of large-memory computer systems that are still being used. From 1986 to 1997, Hunt was Vice President of Computational Logic, Inc., in Austin, Texas, where his research was the cornerstone of the "Short Stack," a fully verified tower of systems from the high-level language level down to hardware. This work stands as the most extensive and complete example of a formally correct computing platform. His current research involves the use of formal mathematics to write specifications for computer hardware and software and to use proof techniques to determine the validity of such specifications. He is also interested in computer architecture, low-power computing, garbage collection, SAT solving, and parallel computing. Dr. Hunt is the Chair of the FMCAD Steering Committee, and he is an ACM Distinguished Engineer.