# Automatic Detection of Vulnerable Variables for CTL Properties of Programs

Naïm Moussaoui Remil, Caterina Urban, Antoine Miné

► To cite this version:

Naïm Moussaoui Remil, Caterina Urban, Antoine Miné. Automatic Detection of Vulnerable Variables for CTL Properties of Programs. 25th Conference on Logic for Programming, Artificial Intelligence and Reasoning, May 2024, Port Louis, Mauritius. pp.116-126, 10.29007/dnpx. hal-04710215

HAL Id: hal-04710215

https://inria.hal.science/hal-04710215v1

Submitted on 26 Sep 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Automatic Detection of Vulnerable Variables for CTL Properties of Programs

Naïm Moussaoui Remil¹, Caterina Urban¹, and Antoine Miné²

¹ Inria & ENS | PSL, Paris, France

`{naim.moussaoui-remil,caterina.urban}@inria.fr`

² Sorbonne Université, CNRS, LIP6, Paris, France

`antoine.mine@lip6.fr`

## Abstract

We present our tool FUNCTION-V for the automatic identification of the minimal sets of program variables that an attacker can control to ensure an undesirable program property. FUNCTION-V supports program properties expressed in Computation Tree Logic (CTL), and builds upon an abstract interpretation-based static analysis for CTL properties that we extend with an abstraction refinement process. We showcase our tool on benchmarks collected from the literature and SV-COMP 2023.

## 1 Introduction

Violations of program properties pose significant risks, particularly when they can be triggered by attackers [8, 14]. This paper presents our tool FUNCTION-V 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.

Let us consider the undesirable robust reachability [8, 9] of the error location in Figure 1. Here, to make sure that the error location is reached, an attacker can either (A) control the value of *x* ensuring that *x* > 0 (error reachable independently of the values of *y* and *z*), or (B) control the value of *y* and *z* ensuring that *y* ≤ *z* (error reachable independently of the value of *x*). In case A, we say that *x* is vulnerable (while *y* and *z* are *safe*), while in case B, we say that *y* and *z* are vulnerable (while *x* is *safe*). Our tool additionally infers the sufficient conditions on the vulnerable variables that ensure the property (robust reachability of the error, in this case) independently of the values of the *safe* variables: *x* > 0 in case A, and *y* ≤ *z* in case B.

Besides robust reachability [8, 9, 18, 19], FUNCTION-V more generally supports program properties expressed in Computation Tree Logic (CTL) [2] (e.g., termination [16], recurrence properties [18, 19], etc.). To improve the precision of our approach, we have equipped FUNCTION-V with a conflict-driven abstraction refinement-style analysis [7].

We report on the experimentation of our tool on benchmarks from [17, 18, 4, 20, 3, 6] as well as from the termination and reachSafety categories of SV-COMP 2023.

## 2 Computation Tree Logic

CTL [2] is a branching-time logic, meaning that its model of time is a tree-like structure in which each state may have several possible futures. Formulas in CTL are formed according to the following grammar:

$$ \phi ::= a \mid l : a \mid \neg \phi \mid \phi \land \phi \mid \phi \lor \phi \mid AX\phi \mid AG\phi \mid A(\phi \cup \phi) \mid EX\phi \mid EG\phi \mid E(\phi \cup \phi) $$
<figure><img src="image_2.png" /><figcaption>Figure 1: Running Example</figcaption></figure>

where a is an atomic proposition, describing properties of individual program states and $l: a$ is an atomic proposition that holds at program point $l$. The universal (A) and the existential (E) quantifiers allow expressing properties of all or some program executions starting in a state. The next temporal operator (X) allows expressing properties about the next state in a program execution. The globally operator (G) allows expressing properties that always (i.e., for all states) hold in a program execution. The until temporal operator (U) allows expressing a property that must hold eventually in a program execution, and another that must always hold until then. For instance, the robust reachability of the error in Figure 1 is expressed by the formula $A(\text{true} \cup \{l_5: \text{true}\})$, which means that for every execution (operator A) starting at the beginning of the program, the sequence of program states encountered during the execution must start with arbitrary states (formula true) followed ultimately (operator U) with a state at program location $l_5$ (formula $\{l_5: \text{true}\}$). In the following, we denote the robust reachability as $AF_\phi$, which is a shortcut for $A(\text{true} \cup \phi)$, meaning that every program execution eventually reaches a state satisfying $\phi$, i.e., $AF_\{l_5: \text{true}\}$ for Figure 1.

The semantics of CTL formulas is formally given by a satisfaction relation $|=$ between program states and CTL formulas. We refer to [1] for its formal definition. We write $s|=\phi$ if and only if the CTL formula $\phi$ holds for (the program executions starting in) the state $s \in \Sigma$.

## 3 Static Analysis of CTL Properties

FUNCTION-V builds upon the static analysis framework proposed by Urban et al. [20]. Following the abstract interpretation theory [5], they derive a sound and complete semantics for proving a CTL property. Specifically, this semantics is a partial function $\Lambda_\phi: \Sigma \to \mathbb{O}$ (where $\mathbb{O}$ is the set of ordinals) defined only over the program states $s \in \Sigma$ that satisfy the CTL property $\phi$, i.e., $s|=\phi$ if and only if $s \in \text{dom}(\Lambda_\phi)$ [20, Theorem 1]. For instance, at the beginning of the program in Figure 1, $\Lambda_{AF_\{l_5: true\}}$ is defined as follows:

$$ \Lambda_{AF_\{l_5: true\}}(s) = \begin{cases} v_1 & s(y) \le s(z) \\ v_2 & s(x) > 0 \\ \text{undefined} & \text{otherwise} \end{cases} $$

where $s(x)$ is value of the variable $x$ in the state $s \in \Sigma$, and $v_1, v_2 \in \mathbb{O}$, meaning that $AF_\{l_5: true\}$ is satisfied in $s$ if and only if $s(y) \le s(z)$ or $s(x) > 0$. The concrete value of $v_1$ and $v_2$ is not relevant in the context of this paper so we do not discuss it (see [20] for further details).

A further sound abstract semantics suitable for static program analysis is derived leveraging the decision tree abstract domain $\mathcal{T}$, which is a numerical abstract domain based on piecewise-defined functions [17, 16]. Specifically, the abstraction $\Lambda_\phi^2 \in \mathcal{T}$ of $\Lambda_\phi$ is a piecewise-defined partial function represented as a decision tree.
<figure><img src="image_3.png" /><figcaption>Figure 2: Decision tree inferred for $\mathbf{AF}\{l_5 : \text{true}\}$ at the beginning of the program in Figure 1.</figcaption></figure>

Figure 2 shows a decision tree abstracting the function $\Lambda_{\mathbf{AF}\{l_5:\text{true}\}}$ shown above. The decision nodes are labeled by linear constraints (of the form $c_1 * X_1 + \dots + c_k * X_k \geq c_{k+1}$) and recursively partition the space of possible values of the program variables: each constraint in a node is satisfied by the left subtree, while its negation is satisfied by the right subtree. The leaf nodes represent the value of the function corresponding to each partition. They are labeled by functions of the program variables ($f_1, f_2, f_3$ in Figure 2), or the special elements $\perp$ or $\top$, which explicitly represent undefined functions. The domain of the function represented by the decision tree in Figure 2 coincides with that of $\Lambda_{\mathbf{AF}\{l_5:\text{true}\}}$ shown above. The partitioning is determined dynamically by the static analysis: partitions are modified by assignments and split (i.e., added) by boolean conditions and when merging control flows. A widening operator [4] extrapolates the function value in each partition and limits the size of the decision trees (and thus the number of partitions) to minimize the cost of the analysis and enforce its termination.

Let $\gamma: \mathcal{T} \to (\Sigma \to \mathcal{O})$ be the concretization function mapping decision trees to piecewise-defined partial functions. We refer to [17, 16] for its formal definition. The abstract semantics $\Lambda_{\phi}^g$ under-approximates the domain of $\Lambda_{\phi}$ (i.e., $\text{dom}(\Lambda_{\phi}^g) \subseteq \text{dom}(\gamma(\Lambda_{\phi}))$), and over-approximates its value (i.e., $\forall s \in \text{dom}(\gamma(\Lambda_{\phi}^g)): \Lambda_{\phi}(s) \leq \gamma(\Lambda_{\phi}^g)(s)$). In this way, $\Lambda_{\phi}^g$ yields sufficient preconditions for a state $s \in \Sigma$ to satisfy the CTL property $\phi$: if $s \in \text{dom}(\gamma(\Lambda_{\phi}^g))$ then $s \models \phi$ [20, Theorem 2]. In Figure 2, the value of $\Lambda_{\mathbf{AF}\{l_5:\text{true}\}}$ is indeed over-approximated when $x \geq 1$, while $\text{dom}(\gamma(\Lambda_{\phi}^g))$ coincides with $\text{dom}(\Lambda_{\phi})$ so the alarm when $y > z$ and $x \leq 0$ (where $\Lambda_{\phi}^g$ has value $\perp$ and is thus undefined) is a true positive (but that is not always the case in general).

# 4 Vulnerable Variable Identification

Let $\mathcal{X}$ denote the set of all program variables. We formally define when a set of variables $S \subseteq \mathcal{X}$ is *safe* with respect to a CTL property $\phi$. Given a variable $x \in \mathcal{X}$ and a value $v \in \mathbb{Z}$, we write $s[x \leftarrow v]$ for the program state obtained by writing the value $v$ into the variable $x$ in $s \in \Sigma$.

**Definition 4.1 (Safe Variables).** A set $S = \{x_0...x_{n-1}\} \subseteq \mathcal{X}$ of program variables is *safe* with respect to a set of program states $D \subseteq \Sigma$, written $\text{SAFE}(S, D)$, when there exists a program state $s \in D$ such that $\forall v_0, ..., v_{n-1} \in \mathbb{Z}^n$ we have $s[x_0 \leftarrow v_0, ..., x_{n-1} \leftarrow v_{n-1}] \in D$.

In other words, there is at least one program state that cannot escape $D$ independently of the values of the safe variables. In the following, given a set of variables $S \subseteq \mathcal{X}$ and a set of program states $D \subseteq \Sigma$, we write $D|_S$ for the subset of all program states in $D$ that remain in $D$ independently of the values of the variables in $S$: $D|_S \stackrel{\text{def}}{=} \{s \in D \mid \forall v_0, ..., v_{n-1} \in \mathbb{Z}^n: s[x_0 \leftarrow$
$v_0, \dots, x_{n-1} \leftarrow v_{n-1}] \in D\}$. Given a CTL property $\phi$, we abuse notation and write $\overline{\text{SAFE}}(S, \phi)$ to denote $\text{SAFE}(S, \{s \in \Sigma \mid s \models \phi\})$. Note that safe variable sets are closed under inclusion, i.e., any subset of a safe variable set remains a safe variable set. We write $\overline{\text{SAFE}}(S, D)$ when $S$ is inclusion-wise maximal, i.e., $\text{SAFE}(S, D) \wedge \forall S' \supseteq S : \neg \text{SAFE}(S', D)$. Inclusion-wise maximal sets are not unique. For example, for the program in Figure 1, we have $\overline{\text{SAFE}}(\{x\}, \text{AF}\{l_5 : \text{true}\})$ as well as $\overline{\text{SAFE}}(\{y, z\}, \text{AF}\{l_5 : \text{true}\})$.

Vulnerable variables are all variables that do not belong to a maximal set of safe variables.

**Definition 4.2 (Vulnerable Variables).** A set $\mathcal{V} \subseteq \mathcal{X}$ of program variables is *vulnerable* with respect to a set of program states $D \subseteq \Sigma$, written $\text{VULNERABLE}(\mathcal{V}, D)$, when $\overline{\text{SAFE}}(\mathcal{X} \setminus \mathcal{V}, D)$.

Namely, vulnerable variable sets are the minimal sets of variables the values of which must be controlled to remain in $D$, independently of the other (safe) variable values. Given a CTL property $\phi$, we write $\text{VULNERABLE}(S, \phi)$ to denote $\text{VULNERABLE}(S, \{s \in \Sigma \mid s \models \phi\})$. Note that a set of variables $\mathcal{X} \subseteq \mathcal{X}$ could be both vulnerable and safe, if both $\overline{\text{SAFE}}(\mathcal{X}, D)$ and $\overline{\text{SAFE}}(\mathcal{X} \setminus \mathcal{X}, D)$ hold. In this case, it means that it is sufficient to control either $\mathcal{X}$ or $\mathcal{X} \setminus \mathcal{X}$ to remain in $D$ despite the values of the other variables. This is the case for the program in Figure 1 as we have $\text{VULNERABLE}(\{y, z\}, \text{AF}\{l_5 : \text{true}\})$ (and $\overline{\text{SAFE}}(\{x\}, \text{AF}\{l_5 : \text{true}\})$) as well as $\text{VULNERABLE}(\{x\}, \text{AF}\{l_5 : \text{true}\})$ (and $\overline{\text{SAFE}}(\{y, z\}, \text{AF}\{l_5 : \text{true}\})$). Indeed, to ensure robust reachability of the error location, it is enough to control the values of $y$ and $z$ (such that $y \le z$), or to control the value of $x$ (such that $x > 0$). It is interesting to infer all vulnerable variables sets as this provides more information and control to the user to choose the more convenient way to achieve the same result.

