In this presentation I will present a static analysis proving Termination Resilience of programs i.e. the absence of Robust Non-Termination vulnerabilities in software systems. Robust Non-Termination characterizes programs where an externally-controlled input can force infinite execution, independently of other uncontrolled variables.
Violations of program properties pose significant risks, particularly when they can be triggered by attackers. Multiple approaches has been proposed recently to detect these vulnerabilities. In this seminar, we will present a new abstract interpretation-based static analysis for this problem. By leveraging a static analysis by abstract interpretation for CTL…
In this work, we propose a static analysis by abstract interpretation for Robust CTL properties by taking advantage of our static analyzer FuncTion. A CTL property robustly hold if a controlled input imply it whatever the value of the uncontrolled input. Furthermore, we enhance Conflict Driven Analysis (CDA), an extension…
