Optimizing Static Instrumentation for Symbolic Execution

Description

A crucial problem in software development and security is finding bugs in code. The fields of automated analysis

and software testing aid in detecting these defects. One essential technique, symbolic execution, replaces regular

inputs with symbolic values and constructs constraints for the paths in a program, allowing automated path exploration.

Recent research in symbolic execution methods uses static instrumentation and concreteness checks to increase performance

significantly. However, a big difference in performance remains between concrete and symbolic execution.

We propose, implement and evaluate an optimization to concreteness checks in static instrumentation, combining the concept

of static analysis and statically instrumented symbolic execution. Instead of performing one concreteness check per instruction,

we use static analysis to analyze instructions value dependencies in an execution block, reducing the concreteness checks by

combining them in a prologue. Extending the symbolic compiler SymCC, we design and create a prototype implementation that

collects concreteness checks for each basic block.

We measure the correctness and performance of our prototype implementation, comparing it to SymCC. While the correctness

evaluation lets us conclude that our implementation is correct for the programming language C, the real-world performance test

of openJPEG and libarchive show a slowdown in the fully concrete execution.

Furthermore, we analyze potential difficulties in the implementation and discuss their solutions. Based on our evaluation, we propose

multiple approaches that can lead to the expected performance increase for future work. In general, we show that static value-flow

analysis is a feasible candidate for further improvements in static instrumentation for symbolic execution.