**Vulnerable Variable Concrete Semantics.** We observe that, since the (domain of the) program semantics $\Lambda_\phi : \Sigma \to \mathcal{O}$ for a CTL property $\phi$ is a sufficient and necessary condition for satisfying $\phi$ [20, Theorem 1] (cf. Section 3), we can abstract $\Lambda_\phi$ to a vulnerable variable semantics $\mathcal{X}_\phi$ that identifies the vulnerable sets of program variables with respect to $\phi$.

**Definition 4.3 (Vulnerable Variable Semantics).** Let $\Lambda_\phi : \Sigma \to \mathcal{O}$ be the program semantics for a CTL property $\phi$. The vulnerable variable semantics $\mathcal{X}_\phi \in \mathcal{P}(\mathcal{P}(\mathcal{X}))$ for $\phi$ is defined as $\mathcal{X}_\phi \stackrel{\text{def}}{=} \alpha_\phi^\mathcal{X}(\Lambda_\phi)$, where $\alpha_\phi^\mathcal{X}(f) \stackrel{\text{def}}{=} \{\mathcal{V} \subseteq \mathcal{X} \mid \text{VULNERABLE}(\mathcal{V}, \text{dom}(f))\}$.

For the program in Figure 1, $\mathcal{X}_\phi = \{\{y, z\}, \{x\}\}$.

We have that just controlling the values of any vulnerable variable set in $\mathcal{X}_\phi$ yields a sufficient condition for satisfying the CTL property $\phi$.

**Theorem 4.1.** Let $\mathcal{V} \in \mathcal{X}_\phi$. The program executions starting in any program state $s \in \text{dom}(\Lambda_\phi)|_{\mathcal{X}\setminus\mathcal{V}}$ satisfy the CTL property $\phi$.

For the program in Figure 1, $\{y, z\} \in \mathcal{X}_\phi$ yields the sufficient condition $\{s \in \Sigma \mid s(y) \le s(z)\}$ (i.e., $y \le z$) and $\{x\} \in \mathcal{X}_\phi$ yields $\{s \in \Sigma \mid s(x) > 0\}$ (i.e., $x > 0$).

**Vulnerable Variable Abstract Semantics.** The vulnerable variable semantics $\mathcal{X}_\phi$ is not computable, so we leverage $\Lambda_\phi^\mathcal{S}$ (cf. Section 3) to derive a sound abstraction $\mathcal{X}_\phi^\mathcal{S}$.

Let $t \in \mathcal{T}$ be a decision tree representing a piecewise-defined partial function $f : \Sigma \to \mathcal{O}$. We observe that, if we havoc the value of a variable $x \in \mathcal{X}$ in $t$ (e.g., we set $x$ to a non-deterministic random value), and the resulting decision tree $t'$ still represents a partially defined function (i.e., $t'$ still contains leaves not labeled with $\perp$ or $\top$), then the variable $x$ is *safe* with respect to $\text{dom}(f)$ (cf. Definition 4.1). This process can be continued iteratively for each program variable, until obtaining (in general, an *under-approximation* of) a maximal safe variable set.
<caption>**Algorithm 1 Safe Variables Identification**</caption>

