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

HAL
open science

# Reachability Analysis of Upper-Stack Manipulating Binary Code ⋆

Shijie Lin, Tayssir Touili

► To cite this version:

Shijie Lin, Tayssir Touili. Reachability Analysis of Upper-Stack Manipulating Binary Code ⋆. 23rd International Conference on Software Engineering and Formal Methods, Nov 2025, Tolède, Spain. hal-05288783

HAL Id: hal-05288783

https://hal.science/hal-05288783v1

Submitted on 29 Sep 2025

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.

Public Domain
Reachability Analysis of Upper-Stack
Manipulating Binary Code*

Shijie Lin¹ and Tayssir Touili¹

IRIF, CNRS and Université Pairs Cité, France

**Abstract.** In this paper, we tackle the reachability analysis problem of binary code that manipulate the part of memory that is just above the stack pointer. To model such programs, we use Upper Stack Push-Down Systems (UPDS), an extension of Pushdown systems (PDS), to simulate the stack operations of assembly codes. UPDS is a kind of PDS with two stacks called upper stack and lower stack where the lower stack works as a normal PDS stack and the upper stack works as the memory space above the stack. We propose several algorithms to perform the reachability analysis of this model. To this aim, we represent regular potentially infinite sets of configurations using finite state automata. The reachability sets of UPDSs being in general not regular, we propose two semi-algorithms for computing accurately the sets of predecessors *pre*\* and successors *post*\* of regular sets of configurations of UPDS. We provide interesting subclasses for which our semi-algorithms are guaranteed to terminate. We show that our approach has several interesting applications like stack overflow detection, stack string detection, return address anomaly detection, etc.

**Keywords:** Reachability analysis · Pushdown System with an Upper Stack · Finite Automata · Binary Code Analysis.

# 1 Introduction

Analyzing programs at the binary code level is nowadays a challenging problem, as in many cases, source code is unavailable, and only executable binaries are accessible. This is the case e.g. for (1) the analysis and detection of malware, (2) the detection of typical vulnerabilities such as call stack overflows, (3) the verification of generic components purchased off-the-shelf, (4) the verification of optimized code correctness, (5) the verification of source code containing portions of assembler, etc.

Several works have been proposed for binary code analysis like CodeSurfer [9, 6, 3, 8], SMODIC [29, 28, 30], or PoMMaDe [27, 23, 24, 26, 25]. In these works, PushDown Systems (PDS) were advocated to be a natural model for sequential binary code, since they allow to keep track of the program's stack, to record function return addresses, and to take into account the different pushes and

<footnote>* This work was partially funded by the french ANR grant Defmal "ANR-22-PECY-0007"</footnote>
pops of the program. However, if we look closer, PushDown Systems cannot
accurately model the operations on the assembly stack. Indeed, in real-world
executions, the assembly stack is implemented using a stack pointer sp that
points to the head of the stack. When a push instruction is executed, the stack
pointer is decremented, and some data is added to the head of the stack; whereas
when a pop instruction is executed, the stack pointer is incremented, removing
the topmost element from the stack. This element is not physically erased from
memory; it remains in its memory region above the current stack pointer and can
potentially be accessed later e.g. using an instruction of the form mov eax, [sp-4]
that puts the value pointed to at address sp-4 in the register eax. In contrast, a
PDS does not keep track of the region above the stack pointer. Thus, in a PDS
model, once a symbol is popped from the stack, it is permanently discarded and
no longer accessible, as shown in Fig.1.. Therefore, using a PDS to model a
binary code does not allow to represent instructions of the form mov eax, [sp-4]
that put the value pointed to at address sp-4 in the register eax, since sp-4 points
to the region above the stack, and a PDS cannot reach this region.

To overcome this problem, Upper Stack Pushdown Systems (UPDS) were
introduced in [19]. Roughly speaking, a UPDS is a PDS equipped with an upper
stack that represents the memory region above the standard stack. Thus, a UPDS
has two stacks: the standard PDS stack, called the lower stack, that mimics the
standard program's stack; and the upper stack that mimics the region above
the program's stack. When a pop instruction is applied, sp is incremented. To
simulate this, the UPDS pops the topmost symbol from its lower stack and
adds it to its upper stack (as described in Fig.2.(a) and Fig.2.(b)). On the
other hand, when a push instruction is applied, sp is decremented. Thus, the
last symbol of the upper stack is destroyed, and is overwritten by the pushed
element that will be added to the top of the lower (standard) stack.

We tackle in this paper the reachability analysis of UPDS. Unfortunately,
unlike standard pushdown systems, it is shown in [19] that the sets of prede-
cessors and successors of a regular set of configurations of a UPDS are both
not regular. To overcome this irregularity, we propose in this paper a semi-
algorithm that computes the set of successors (resp.predecessors) of a regular set
of configurations. Our semi-algorithms are based on (1) representing regular (po-
tentially infinite) sets of configurations of UPDSs using finite state automata,
and (2) applying saturation procedures on the finite state automata in order
to take into account the effect of applying the rules of the UPDS. Our semi-
algorithms are not guaranteed to terminate, but when they do, they compute a
finite-state automaton that represents the set of successors (resp.predecessors)
of the UPDS. We give concrete examples that show that our semi-algorithms
can terminate in several interesting cases. Moreover, we highlight subclasses of
UPDS for which our semi-algorithms are guaranteed to terminate and compute
finite-state automata representing the sets of successors (resp. predecessors) of
UPDS. Our semi-algorithms can be adapted to produce over-approximations and
under-approximations of the reachability sets.
Finally, we show that our UPDS model and our results have several applications in binary code analysis, like stack overflow detection, stack string detection, return address anomaly detection, shellcode detection, etc.

**Outline.** We introduce our model in Section 2. Our procedures that compute the set of predecessors (resp. successors) are given in Section 3 (resp. Section 4). Section 5 describes different interesting applications of our approach.

<figure><img src="image_2.png" /><figcaption>**Fig. 1.** (a): The assembly stack before the pop *a* instruction, (b): The assembly stack after the pop *a* instruction, (c): The Pushdown System stack before the pop *a* instruction, (d): The Pushdown System stack after the pop *a* instruction</figcaption></figure>

<figure><img src="image_3.png" /><figcaption>**Fig. 2.** (a): UPDS stacks before the pop *a* instruction, (b): UPDS stacks after the pop *a* instruction</figcaption></figure>

**Related work.** Reachability analysis of standard Pushdown systems was considered in [1, 10, 18, 22, 11], where the forward and backward reachability sets of a regular set of configurations of a PDS are shown to be regular and effectively computable. UPDSs are more expressive than PDS since they involve an upper-stack in addition to the standard stack. Our semi-algorithms can be seen as extensions of the saturation procedures that compute finite-state automata representing the sets of predecessors and successors for PDS.

Pushdown systems with multiple stacks were introduced in [21]. The reachability analysis of these systems being undecidable, the authors proposed bounded-phase analysis that allows to compute regular under-approximations of the reachability sets, where during a phase, only one stack can evolve. This approach can be used to compute under-approximations of UPDSs since a UPDS can be seen as a 2-stack pushdown system. However, this approach is not well adapted for UPDSs, since a phase involves the manipulation of a single stack, therefore, a UPDS push or pop will be represented by a phase change. Thus, using the approach of bounded-phase analysis of [21] to compute under-approximations for UPDSs will not allow making an unbounded number of pushes or pops.
Several subclasses of pushdown systems with multiple stacks have been pro-
posed in [4, 15, 17, 16]. However, these works cannot be used to perform the
reachability analysis of UPDSs as they consider severe restrictions on the use
of the push and/or pop rules. 2-Visibly Pushdown Automata were defined in
[12] as a variant of two-stack automata where the stack operations are driven by
the input word. Reachability is decidable for a subclass of 2-Visibly Pushdown
Automata. This subclass cannot simulate UPDSs.

Several models and tools were proposed to deal with memory manipulating
programs [20, 9, 5, 2]. However, these works cannot record the content of the
upper-stack (the part of the memory just above the stack) as our UPDS model
does.

## 2 Preliminaries

2.1 Pushdown Systems with an Upper Stack

**Definition 1.** A Pushdown System with an Upper stack is a pair $\mathcal{P} = (\Gamma, \Delta)$, where $\Gamma$ is a finite stack alphabet and $\Delta \subseteq \Gamma \times (\{\epsilon\} \cup \Gamma \cup \Gamma^2)$ is a finite set of transition rules.

Let $\gamma \in \Gamma$ and $w \in \{\epsilon\} \cup \Gamma \cup \Gamma^2$, a rule $\delta = (\gamma, w) \in \Delta$ can also be written as $\delta = \gamma \leftrightarrow w$. A UPDS has an upper stack and a lower stack. The lower stack corresponds to the standard stack for standard pushdown systems. The upper stack allows to model the region above the stack in assembly programs. A configuration of a UPDS $\mathcal{P}$ is a pair $c = (w_u, w_l)$, where $w_u \in \Gamma^*$ is the content of the upper stack and $w_l \in \Gamma^*$ is the content of the lower stack.

We infer an immediate successor relation $\Rightarrow_P$ on configurations of $\mathcal{P}$ as follows:

**Pop Rules:** if $\delta = a \leftrightarrow \epsilon \in \Delta$, then $\forall w_u \in \Gamma^*$ and $\forall w_l \in \Gamma^*$, $\langle w_u, aw_l \rangle \Rightarrow_P \langle w_u a, w_l \rangle$. The top letter $a$ of the lower stack is popped and moved to the bottom of the upper stack (the stack pointer moves to the right).

**Switch Rules:** if $\delta = a \leftrightarrow c \in \Delta$, then $\forall w_u \in \Gamma^*$ and $\forall w_l \in \Gamma^*$, $\langle w_u, aw_l \rangle \Rightarrow_P \langle w_u, cw_l \rangle$. The top letter $a$ of the lower stack is replaced by the letter $c$ (the stack pointer does not move).

**Push Rules:** if $\delta = a \leftrightarrow bc \in \Delta$, then $\forall w_u \in \Gamma^*$ and $\forall w_l \in \Gamma^*$, $\forall \gamma \in \Gamma$, $\langle w_u \gamma, aw_l \rangle \Rightarrow_P \langle w_u, bcw_l \rangle$. Moreover, if the upper stack is empty, then $\langle \epsilon, aw_l \rangle \Rightarrow_P \langle \epsilon, bcw_l \rangle$. The top letter $a$ of the lower stack is replaced by two letters $bc$ and the last letter of the upper stack is deleted in order to make room for it (the stack pointer moves to the left), unless there is nothing in the upper stack.

Let $c$ and $c'$ be two configurations of $\mathcal{P}$ such that $c' \Rightarrow_P c$. Then $c$ is called
the successor of $c'$ and $c'$ is called the predecessor of $c$. Let $\Rightarrow_P^*$ be the reflexive
and transitive closure of $\Rightarrow_P$. We define $\overset{i}{\Rightarrow}$ as follows: $c \overset{i}{\Rightarrow} c'$ iff there exists
a sequence of configurations $c_0 \Rightarrow_P c_1 \Rightarrow_P \cdots \Rightarrow_P c_i$ s.t. $c_0 = c$ and $c_i = c'$.
Given a configuration of a UPDS $\mathcal{P}$, the set of immediate predecessors (resp.
successors) of $c$ is $\text{pre}(c) = \{c' \mid c' \Rightarrow_P c\}$ (resp. $\text{post}(c) = \{c' \mid c \Rightarrow_P c'\}$).
Let $pre^*$ (resp. $post^*$) denote the reflexive-transitive closure of $pre$ (resp. $post$).
Given a set of configurations $C$ of a UPDS $\mathcal{P}$, $pre^*(C) = \{c \mid \exists c' \in C, c \Rightarrow_P^* c'\}$
and $post^*(C) = \{c \mid \exists c' \in C, c' \Rightarrow_P^* c\}$. In the following, we drop the index $\mathcal{P}$
from the relations $\Rightarrow_P$ if it is understood from the context.

## 2.2 P-automata

To finitely represent potentially infinite sets of configurations of a UPDS, we use
finite-state automata as follows. Let $\bar{\Gamma} = \{\bar{\gamma} \mid \gamma \in \Gamma\}$. For any $w = \gamma_1\gamma_2\cdots\gamma_n \in \Gamma^*$, we denote by $\bar{w}$ the word $\bar{\gamma_1}\bar{\gamma_2}\cdots\bar{\gamma_n}$. Let $L \subseteq \Gamma^*$, we denote by $\bar{L} = \{\bar{w} \mid w \in L\}$. A set of configurations $C$ of a UPDS $\mathcal{P}$ is called **regular** if and only if the set $\{\overline{w_u}w_l \mid \langle w_u, w_l \rangle \in C\}$ is accepted by a finite-state automaton called $\mathcal{P}$-automaton defined as follows:

**Definition 2.** A $\mathcal{P}$-automaton is a tuple $\mathcal{A} = (Q, \Gamma, T, p, F)$ where $Q$ is a finite set of states, $T \in Q \times (\Gamma \cup \bar{\Gamma} \cup \{\epsilon\} \cup \{\bar{\epsilon}\}) \times Q$ is a set of transitions, $p \in Q$ is the initial state and $F \subseteq Q$ is the set of final states.

Note that $\epsilon$-transitions are allowed. For the sake of harmonisation, we introduce $\bar{\epsilon}$, which behaves exactly as $\epsilon$. If $(q, \gamma, q') \in T$, we write $q \xrightarrow{\gamma} q'$. For every word $w = \gamma_1\gamma_2\cdots\gamma_n \in \Gamma^*$ (resp. $\bar{\Gamma}^*$) where $\gamma_i \in \Gamma \cup \{\epsilon\}$ (resp. $\bar{\Gamma} \cup \{\bar{\epsilon}\}$), for all $1 \le i \le n$, $q \xrightarrow{w} q_n$ iff $q \xrightarrow{\gamma_1} q_1 \xrightarrow{\gamma_2} q_2 \cdots \xrightarrow{\gamma_n} q_n$ for $q, q_i \in Q$, $1 \le i \le n$. If $q \xrightarrow{w} q_n$ holds, we say that $q \xrightarrow{w} q_n$ is a path of $\mathcal{A}$. A configuration $\langle w_u, w_l \rangle$ is accepted by $\mathcal{A}$ iff there exists a path $p \xrightarrow{\bar{w}_u} q_1 \xrightarrow{w_l} q$ where $q \in F$ and $q_1 \in Q$. Let $L(\mathcal{A})$ be the set of configurations accepted by $\mathcal{A}$. Note that only paths reading first bar symbols from $\bar{\Gamma}$ (corresponding to the upper stack content), and then symbols from $\Gamma$ (corresponding to the lower stack content) are accepting.

**Example 1.** Let $A_1$ be a $\mathcal{P}$-automaton shown in **Fig.3**. The set of configurations $\langle ab^*d, b^*a \rangle$ is accepted by $A_1$ since there are paths reading first bar symbols and then symbols from $\Gamma$ accepting these configurations. However, the set $\langle ad, c^*b^*a \rangle$ is not accepted by $A_1$ since paths reading first bar symbols and then symbols from $\Gamma$ do not correspond to these configurations.

<figure><img src="image_4.png" /><figcaption>Fig. 3. The $\mathcal{P}$-automaton $A_1$</figcaption></figure>

Unfortunately, it was shown in [19] that the sets of predecessors and successors of regular sets of configurations are not necessarily regular:

**Theorem 1.** [19] There exists a UPDS $\mathcal{P}$ and a regular set of configurations $C$ s.t. $pre^*(C)$ (resp. $post^*(C)$) is not regular.
## 3 Computing the set of predecessors

In this section, we propose a semi-algorithm that attempts to compute the set of predecessors $pre^*$ of a UPDS. Our semi-algorithm is not guaranteed to terminate, in particular if the set of predecessors is not regular; but when it does, it gives a $\mathcal{P}$-automaton representing the exact set of predecessors. We show that our semi-algorithm terminates in several cases. We also show how by applying slight modifications to our semi-algorithm, we can compute $\mathcal{P}$-automata representing under and over-approximations of the set of predecessors.

### 3.1 A semi-algorithm

From now on, we fix a UPDS $\mathcal{P} = (\Gamma, \Delta)$ and a $\mathcal{P}$-automaton $\mathcal{A} = (Q, \Gamma, T, p, F)$ accepting a regular set of configurations $\mathcal{C}$ ($\mathcal{C} = L(\mathcal{A})$). We assume w.l.o.g. that $\mathcal{A}$ has no transitions leading to the initial state $p$, and that $Q = Q_{up} \cup Q_{low}$ ($p \in Q_{up}$ and $F \subseteq Q_{low}$) and $T = T_{up} \cup T_{inter} \cup T_{low}$ s.t. $T_{up} \subseteq Q_{up} \times \bar{\Gamma} \times Q_{up}$, $T_{inter} \subseteq Q_{up} \times \Gamma \times Q_{low}$ and $T_{low} \subseteq Q_{low} \times \Gamma \times Q_{low}$. This means that $\mathcal{A}$ has two parts: the upper stack part with only bar symbols from $\bar{\Gamma}$, represented by states $Q_{up}$ and transitions $T_{up}$, and the lower stack part with symbols from $\Gamma$, represented by states $Q_{low}$ and transitions $T_{low}$. These two parts are linked by transitions in $T_{inter}$ of the form $q_1 \xrightarrow{a} q_2$, for $q_1 \in Q_{up}$ and $q_2 \in Q_{low}$.

Our semi-algorithm attempts to compute a $\mathcal{P}$-automaton $\mathcal{A}_{pre^*}$ (with possibly an infinite number of states) representing $pre^*(\mathcal{C})$. The procedure follows the same idea as the one that computes predecessors for standard pushdown systems [14, 10]. It consists in adding iteratively new transitions to the automaton $\mathcal{A}$ according to saturation rules (reflecting the backward application of the transition rules in the system). Unlike [14, 10], new states need to be added during the saturation procedure, which can lead to non termination.

We define $\mathcal{A}_{pre^*}$ to be the $\mathcal{P}$-automaton $\mathcal{A}_{pre^*} = (Q', \Gamma, T', p, F)$, where $Q'$ and $T'$ are computed using the following saturation rules: initially, $Q' = Q$ and $T' = T$;

(α) If $a \leftrightarrow \epsilon$ is a pop rule, and there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{\overline{a}} q_2 \xrightarrow{w_l} q$ for $w_u \in \Gamma^*$ and $w_l \in \Gamma^*$, then add $q_1 \xrightarrow{a} q_2 \in T'$

(β) If $a \leftrightarrow bc$ is a push rule, and:

(β₁) if there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{b} q_2 \xrightarrow{c} q_3 \xrightarrow{w_l} q$ for $w_u \in \Gamma^+$ and $w_l \in \Gamma^*$, first add a new state $q_3^a \in Q'$, then add $q_3^a \xrightarrow{a} q_3 \in T'$ and $q_1 \xrightarrow{\tilde{\gamma}} q_3^a \in T'$, for every $\gamma \in \Gamma$.

(β₂) if there exists in $T'$ a path of the form $p \xrightarrow{b} q_1 \xrightarrow{c} q_2 \xrightarrow{w_l} q$ for $w_l \in \Gamma^*$, first add a new state $q_2^a \in Q'$, then add $p \xrightarrow{\tilde{\epsilon}} q_2^a \in T'$, $q_2^a \xrightarrow{a} q_2 \in T'$, and $p \xrightarrow{\tilde{\gamma}} q_2^a \in T'$ for every $\gamma \in \Gamma$.

(λ) If $a \leftrightarrow c$ is a switch rule and there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{c} q_2 \xrightarrow{w_l} q$, for $w_u \in \Gamma^*$, $w_l \in \Gamma^*$, then add $q_1 \xrightarrow{a} q_2 \in T'$.
Note that rules $(\beta_2)$ add states of the form $q^a$ to $Q'$. Let $Q_{push}$ be the set of these added states (i.e., $Q' = Q \cup Q_{push}$). This set of states may be unbounded. Thus, the procedure above is not guaranteed to terminate.

Let us explain the intuition behind these saturation rules. Let us consider first the saturation rule $(\alpha)$. Let $r_1 : a \leftrightarrow \epsilon \in \Delta$ be a pop rule. Consider a path in the automaton $\mathcal{A}_{pre^*}$ of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{\bar{a}} q_2 \xrightarrow{w_l} q$ where $q_1, q_2 \in Q'$ and $w_u, w_l \in \Gamma^*$. This path corresponds to the configuration $\langle w_u a, w_l \rangle$. By applying $r_1$ to the configuration $\langle w_u, aw_l \rangle$, we get that $\langle w_u, aw_l \rangle \stackrel{r_1}{\implies} \langle w_u a, w_l \rangle$. Thus, $\langle w_u, aw_l \rangle$ is a predecessor of $\langle w_u a, w_l \rangle$ and should be accepted by $\mathcal{A}_{pre^*}$. We achieve this by the saturation rule $(\alpha)$ that adds a new transition $q_1 \xrightarrow{a} q_2$ to $T'$ so that we have a new path $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{a} q_2 \xrightarrow{w_l} q$ which accepts the configuration $\langle w_u, aw_l \rangle$.

Let us consider the saturation rule $(\beta_1)$. Let $r_2 : a \leftrightarrow bc \in \Delta$ be a push rule. Consider a path in the automaton $\mathcal{A}_{pre^*}$ of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{b} q_2 \xrightarrow{c} q_3 \xrightarrow{w_l} q$ where $q_1, q_2, q_3 \in Q'$ and $w_u \in \Gamma^+$, $w_l \in \Gamma^*$. This path corresponds to the configuration $\langle w_u, bcw_l \rangle$. By applying $r_2$ to the configuration $\langle w_u \gamma, aw_l \rangle$ for $\gamma \in \Gamma$, we get that $\langle w_u \gamma, aw_l \rangle \stackrel{r_2}{\implies} \langle w_u, bcw_l \rangle$. $\langle w_u \gamma, aw_l \rangle$ is thus a predecessor of $\langle w_u, bcw_l \rangle$ and should be accepted by $\mathcal{A}_{pre^*}$. We achieve this by the saturation rule $(\beta_1)$ that adds a new state $q_3^a$ to $Q'$ and adds two new transitions $q_1 \xrightarrow{\bar{\gamma}} q_3^a$ and $q_3^a \xrightarrow{a} q_3$ to $T'$ so that we have the new path $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{\bar{\gamma}} q_3^a \xrightarrow{a} q_3 \xrightarrow{w_l} q$ which accepts $\langle w_u \gamma, aw_l \rangle$.

