Formalization of x86 Machine-Code Programs with System Calls
Presented as part of the 2014 HCSS conference.
Abstract:
Most user-level programs use system calls to perform operations like I/O and memory management. Verification of these programs is required to assure their correct execution. We have extended our formal, executable model of the x86 instruction-set architecture (ISA), implemented in the ACL2 theorem-proving system, by adding support for system calls. We can now simulate and formally analyze user-level x86 machine-code programs that exhibit non-determinism caused by system calls and some x86 instructions, such as RDRAND, which is used in cryptographic applications.
Our model has two modes of operation: a logical mode that formalizes interaction with an external environment to support reasoning, and an execution mode that queries an underlying operating system to support simulation. We validate the execution mode with respect to both the logical mode and the real machine through extensive testing. This provides assurance that our model faithfully represents the semantics of an actual x86 machine. Using our model, we analyze x86 machine-code programs, which we usually obtain by running the GCC or Clang tool chain on C code. As a demonstration of the capabilities of our model, we mechanically verified a simple word-count (Linux-like “wc”) program that calculates the number of characters, lines, and words in an input stream.
Presenter Bio:
Dr. Warren A. Hunt, Jr. is a Professor at the University of Texas Computer Science Department, where he teaches formal methods and computer architecture, and where he investigates and develops methods for microprocessor specification and program verification, automated theorem-proving methods, and computational biology tools. Dr. Hunt is currently the PI for DARPA's CRASH effort at UT.
Dr. Hunt has been active in the hardware verification area for more than 25 years, and he has applied formal verification tools and methods to a litany of microprocessor designs: FM8501, FM8502, FM9001, Motorola CAP DSP, FM9801, VIA Nano, and Oracle SPARC. Dr. Hunt completed the first complete mechanical verification of a microprocessor design in 1985, and he, along with Bishop Brock, specified, designed, and mechanically verified, the 32-bit FM9001, the first and only such verified microprocessor ever to be built. Dr. Hunt is the steering committee chairman of the FMCAD Conference series, and he serves as an associate editor of the "Formal Methods in System Design" journal.
Prior to his 2002 arrival at UT, Dr. Hunt worked as a Research Staff Member and Manager at IBM's Austin Research Laboratory from 1997 to 2002, where he was involved with formal verification and high-performance computing as one of the founders and PIs of IBM's DARPA PERCS project. From 1986 until 1997, he served as Vice President of Hardware Engineering at Computational Logic, Inc. From 1982 until 1985, Hunt served as Hardware and Systems Manager for Cyb Systems. Dr. Hunt has a BSEE from Rice University and a computer science PhD from UT Austin.