Dynamic Optimizations for Symbolic Execution

Description

Symbolic execution is becoming widespread in security development lifecycles however it
remains an expensive technique for test generation. Research has shown that performance is
still an issue and requires further improvement. This thesis proposes a framework for
implementing dynamic optimizations in symbolic engines via dynamic binary instrumentation.
For its technologies, this framework combines the binary instrumentation framework
DynamoRIO and the symbolic engine of Triton. We propose several improvements for the
framework, targeting binary symbolic execution. Improvements from compiler optimizations,
such as strength reduction towards expression optimization techniques, are introduced. These
optimizations are inspired by other state-of-the-art solutions available.  We hope this thesis
motivates future research on the optimization of symbolic execution to help enhance its 
accuracy, efficiency, and reliability. 

Motivation

Recent works [1-3] have shown that the symbolic emulation of code plays an important role in the efficiency of symbolic execution. Also, it has been shown that program transformations can significantly affect the performance of symbolic execution engines [4]. However, currently each instruction is currently emulated by itself and no optimizations are performed. Therefore, there exists a potential in applying optimizations to reduce the amount of instrumentation and the overhead induced by symbolic emulation. For example, incrementing a memory location usually consists of a load, inc and store instruction which all
need to be emulated and instrumented. A simple optimization could summarize this and reduce overall necessary amount of emulation. Further potential for optimization lies in dynamic nature of (dynamic) symbolic execution: Similarly to optimizations
in Just-In-Time (JIT) Compilers, optimizations could dynamically be adjusted based on dynamic context information (e.g. what variables in the context are symbolized).

Topic

The goal of this research is to implement a framework to allow dynamic optimizations of symbolic execution. It should extend on State-of-the-Art approaches that use Dynamic Binary Instrumentation (DBI) [1,4]. Then, several optimizations should be designed and implemented. Finally, the performance of the resulting framework is evaluated. The steps can roughly be summarized as follows:

1. Study existing approaches and tools to identify what can be re-used/extended upon
2. Identify optimizations to implement
3. Implement a framework allowing for dynamic optimization of symbolic execution instrumentation (using existing tools)
4. Evaluate optimizations concerning performance

Requirements

• Programming Skills in C/C++ (for efficiency and to interact with DBI frameworks)
• Interest in symbolic execution
• Ability to work self-directed and systematically
• (Optional) Some background regarding program optimizations

Contact

kilger@sec.in.tum.de

References

[1] http://www.s3.eurecom.fr/tools/symbolic_execution/symqemu.html
[2] http://s3.eurecom.fr/tools/symbolic_execution/symcc.html
[3] https://www.usenix.org/system/files/conference/usenixsecurity18/sec18-yun.pdf , https://github.com/sslab-gatech/qsym
[4] https://ieeexplore.ieee.org/abstract/document/7381814