On the Practicality of Input Crafting with Symbolic Execution on Binary Code


Betreuer: Behrad Garmany

Beginn: as soon as possible

Dauer: 6 months

Weitere Details:


Symbolic Execution is a process of executing a program by means of symbolic expressions for variables and data. The basic idea is to treat input data of interest as symbols rather than concrete values. These symbols can represent any possible value and as the execution approaches, the symbolic variables become constrained. At branches, for instance, a set of constraints provides conditions to be fulfilled for a specific branch target.

Input crafting poses the challenge to produce inputs that leads the execution flow into spots of interest. It seems reasonable that symbolic execution can aid us to guide the execution into the area of interesting spots. For the security field, it provides a valuable tool in evaluating those spots for vulnerability assessment, especially on large code bases when source code is not available. Patched based approaches can also benefit from input crafting. In a patched based approach, execution is lead into patched areas of code that are not tested well.

The aim of this thesis is to examine the practicality of symbolic execution concerning the problem of generating inputs that lead us into specified areas of the binary code.

Tasks to be solved include: * Familiarize with a symbolic execution engine of choice (Angr, S2E, Triton or amoco). * Analysis of different search strategies and heuristics. * Evaluation on real world binaries.


The student is expected to have an interest in the field of reverse engineering and program analysis. Experience in common tools like IDA, gdb, radare etc. is beneficial. The student should also be comfortable in programming in C/Python/x86 assembly.

The choice of operating system is up to the student.