Enhancing Symbolic Execution with Self-Configuring Parameters

We present ${{\rm\small {PARASUIT}}}$, a self-configuring technique that enhances symbolic execution by autonomously adjusting its parameters tailored to each program under test. Modern symbolic execution tools are typically equipped with various external parameters to effectively test real-world programs. However, the need for users to fine-tune a multitude of parameters for optimal testing outcomes makes these tools harder to use and limits their potential benefits. Despite recent efforts to improve this tuning process, existing techniques are not self-configuring; they cannot dynamically identify which parameters to tune for each target program, and for each manually selected parameter, they sample a value from a fixed, user-defined set of candidate values that is specific to that parameter and remains unchanged across programs. The goal of this paper is to automatically configure symbolic execution parameters from scratch for each program. To this end, ${{\rm\small {PARASUIT}}}$ begins by automatically identifying all available parameters in the symbolic execution tool and evaluating each parameter’s impact through interactions with the tool. It then applies a specialized algorithm to iteratively select promising parameters, construct sampling spaces for each, and update their sampling probabilities based on data accumulated from symbolic execution runs using sampled parameter values. We implemented ${{\rm\small {PARASUIT}}}$ on KLEE and assessed it across 12 open-source C programs. The results demonstrate that ${{\rm\small {PARASUIT}}}$ significantly outperforms the state-of-the-art method without self-configuring parameters, achieving an average of 26% higher branch coverage. Remarkably, ${{\rm\small {PARASUIT}}}$ identified 11 unique bugs, four of which were exclusively discovered by ${{\rm\small {PARASUIT}}}$.