Methods for binary symbolic execution [electronic resource]
At the library
Special Collections
Limited on-site access
Researchers in the Stanford community can request to view these materials in the Special Collections Reading Room. Entry to the Reading Room is by appointment only.
| Call number | Status |
|---|---|
| 3781 2014 R |
More options
Description
Creators/Contributors
- Author/Creator
- Romano, Tony, 1957-
- Contributor
- Engler, Dawson R. primary advisor.
- Aiken, Alexander advisor.
- Mazières, David (David Folkman), 1972- advisor.
- Stanford University. Computer Science Department.
Contents/Summary
- Summary
- 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.
Bibliographic information
- Publication date
- 2014
- Note
- Submitted to the Department of Computer Science.
- Note
- Thesis (Ph.D.)--Stanford University, 2014.
Browse related items
Start at call number:
