Under-constrained symbolic execution : correctness checking for real code
Abstract/Contents
- Abstract
- Software defects pose a frequent challenge to developers, and their consequences are far-reaching. Despite advances in software engineering practices, programming language design, and debugging tools, bugs remain ubiquitous. Traditional testing techniques, while useful, have failed to prevent a significant number of bugs from affecting end users. One promising technique for automatically detecting bugs is dynamic symbolic execution, which aims to test all possible execution paths through a program and identify inputs that cause the program to crash. Unfortunately, symbolic execution suffers from the well-known path explosion problem because the number of distinct execution paths through a program is, in the best case, exponential in the number of branch statements. Consequently, symbolic execution tools are typically ineffective for programs consisting of more than a few thousand lines of code, let alone large codebases with line counts in the millions. This dissertation presents a new, scalable approach to symbolic execution, under-constrained symbolic execution, that targets individual functions rather than whole programs. This technique supports direct symbolic execution of arbitrary C functions and automatically synthesizes their inputs, even for complex, pointer-rich data structures. We demonstrate this technique's feasibility by thoroughly evaluating three use cases, although many others are possible. First, we use it to check the equivalence of library routines from different implementations that share a common interface (e.g., the C standard library). Second, we check whether code patches introduce new bugs by comparing two versions of the same function: before and after a patch is applied. Third, we use under-constrained symbolic execution to test a single version of a function, using a combination of heuristics to separate important errors from those likely to be false positives. In this dissertation, we describe UC-KLEE, a tool we built that implements under-constrained symbolic execution and supports the above use cases. We evaluate our tool on large, mature codebases including BIND, OpenSSL, and the Linux kernel and describe previously-unknown bugs we discovered in each of these codebases.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2015 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| Associated with | Ramos, David A |
|---|---|
| Associated with | Stanford University, Department of Computer Science. |
| Primary advisor | Engler, Dawson R |
| Thesis advisor | Engler, Dawson R |
| Thesis advisor | Aiken, Alexander |
| Thesis advisor | Dill, David L |
| Advisor | Aiken, Alexander |
| Advisor | Dill, David L |
Subjects
| Genre | Theses |
|---|
Bibliographic information
| Statement of responsibility | David A. Ramos. |
|---|---|
| Note | Submitted to the Department of Computer Science. |
| Thesis | Thesis (Ph.D.)--Stanford University, 2015. |
| Location | electronic resource |
Access conditions
- Copyright
- © 2015 by David Antonio Ramos
- 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...