Methods for binary symbolic execution
Abstract/Contents
- Abstract
- Binary symbolic execution systems are built from complicated stacks of unreliable software components, process large program sets, and have few shallow decisions. Failure to accurately symbolically model execution produces infeasible paths which are difficult to debug and ultimately inhibits the development of new system features. This dissertation describes the design and implementation of klee-mc, a novel binary symbolic executor that emphasizes self-checking and bit-equivalence properties. This thesis first presents cross-checking for detecting causes of infeasible paths. Cross-checking compares outputs from similar components for equivalence and reports mismatches at the point of divergence. This approach systematically finds errors throughout the executor stack from binary translation to expression optimization. The second part of this thesis considers the symbolic execution of floating-point code. To support floating-point program instructions, klee-mc emulates floating- point operations with integer-only off-the-shelf soft floating-point libraries. Symbolically executing these libraries generates test cases where soft floating-point implementations and floating-point constraint solvers diverge from hardware results. The third part of this thesis discusses a term rewriting system based on program path derived expression reduction rules. These reduction rules improve symbolic execution performance and are machine verifiable. Additionally, these rules generalize through further processing to optimize larger classes of expressions. Finally, this thesis describes a flexible mechanism for symbolically dispatching memory accesses. klee-mc forwards target program memory accesses to symbolically executed libraries which retrieve and store memory data. These libraries simplify access policy implementation and ease the management of rich analysis metadata.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2014 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Romano, Tony, 1957- |
|---|---|
| Associated with | Stanford University, Department of Computer Science. |
| Primary advisor | Engler, Dawson R |
| Thesis advisor | Engler, Dawson R |
| Thesis advisor | Aiken, Alexander |
| Thesis advisor | Mazières, David (David Folkman), 1972- |
| Advisor | Aiken, Alexander |
| Advisor | Mazières, David (David Folkman), 1972- |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | Anthony Romano. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph.D.)--Stanford University, 2014. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2014 by Anthony Joseph Romano
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...