EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software

• URL: http://arxiv.org/abs/2312.03335v1
• Date: Wed, 6 Dec 2023 08:13:30 GMT
• Title: EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software
• Authors: Yao Zhang, Xiaofei Xie, Yi Li, Sen Chen, Cen Zhang, Xiaohong Li
• Abstract summary: We propose a practical termination checking technique, called EndWatch, for detecting non-termination caused by infinite loops through testing. We introduce two methods to generate non-termination oracles based on checking state revisits. The non-termination oracles can be incorporated into testing tools to detect non-termination in large programs.
• Score: 30.67959999716073
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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).

Related papers

• LLMs versus the Halting Problem: Revisiting Program Termination Prediction [28.324966803819752]
  determining whether a program terminates is a central problem in computer science.<n>Recent success and progress in large language models (LLMs) raises the following question: can LLMs reliably predict program termination?<n>We evaluate LLMs on a diverse set of C programs from the Termination category of the International Competition on Software Verification (SV-Comp) 2025.
  arXiv  Detail & Related papers  (2026-01-26T21:44:12Z)
• Rethinking Metrics and Benchmarks of Video Anomaly Detection [58.37571339811799]
  Video Anomaly Detection (VAD) aims to detect anomalies that deviate from expectation.<n>Existing VAD metrics are influenced by single annotation bias.<n>Existing benchmarks lack the capability to evaluate scene overfitting of fully/weakly-supervised algorithms.
  arXiv  Detail & Related papers  (2025-05-25T08:09:42Z)
• SILENT: A New Lens on Statistics in Software Timing Side Channels [10.872605368135343]
  Recent attacks have challenged our understanding of what it means for code to execute in constant time on modern CPUs. We introduce a new algorithm for the analysis of timing measurements with strong, formal statistical guarantees. We demonstrate the necessity, effectiveness, and benefits of our approach on both synthetic benchmarks and real-world applications.
  arXiv  Detail & Related papers  (2025-04-28T14:22:23Z)
• Studying the Impact of Early Test Termination Due to Assertion Failure on Code Coverage and Spectrum-based Fault Localization [48.22524837906857]
  This study is the first empirical study on early test termination due to assertion failure. We investigated 207 versions of 6 open-source projects. Our findings indicate that early test termination harms both code coverage and the effectiveness of spectrum-based fault localization.
  arXiv  Detail & Related papers  (2025-04-06T17:14:09Z)
• Loop unrolling: formal definition and application to testing [33.432652829284244]
  Testing processes usually aim at high coverage, but loops severely limit coverage ambitions since the number of iterations is generally not predictable. This article provides a formal definition and a set of formal properties of unrolling. Using this definition as the conceptual basis, we have applied an unrolling strategy to an existing automated testing framework.
  arXiv  Detail & Related papers  (2025-02-21T15:36:21Z)
• A shallow dive into the depths of non-termination checking for C programs [3.4144415576897624]
  Unintended Non-Termination (NT) is common in real-world software development. We propose a sound and efficient technique for NT checking that is also effective on realworld software. Our experiments on wide ranging software benchmarks show that the technique outperforms state-of-the-art NT checkers.
  arXiv  Detail & Related papers  (2024-09-04T22:47:46Z)
• Demystifying Behavior-Based Malware Detection at Endpoints [22.3867935906334]
  We present the first measurement study of the performance of ML-based malware detectors at real-world endpoints. We identify a wide gap between prior methods' sandbox-based detection performance. We propose that yield a relative improvement of 5-30% over the baselines.
  arXiv  Detail & Related papers  (2024-05-09T22:04:55Z)
• Parallel Program Analysis on Path Ranges [3.018638214344819]
  Ranged symbolic execution performs symbolic execution on program parts, so called path ranges, in parallel. We present a verification approach that splits programs into path ranges and then runs arbitrary analyses on the ranges in parallel.
  arXiv  Detail & Related papers  (2024-02-19T08:26:52Z)
• Semi-Oblivious Chase Termination for Linear Existential Rules: An Experimental Study [5.936402320555635]
  The chase procedure is a fundamental algorithmic tool in databases that allows us to reason with constraints. It takes as input a database and a set of constraints, and iteratively completes the database as dictated by the constraints. A key challenge, though, is the fact that it may not terminate, which leads to the problem of checking whether it terminates given a database and a set of constraints.
  arXiv  Detail & Related papers  (2023-03-22T18:21:01Z)
• Using Graph Neural Networks for Program Termination [0.0]
  We move away from formal methods to embrace the nature of machine learning models. We take advantage of the graph representation of programs by employing Graph Neural Networks. We adapt the notions of attention and semantic segmentation, previously used for other application domains, to programs.
  arXiv  Detail & Related papers  (2022-07-28T12:16:37Z)
• Benchmarking Node Outlier Detection on Graphs [90.29966986023403]
  Graph outlier detection is an emerging but crucial machine learning task with numerous applications. We present the first comprehensive unsupervised node outlier detection benchmark for graphs called UNOD.
  arXiv  Detail & Related papers  (2022-06-21T01:46:38Z)
• Fault-Aware Neural Code Rankers [64.41888054066861]
  We propose fault-aware neural code rankers that can predict the correctness of a sampled program without executing it. Our fault-aware rankers can significantly increase the pass@1 accuracy of various code generation models.
  arXiv  Detail & Related papers  (2022-06-04T22:01:05Z)
• A2Log: Attentive Augmented Log Anomaly Detection [53.06341151551106]
  Anomaly detection becomes increasingly important for the dependability and serviceability of IT services. Existing unsupervised methods need anomaly examples to obtain a suitable decision boundary. We develop A2Log, which is an unsupervised anomaly detection method consisting of two steps: Anomaly scoring and anomaly decision.
  arXiv  Detail & Related papers  (2021-09-20T13:40:21Z)
• Global Optimization of Objective Functions Represented by ReLU Networks [77.55969359556032]
  Neural networks can learn complex, non- adversarial functions, and it is challenging to guarantee their correct behavior in safety-critical contexts. Many approaches exist to find failures in networks (e.g., adversarial examples), but these cannot guarantee the absence of failures. We propose an approach that integrates the optimization process into the verification procedure, achieving better performance than the naive approach.
  arXiv  Detail & Related papers  (2020-10-07T08:19:48Z)
• Real-Time Anomaly Detection in Edge Streams [49.26098240310257]
  We propose MIDAS, which focuses on detecting microcluster anomalies, or suddenly arriving groups of suspiciously similar edges. We further propose MIDAS-F, to solve the problem by which anomalies are incorporated into the algorithm's internal states. Experiments show that MIDAS-F has significantly higher accuracy than MIDAS.
  arXiv  Detail & Related papers  (2020-09-17T17:59:27Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.