一句话：通过状态重访预言机将非终止检测融入测试，可扩展地发现大型程序中的无限循环。
终止性分析长期面临可扩展性不足的问题，现有方法仅适用于小规模程序。本文提出 EndWatch，一种通过测试检测无限循环导致非终止的实用技术。其核心是基于状态重访生成非终止预言机：若程序在同一位置回到已访问状态则不终止。对线性循环，通过对单个循环符号执行推断状态重访条件（SRC）并插桩到目标循环；对非线性循环，则插桩以在运行期检查具体状态重访。这些预言机可集成到测试工具（如 AFL）中以检测大型程序的非终止。在标准基准上，EndWatch 检测出 87% 的非终止程序，优于最佳基线的 67%；在真实项目中，检测出 90% 的已知非终止 CVE 及 4 个未知缺陷。
Detecting non-termination is crucial for ensuring program correctness and security, such as preventing denial-of-service attacks. While termination analysis has been studied for many years, existing methods have limited scalability and are only effective on small programs. To address this issue, we propose a practical termination checking technique, called EndWatch, for detecting non-termination caused by infinite loops through testing. Specifically, we introduce two methods to generate non-termination oracles based on checking state revisits, i.e., if the program returns to a previously visited state at the same program location, it does not terminate. The non-termination oracles can be incorporated into testing tools (e.g., AFL used in this paper) to detect non-termination in large programs. For linear loops, we perform symbolic execution on individual loops to infer State Revisit Conditions (SRCs) and instrument SRCs into target loops. For non-linear loops, we instrument target loops for checking concrete state revisits during execution. We evaluated EndWatch on standard benchmarks with small-sized programs and real-world projects with large-sized programs. The evaluation results show that EndWatch is more effective than the state-of-the-art tools on standard benchmarks (detecting 87% of non-terminating programs while the best baseline detects only 67%), and useful in detecting non-termination in real-world projects (detecting 90% of known non-termination CVEs and 4 unknown bugs).
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{abs-2312-03335,
title = {EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software},
author = {Yao Zhang and Xiaofei Xie and Yi Li and Sen Chen and Cen Zhang and Xiaohong Li},
booktitle = {ASE},
year = {2023},
doi = {10.1109/ase56229.2023.00061}
}