- Ph.D. Candidate
- Department of Computer Science
- The University of Texas at Austin
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.