Dynamic Optimizations for Symbolic Execution

Description

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