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 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 (SRC) and instrument SRC 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).
Real-world programs are often large and contain many loops, making it difficult to statically determine the context of deep loops, which is required for recurrent-set analysis.
Inferring recurrent-sets is undecidable and cannot be fully automated, especially for complex loops that involve pointers, arrays, and custom data structures.
To tackle challenges (1), we adopt a divide-and-conquer strategy that analyzes each loop individually instead of the entire program.
To address challenge (2), we propose to sacrifice on generality, and design more practical and tractable non-termination oracles. We employ two strategies for generating non-termination oracles: i.e., State Revisit Condition (SRC) extraction and Revisit Monitoring
For more detail information, please visit the following pages: