Symbolic execution in program analysis

OData support
Izsó Tamás
Department of Networked Systems and Services

Program analysis techniques have been widely used in the different phases of software engineering for decades. Prevalent examples include optimizing compilers and software validation tools. Symbolic execution was first proposed in 1976 but it was only with the recent advances in SMT solvers and computing power and the advent of binary analysis frameworks that its use became feasible for more than trivial programs.

Symbolic execution has also seen a surge of interest for aiding the understanding of compiled code and security testing. Several systems were proposed for such uses, one of the most well-known being Microsoft's SAGE white-box fuzzer, which has found a significant chunk of all Windows 7 security bugs.

In this thesis, I attempt to evaluate the usability of symbolic execution in a software security testing and reverse engineering context by modifying the white-box fuzzing framework egas, which is a clone of SAGE, to allow the targeting of network-facing programs. I will also show that the artifacts of white-box fuzzing, like code coverage information, can be used to help the understanding of binaries by integrating such information into a disassembler.


Please sign in to download the files of this thesis.