1: **function** DEFINITELY-SAFE($\mathbb{X}$, t, S)
2:     $R \leftarrow \emptyset$
3:     **for** $x \in \mathbb{X}$ **do**
4:         $C \leftarrow S \cup \{x\}$
5:         **if** CLOSED($C$) **then** $R \leftarrow R \cup \{C\}$
6:         **else**
7:             **if** $\neg$BLOCKED($C$) **then**
8:                 $t' \leftarrow$ FORGET($t$, $\{x\}$)
9:                 **if** UNDEFINED($t'$) **then** BLOCK($C$)
10:             **else**
11:                 $E \leftarrow$ UNCONSTRAINED($t'$)
12:                 $R' \leftarrow$ DEFINITELY-SAFE($\mathbb{X} \setminus E$, $t'$, $C \cup E$)
13:                 $R \leftarrow R \cup R'$
14:             **if** $R = \emptyset$ **then**
15:                 CLOSE($S$)
16:             $R = \{S\}$
17:         **return** $R$

<figure><img src="image_4.png" /></figure>

<figure><img src="image_5.png" /><figcaption>Figure 3: Figure 2 after FORGET(·, {x}). Figure 4: Figure 2 after FORGET(·, {w}), w ∈ {y, z}.</figcaption></figure>

The function DEFINITELY-SAFE in Algorithm 1 considers all subsets of program variables to determine which ones are safe, and returns the set of all maximal safe variables sets it can find. Havoc is performed by the function FORGET invoked at Line 8 [16, Section 5.2.3]. If the resulting tree $t'$ represents a totally undefined function (cf. Line 9), it means that the current candidate set $C$ of variables (cf. Line 4) is not safe and so the recursive iteration should be stopped. The set $C$ is *blocked* (cf. Line 9) to shortcut future iterations with candidate sets that are supersets of $C$, since they cannot be safe either (cf. Line 7). Let us consider the decision tree in Figure 2. The tree resulting after the call to FORGET(·, {x}) is depicted in Figure 3. Further attempts to havoc any of the other variables result in the blocked sets {$x, y$} and {$x, z$}. The definitely safe variable set {$x$} is thus *closed* (cf. Line 15) and added to the returned result set (cf. Line 16). The decision tree resulting from either FORGET(·, {y}) or FORGET(·, {z}) is shown in Figure 4. Either call results in the simultaneous havoc of the other variable. Line 11 thus collects all variables that are unconstrained in $t'$ (i.e., $y$ and $z$) and adds them to the candidate definitely safe variable set in the recursive call (cf. Line 12). The call results in closing the set {$y, z$} because a further havoc of $x$ is shortcut since {$x, y$} $\subseteq$ {$y, z$} $\cup$ {$x$} is blocked. Further iterations encountering already closed sets are also shortcut (cf. Line 5) and so the result returned by DEFINITELY-SAFE is $R = \{{x}, \{y, z\}$}.

We can now define the potentially vulnerable variable semantics $X_{\phi}^{\mathfrak{b}}$.

**Definition 4.4 (Potentially Vulnerable Variable Semantics).** Let $\Lambda_{\phi}^{\mathfrak{b}} \in \mathcal{T}$ be the abstract program semantics for a CTL property $\phi$. The potentially vulnerable variable semantics $X_{\phi}^{\mathfrak{b}} \in$
<figure><img src="image_6.png" /><figcaption>Figure 5: Decision tree inferred for the program in Figure 1 without CDA.</figcaption></figure>

$\mathcal{P}(\mathcal{P}(\mathcal{X}))$ for $\phi$ is defined as $\mathcal{X}_{\phi}^{\natural} \stackrel{\text{def}}{=} \{\mathcal{X} \setminus \mathcal{S} \mid \mathcal{S} \in \text{DEFINITELY-SAFE}(\Lambda_{\phi}^{\natural}, \mathcal{X})\}$.

For any $W \in \mathcal{X}_{\phi}^{\natural}$ there exists $V \in \mathcal{X}_{\phi}$ such that $V \subseteq W$. Thus, we lose the minimality of vulnerable variable sets. Nonetheless, controlling the values of the potentially vulnerable variables still yields a sufficient condition for satisfying the CTL property $\phi$.

**Theorem 4.2.** Let $V \in \mathcal{X}_{\phi}$. The program executions starting in any program state $s \in \text{dom}(\gamma(\text{FORGET}(\Lambda_{\phi}^{\natural}, \mathcal{X} \setminus V)))$ satisfy the CTL property $\phi$.

# 5 Conflict-Driven CTL Analysis

In order to improve the precision of the analysis, we have equipped FUNCTION-V with a conflict-driven analysis (CDA) [7], generalized to handle all program properties expressed in CTL (and not just program termination as in [7]). Following an imprecise CTL analysis, the inferred decision tree defines a partition of the program states where the property is verified (tree leaves labeled with defined functions) and where the analysis is inconclusive (tree leaves labeled with $\perp$ or $\top$). The partitions corresponding to the undefined leaves of the tree form the conflicting domain. For instance, Figure 5 shows another possible decision tree abstraction of $\Lambda_{\text{AF}\{l_5:\text{true}\}}$ for the program in Figure 1 (less precise than that in Figure 2). The conflicting domain in this case is $y - z \ge 0 \land x < y - z$. Drawing inspiration from constraint programming [21], we split the conflicting domain using various cutting heuristic (e.g., splitting on the variable with the largest range of values in the conflicting domain), and repeat the CTL analysis on each resulting partition. For the tree in Figure 5, we split on $x$ and repeat the analysis with $x \le 0$ and $x > 0$. The process proceeds recursively until the CTL property is verified, or a threshold is exceeded. This yields the tree in Figure 2, for which FUNCTION-V precisely finds the vulnerable variable sets $\{y, z\}$ and $\{x\}$. Instead, with the decision tree in Figure 5, FUNCTION-V only finds $\{y, z\}$.

# 6 Tool Architecture

FUNCTION-V is implemented in OCaml. Figure 6 shows an overview of its architecture.

The tool takes as input a C program and a CTL property of interest (cf. Section 2). The front-end takes care of parsing the program (using an ad-hoc LR parser generated using Menhir<fnref n="1" />), building its internal representation, and passing it to the CTL analysis engine (cf. Section 3). The decision tree abstract domain (cf. Section 3) used by the CTL analysis can be configured (SETTINGS in Figure 6) to use different (more or less precise) domain and value

<footnote n="1">¹https://gallium.inria.fr/~fpottier/menhir/</footnote>
<figure><img src="image_7.png" /><figcaption>Figure 6: Overview of FUNCTION-V's architecture.</figcaption></figure>

representations [17] provided by the APRON numerical abstract domain library [10], as well as different (more or less sophisticated) widening heuristics [4]. The CTL analysis can optionally be refined using CDA (cf. Section 5, CDA in Figure 6).

The resulting decision tree is finally passed to the vulnerable variables identification analysis (cf. Section 4), which outputs the potentially vulnerable variables sets found and their corresponding sufficient preconditions for satisfying the given CTL property of interest.

## 7 Experimental Evaluation

We evaluated our tool on a number of test cases obtained from the literature [17, 18, 4, 20, 3, 6] and from the termination and reachSafety categories of the 11th International Competition on Software verification (SV-COMP 2023). The experiments were conducted on a 64-bit 8-Core CPU (AMD® Ryzen 7 pro 5850u) with 16 GB of RAM on Ubuntu 20.04 with a timeout of 120s. We configured the analysis to use decision tree with polyhedral constraints for all tests, and we evaluate the impact of the CDA extension on its precision.

<table><caption>Figure 7: Number of potentially vulnerable variable sets.</caption><thead><tr><th></th><th>Vulnerable Sets</th><th>Number of Programs</th><th>Total Time</th><th>Average Time</th><th>Average LOC</th></tr></thead><tbody><tr><td rowspan="4">no-CDA</td><td>0</td><td>146</td><td>15 s</td><td>0.1 s</td><td>79</td></tr><tr><td>1</td><td>165 (+15)</td><td>21 s</td><td>0.1 s</td><td>22</td></tr><tr><td>2</td><td>30</td><td>10 s</td><td>0.33 s</td><td>24</td></tr><tr><td>3</td><td>6</td><td>5 s</td><td>0.7 s</td><td>25</td></tr><tr><td rowspan="4">CDA</td><td>0</td><td>154</td><td>23 s</td><td>0.15 s</td><td>77</td></tr><tr><td>1</td><td>160 (+14)</td><td>934 s</td><td>5 s</td><td>22</td></tr><tr><td>2</td><td>79</td><td>432 s</td><td>15 s</td><td>25</td></tr><tr><td>3</td><td>5</td><td>124 s</td><td>25 s</td><td>26</td></tr></tbody></table>

For each test case, FUNCTION-V found between zero and three potentially vulnerable variables sets. We present in Figure 7 the number of programs for which FUNCTION-V found no potentially vulnerable set (i.e., the property of interest always holds), and for which there are *n* potentially vulnerable sets (i.e., one of these set must be controlled to ensure the property). We additionally detail the total (for all programs) and average (for each program) analysis time,
<table><caption>Figure 8: Average minimum percentage of potentially vulnerable variables.</caption><thead><tr><th></th><th>Termination</th><th>Robust Reachability</th><th>CTL</th></tr></thead><tbody><tr><th>no-CDA</th><td>17%</td><td>26%</td><td>32%</td></tr><tr><th>CDA</th><td>16%</td><td>22%</td><td>28%</td></tr></tbody></table>

and the average number of lines of code. When the CTL analysis returns a totally undefined function (i.e., a decision tree with only ⊥ or ⊤ leaves), FUNCTION-V returns a single potentially vulnerable variable set containing all program variables, but no sufficient condition can be found to ensure the property of interest. These cases are indicated in parentheses in Figure 7.

In Figure 8, tests are categorized based on the property of interest: termination (242 tests), robust reachability (95 tests), and CTL (130 tests) for other CTL properties. For each category, we report the average minimum percentage of (potentially vulnerable) variables that FUNCTION-V identified (excluding the cases in which no sufficient condition can be found).

Figure 7 and Figure 8 show that CDA improves the precision of FUNCTION-V, allowing it to identify fewer and smaller potentially vulnerable variables sets. This precision improvement comes with a non-negligible (but still small on average) performance cost (cf. Figure 7).

The full experimental results for each test case can be found as part of our artifact<fnref n="2" />.

## 8 Related Work

The program property of robust reachability [8, 9] refines the standard notion of reachability of a bug given a partition of the program variables in a controlled and an uncontrolled set: a bug is robustly reachable if it is reachable whatever the values of the uncontrolled variables. FUNCTION-V can analyze robust reachability properties expressible as a CTL formula of the form $AF_\phi$. The vulnerable variables sets identified by FUNCTION-V identify the controlled program variables, and the corresponding sufficient preconditions inferred by FUNCTION-V yield the space of values for the controlled program variables that ensure the robust reachability property, i.e., instead of returning a single bug witness like the symbolic execution framework proposed by [8, 9], FUNCTION-V returns a set of bug witnesses. Instead, the approach recently proposed by Sellami et al. [15] infers constraints on the uncontrolled program variables.

The non-exploitability analysis proposed by Parolini and Miné [14] uses a combination of forward taint and value analyses by abstract interpretation to infer the absence of (potentially) exploitable runtime errors. A runtime error is (potentially) exploitable if it is triggered by a subset of the variables initialized by an external *input* (that models a potential attacker). Our tool is able to prove non-exploitability by analyzing the absence of (runtime) errors (as a CTL property). If the *input* variables are safe then the runtime errors are non-exploitable (i.e., there is no choice of values for the *input* variables that ensures the presence of runtime errors).

The under-approximating analysis proposed by Miné [13] (recently extended in [12]) aims at finding sufficient preconditions for (un)desired program properties. It is used by the CTL analysis in FUNCTION-V to handle existential CTL properties. We could also use it by itself, as an alternative to the CTL analysis, before the vulnerable variable identification. In this case, however, we would lose the sensitivity to termination, i.e., the (un)desired program property is satisfied provided that the relevant program point(s) are reached by the program execution.

<footnote n="2">²https://zenodo.org/records/10964500</footnote>
# 9 Conclusion and Future Work

In this work, we have presented a new static analyzer called FUNCTION-V for the automatic identification of vulnerable program variables that could be controlled to ensure an (un)desirable CTL property. We have derived our static analysis within the framework of abstract interpretation, building upon a static analysis for CTL program properties that we extended with a conflict-driven abstraction refinement-style analysis. Using experimental evidence on a wide variety of benchmarks, we showed that FUNCTION-V is able to discover vulnerable variables and the corresponding sufficient conditions to ensure the CTL property of interest. It remains for future work to extend the analysis to support a broader range of programs (e.g., array- and pointer-manipulating programs). We also plan to investigate a combination of the non-exploitability analysis of Parolini and Miné [14] with our CTL and vulnerable variable analysis. Finally, we would like to study the applicability of our approach for identifying relevant input features in the context of machine learning explainability [11].

# References

[1] Christel Baier and Joost-Pieter Katoen. *Principles of Model Checking*. MIT Press, 2008.

[2] Edmund M. Clarke and E. Allen Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Orna Grumberg and Helmut Veith, editors, *25 Years of Model Checking - History, Achievements, Perspectives*, volume 5000 of *Lecture Notes in Computer Science*, pages 196–215. Springer, 2008.

[3] Byron Cook, Eric Koskinen, and Moshe Y. Vardi. Temporal Property Verification as a Program Analysis Task. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, *Computer Aided Verification - 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011. Proceedings*, volume 6806 of *Lecture Notes in Computer Science*, pages 333–348. Springer, 2011.

[4] Nathanaël Courant and Caterina Urban. Precise Widening Operators for Proving Termination by Abstract Interpretation. In Axel Legay and Tiziana Margaria, editors, *Tools and Algorithms for the Construction and Analysis of Systems - 23rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Part I*, volume 10205 of *Lecture Notes in Computer Science*, pages 136–152, 2017.

[5] Patrick Cousot and Radhia Cousot. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Robert M. Graham, Michael A. Harrison, and Ravi Sethi, editors, *Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977*, pages 238–252. ACM, 1977.

[6] Daniel Dietsch, Matthias Heizmann, Vincent Langenfeld, and Andreas Podelski. Fairness Modulo Theory: A New Approach to LTL Software Model Checking. In Daniel Kroening and Corina S. Pasareanu, editors, *Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part I*, volume 9206 of *Lecture Notes in Computer Science*, pages 49–66. Springer, 2015.

[7] Vijay D'Silva and Caterina Urban. Conflict-Driven Conditional Termination. In Daniel Kroening and Corina S. Pasareanu, editors, *Computer Aided Verification - 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II*, volume 9207 of *Lecture Notes in Computer Science*, pages 271–286. Springer, 2015.

[8] Guillaume Girol, Benjamin Farinier, and Sébastien Bardin. Not All Bugs Are Created Equal, But Robust Reachability Can Tell the Difference. In Alexandra Silva and K. Rustan M. Leino, editors, *Computer Aided Verification - 33rd International Conference, CAV 2021, Virtual Event*,
July 20-23, 2021, Proceedings, Part I, volume 12759 of Lecture Notes in Computer Science, pages 669-693. Springer, 2021.

[9] Guillaume Girol, Benjamin Farinier, and Sébastien Bardin. Introducing Robust Reachability. Formal Methods in System Design, November 2022.

[10] Bertrand Jeannet and Antoine Miné. Apron: A Library of Numerical Abstract Domains for Static Analysis. In Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings, volume 5643 of Lecture Notes in Computer Science, pages 661-667. Springer, 2009.

[11] João Marques-Silva, Thomas Gerspacher, Martin C. Cooper, Alexey Ignatiev, and Nina Narodytska. Explanations for monotonic classifiers. In Marina Meila and Tong Zhang, editors, Proceedings of the 38th International Conference on Machine Learning, ICML 2021, 18-24 July 2021, Virtual Event, volume 139 of Proceedings of Machine Learning Research, pages 7469-7479. PMLR, 2021.

[12] Marco Milanese and Antoine Miné. Generation of Violation Witnesses by Under-Approximating Abstract Interpretation. In Rayna Dimitrova, Ori Lahav, and Sebastian Wolff, editors, Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part I, volume 14499 of Lecture Notes in Computer Science, pages 50-73. Springer, 2024.

[13] Antoine Miné. Backward Under-Approximations in Numeric Abstract Domains to Automatically Infer Sufficient Program Conditions. Sci. Comput. Program., 93:154-182, 2014.

[14] Francesco Parolini and Antoine Miné. Sound Abstract Nonexploitability Analysis. In Rayna Dimitrova, Ori Lahav, and Sebastian Wolff, editors, Verification, Model Checking, and Abstract Interpretation - 25th International Conference, VMCAI 2024, London, United Kingdom, January 15-16, 2024, Proceedings, Part II, volume 14500 of Lecture Notes in Computer Science, pages 314-337. Springer, 2024.

[15] Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, and Sébastien Bardin. Inference of robust reachability constraints. Proc. ACM Program. Lang., 8(POPL):2731-2760, 2024.

[16] Caterina Urban. Static Analysis by Abstract Interpretation of Functional Temporal Properties of Programs. PhD thesis, 2015.

[17] Caterina Urban and Antoine Miné. A Decision Tree Abstract Domain for Proving Conditional Termination. In Markus Müller-Olm and Helmut Seidl, editors, Static Analysis - 21st International Symposium, SAS 2014, Munich, Germany, September 11-13, 2014. Proceedings, volume 8723 of Lecture Notes in Computer Science, pages 302-318. Springer, 2014.

[18] Caterina Urban and Antoine Miné. Proving Guarantee and Recurrence Temporal Properties by Abstract Interpretation. In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation - 16th International Conference, VMCAI 2015, Mumbai, India, January 12-14, 2015. Proceedings, volume 8931 of Lecture Notes in Computer Science, pages 190-208. Springer, 2015.

[19] Caterina Urban and Antoine Miné. Inference of ranking functions for proving temporal properties by abstract interpretation. Comput. Lang. Syst. Struct., 47:77-103, 2017.

[20] Caterina Urban, Samuel Ueltschi, and Peter Müller. Abstract Interpretation of CTL Properties. In Andreas Podelski, editor, Static Analysis - 25th International Symposium, SAS 2018, Freiburg, Germany, August 29-31, 2018, Proceedings, volume 11002 of Lecture Notes in Computer Science, pages 402-422. Springer, 2018.

[21] Ghiles Ziat. A Combination of Abstract Interpretation and Constraint Programming. PhD thesis, 2019.