OptSE: Toward Optimal Symbolic Execution

Symbolic execution is a powerful technique that can accurately synthesize program inputs for program testing. However, the scalability of symbolic execution is often limited by the capability of the constraint solver and time for testing. With limited time budget, it is desirable to optimally select paths for symbolic execution and furthermore variables for symbolization in order to achieve the maximum code coverage. In this work, we make two technical contributions towards solving this problem. First, different from most existing solving strategies based on heuristic path selection, we formally define the ‘optimal’ strategy based on <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">the reward of executing a given program path considering both possible code coverage and the cost of constraint solving</i>. We further prove that the problem of identifying the optimal strategy for symbolic execution can be reduced to a classic knapsack problem, whose decision problem form is NP-complete. Second, in view of the complexity in identifying the optimal strategy, we design a practical greedy algorithm, named OPTSE, for approximating the optimal strategy. We implemented OPTSE in KLEE and extensively evaluate it on a diverse set of programs. The results show that OPTSE is effective, i.e., achieving 12% more code coverage and detects 17% more security violations than the state-of-the-art symbolic execution tool and outperforming a collection of strategies that only consider either path selection, solving strategies or simply superimpose them.