Strong Optimistic Solving for Dynamic Symbolic Execution

TL;DR

This paper introduces a strong optimistic solving method for dynamic symbolic execution that improves branch inversion accuracy and code coverage by eliminating irrelevant constraints and handling nested control transfers.

Contribution

The paper proposes a novel strong optimistic solving technique for DSE that enhances branch inversion efficiency and accuracy, implemented in the Sydr tool.

Findings

Combining strategies increases code coverage and branch inversion rate.

The proposed method outperforms existing strategies in accuracy and efficiency.

Implementation in Sydr demonstrates practical benefits in dynamic symbolic execution.

Abstract

Dynamic symbolic execution (DSE) is an effective method for automated program testing and bug detection. It is increasing the code coverage by the complex branches exploration during hybrid fuzzing. DSE tools invert the branches along some execution path and help fuzzer examine previously unavailable program parts. DSE often faces over- and underconstraint problems. The first one leads to significant analysis complication while the second one causes inaccurate symbolic execution. We propose strong optimistic solving method that eliminates irrelevant path predicate constraints for target branch inversion. We eliminate such symbolic constraints that the target branch is not control dependent on. Moreover, we separately handle symbolic branches that have nested control transfer instructions that pass control beyond the parent branch scope, e.g. return, goto, break, etc. We implement the proposed method in our dynamic symbolic execution tool Sydr. We evaluate the strong optimistic strategy, the optimistic strategy that contains only the last constraint negation, and their combination. The results show that the strategies combination helps increase either the code coverage or the average number of correctly inverted branches per one minute. It is optimal to apply both strategies together in contrast with other configurations.