Research Preparation Exam: Shilpi Goel

Date: April 2, 2013
Time: 4:30pm
Place: GDC 7.808
RPE Committee: Warren A. Hunt, Jr. (chair), J Moore, Calvin Lin

Title: A Formal Model of the X86 ISA for Binary Program Verification

----------------------------------------------------------------------

Abstract:

Verification of programs based purely on analysis of higher-level code
does not account for bugs introduced by compilers, thereby decreasing
confidence that the programs will behave as expected during
run-time. Moreover, higher-level code may not always be available for
such an analysis. Formal verification of binary programs is often the
only means available to ensure correctness of higher-level
programs. To this end, many verification projects entail the
development of a formal model of a processor's instruction set
architecture (ISA); such a model formalizes the semantics of binary
programs, which enables reasoning about them as well. However, such
undertakings often involve simplified formal processor models,
significant user expertise, as well as time-consuming manual effort.

In this talk, we briefly describe a formal, executable model of a
significant subset of the X86 ISA in the ACL2 programming language.
Our ISA model can run X86 binary programs and we can reason about them
using the ACL2 theorem proving system. Our effort has two main driving
forces: one, to develop an accurate, non-idealized X86 ISA model and
two, to develop infrastructure that will reduce the time and manual
effort required to reason about binary programs on this model. Towards
our latter goal, we present our approach of using symbolic execution
to verify some non-trivial user-level binary programs fully
automatically in ACL2.