EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software
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).
EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software (Loop-nonterm-v8.pdf) | 1.11MiB |
Wed 13 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
13:30 - 15:00 | Program Verification 1Research Papers / NIER Track / Tool Demonstrations at Room C Chair(s): Nico Rosner Amazon Web Services | ||
13:30 12mTalk | CPA-DF: A Tool for Configurable Interval Analysis to Boost Program Verification Tool Demonstrations Pre-print Media Attached File Attached | ||
13:42 12mTalk | Demystifying Template-based Invariant Generation for Bit-Vector Programs Research Papers Peisen Yao Zhejing University, Jingyu Ke Shanghai Jiao Tong University, Jiahui Sun Zhejiang University, Hongfei Fu Shanghai Jiao Tong University, Rongxin Wu Xiamen University, Kui Ren Zhejiang University | ||
13:54 12mTalk | PSMT: Satisfiability Modulo Theories Meets Probability Distribution NIER Track Fuqi Jia Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Rui Han Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Xutong Ma State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing, China, Baoquan Cui Institute of Software at Chinese Academy of Sciences, China, Minghao Liu Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Pei Huang Stanford University, Feifei Ma Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences, Jian Zhang Institute of Software at Chinese Academy of Sciences; University of Chinese Academy of Sciences Pre-print File Attached | ||
14:06 12mTalk | EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software Research Papers Yao Zhang Tianjin University, Xiaofei Xie Singapore Management University, Yi Li Nanyang Technological University, Sen Chen Tianjin University, Cen Zhang Nanyang Technological University, Xiaohong Li Tianjin University Pre-print File Attached | ||
14:18 12mTalk | Symbolic Fixpoint Algorithms for Logical LTL Games Research Papers Stanly Samuel Indian Institute of Science, India, Deepak D'Souza IISc Bangalore, Raghavan Komondoor Indian Institute of Science, India Pre-print Media Attached File Attached | ||
14:30 12mTalk | SAT-verifiable LTL Satisfiability Checking via Graph Representation LearningRecorded talk NIER Track Weilin Luo Sun Yat-Sen University, Yuhang Zheng Sun Yat-Sen University, Rongzhen Ye Sun Yat-Sen University, Hai Wan School of Data and Computer Science, Sun Yat-sen University, Jianfeng Du Guangdong University of Foreign Studies, Pingjia Liang Sun Yat-Sen University, Polong Chen Sun Yat-Sen University Media Attached |