For the saturation rule $(\beta_2)$, let $r_2 : a \leftrightarrow bc \in \Delta$ be a push rule. Consider a path in the automaton $\mathcal{A}_{pre^*}$ of the form $p \xrightarrow{b} q_1 \xrightarrow{c} q_2 \xrightarrow{w_l} q$ where $q_1, q_2 \in Q'$ and $w_l \in \Gamma^*$. This path corresponds to the configuration $\langle \epsilon, bcw_l \rangle$. By applying $r_2$ to the configuration $\langle \gamma, aw_l \rangle$ or to the configuration $\langle \epsilon, aw_l \rangle$ for $\gamma \in \Gamma$ can be any symbol in the alphabet, we get that $\langle \gamma, aw_l \rangle \stackrel{r_2}{\implies} \langle \epsilon, bcw_l \rangle$ and $\langle \epsilon, aw_l \rangle \stackrel{r_2}{\implies} \langle \epsilon, bcw_l \rangle$. Thus, $\langle \gamma, aw_l \rangle$ and $\langle \epsilon, aw_l \rangle$ are both predecessors of $\langle \epsilon, bcw_l \rangle$ and should be accepted by $\mathcal{A}_{pre^*}$. We achieve this by the saturation rule $(\beta_2)$ that adds a new state $q_2^a$ to $Q'$ and adds the new transitions $p \xrightarrow{\bar{\gamma}} q_2^a$, $p \xrightarrow{\bar{\epsilon}} q_2^a$, and $q_2^a \xrightarrow{a} q_2$ to $T'$ so that we have the new paths $p \xrightarrow{\bar{\gamma}} q_2^a \xrightarrow{a} q_2 \xrightarrow{w_l} q$ and $p \xrightarrow{\bar{\epsilon}} q_2^a \xrightarrow{a} q_2 \xrightarrow{w_l} q$ that accept $\langle \gamma, aw_l \rangle$ and $\langle \epsilon, aw_l \rangle$, respectively.

Finally, consider the saturation rule $(\lambda)$. Let $r_3 : a \leftrightarrow c \in \Delta$ be a switch rule. Consider a path in the automaton $\mathcal{A}_{pre^*}$ of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{c} q_2 \xrightarrow{w_l} q$, for $q_1, q_2 \in Q'$ and $w_u, w_l \in \Gamma^*$. This path accepts the configuration $\langle w_u, cw_l \rangle$. By applying $r_3$ to the configuration $\langle w_u, aw_l \rangle$, we get that $\langle w_u, aw_l \rangle \stackrel{r_3}{\implies} \langle w_u, cw_l \rangle$. Thus, $\langle w_u, aw_l \rangle$ is a predecessor of $\langle w_u, cw_l \rangle$ and should be accepted by $\mathcal{A}_{pre^*}$. We achieve this by the saturation rule $(\lambda)$ that adds the new transition $q_1 \xrightarrow{a} q_2$ to $T'$ so that we have a new path $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{a} q_2 \xrightarrow{w_l} q$ which accepts $\langle w_u, aw_l \rangle$.
The above procedure does not always terminate, especially if $pre^*(C)$ is not regular. Fortunately, in several cases it terminates and gives the exact set of reachable configurations, as shown in Example 2. We can show that:

**Theorem 2.** $L(\mathcal{A}_{pre^*}) = pre^*(L(\mathcal{A}))$.

It follows that if the set of states $Q_{push}$ of $\mathcal{A}_{pre^*}$ is finite, then $pre^*(L(\mathcal{A}))$ is regular and can be effectively computed by the above procedure. To prove this theorem, we show these two directions:

**Lemma 1.** For every configuration $\langle w_u, w_l \rangle \in L(\mathcal{A})$, if there exist $w'_u, w'_l \in \Gamma^*$ such that $\langle w'_u, w'_l \rangle \Rightarrow^* \langle w_u, w_l \rangle$, then $p \xrightarrow{w'_u w'_l} q$ for a final state $q \in F$ of $\mathcal{A}_{pre^*}$.

We use $\to_i$ to denote the transition relation in the $\mathcal{P}$-automaton $\mathcal{A}_{pre^*}$ after adding $i$ new transitions. In particular, $\to_0$ is the transition relation of $\mathcal{A}$.

**Lemma 2.** If $p \xrightarrow{\overline{w_u w_l}}_i q$, then the following properties hold:

(a) if $q \in Q$, then there exist $w'_u, w'_l \in \Gamma^*$ such that $\langle w_u, w_l \rangle \Rightarrow^* \langle w'_u, w'_l \rangle$ and
$p \xrightarrow{\overline{w'_u w'_l}}_0 q$;

