Practice talk: Ph.D. Final Oral Defense
----------------------------------------------------------------------
Note: Details of the *final* talk are as follows:
Time: 10 AM
Date: Thursday, 3rd November, 2016
Location: GDC 7.808
Committee: Warren A. Hunt, Jr. (supervisor), Lorenzo Alvisi, Matt
Kaufmann, Calvin Lin, J Strother Moore, and Robert Watson
----------------------------------------------------------------------

Title: Formal Verification of Application and System Programs Based on
a Validated x86 ISA Model

Shilpi Goel

Talk Abstract:
Our research demonstrates that formal verification of complex program
properties can be made practical, without any loss of accuracy and
expressiveness, by employing a machine-code analysis framework
implemented using a mechanical theorem prover.  Much of the previous
work related to formal software verification has resulted in tools
that facilitate bug-hunting or proving a fixed set of properties, such
as establishing the absence of buffer overflows.  These tools have
become a practical choice in the development and analysis of serious
software systems.  However, although these tools are easy to use, they
are limited in their scope.  On the other hand, general-purpose tools
have a higher user overhead, and they often use incomplete and/or
unrealistic models, in part to reduce this overhead.  Formal
verification based on such models can be restrictive and worse, can
offer a false sense of security.

For our research, we have constructed a formal and executable model of
the x86 Instruction-Set Architecture using the ACL2 theorem-proving
system.  This model includes a specification of 400+ x86 opcodes and
architectural features like segmentation and paging.  The model's high
execution speed allows it to be validated regularly by performing
co-simulations against a physical x86 processor --- thus, formal
analysis based on this model is reliable.  We have also developed a
general framework for x86 machine-code analysis that can be used for
the verification of a broad spectrum of program properties, including
correctness with respect to behavior, security, and resource
requirements.  We illustrate the capabilities of our framework by
describing the verification of two application programs, "population
count" and "word count", and one system program, "zero copy".

In addition to its direct contributions in the areas of formal
specification and software verification, this work paves the way for
research opportunities that would otherwise have been difficult to
pursue.  For example, it can be used to reason about hardware,
including verification of microarchitecture designs and proving
properties of the memory hierarchy.  Our machine-code analysis
framework, along with its documentation, is available online as a part
of the ACL2 Community books.