Shilpi Goel

Shilpi Goel

  • Ph.D. Candidate
  • Department of Computer Science
  • The University of Texas at Austin

Ph.D. Dissertation Topic

Analysis of x86 Application and System Programs via Machine-Code Verification

Overview

Ensuring the reliability of high-level programs is becoming more difficult with the ever-increasing complexity of computing systems. Although automatic program analysis tools have found great success, they have limited scope because they target specific kinds of undesirable behavior, such as buffer overflows. Incorrect compiler transformations and the absence of analysis systems for some high-level languages suggest that a lowest-common-denominator strategy, namely machine-code analysis, will facilitate extensive program verification.

For this dissertation project, we are developing a general framework for the mechanical verification of software by analyzing its corresponding machine code. To this end, we are specifying a formal and executable model of the x86 instruction set architecture (ISA) using the ACL2 theorem-proving system. Notably, this model can be used for the functional verification of user-mode as well as supervisor-mode programs. This project will provide the capability to mechanically verify a wide variety of properties of x86 programs, including their correctness with respect to behavior, security, and resource requirements.

Current Status

  • The x86 model supports 400+ instructions, including some floating-point and supervisor-mode instructions. It can execute almost all user-level programs emitted by GCC/LLVM. We have successfully co-simulated a contemporary SAT solver on our model.

  • The model includes the specification of segment-based addressing and IA-32e paging for all page configurations (4K, 2M, 1G).

  • Simulation speed (measured on an Intel Xeon E31280 CPU @ 3.50GHz):
    ~3.3 million instructions/second (paging disabled)
    ~330,000 instructions/second (with 1G pages)

  • We have formally verified properties of application programs like popcount and wordcount, and supervisor programs like zero-copy.

  • Lines of Code: ~85,000 (not including blank lines)


Contributions

  • Our framework serves as a simulator for safely executing x86 programs and as a formal analysis tool for program verification. It is also an accurate reference for the x86 ISA.

  • Proofs of critical properties of x86 system structures (e.g., paging data structures) will give insight into supervisor-mode code verification.

  • This work can serve as the foundation for future research by facilitating information-flow analysis, resource usage guarantees, ensuring process isolation, etc.

Source Code and Documentation

The x86isa library is freely available (BSD 3-Clause license) from the ACL2+Community Books Github page.

For more details about this project, see the user and developer manual.