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 properties, we have created a static analysis for the automatic identification of the minimal set(s) of program variables that are vulnerable to be controlled by an attacker to potentially violate a (desirable) program property, or, equivalently, the minimal variable set(s) the values of which must be controlled to ensure an (undesirable) program property. Furthermore, we propose conflict-driven abstraction refinement-style analysis to improve the precision of the analysis. Finally, we showcase our analysis on benchmarks collected from the literature and SV-COMP 2023.
