Formal verification of application and system programs based on a validated x86 ISA model

dc.contributor.advisorHunt, Warren A., 1958-
dc.contributor.committeeMemberAlvisi, Lorenzo
dc.contributor.committeeMemberKaufmann, Matt
dc.contributor.committeeMemberLin, Calvin
dc.contributor.committeeMemberMoore, J S
dc.contributor.committeeMemberWatson, Robert
dc.creatorGoel, Shilpi
dc.creator.orcid0000-0001-8037-0201 2016
dc.description.abstractTwo main kinds of tools available for formal software verification are point tools and general-purpose tools. Point tools are targeted towards 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, largely because they are easy to use. However, point tools are limited in their scope because they are pre-programmed to reason about a fixed set of behaviors. In contrast, general-purpose tools,like theorem provers, have a wider scope. Unfortunately, they also have a higher user overhead. These tools often use incomplete and/or unrealistic software models, in part to reduce this overhead. Formal verification based on such a model can be restrictive because it does not account for program behaviors that rely on missing features in the model. The results of such formal verification undertakings may be unreliable --- consequently, they can offer a false sense of security. This dissertation demonstrates that formal verification of complex program properties can be made practical, without any loss of accuracy or expressiveness, by employing a machine-code analysis framework implemented using a mechanical theorem prover. To this end, we 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 routinely by performing co-simulations against a physical x86 processor --- thus, formal analysis based on this model is reliable. We also developed a general framework for x86 machine-code analysis that can lower the overhead associated with the verification of a broad range 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.
dc.description.departmentComputer Sciences
dc.subjectFormal verification
dc.subjectx86 Machine-code analysis
dc.subjectx86 ISA
dc.subjectTheorem proving
dc.subjectProgram verification
dc.titleFormal verification of application and system programs based on a validated x86 ISA model
dc.type.materialtext Sciences science University of Texas at Austin of Philosophy
Original bundle
Now showing 1 - 1 of 1
Thumbnail Image
803.05 KB
Adobe Portable Document Format
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
4.45 KB
Plain Text
No Thumbnail Available
1.84 KB
Plain Text