IFSE: Taming Closed-Box Functions in Symbolic Execution via Fuzz Solving

Modern symbolic execution techniques face the challenge of handling closed-box (CB) functions (e.g., system calls, library functions) whose source code is unavailable. One interesting solution in the literature is deferred concretization with fuzz solving. However, no open-source implementation of such techniques exists, and thus it is difficult to evaluate and investigate the effectiveness. In this paper, we present IFSE (Integrating Fuzz Solving into Symbolic Execution), an open-source tool implementing the relevant techniques on top of KLEE to handle the CB functions in symbolic execution. We evaluated IFSE on GNU Coreutils. The results show that IFSE achieves the line and branch code coverage improvement by 28.3% and 12.2% respectively compared to vanilla KLEE. The satisfaction rate of fuzz solver achieves 80.2%, demonstrating its ability to reason CB function related constraints. IFSE is publicly available at https://github.com/ecnusse/ifse and a demonstration video is at https://youtu.be/xMv6-MOlE-I.