Computer Science Colloquium
Warren A. Hunt Jr
University of Texas
Specification and Verification of x86 Machine-Level Code
Mon 28.05.2018, 17:15, 60 minutesRoom JKU MT 127 in Science Park 1
Abstract
We are using theorem-proving techniques to model and analyze x86 software for the purpose of increasing the accuracy and reliability of x86-based products. We have developed an ISA-level x86 emulator in the ACL2 logic; this emulator serves as a precise specification for x86 software. Using the ACL2 theorem-proving system, we describe how our x86 ISA model is used to prove the correctness of x86 binary-level programs. We verify X86 binary programs by placing their binary representation into our ACL2-based, x86 emulator, and analyzing the effect of such programs on the x86 state. Our x86 ISA-level specification includes the x86 segment and paging data structures; this, in turn, allows for the emulation and analysis of programs that modify the data held within the page tables. We use our model to verify a "zero-copy" program; this program copies pages of information by changing x86 page-table entries.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 theoremproving 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 PhD in computer science from UT Austin.
Invited by Univ.-Prof. Dr. Armin Biere, Institute for Formal Models and Verification
The Computer Science Colloquium is organized by the Department of Coputer Science at JKU, the Österreichische Gesellschaft für Informatik (ÖGI) and the Österreichische Computergesellschaft (OCG).