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
dc.date.accessioned2017-04-12T21:55:26Z
dc.date.available2017-04-12T21:55:26Z
dc.date.issued2016-12
dc.date.submittedDecember 2016
dc.date.updated2017-04-12T21:55:27Z
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.format.mimetypeapplication/pdf
dc.identifierdoi:10.15781/T2SX64G0Q
dc.identifier.urihttp://hdl.handle.net/2152/46437
dc.language.isoen
dc.subjectFormal verification
dc.subjectx86 Machine-code analysis
dc.subjectx86 ISA
dc.subjectACL2
dc.subjectTheorem proving
dc.subjectProgram verification
dc.titleFormal verification of application and system programs based on a validated x86 ISA model
dc.typeThesis
dc.type.materialtext
thesis.degree.departmentComputer Sciences
thesis.degree.disciplineComputer science
thesis.degree.grantorThe University of Texas at Austin
thesis.degree.levelDoctoral
thesis.degree.nameDoctor of Philosophy
Files
Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
GOEL-DISSERTATION-2016.pdf
Size:
803.05 KB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 2 of 2
No Thumbnail Available
Name:
PROQUEST_LICENSE.txt
Size:
4.45 KB
Format:
Plain Text
Description:
No Thumbnail Available
Name:
LICENSE.txt
Size:
1.84 KB
Format:
Plain Text
Description: