Strong Optimistic Solving for Dynamic Symbolic Execution

2022-09-08 2022-12-25

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.

Computer Science - Cryptography and Security; Computer Science - Software Engineering; text

10.1109.IVMEM57067.2022.9983965

Open access content. Open access content

COO oai:arXiv.org:2209.03710
2022 Ivannikov Memorial Workshop (IVMEM), IEEE, 2022, pp. 43-53
doi:10.1109/IVMEM57067.2022.9983965
1381564645

CORNELL UNIV
From OAIster®, provided by the OCLC Cooperative.

edsoai.on1381564645