Symerge: Replacing Calls in Under-Constrained Symbolic Execution and Find Vulnerabilities
摘要
Vulnerability poses a significant threat to software security. Under-constrained symbolic execution (UCSE) plays a prevalent role in vulnerability detection. It can initiate from any code region, enabling flexible and scalable analysis. However, function calls present a dilemma for UCSE: either explore the function thoroughly, incurring substantial overhead, or limit the exploration and risk overlooking crucial operations. Besides, UCSE is unable to process indirect calls when the destination of the call cannot be determined within the current code region. Employing function summaries is a solution to these challenges. Function summaries can simulate function behaviors and replace the UCSE in actual functions. Currently, symbolic execution tools only manually implement function summaries for limited libc functions, and research on the automated generation of function summaries for symbolic execution remains insufficient. In this paper, we propose Symerge, a new approach to generate function summaries for symbolic execution. We conduct UCSE within a function, assess differences between initial and return states, and summarize these differences to build a function summary. We employ multi-level state merging to manage states within a function, thereby preventing state explosion. State merging introduces complex expressions and increases the execution overhead. To mitigate this, we apply acceleration strategies such as expression simplification. Finally, we use information in function summaries to find vulnerabilities. The overall performance of Symerge on Juliet Test Suite outperforms that of the baseline tools. Symerge solves most indirect calls in 4 real-world binaries and finds 17 bugs, including four 0-day vulnerabilities.