Synergizing Symbolic Execution and Fuzzing By Function-level Selective Symbolization
Constraint solving and environment modeling are two challenging problems for symbolic execution. When a program contains non-linear expressions, it is difficult for symbolic execution to explore the program’s whole path space due to the high complexity of the constraint solving for the nonlinear constraints. Besides, when the program uses a third-party library and the source code of the library is not available, the symbolic execution of the program often under-approximates the analysis by concrete execution or over-approximates by introducing new symbolic variables, which may fail to explore the whole path space or introduce false alarms, respectively. This paper proposes FUSE, a framework of synergizing symbolic execution and fuzzing by function-level selective symbolization to tackle these problems. First, FUSE collects the path constraints of each function selectively and introduces symbolic function invocation expressions for the complex or third-party functions. Then, FUSE combines SMT solving and fuzzing to solve the path constraints. We have implemented FUSE on the start-of-theart symbolic execution engine KLEE. The experimental results demonstrate that FUSE effectively and efficiently improves the code coverage. Compared with the state-of-the-art, FUSE achieves 6.6x speedups for achieving the same code coverage.
Fri 9 DecDisplayed time zone: Osaka, Sapporo, Tokyo change
13:00 - 14:00 | |||
13:00 20mPaper | Symbolic Execution of Floating-point Programs: How far are we? Technical Track Guofeng Zhang National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Ziqi Shuai National University of Defense Technology | ||
13:20 20mPaper | Optimal Refinement-based Array Constraint Solving for Symbolic Execution Technical Track Meixi Liu National University of Defense Technology, Changsha, China, Ziqi Shuai National University of Defense Technology, Luyao Liu National University of Defense Technology, Kelin Ma National University of Defense Technology, Ke Ma | ||
13:40 20mPaper | Synergizing Symbolic Execution and Fuzzing By Function-level Selective Symbolization Technical Track Guofeng Zhang National University of Defense Technology, Zhenbang Chen National University of Defense Technology, Ziqi Shuai National University of Defense Technology, Yufeng Zhang Hunan University, Ji Wang College of Computer, National University of Defense Technology |