Abstract

Software bugs vary significantly in their severity and impact. While some bugs may be minor inconveniences that cause small glitches or inefficiencies, others pose much greater risks — especially those that can be exploited by an external adversary (e.g., attacker, scheduler, etc.). Recognizing and prioritizing such critical vulnerabilities is essential for maintaining software safety and security. While they might not always present the immediate dangers of security vulnerabilities, bugs that cause non-termination can be weaponized by a malicious actor to be equally critical software issues. These bugs lock software into an endless cycle of execution leading to system slowdowns, resource exhaustion, and denial-of-service conditions. Identifying and fixing these bugs is essential to ensuring the reliability of software systems, especially in environments where performance and availability are crucial. In this talk, we formally introduce the Robust Non-Termination program vulnerability, to characterize programs for which there exists an externally-controlled input value that forces their execution into an infinite loop, independently of the values of other uncontrolled variables (e.g., random seeds, etc.). We design an abstract interpretation-based static analysis framework to prove Termination Resilience — the absence of Robust Non-Termination vulnerabilities. Our framework is a more expressive semantic generalization of Cousot and Cousot’s idea of computing a ranking function by abstract interpretation. Specifically, we extend their semantic definitions to handle both demonic and angelic non-determinism, distinguishing cases where the program execution is influenced by externally-controlled inputs from those where it is not. We derive a sound static analysis for Termination Resilience by building upon Urban and Miné’s decision tree abstract domain, enhancing it with novel and non-trivial transformer operators to effectively manage the distinction between controlled and uncontrolled program variables. Our static analysis automatically infers sufficient preconditions that ensure Termination Resilience for a program. The analysis is evaluated on benchmarks from the International Competition on Software Verification (SV-COMP), demonstrating its practical effectiveness for verifying Termination Resilience, and detecting Robust Non-Termination vulnerabilities.