(b) if $q \in Q_{push}$, then there exists $w'_u \in \Gamma^*$ such that $\langle w_u, w_l \rangle \Rightarrow^* \langle w'_u, \epsilon \rangle$ and
$p \xrightarrow{\overline{w'_u}}_k q$ for $k \le i$ is the iteration on which $q$ is added to $Q_{push}$.

**Example 2.** Consider a $\mathcal{P}$-automaton $\mathcal{A}$ depicted on **Fig. 4** that recognizes the set of configurations $\langle a(b + c)^*, da^+c \rangle$ of a UPDS $\mathcal{P} = (\Gamma, \Delta)$, where $\Gamma = \{a, b, c, d\}$ and $\Delta$ is the set of rules shown on the left side of **Fig. 4**. We show in this example how our procedure terminates and computes the exact and regular reachability set. Let us first explain step by step how our semi-algorithm adds new transitions and new states.

1. Since $r_1$ is a pop rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{\bar{b}} q_1 \xrightarrow{d} q_2 \xrightarrow{a} q_3 \xrightarrow{c} q$; the saturation rule $(\alpha)$ adds the new transition $q_1 \xrightarrow{b} q_1$ to $T'$;

2. Since $r_3$ is a switch rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{b} q_1 \xrightarrow{d} q_2 \xrightarrow{a} q_3 \xrightarrow{c} q$; the saturation rule $(\lambda)$ adds the new transition $q_1 \xrightarrow{c} q_1$ to $T'$;

3. Since $r_2$ is a push rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{d} q_2 \xrightarrow{a} q_3 \xrightarrow{c} q$; the saturation rule $(\beta_1)$ adds a new state $q_3^b$ to $Q'$ and adds the new transition $q_1 \xrightarrow{\bar{\gamma}} q_3^b$ for any $\gamma \in \Gamma$ and another new transition $q_3^b \xrightarrow{b} q_3$ to $T'$;

4. Since $r_1$ is a pop rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{\bar{\gamma}} q_3^b \xrightarrow{b} q_3 \xrightarrow{c} q$ for $\gamma$ can be any symbol in $\Gamma$, let $\gamma = b$; the saturation rule $(\alpha)$ adds the new transition $q_1 \xrightarrow{b} q_3^b$ to $T'$;

5. Since $r_3$ is a switch rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{b} q_3^b \xrightarrow{b} q_3 \xrightarrow{c} q$; the saturation rule $(\lambda)$ adds the new transition $q_1 \xrightarrow{c} q_3^b$ to $T'$;

6. Since $r_4$ is a push rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{\bar{\gamma}} q_3^b \xrightarrow{c} q_3 \xrightarrow{a} q_3 \xrightarrow{c} q$; the saturation rule $(\beta_1)$ adds a new state $q_3^e$ to $Q'$ and adds the new transition $q_3^b \xrightarrow{\bar{\gamma}} q_3^e$ for any $\gamma \in \Gamma$ and another new transition $q_3^e \xrightarrow{e} q_3$ to $T'$;
7. Since $r_1$ is a pop rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{\bar{\gamma}} q_3^b \xrightarrow{\bar{e}} q_3^e \xrightarrow{c} q$ and $\gamma$ can be any symbol in $\Gamma$, let $\gamma = b$; the saturation rule $(\alpha)$ adds the new transition $q_3^b \xrightarrow{b} q_3^e$ to $T'$;

8. Since $r_3$ is a switch rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{\bar{\gamma}} q_3^b \xrightarrow{b} q_3^e \xrightarrow{e} q_3 \xrightarrow{c} q$; the saturation rule $(\lambda)$ adds the new transition $q_3^b \xrightarrow{e} q_3^e$ to $T'$;

9. Since $r_4$ is a push rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{\bar{\gamma}} q_3^b \xrightarrow{\bar{e}} q_3^e \xrightarrow{e} q_3 \xrightarrow{a} q_3 \xrightarrow{c} q$; since $q_3^e$ and the transition $q_3^e \xrightarrow{e} q_3$ already exists, the saturation rule $(\beta_1)$ adds the new transition $q_3^e \xrightarrow{\bar{\gamma}} q_3^e$ for any $\gamma \in \Gamma$ to $T'$;

10. Since $r_1$ is a pop rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{\bar{\gamma}} q_3^b \xrightarrow{\bar{e}} q_3^e \xrightarrow{e} q_3 \xrightarrow{c} q$ and $\gamma$ can be any symbol in $\Gamma$, let $\gamma = b$; the saturation rule $(\alpha)$ adds the new transition $q_3^e \xrightarrow{b} q_3^e$ to $T'$;

11. Since $r_3$ is a switch rule, and there exists a path $p \xrightarrow{\bar{a}} q_1 \xrightarrow{\bar{\gamma}} q_3^b \xrightarrow{\bar{e}} q_3^e \xrightarrow{b} q_3^e \xrightarrow{e} q_3 \xrightarrow{c} q$; the saturation rule $(\lambda)$ adds the new transition $q_3^e \xrightarrow{e} q_3^e$ to $T'$;

Since no new transition can be added, the semi-algorithm terminates. Thus, in this case, our procedure succeeds in computing the reachability set, and shows that it is regular. Note that despite the fact that there is an infinite number of configurations that should be added to compute $pre^*(L(\mathcal{A}))$, our construction terminates and produces the *exact* reachability set. Observe that the procedure adds loops. This allows to introduce regular *infinite* sets of configurations. Note also that in the computed automaton, bar symbols from $\bar{\Gamma}$ and symbols from $\Gamma$ are mixed. However, accepted paths have to read bar symbols first. Paths that consider symbols from $\Gamma$ before bar symbols are discarded and do not correspond to any valid configuration.

## 3.2 A sufficient condition for termination

In this section, we show that by imposing specific restrictions on the transition rules, our semi-algorithm is guaranteed to terminate.

**Definition 3.** A *UPDS* $\mathcal{P} = (\Gamma, \Delta)$ is called *push rule limited if for all push rules* $\gamma \mapsto \gamma_1\gamma_2 \in \Delta$, $\gamma, \gamma_1, \gamma_2 \in \Gamma$, *there does not exist* $w_1 \in \Gamma^*$ *such that* $\langle\epsilon, \gamma_1\gamma_2\rangle \Rightarrow^* \langle w_1, \epsilon\rangle$.

Intuitively, a UPDS is push rule limited if for every push rule $\gamma \mapsto \gamma_1\gamma_2$ in $\Delta$, $\gamma_1$ and $\gamma_2$ cannot be popped both.

**Theorem 3.** With a push rule limited UPDS, the semi-algorithm terminates.

*Proof.* Since the saturation rule $(\beta)$ adds new states in the form $q^a$ for $q \in Q'$ and push rule $a \mapsto bc$, where $a, b, c \in \Gamma$, the semi-algorithm may generate an infinite number of states of the form $q^{a^b \epsilon^{c^d \dots}}$. Let us see the different scenarios where this can happen. Consider a push rule $a \mapsto bc$ and consider a path of the initial $\mathcal{P}$-automaton $\mathcal{A}$ of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{b} q_2 \xrightarrow{c} q_3 \xrightarrow{w_l} q$
<figure><img src="image_5.png" /><figcaption>**Fig. 4.** The automaton $\mathcal{A}$ (above) and $\mathcal{A}_{pre^*}$ (below)</figcaption></figure>

Then, applying $(\beta)$, we add a new state $q_3^a$ and we get new paths $\rho$ of the form $\rho : p \xrightarrow{\bar{w}_u} q_1 \xrightarrow{\bar{\gamma}} q_3^a \xrightarrow{a} q_3 \xrightarrow{w_l} q$ for any $\gamma \in \Gamma$.

Now in order to have a new state of the form $q_3^{a^z}$ for a push rule in the form $z \leftrightarrow fg$, we need to have a path $\rho'$ of the form

$$ \rho' : p \xrightarrow{\bar{w}'_u} q_0 \xrightarrow{f} q_1 \xrightarrow{g} q_3^a \xrightarrow{w'_l} q $$

for $q_0 \in Q'$ and $w'_u, w'_l \in \Gamma^*$.

Let $w_u = w'_u f, \gamma = g$ so that $\rho$ can be rewritten as:

$$ p \xrightarrow{\bar{w}'_u} q_0 \xrightarrow{\bar{f}} q_1 \xrightarrow{\bar{g}} q_3^a \xrightarrow{a} q_3 \xrightarrow{w_l} q $$

for $q_0 \in Q$.

According to the saturation rules, the only possibility to obtain a path of the form $\rho'$ from $\rho$, i.e. the only possibility to have $q_0 \xrightarrow{f} q_1 \xrightarrow{g} q_3^a$ is if both $f$ and $g$ can be popped. Indeed, since $q_0 \xrightarrow{\bar{f}} q_1$ in $\rho$, then the saturation rule will add the transition $q_0 \xrightarrow{f} q_1$ to $T'$ only if $f$ can be popped. Moreover, since we have $q_1 \xrightarrow{\bar{g}} q_3^a$ in $\rho$, then the saturation rule will add the transition $q_1 \xrightarrow{g} q_3^a$ to $T'$ only if $g$ can be popped. In this case, we get a path of the form $\rho'$, and the saturation rule $(\beta)$ will add the transitions $q_1 \xrightarrow{\bar{\gamma}} q_3^{a^z}$ and $q_3^{a^z} \xrightarrow{\bar{z}} q_3^a$. Thus if either $f$ or $g$ cannot be popped or both $f$ and $g$ cannot be popped, we cannot have a path $\rho'$ and thus we can never add a state of the form $q_3^{a^z}$. Since the number of states of the form $q^a$ is finite, we can make sure we will add only a finite number of new states with a push rule limited UPDS and the semi-algorithm will terminate. $\square$
It follows that:

**Theorem 4.** Let $\mathcal{P}$ be a push rule limited UPDS, and let $\mathcal{C}$ be a regular set of configurations of $\mathcal{P}$. Then $\text{pre}^*(\mathcal{C})$ is regular and can be effectively computed by the procedure above.

### 3.3 Computing an over-approximation of the set of predecessors

By computing over-approximations of the set of predecessors, we can show that a program is safe. Indeed, let $C_{init}$ (resp. $C_{bad}$) be the set of initial (resp. bad) configurations of a program. Let $\mathcal{O}$ be an over-approximation of $\text{pre}^*(C_{bad})$, then if $C_{init} \cap \mathcal{O} = \emptyset$, we are sure that starting from the initial configurations $C_{init}$, the set of bad configurations $C_{bad}$ cannot be reached.

To compute such an over-approximation, we modify slightly our semi-algorithm

by collapsing all states of the form $q^{a^{b^{\ddots^{d}}}}$ into a single state $q^d$ (all these states have a $d$-transition to $q$). This leads to termination since only a finite number of states are added. More precisely, we compute an over-approximation of the set of predecessors as follows:

(α') If $a \leftrightarrow \epsilon$ is a pop rule, and there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{\bar{a}} q_2 \xrightarrow{\overline{w_l}} q$ for $w_u \in \Gamma^*$ and $w_l \in \Gamma^*$, then add $q_1 \xrightarrow{a} q_2$

(β') If $a \leftrightarrow bc$ is a push rule, and:

(β'_1) if there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{b} q_2 \xrightarrow{c} q_3 \xrightarrow{\overline{w_l}} q$ for $w_u \in \Gamma^+$ and $w_l \in \Gamma^*$,

(β'_{1,1}) if $q_3 \in Q$, first add a new state $q_3^a$, then add $q_3^a \xrightarrow{a} q_3 \in T'$ and $q_1 \xrightarrow{\tilde{\gamma}} q_3^a \in T'$, for every $\gamma \in \Gamma$

(β'_{1,2}) if $q_3 \in Q_{push}$, let $s \in Q$ s.t. $q_3 = s^d$. Then, first add a new state $s^a \in Q'$, then add $s^a \xrightarrow{a} q_3 \in T'$ and $q_1 \xrightarrow{\tilde{\gamma}} s^a \in T'$, for every $\gamma \in \Gamma$

(β'_2) if there exists in $T'$ a path of the form $p \xrightarrow{b} q_2 \xrightarrow{c} q_3 \xrightarrow{\overline{w_l}} q$ for $w_l \in \Gamma^*$,

(β'_{2,1}) if $q_3 \in Q$, first add a new state $q_3^a$, then add $q_3^a \xrightarrow{a} q_3 \in T'$, $q_1 \xrightarrow{\bar{\epsilon}} q_3^a \in T'$, and $q_1 \xrightarrow{\tilde{\gamma}} q_3^a \in T'$, for every $\gamma \in \Gamma$

(β'_{2,2}) if $q_3 \in Q_{push}$, let $s \in Q$ s.t. $q_3 = s^d$. Then, first add a new state $s^a \in Q'$, then add $s^a \xrightarrow{a} q_3 \in T'$, $q_1 \xrightarrow{\bar{\epsilon}} s^a \in T'$, and $q_1 \xrightarrow{\tilde{\gamma}} s^a \in T'$ for every $\gamma \in \Gamma$.

(λ') If $a \leftrightarrow c$ is a switch rule and there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_1 \xrightarrow{c} q_2 \xrightarrow{\overline{w_l}} q$ for $w_u \in \Gamma^*, w_l \in \Gamma^*$, then add $q_1 \xrightarrow{a} q_2 \in T'$

### 3.4 Computing an under-approximation of the set of predecessors

By computing under-approximations of the set of predecessors, we can discover errors. Indeed, let $C_{init}$ (resp. $C_{bad}$) be the set of initial (resp. bad) configurations of a program. Let $\mathcal{U}$ be an under-approximation of $\text{pre}^*(C_{bad})$, then if $C_{init} \cap \mathcal{U} \neq \emptyset$, we are sure that starting from the initial configurations $C_{init}$, the set of bad
configurations $C_{bad}$ can be reached. We can compute an under-approximation of
the set of predecessors with our semi-algorithm by bounding the number of new
added states. We can also apply a kind of CEGAR (Counter Example Guided
Abstraction Refinement) [13] schema by increasing the bound at each CEGAR
round.

4 Computing the set of successors

In this section, we provide a semi-algorithm that attempts to compute the set of successors *post*\* of a UPDS. This semi-algorithm is not guaranteed to terminate, especially if the set of successors is not regular. In case of termination, it gives a *P*-automaton representing the *exact* set of successors. We show that our semi-algorithm terminates in multiple cases. Moreover, we adjust it in order to compute *P*-automata representing over and under-approximations of the set of successors.

Consider the UPDS $\mathcal{P} = (\Gamma, \Delta)$ and the $\mathcal{P}$-automaton $\mathcal{A} = (Q, \Gamma, T, p, F)$ accepting the regular set of configurations $C (C = L(\mathcal{A}))$ as defined in Section 3.1. Our semi-algorithm tries to compute a (possibly infinite state) $\mathcal{P}$-automaton $\mathcal{A}_{post^*}$ representing $post^*(C)$. The procedure follows the same idea as the one that computes successors for standard pushdown systems [14]. As previously, it consists in adding iteratively new transitions to the automaton $\mathcal{A}$ according to saturation rules (reflecting the forward application of the transition rules in the system). Unlike [14], new states need to be added during the saturation procedure, which can lead to non termination.

We define $\mathcal{A}_{post^*}$ to be the $\mathcal{P}$-automaton $\mathcal{A}_{post^*} = (Q', \Gamma, T', p, F)$, where $Q'$ and $T'$ are computed using the following saturation rules: initially, $Q' = Q$ and $T' = T$;

(α) If $r_1 : a \to \epsilon$ is a pop rule, and:

(α₁) if there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_0 \xrightarrow{\bar{\gamma}} q_1 \xrightarrow{a} q_2 \xrightarrow{w_l} q$ for $w_u, w_l \in \Gamma^*, \gamma \in \Gamma$, first add a new state $q_2^{r_1} \in Q'$, then add $q_0 \xrightarrow{\bar{\gamma}} q_2^{r_1} \in T'$ and $q_2^{r_1} \xrightarrow{\bar{a}} q_2 \in T'$

(α₂) if there exists in $T'$ a path of the form $p \xrightarrow{a} q_1 \xrightarrow{w_l} q$ for $w_l \in \Gamma^*$, first add a new state $q_1^{r_1} \in Q'$, then add $p \xrightarrow{\bar{\epsilon}} q_1^{r_1} \in T'$ and $q_1^{r_1} \xrightarrow{\bar{a}} q_1 \in T'$

(β) If $r_2 : a \to bc$ is a push rule, and:

(β₁) if there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_0 \xrightarrow{\bar{\gamma}} q_1 \xrightarrow{a} q_2 \xrightarrow{w_l} q$ for $w_u, w_l \in \Gamma^*, \gamma \in \Gamma$, first add a new state $q_2^{r_2} \in Q'$, then add $q_0 \xrightarrow{b} q_2^{r_2} \in T'$ and $q_2^{r_2} \xrightarrow{c} q_2 \in T'$

(β₂) if there exists in $T'$ a path of the form $p \xrightarrow{a} q_1 \xrightarrow{w_l} q$ for $w_l \in \Gamma^*$, first add a new state $q_1^{r_2} \in Q'$, then add $p \xrightarrow{b} q_1^{r_2} \in T'$ and $q_1^{r_2} \xrightarrow{c} q_1 \in T'$

(λ) If $r_3 : a \to c$ is a switch rule, and:

(λ₁) if there exists in $T'$ a path of the form $p \xrightarrow{\overline{w_u}} q_0 \xrightarrow{\bar{\gamma}} q_1 \xrightarrow{a} q_2 \xrightarrow{w_l} q$ for $w_u, w_l \in \Gamma^*, \gamma \in \Gamma$, first add a new state $q_2^{r_3} \in Q'$, then add $q_0 \xrightarrow{\bar{\gamma}} q_2^{r_3} \in T'$ and $q_2^{r_3} \xrightarrow{c} q_2 \in T'$
($\lambda_2$) if there exists in $T'$ a path of the form $p \xrightarrow{a} q_1 \xrightarrow{w_l} q$ for $w_l \in \Gamma^*$, first
add a new state $q_1^{r_3} \in Q'$, then add $p \xrightarrow{\bar{\epsilon}} q_1^{r_3} \in T'$ and $q_1^{c} \xrightarrow{q_1} q_1 \in T'$

The intuitions behind these rules are similar to the ones of the pre* procedure.
We can show that:

**Theorem 5.** $L(\mathcal{A}_{post^*}) = post^*(L(\mathcal{A}))$.

It follows that if the set of states $Q'$ of $\mathcal{A}_{post^*}$ is finite, then $post^*(L(\mathcal{A}))$ is
regular and can be effectively computed by the above procedure.

**Definition 4.** A *UPDS* $\mathcal{P} = (\Gamma, \Delta)$ is called *non-repeating head* if for any $\gamma \in \Gamma$, there does not exist $w_u, w_l, w_u', w_l' \in \Gamma^*$ s.t. $\langle w_u, \gamma w_l \rangle \Rightarrow^* \langle w_u', \gamma w_l' \rangle$.

Intuitively, a UPDS is non-repeating head if for every configuration $\langle w_u, \gamma w_l \rangle$
with $\gamma$ on the top of the stack, we cannot reach another configuration $\langle w_u', \gamma w_l' \rangle$
with the same $\gamma$ on the top of the stack. Since rules of the UPDS depend on the
top of the stack, this means a UPDS rule can only be applied once in a path.

Therefore, the above procedure cannot add states of the form $q_1^{r_1} q_2^{r_2} \cdots q_{r_1}^{r_3} \cdots r_1$ where a
rule $r_1$ appears twice. Thus, only a finite number of states can be added. Hence,
we can show that:

**Theorem 6.** With a non-repeating head UPDS, the semi-algorithm terminates.

It follows that:

**Theorem 7.** Let $\mathcal{P}$ be a non-repeating head UPDS, and let $\mathcal{C}$ be a regular set of configurations of $\mathcal{P}$. Then $post^*(\mathcal{C})$ is regular and can be effectively computed by the procedure above.

**Computing under and over-approximations of the set of successors.**

As previously, by bounding the number of states of the above procedure, we
obtain an under-approximation of the reachability set. Moreover, by collapsing

all states of the form $q_1^{r_1} q_2^{r_2} \cdots q_{r_1}^{r_m} \cdots r_m$ into a single state $q^{r_m}$, we compute an over-approximation of the set of successors.

# 5 Applications

Our results have several applications in binary code analysis. We present in this
section some of these applications.
## 5.1 Stack Overflow Detection

Stack overflow refers to a situation where a program's call stack exceeds the memory allocated by the system. If we model the code under analysis using a UPDS, our results can be used to detect whether the program has a stack overflow error or not as follows. Let $C = \Gamma^m \times L$ be the set of initial configurations, where $\Gamma \notin C$ denotes a special upper stack symbol that does not appear in any rule in $\Delta$, $m$ is the maximal authorized size of the stack, and $L \subseteq \Gamma^*$ is a regular language representing the initial set of configurations of the lower stack. If the top stack symbol $\Gamma$ is overwritten, this means a stack overflow occured. Let $\mathcal{X} = \Gamma^* \times \Gamma^*$ be the set of configurations which represents the stack overflow error. If the intersection of $C$ with an under-approximation of $\text{pre}^*(\mathcal{X})$ is not empty, then we know a stack overflow error occured. Moreover, if the intersection of $\mathcal{X}$ with an over-approximation of $\text{post}^*(C)$ is empty, then we are sure a stack overflow error will not occur in the program.

## 5.2 Reading the upper stack

Consider the program in Fig.5. We can see that the register *eax* is assigned the value stored in *sp* − 8 (which is in the upper stack), and then compared with the value *a*. If the two are equal, the program jumps to an unsafe state. With a simple PDS model, it is not possible to determine what is the value stored in *sp* − 8, since it is above the stack. This becomes possible using our UPDS model. Indeed, let $\mathcal{X} = \Gamma^*a\Gamma \times \Gamma^*$ be the set of forbidden configurations, and let *C* be the set of initial configurations of the program. If the intersection of an underapproximation of $\text{pre}^*(\mathcal{X})$ with *C* is not empty, then the program is unsafe, whereas if the intersection of an over-approximation of $\text{post}^*(C)$ with $\mathcal{X}$ is empty, then we are sure the program is safe.

<figure><img src="image_6.png" /><figcaption>Fig. 5. Example of a program reading the upper stack</figcaption></figure>

## 5.3 Changing the stack pointer

Certain malicious instructions can deliberately manipulate the stack pointer to alter the starting point of the stack. For instance, an instruction such as **mov sp**, **sp-4** effectively shifts the stack pointer backwards, enabling access to previously popped data. This behavior may be exploited to retrieve stale or sensitive information that should have been discarded, potentially leading to security vulnerabilities.
<figure><img src="image_7.png" /><figcaption>**Fig. 6.** The configuration before the instruction executes (Left) and the configuration after the instruction executes (Right)</figcaption></figure>

If we model the program as a UPDS, we can use our algorithms to compute (approximations of) the reachability sets, which will allow us to determine (an approximation of) the content of the new stack after the stack pointer changes.

## 5.4 Stack String Detection

Stack String is a technique that is widely used by malware writers in order to hide some strings so that they cannot be discovered by classic static analyzers and malware detectors. Typically, these strings are names of API functions calls that are known to cause malicious behaviors. For example, the Email Worm Avron calls the API function **GetModuleHandleA** with 0 as its parameter in order to get the entry address of its own executable so that later, it can infect other files by copying this executable into them. To detect such malicious behavior, malware detectors look for the string corresponding to the name of the API function **GetModuleHandleA**. If this string 'GetModuleHandleA' is stored on the stack, a malware detector can easily detect its presence. However, a worm writer can easily escape the detection by putting the string letter by letter into the memory region above the stack (i.e., the upper stack), which is typically not scanned by detectors. The instruction can then be executed by manipulating the stack pointer in order to reconstruct the API function's name from the upper stack. If we model the program as a UPDS, we can verify whether the program will hide strings corresponding to malware related API functions on the memory region above the stack. For example, if we are looking for the string GetModuleHandleA, then, let $C$ be the set of initial configurations of the program. Let $\mathcal{X} = \langle \Gamma^* GetModuleHandleA \Gamma^*, \Gamma^* \rangle$ be the set of forbidden configurations (i.e., configurations containing GetModuleHandleA in the upper stack. If the intersection of $C$ with an under-approximation of $pre^*(\mathcal{X})$ is not empty, then the program will hide the string, whereas if the intersection of an over-approximation of $post^*(C)$ with $\mathcal{X}$ is empty, then we are sure the program will not hide the string under consideration.

<figure><img src="image_8.png" /><figcaption>**Fig. 7.** The string GetModuleHandleA is hidden in the upper stack</figcaption></figure>
## 5.5 Return Address Anomaly Detection

In binary code execution, the return address is pushed onto the stack and then, popped during the function return. Some worms can overwrite some return addresses in the stack, so that the function returns to the malicious code; in order to make the program execute this malicious code. In order to determine whether the return address has been overwritten by any other data or not, we can check each return address pushed onto the stack to verify whether it is subsequently popped and stored in the memory region above the stack. To do this, we can model the program as a UPDS and for each return address, we use a special symbol like $. Let the set of initial configurations be $C = \langle \Gamma^*, \Gamma^*\$\Gamma^* \rangle$ where the return address is still on the stack. Let $\mathcal{X} = \langle \Gamma^*\$\Gamma^*, \Gamma^* \rangle$ be the set of configurations where $\$$ is correctly popped. If the intersection of $\mathcal{X}$ with an over-approximation of $post^*(C)$ is empty, we deduce that $\$$ is not correctly popped and a Return Address Anomaly has occurred.

## 5.6 Shellcode Detection

A shellcode is a piece of code designed to be injected in the host program and executed via a vulnerability like stack overflow. It is typically used to gain control of the system or perform malicious actions specified by the attacker. Usually, shellcode relies on vulnerabilities like stack overflow. Thus, the procedure that allows the detection of stack overflow described in section 5.1 can help checking the presence of a shellcode.

## References

1. ABDULLA, P. A., ATIG, M. F., REZINE, O., AND STENMAN, J. Budget-bounded model-checking pushdown systems. *Form. Methods Syst. Des.* 45, 2 (Oct. 2014), 273–301.

2. ALGLAVE, J., KROENING, D., NIMAL, V., AND TAUTSCHNIG, M. Software verification for weak memory via program transformation. In *Programming Languages and Systems* (Berlin, Heidelberg, 2013), M. Felleisen and P. Gardner, Eds., Springer Berlin Heidelberg, pp. 512–532.

3. ANDERSON, P. Codesurfer/path inspector. In *20th IEEE International Conference on Software Maintenance, 2004. Proceedings*. (2004), pp. 508–.

4. ATIG, M. F. Global Model Checking of Ordered Multi-Pushdown Systems. In *IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010)* (Dagstuhl, Germany, 2010), K. Lodaya and M. Mahajan, Eds., vol. 8 of *Leibniz International Proceedings in Informatics (LIPIcs)*, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, pp. 216–227.

5. ATIG, M. F., BOUAJJANI, A., KUMAR, K., AND SAIVASAN, P. On bounded reachability analysis of shared memory systems. *Leibniz International Proceedings in Informatics, LIPIcs* 29 (12 2014), 611–623.

6. BALAKRISHNAN, G., GRUIAN, R., REPS, T., AND TEITELBAUM, T. Codesurfer/x86—a platform for analyzing x86 executables. In *Compiler Construction* (Berlin, Heidelberg, 2005), R. Bodik, Ed., Springer Berlin Heidelberg, pp. 250–254.
7. BALAKRISHNAN, G., AND REPS, T. Analyzing memory accesses in x86 executables. In *Compiler Construction* (Berlin, Heidelberg, 2004), E. Duesterwald, Ed., Springer Berlin Heidelberg, pp. 5–23.

8. BALAKRISHNAN, G., AND REPS, T. Wysinwyx: What you see is not what you execute. *ACM Trans. Program. Lang. Syst.* 32, 6 (Aug. 2010).

9. BALAKRISHNAN, G., REPS, T., KIDD, N., LAL, A., LIM, J., MELSKI, D., GRUIAN, R., YONG, S., CHEN, C. H., AND TEITELBAUM, T. Model checking x86 executables with codesurfer/x86 and wpds++. In *Computer Aided Verification* (Berlin, Heidelberg, 2005), K. Etessami and S. K. Rajamani, Eds., Springer Berlin Heidelberg, pp. 158–163.

10. BOUAJJANI, A., ESPARZA, J., AND MALER, O. Reachability analysis of pushdown automata: Application to model-checking. In *CONCUR '97: Concurrency Theory* (Berlin, Heidelberg, 1997), A. Mazurkiewicz and J. Winkowski, Eds., Springer Berlin Heidelberg, pp. 135–150.

11. CARAYOL, A., AND HAGUE, M. Saturation algorithms for model-checking pushdown systems. *arXiv preprint arXiv:1405.5593* (2014).

12. CAROTENUTO, D., MURANO, A., AND PERON, A. 2-visibly pushdown automata. In *International Conference on Developments in Language Theory* (2007), Springer, pp. 132–144.

13. CLARKE, E., GRUMBERG, O., JHA, S., LU, Y., AND VEITH, H. Counterexample-guided abstraction refinement for symbolic model checking. *J. ACM* 50, 5 (Sept. 2003), 752–794.

14. ESPARZA, J., HANSEL, D., ROSSMANITH, P., AND SCHWOON, S. Efficient algorithms for model checking pushdown systems. In *International Conference on Computer Aided Verification* (2000).

15. LA TORRE, S., MADHUSUDAN, P., AND PARLATO, G. A robust class of context-sensitive languages. In *Proceedings - 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007* (2007), Proceedings - Symposium on Logic in Computer Science, pp. 161–170. 22nd Annual IEEE Symposium on Logic in Computer Science, LICS 2007; Conference date: 10-07-2007 Through 14-07-2007.

16. LA TORRE, S., MADHUSUDAN, P., AND PARLATO, G. Reducing context-bounded concurrent reachability to sequential reachability. In *Computer Aided Verification* (Berlin, Heidelberg, 2009), A. Bouajjani and O. Maler, Eds., Springer Berlin Heidelberg, pp. 477–492.

17. LA TORRE, S., AND NAPOLI, M. Reachability of multistack pushdown systems with scope-bounded matching relations. In *CONCUR 2011 – Concurrency Theory* (Berlin, Heidelberg, 2011), J.-P. Katoen and B. König, Eds., Springer Berlin Heidelberg, pp. 203–218.

18. LANG, M. Resource-bounded reachability on pushdown systems. *Master's thesis*, RWTH Aachen University (2011).

19. POMMELLET, A., DIAZ, M., AND TOUILI, T. *Reachability Analysis of Pushdown Systems with an Upper Stack*. Springer International Publishing, 2017, p. 447–459.

20. REPS, T., LAL, A., AND KIDD, N. Program analysis using weighted pushdown systems. In *FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science* (Berlin, Heidelberg, 2007), V. Arvind and S. Prasad, Eds., Springer Berlin Heidelberg, pp. 23–51.

21. SETH, A. Global reachability in bounded phase multi-stack pushdown systems. In *International Conference on Computer Aided Verification* (2010).

22. SHU, L., SHI, J., YE, X., JIANG, N., AND LI, Y. A new parallel approach for reachability analysis of pushdown models. In *Proceedings of the 2017 International Conference on Computer Aided Verification and Design* (Barcelona, Spain, 2017), J. D. P. M. P. and L. C. P. P. (Eds.), pp. 111–120.
tional Conference on Management Engineering, Software Engineering and Service Sciences (2017), pp. 113–118.

23. SONG, F. On pushdown systems model checking : application to malware detection and software model-checking. PhD thesis, 2013. Thèse de doctorat dirigée par Touili, Tayssir Informatique Paris 7 2013.

24. SONG, F., AND TOUILI, T. Efficient malware detection using model-checking. In *FM 2012: Formal Methods* (Berlin, Heidelberg, 2012), D. Giannakopoulou and D. Méry, Eds., Springer Berlin Heidelberg, pp. 418–433.

25. SONG, F., AND TOUILI, T. Pushdown model checking for malware detection. In *Tools and Algorithms for the Construction and Analysis of Systems* (Berlin, Heidelberg, 2012), C. Flanagan and B. König, Eds., Springer Berlin Heidelberg, pp. 110–125.

26. SONG, F., AND TOUILI, T. Ltl model-checking for malware detection. In *Tools and Algorithms for the Construction and Analysis of Systems* (Berlin, Heidelberg, 2013), N. Piterman and S. A. Smolka, Eds., Springer Berlin Heidelberg, pp. 416–431.

27. SONG, F., AND TOUILI, T. Pommade: pushdown model-checking for malware detection. In *Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering* (New York, NY, USA, 2013), ESEC/FSE 2013, Association for Computing Machinery, p. 607–610.

28. TOUILI, T., AND YE, X. Ltl model checking of self modifying code, 2019.

29. TOUILI, T., AND YE, X. Smodic: A model checker for self-modifying code. In *Proceedings of the 17th International Conference on Availability, Reliability and Security* (New York, NY, USA, 2022), ARES '22, Association for Computing Machinery.

30. TOUILI, T., AND YE, X. Reachability analysis of self modifying code. *International Journal of Foundations of Computer Science* 34, 05 (2023), 507–536.