# LTL Model Checking of Concurrent Self Modifying Code ⋆

Tayssir Touili, Olzhas Zhangeldinov

► To cite this version:

Tayssir Touili, Olzhas Zhangeldinov. LTL Model Checking of Concurrent Self Modifying Code ⋆. 29th International Conference on Engineering of Complex Computer Systems, Jul 2025, Hang Zhou, China. hal-05288796

HAL Id: hal-05288796

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

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.

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

Distributed under a Creative Commons Attribution 4.0 International License
# LTL Model Checking of Concurrent Self-Modifying Code\*

Tayssir Touili and Olzhas Zhangeldinov

IRIF, CNRS, and University Paris Cité

**Abstract.** We consider the LTL model-checking problem of concurrent self modifying code, i.e., concurrent code that has the ability to modify its own instructions during execution time. This style of code is frequently utilized by malware developers to make their malicious code hard to detect. To model such programs, we consider Self-Modifying Dynamic Pushdown Networks (SM-DPN). A SM-DPN is a network of Self-Modifying Pushdown processes, where each process has the ability to modify its current set of rules and to spawn new processes during execution time. We consider model checking SM-DPNs against single indexed LTL formulas, i.e., conjunctions of separate LTL formulas on each single process. This problem is non trivial since the number of spawned processes in a given run can be infinite. Our approach is based on computing finite automata representing the set of configurations from which the SM-DPN has a run that satisfies the single-indexed LTL formula. We implemented our techniques in a tool and obtained promising results. In particular, our tool was able to detect concurrent, self-modifying malware.

# 1 Introduction

Most of programs implement concurrent routines for efficiency. However, analysis of concurrent programs is a notoriously hard challenge. Therefore, significant efforts were made in the direction of automatic verification of concurrent programs [8, 13, 17, 19–21, 25].

On the other hand, self-modifying code is a code that modifies its own instructions during the execution time. This technique is widely used by packers to decrease the size of a program and by malware developers to confuse anti-virus software and make their malware hard to detect. The problem of analysing self-modifying code was approached by more recent studies [7, 9, 19, 26].

This paper focuses on analysing programs that are both *concurrent* and *self-modifying*. Indeed, modern malware employs concurrency for parallel execution of different tasks and contains self-modifying code to stay undetected for as long as possible.

Self-modifying behaviour of a program is achieved by writing to the executable region of the binary, which is an array of memory locations from where

<footnote>\* This work was partially funded by the french ANR grant Defmal “ANR-22-PECY-0007”</footnote>
<table><caption>Listing 1.1. Binary code with a self-modifying instruction.</caption><thead><tr><th>#</th><th>Address</th><th>Bytecode</th><th>Assembly</th></tr></thead><tbody><tr><td>0x04</td><td></td><td>0x31c0</td><td>xor eax, eax</td></tr><tr><td>0x06</td><td></td><td>0xb001</td><td>mov al, 1</td></tr><tr><td>0x08</td><td></td><td>0xbb80cd02b0</td><td>mov ebx, 0xb002cd80</td></tr><tr><td>0x0d</td><td></td><td>0x891d04000000</td><td>mov [0x04], ebx</td></tr><tr><td>0x13</td><td></td><td>0xebe7</td><td>jmp 0x04</td></tr></tbody></table>

<table><caption>Listing 1.2. Binary code after executing a self-modifying instruction.</caption><thead><tr><th>#</th><th>Address</th><th>Assembly</th></tr></thead><tbody><tr><td>0x04</td><td></td><td>xor eax, eax # - executing --> mov al, 0x2<br/> # mov [0x04], ebx</td></tr><tr><td>0x06</td><td></td><td>mov al, 1 # - executing --> int 0x80<br/> # mov [0x04], ebx</td></tr><tr><td>0x08</td><td></td><td>mov ebx, 0xb002cd80</td></tr><tr><td>0x0d</td><td></td><td>mov [0x04], ebx</td></tr><tr><td>0x13</td><td></td><td>jmp 0x04</td></tr></tbody></table>

a computer reads instructions to execute. Self-modification can be implemented using different techniques. For example, let us consider a self-modifying concurrent binary code of a Linux program running on a CPU with x86 architecture. Programs for this architecture mostly use `mov` instructions to write data into memory, including the memory of executable instructions. A portion of the program's assembly is demonstrated in Listing 1.1. The first column denotes relative addresses of instructions. The second column contains bytes stored at that address, and the third column is the corresponding assembly code for the binary code. `eax` and `ebx` are CPU registers, and `al` points to the lowest byte of `eax`.

Let us explain why this code is self-modifying and concurrent. First, a process starts executing the program at the address `0x04` and reads bytes `0x31c0` stored at this location. Bytecode `0x31c0` corresponds to the instruction `xor eax, eax`, which means the process sets `eax` to 0. This instruction is two bytes long, so the process reads the next instruction from the address `0x06`. This address contains bytes `0xb001`, which is the bytecode of the instruction `mov al, 0x1`, which sets the lowest byte of `eax` to `0x1`. Then, the process executes the instruction `mov ebx, 0xb002cd80`, which corresponds to the bytecode `0xbb80cd02b0` stored at the address `0x08`. This sets `ebx` to `0xb002cd80`. Next, the process executes the instruction stored at the address `0x0d`. This instruction is `mov [0x04], ebx` and it stores the value of `ebx` (previously set to `0xb002cd80`) to the address `0x04`. This changes the instructions stored at address `0x04`. Since `0xb002cd80` is the binary code for instructions `mov al, 0x2` and `int, 0x80`, the instructions at the addresses `0x04` and `0x06` will be replaced by these two instructions. Therefore, `mov [0x04], ebx` is a self-modifying instruction. The code of the program after self-modification occurs is presented in Listing 1.2. The next instruction the process reads will be `jmp 0x04` (corresponding to the bytecode `0xebe7` contained at the location `0x13`), which will make the process jump to the address `0x04`. As explained, this address now contains a modified instruction with the bytecode `0 ROAD80`. The new assembly is `mov al, 0x2`, which sets `eax` to 2 (remember that
we set higher bytes of `eax` to 0 with `xor eax, eax`). Then, the process will execute the modified instruction at the address `0x06` with the new bytecode `0xcd80`, which corresponds to the assembly `int, 0x80`. This instruction tells Linux kernel to execute a system function with the function code stored in `eax`. The function code `0x2` corresponds to the kernel's `fork` function, which spawns a copy of the current process. Since the previous instruction sets `eax` to `0x2`, Linux kernel executes the `fork` function, making this program also concurrent.

<figure><img src="image_2.png" /><figcaption>Fig. 1. Naive and accurate CFGs of code from Listing 1.1.</figcaption></figure>

You can see that if we analyse this program blindly, using the instructions of Listing 1.1, without taking into account the self-modifying nature of the instruction `mov [0x04], ebx`, then we will obtain the Control Flow Graph (CFG) shown in Figure 1(a). However in reality, the program will spawn parallel processes indefinitely. This is clear if we look at the more accurate CFG in Figure 1(b). This is one of the techniques malware developers use to obscure the real behaviour of the malware from antivirus software. Therefore, it is necessary to take into account the self-modifying nature of the code for an accurate analysis.

The aim of this paper is to provide an efficient algorithm for model checking such self-modifying and concurrent code. To analyse such kind of programs, we need an abstract model suitable for both self-modifications and concurrency. Pushdown System (PDS) was shown to be a natural abstraction for sequential programs [14]. To deal with concurrency, Dynamic Pushdown Networks (DPNs) were proposed to model how a program can spawn parallel processes [8]. A DPN is a network of pushdown systems where each PDS is able to spawn new processes controlled by other PDSs. On the other hand, to model programs with self-modifying instructions, authors of [26] proposed Self-Modifying Pushdown Systems (SM-PDS). Intuitively, SM-PDS is a PDS with the ability to modify its set of rules during runtime. To model both concurrent and self-modifying programs, a previous work [19] introduced Self-Modifying Dynamic Pushdown Networks (SM-DPNs) as a network of self-modifying pushdown systems. [19] proposed an efficient algorithm for reachability analysis of SM-DPNs. In this work,
we go one step further and propose an efficient LTL model checking algorithm for SM-DPNs.

Model checking concurrent programs imposes additional challenges. In fact, model checking LTL formulas that reason about two concurrent processes is undecidable [16], even in the absence of thread creation. To overcome this problem, we consider single-indexed LTL formulas of the form $f = \bigwedge_i f_i$, such that $f_i$ is an LTL formula over process $i$. This problem of single-indexed LTL model checking of DPNs was tackled by [25], however, this work does not take into account self-modification of programs.

In this paper, we go one step further and consider LTL model checking of Self-Modifying Dynamic Pushdown Networks (SM-DPNs). Since SM-DPNs are equivalent to standard DPNs, we could translate the SM-DPN into a DPN, and then use the LTL model checking algorithm of [25]. But, as shown by our experiments in Section 4, this approach is not efficient. Therefore, we propose a *direct* and *efficient* model checking algorithm for SM-DPNs against single-indexed LTL formulas. To this aim, we first construct an automaton $A_i$ for each sequential process $i$, such that $A_i$ accepts a configuration of the process $i$ if it has a run that satisfies the corresponding LTL formula $f_i$. During the construction of $A_i$, to tackle the self-modifying instructions, we keep track of the current *phase* of the process $i$ (the current set of the transitions of the process). $A_i$ also keeps track of the spawned processes during the execution because we need to check that every spawned process $j$ satisfies the formula $f_j$ as well. Then, we use all of the obtained automata to compute the largest set of processes $D_{fp}$, such that every process $i$ in $D_{fp}$ satisfies the LTL formula $f_i$, and does not spawn a process $j$ that violates the formula $f_j$ ($j \ge 0$). Then, we check that every initial process satisfies the LTL formula and spawns only processes from $D_{fp}$. Our experiments show that our direct approach is much more efficient than model checking an equivalent DPN using the approach in [25]. Moreover, we show the applicability of our approach for malware detection.

**Related Works.** Model checking of sequential binaries has been extensively studied in [4, 5, 16, 24]. However, these studies do not consider neither concurrency of programs, nor self-modifying instructions.

To solve the problem of model checking concurrent programs, different models were proposed. Some studies use Dynamic Pushdown Network (DPN) model [8, 20, 25] and its extensions [13, 19]. Other studies [17, 21, 22] performed model checking on networks of pushdown systems. However, these works do not consider self-modifying code.

To analyse self-modifying programs, several dynamic analysis approaches were proposed [11, 28], which imply executing the binary in a debugger and observing the behaviour of the program. However, these techniques do not allow to analyse every possible behaviour of the program. Static analysis of self-modifying code was proposed in, for example, [7, 9, 12]. However, [9] needs extra invariant annotations, [12] can deal with only packing and unpacking of binaries. As for [7], it proposes an abstract representation without a specific approach to automated analysis. Another model to represent self-modifying code is State-
Enhanced Control Flow Graph (SE-CFG) [3]. Reachability analysis of binaries with self-modifying instructions was also proposed by [6]. However, both of these studies [3, 6] do not take into account the stack of the program, and thus, do not provide an accurate enough model of execution. Self-modifying pushdown systems (SM-PDS) were successfully used for model checking self-modifying programs [26]. However, this work does not support concurrency.

As far as we know, the only work that considers both concurrent and self-modifying programs is [19], where the SM-DPN model was proposed. But, [19] considers only reachability analysis. In this paper, we go one step further and propose an efficient LTL model checking of SM-DPNs. Moreover, we extend the SM-DPN model to allow modelling programs when an instruction can modify several instructions (not only one as in [19]).

**Outline.** Section 2 introduces our SM-DPN model. Section 3 describes the proposed algorithm for efficient model checking SM-DPNs. Section 4 provides results of practical experiments conducted using the proposed LTL model checking. For lack of space, proofs are omitted. They can be found in the full version of the paper [27].

# 2 Preliminaries

In this section, we introduce Self-Modifying Pushdown Networks (SM-DPNs).

## 2.1 Self-Modifying Pushdown Network

A *Self-Modifying Dynamic Pushdown Network* (SM-DPN) is an extension of standard Pushdown Systems (PDS) that models programs that can spawn parallel processes and can change their instruction set in real-time. SM-DPN consists of several *Self-Modifying Dynamic Pushdown Systems* (SM-DPDS) each modelling a single sequential process. Formally:

**Definition 1.** A *Self-Modifying Dynamic Pushdown Network* (SM-DPN) is a tuple $\mathcal{M} = (\mathcal{P}_1, \mathcal{P}_2, \dots, \mathcal{P}_n)$, s.t. for every $i$, $1 \le i \le n$, $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$ is a *Self-Modifying Dynamic Pushdown System* (SM-DPDS), where $P_i$ is a finite set of control locations (for every $j \ne k$, $P_j \cap P_k = \emptyset$), $\Gamma_i$ is the stack alphabet, $\Delta_i$ is a finite set of rules of the forms: (a) $p\gamma \to p_1\omega_1$ and (b) $p\gamma \to p_1\omega_1 \triangleright p_2\omega_2\theta_2$, such that $p, p_1 \in P_i$, $\gamma \in \Gamma_i$, $\omega_1 \in \Gamma_i^*$, $p_2 \in P_j$, $\omega_2 \in \Gamma_j^*$, $\theta_2 \subseteq \Delta_j \cup \Delta_j^c$, and $\Delta_i^c$ is a finite set of self-modifying rules of the form $p \stackrel{(\rho_1, \rho_2)}{\longrightarrow} p_1$, such that $\rho_1, \rho_2 \subseteq \Delta_i \cup \Delta_i^c$. A *Dynamic Pushdown System* (DPDS) is a SM-DPDS, such that $\Delta_i^c = \emptyset$. A *Dynamic Pushdown Network* (DPN) is a SM-DPN, such that for every $1 \le i \le n$, $\mathcal{P}_i$ is a DPDS.

Consider a SM-DPN $\mathcal{M} = (\mathcal{P}_1, \mathcal{P}_2, \dots, \mathcal{P}_n)$. A SM-DPDS $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$ can be seen as a Pushdown System with the ability (1) to spawn a new process and (2) to change its current set of rules during its execution. Because a process modelled by a SM-DPDS can change its set of rules at runtime, we introduce
the notion of a phase. A phase $\theta \subseteq \Delta_i \cup \Delta_i^c$ is the current set of rules that can be applied. $\theta$ changes when a self-modifying rule of type $p \stackrel{(\rho_1, \rho_2)}{\rightleftharpoons} p_1 \in \theta$ is applied. Such rule denotes that if the process is at the control location $p$, it can transition to the control location $p_1$ while removing rules in $\rho_1$ from $\theta$ and adding rules from $\rho_2$ to $\theta$. **Note that unlike the definition of SM-DPN in [19], we allow $\rho_1$ and $\rho_2$ to have different numbers of rules.** The rules of type $p\gamma \leftrightarrow p_1\omega_1 \in \theta$ define that if the process is at the control location $p$ and has $\gamma$ on the top of its stack, then it can pop $\gamma$ from the stack, push $\omega_1$ onto it, and go to the control location $p_1$. Similarly, the rules of type $p\gamma \leftrightarrow p_1\omega_1 \triangleright p_2\omega_2\theta_2 \in \theta$ describe the same behaviour as $p\gamma \leftrightarrow p_1\omega_1$ but additionally, the rule spawns another process at the control location $p_2$, with $\omega_2$ as content of the stack, and phase $\theta_2$. This new process will be executed by its corresponding SM-DPDS $\mathcal{P}_j = (P_j, \Gamma_j, \Delta_j, \Delta_j^c) \in \mathcal{M}$, such that $p_2 \in P_j$.

## 2.2 Configurations and DCLICs

A local configuration of a SM-DPDS $\mathcal{P}_i$ is a tuple $((p_i, \omega_i), \theta_i)$, where $p_i \in P_i$ is the current state of the process, $\omega_i \in \Gamma_i^*$ is the current stack content, and $\theta_i \subseteq \Delta_i \cup \Delta_i^c$ is the current phase. The set of all local configurations of a process of $\mathcal{P}_i$ is denoted as $Conf_i$. A global configuration of a SM-DPN is a multi-set over $\bigcup_{i=1}^n Conf_i$.

When a process can spawn a new process starting at the local configuration $((p_j, \omega_j), \theta_j)$, we say that $p_j\omega_j\theta_j$ is a *Dynamically Created Local Initial Configuration (DCLIC)*. The finite set of all DCLICs created by a process of $\mathcal{P}_i$ is denoted as $\mathcal{D}_i$ and is equal to $\{p_2\omega_2\theta_2 \in P_j \times \Gamma_j^* \times 2^{\Delta_j \cup \Delta_j^c} \mid \exists p, p' \in P_i, \gamma \in \Gamma_i, \omega' \in \Gamma_i^*, p\gamma \leftrightarrow p'\omega' \triangleright p_2\omega_2\theta_2 \in \Delta_i\}$.

For a SM-DPDS $\mathcal{P}_i$ and a set of DCLICs $D \subseteq \mathcal{D}_i$, we define the *successor operator* $\stackrel{D}{\Rightarrow}_i$ on a pair of local configurations of $\mathcal{P}_i$ as follows: $((p, \omega), \theta) \stackrel{D}{\Rightarrow}_i ((p', \omega'), \theta')$ means that a process at the configuration $((p, \omega), \theta)$ can transition into the configuration $((p', \omega'), \theta')$ by applying one of the rules in the current phase $\theta$ and the rule applied spawns processes with DCLICs $D$. Formally, $((p, \omega), \theta) \stackrel{D}{\Rightarrow}_i ((p', \omega'), \theta')$ iff one of these conditions holds:

1. $\exists \gamma \in \Gamma_i, u, v \in \Gamma_i^*$, s.t. $\omega = \gamma u, \omega' = vu, \theta = \theta', D = \emptyset$, and $p\gamma \leftrightarrow p'v \in \theta$, or

2. $\omega = \gamma u, \omega' = vu, \theta = \theta', D = \{p_2\omega_2\theta_2\}$, and $p\gamma \leftrightarrow p'v \triangleright p_2\omega_2\theta_2 \in \theta$, or

3. $\omega = \omega', D = \emptyset, p \stackrel{(\rho_1, \rho_2)}{\rightleftharpoons} p' \in \theta, \rho_1 \subseteq \theta, \theta' = (\theta \setminus \rho_1) \cup \rho_2$.

Intuitively, condition 1 specifies that if the process is at the local configuration $((p, \gamma u), \theta)$, such that the rule $p\gamma \leftrightarrow p'v$ is in the current phase $\theta$, then the process can pop $\gamma$ from the stack, push $v$ onto it, and transition to the state $p'$ without spawning any new process, getting $((p', vu), \theta)$. Condition 2 means that if the process is at the local configuration $((p, \gamma u), \theta)$, such that the current phase $\theta$ contains a rule $p\gamma \leftrightarrow p'v \triangleright p_2\omega_2\theta_2$, then it can pop $\gamma$ from the top of the stack, push $v$, go to $p'$, getting $((p', vu), \theta)$, and also spawn a new process with
the DCLIC $p_2\omega_2\theta_2$, i.e. starting at local configuration $((p_2, \omega_2), \theta_2)$. Condition 3 defines that if the process is at the local configuration $((p, \omega), \theta)$, such that the rule $p \xrightarrow{(\rho_1, \rho_2)} p'$ is in the current phase $\theta$, the process can remove all rules $r_1 \in \rho_1$ from the phase $\theta$ and add all rules $r_2 \in \rho_2$ to $\theta$, changing the current state to $p'$, getting $((p', \omega), \theta')$, such that $\theta' = (\theta \setminus \rho_1) \cup \rho_2$.

For local configurations $c, c' \in Conf_i$ and set of DCLICs $D \subseteq D_i$, we define a reflexive-transitive closure $c \stackrel{D}{\implies}_i^* c'$ as follows, where $c'' \in Conf_i$ and $D', D'' \subseteq D_i$: (1) $c \stackrel{\emptyset}{\implies}_i^* c$ and (2) if $c \stackrel{D'}{\implies}_i c'$ and $c' \stackrel{D''}{\implies}_i^* c''$, then $c \stackrel{D}{\implies}_i^+ c'$, where $D = D' \cup D''$. We also define the non-reflexive transitive closure $c \stackrel{D}{\implies}_i^+$ as follows: $c \stackrel{D}{\implies}_i^+ c'$ iff $\exists D', D'' \subseteq D_i$, such that $D = D' \cup D''$, $c \stackrel{D'}{\implies}_i c''$ and $c'' \stackrel{D''}{\implies}_i^* c'$.

Consider an arbitrary set of pairs of local configurations and sets of DCLICs $W \subseteq Conf_i \times 2^{D_i}$. Let $pre: 2^{Conf_i \times 2^{D_i}} \to 2^{Conf_i \times 2^{D_i}}$ be such that $pre(W) = \{(c, D \cup D'), c \in Conf_i \mid \exists D \subseteq D_i, (c', D') \in W : c \stackrel{D}{\implies}_i c'\}$. Let $pre^+$ and $pre^*$ be the transitive and reflexive-transitive closures of $pre$, respectively. In other words, $pre$ takes a pair of a local configuration and a set of DCLICs, and returns a set of predecessors of the given configurations paired with a superset of the given DCLICs that will be generated by the predecessors.

A local run of $\mathcal{P}_i$ is a possibly infinite sequence of local configurations $c_0c_1\dots$, s.t. $\forall j \ge 0 : \exists D \subseteq D_i : c_j \stackrel{D}{\implies}_i c_{j+1}$. A global run $\sigma$ starting from a global configuration $g_0 = c_0^0c_0^1c_0^2\dots c_0^m, m \ge 0$, is a (potentially infinite) set of local runs. Initially, $\sigma$ contains local runs for $m$ given processes, with each starting from initial local configuration $c_0^i$ for $0 \le i \le m$. Whenever a SM-DPDS responsible for a local run spawns a new process with the DCLIC $p_2\omega_2\theta_2$, a local run starting from $((p_2, \omega_2), \theta_2)$ is added to $\sigma$. From now on, we will omit the index $i$ for $\stackrel{D}{\implies}_i$ when it is understood from the context.

## 2.3 From SM-DPN to DPN

We show in this section that every SM-DPN model is equivalent to a non self-modifying DPN. Since the number of phases is finite, we can show that encoding every phase into the state set gives an equivalent DPN. Our translation follows the logic of the translation given in [19].

Let $\mathcal{M} = (\mathcal{P}_1, \mathcal{P}_2, \dots, \mathcal{P}_n)$ be a SM-DPN for $n \in \mathbb{N}$, such that for $i \le n$, $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$ is a SM-DPDS. We can construct an equivalent DPN $\mathcal{M}' = (\mathcal{P}'_1, \mathcal{P}'_2, \dots, \mathcal{P}'_n)$, where for $i \le n$, $\mathcal{P}'_i = (P'_i, \Gamma'_i, \Delta'_i)$ is a DPDS equivalent to $\mathcal{P}_i$, such that $P'_i = P_i \times 2^{\Delta_i \cup \Delta_i^c}$ and $\Delta'_i$ is computed as follows. Initially, $\Delta'_i$ is empty. For every $r \in \Delta_i \cup \Delta_i^c$ and for every phase $\theta \in 2^{\Delta_i \cup \Delta_i^c}$, such that $r \in \theta$:

1. if $r = p\gamma \hookrightarrow p_1\omega_1$, then add $(p, \theta)\gamma \hookrightarrow (p_1, \theta)\omega_1 \in \Delta'_i$;

2. if $r = p\gamma \hookrightarrow p_1\omega_1 \triangleright p_2\omega_2\theta_2$, then add $(p, \theta)\gamma \hookrightarrow (p_1, \theta)\omega_1 \triangleright (p_2, \theta_2)\omega_2 \in \Delta'_i$;
3. if $r = p \stackrel{(\rho_1, \rho_2)}{\rightleftharpoons} p_1$ and $\rho_1 \subseteq \theta$, then for every $\gamma \in \Gamma$, add $(p, \theta)\gamma \hookrightarrow (p_1, (\theta \setminus \rho_1) \cup \rho_2)\gamma \in \Delta'_i$.

This algorithm terminates because we have a finite number of rules and hence, a finite number of phases. We can show that: (the proof can be found in the full version of the paper [27])

**Proposition 1.** Let $(\langle p, \omega \rangle, \theta)$ and $(\langle p_1, \omega_1 \rangle, \theta_1)$ be configurations of $\mathcal{P}_i$, and $D \subseteq \mathcal{D}_i$. $(\langle p, \omega \rangle, \theta) \stackrel{D}{\Longrightarrow} \mathcal{M}$ $(\langle p_1, \omega_1 \rangle, \theta_1)$ iff $\langle (p, \theta), \omega \rangle \stackrel{D'}{\Longrightarrow} \mathcal{M}' \langle (p_1, \theta_1), \omega_1 \rangle$, such that $D' = \{(p_2, \theta_2)\omega_2 \mid p_2\omega_2\theta_2 \in D\}$

Thus, we get:

**Theorem 1.** Let $\mathcal{M} = (\mathcal{P}_1, \mathcal{P}_2, \dots, \mathcal{P}_n)$ be a SM-DPN for $n \in \mathbb{N}$, such that for $i \le n$, $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$ is a SM-DPDS. We can construct an equivalent DPN $\mathcal{M}' = (\mathcal{P}'_1, \mathcal{P}'_2, \dots, \mathcal{P}'_n)$, where for $i \le n$, $\mathcal{P}'_i = (P'_i, \Gamma_i, \Delta'_i)$ such that $O(|P'_i|) = |P_i| \cdot 2^{O(|\Delta'_i|+|\Delta_i^c|)}$ and $O(|\Delta'_i|) = (|\Delta_i| + |\Delta_i^c||\Gamma|) \cdot 2^{O(|\Delta'_i|+|\Delta_i^c|)}$

## 2.4 Modelling Self-Modifying Concurrent Code with SM-DPN

We give in this section a general process of converting a binary executable containing self-modifying code and concurrency into a SM-DPN. We suppose that we have an oracle that translates a binary program into a Control Flow Graph (CFG), such that each CFG transition corresponds to one instruction. One can obtain such an oracle using existing tools like Jakstab [18], IDA Pro [15], Radare2 [2], or ANGR [23].

We use the translation of [24] that models non self-modifying sequential instructions of the program by a standard PDS. We concentrate here on the translation of self-modifying and spawning instructions. For more details on the translation for sequential instructions, we refer the reader to [24].

If a CFG transition spawns a new thread, we add a rule $p\gamma \hookrightarrow p'\omega \triangleright p_2\omega_2\theta_2$, where $(\langle p_2, \omega_2 \rangle, \theta)$ is the initial configuration of the newly created process.

A self-modifying CFG transition that writes a binary value v to an address d, where d is the destination address for an executable region and v is a new value, is translated as follows: let $\rho_1$ be the set of SM-DPN rules obtained by our translation from instructions at d before self-modification and let $\rho_2$ be the set of SM-DPN rules obtained by our translation at d after the memory is modified. Suppose the CFG transition starts at control location p and leads to a control location $p'$. In this case, we add a rule $p \stackrel{(\rho_1, \rho_2)}{\rightleftharpoons} p'$ to the SM-DPN model.

## 2.5 LTL and Büchi Automata

In this section, we consider standard LTL formulas and Büchi Automata. Let AP be a set of atomic propositions.

**Definition 2.** An LTL formula $\psi$ is defined as follows (where $a \in AP$):

$$ \psi ::= \top \mid \bot \mid a \mid \neg \psi \mid \psi \land \psi \mid \mathbf{X} \psi \mid \psi \mathbf{U} \psi $$
Let $w = \alpha_0\alpha_1\alpha_2...$ be an $\omega$-word over $2^{AP}$ and $\psi$ be an LTL formula. Let $w^i = \alpha_i\alpha_{i+1}...$ be the subsequence of $w$ starting from the $i$-th symbol, where $i \ge 0$. The satisfiability $w \models \psi$ is defined as follows: $w \models \top$; $w \not\models \bot$; $w \models a$ iff $a \in \alpha_0$; $w \models \neg\psi$ iff $w \not\models \psi$; $w \models \psi_1 \wedge \psi_2$ iff $w \models \psi_1$ and $w \models \psi_2$; $w \models \mathbf{X}\psi$ iff $w^1 \models \psi$; $w \models \psi_1\mathbf{U}\psi_2$ iff there exists $k \ge 0$ such that for $j < k$, $w^j \models \psi_1$, and $w^k \models \psi_2$. We define the eventually operator as follows: $\mathbf{F}\psi = \top\mathbf{U}\psi$, which means that $\psi$ will hold at some point of the run. The globally operator $\mathbf{G}\psi = \neg\mathbf{F}\neg\psi$ means that $\psi$ holds universally along the run.

**Definition 3.** A Büchi Automaton (BA) is a tuple $\mathcal{B} = (G, \Sigma, T, g_0, F)$, where $G$ is a finite set of states, $T \subseteq G \times \Sigma \times G$ is the set of transitions, $g_0 \in G$ is the initial state, and $F \subseteq G$ is the set of accepting states.

For an $\omega$-word $w = \alpha_0\alpha_1\alpha_2...$, such that $\alpha_i \in \Sigma, i \ge 0$, a run on a BA $\mathcal{B}$ is an infinite sequence $r = g_0g_1g_2...$, such that $(g_{i-1}, \alpha_{i-1}, g_i) \in T$ for $i \ge 1$. A run $r$ is accepting if it visits some accepting states in $F$ infinitely often. $\mathcal{B}$ accepts an infinite word iff there is an accepting run on $\mathcal{B}$. It is well known that given an LTL formula $\psi$, we can construct a Büchi Automaton (BA) $\mathcal{B}_\psi$ on words over $\Sigma = 2^{AP}$ that accepts all $\omega$-words that satisfy $\psi$ [29].

## 2.6 Single-Indexed LTL for SM-DPNs

Let $AP = AP_1 \cup AP_2 \cup \dots \cup AP_n$ be a set of atomic propositions, such that $AP_i$ is the set of atomic propositions for process $P_i$, $1 \le i \le n$ (for $i \ne j$, $AP_i \cap AP_j = \emptyset$).

**Definition 4.** A Single-indexed LTL formula is a formula of the form $f = \bigwedge_{i=1}^n f_i$, where $f_i$ is a standard LTL formula over $AP_i$.

Let us consider a SM-DPN $\mathcal{M} = (P_1, P_2, \dots, P_n)$, where $P_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$, $1 \le i \le n$, and a single-indexed LTL formula $f = \bigwedge_{i=1}^n f_i$ over $AP$, where $f_i$ is an LTL formula over $AP_i$ for $P_i$, and let $\lambda_i$ be a labelling function $\lambda_i : P_i \to 2^{AP_i}$. For each control location $p \in \bigcup_{i=1}^n P_i$, let $\pi(p)$ be a function that maps $p$ to the index $i$ of its corresponding SM-DPDS, i.e. $\pi(p) = i$ if $p \in P_i$. For a local run $\sigma = (\langle p_0, \omega_0 \rangle, \theta_0)(\langle p_1, \omega_1 \rangle, \theta_1)\dots$, let $\pi(\sigma) = \pi(p_0)$. Let $\tau = \sigma_0\sigma_1\dots$ be a global run on $\mathcal{M}$, where for $j \ge 0$, $\sigma_j$ is a local run in $\tau$. We define the satisfiability condition for a global run $\tau = \sigma_0\sigma_1\dots$ on SM-DPN $\mathcal{M}$ and a single-indexed LTL formula $f$ as follows:

**Definition 5.** For a local run of $P_i$, $\sigma = (\langle p_0, \omega_0 \rangle, \theta_0)(\langle p_1, \omega_1 \rangle, \theta_1)\dots$, we say that $\sigma \models_D f_i$ if the $\omega$-word $w = \lambda_i(p_0)\lambda_i(p_1)\dots$ satisfies $f_i$ and $\sigma$ spawns new processes with DCLICs $D$. For a local configuration $c$, $c \models_D f_i$ if $P_i$ has a local run $\sigma_c = cc_2c_3\dots$, such that $\sigma_c \models_D f_i$.

For a global run $\tau = \sigma_0\sigma_1\dots$, we say that $\tau \models f$ if for every local run $\sigma_j \in \tau$, where $j \ge 0$:

1. there exists $D_j = \{p_j^0\omega_j^0\theta_j^0, p_j^1\omega_j^1\theta_j^1, \dots, p_j^m\omega_j^m\theta_j^m\}$, such that $\sigma_j \models_{D_j} f_{\pi(\sigma_j)}$,
2. for every $0 \le k \le m$ there exists a local run $\sigma_j^k$ starting from $(\langle p_j^k, \omega_j^k \rangle, \theta_j^k)$, such that $\sigma_j^k \models f$.

In other words, a global run $\tau = \sigma_0\sigma_1\dots$ satisfies a single-indexed LTL formula $f$ if every local run $\sigma$ in $\tau$ satisfies $f_{\pi(\sigma)}$ and if for every local run $\sigma_j^k$ spawned during $\sigma$, $\sigma_j^k$ satisfies $f$.

## 3 LTL Model-Checking for SM-DPNs

From now on, we fix a SM-DPN $\mathcal{M} = (\mathcal{P}_1, \mathcal{P}_2, \dots, \mathcal{P}_n)$, where for $1 \le i \le n$, $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$ is a SM-DPDS, and a single-indexed LTL formula $f = \bigwedge_{i=1}^n f_i$, such that $f_i$ is an LTL formula over atomic propositions $AP_i$ corresponding to $\mathcal{P}_i$. Let $\mathcal{B}_i = (G_i, 2^{AP_i}, T_i, g_i^0, F_i)$ be a Büchi automaton for the corresponding LTL formula $f_i$. Model checking a global configuration $\mathcal{G}$ of $\mathcal{M}$ over $f$ is not trivial for two reasons. First, it is not enough to check every local run starting from local configurations in $\mathcal{G}$, because we also need to check spawned processes. Second, model checking every possibly spawned process is too restrictive, because not all processes are required to be spawned during an accepting run, so even if they violate their LTL formulas, a global run would still be accepting if it does not spawn such processes. Therefore, when model checking $\mathcal{P}_i$ over $f_i$, it is important to remember which processes were spawned during the accepting run. We divide the problem of checking whether a global run starting from $\mathcal{G}$ satisfies $f$ into the following steps:

1. We compute a Self-Modifying Büchi Dynamic Pushdown System $\mathcal{BP}_i$ for each pair of $\mathcal{P}_i$ and $\mathcal{B}_i$, $1 \le i \le n$, which corresponds to a kind of synchronization between the SM-DPDS $\mathcal{P}_i$ and the LTL formula $f_i$.

2. For each $\mathcal{BP}_i$, we compute the set of pairs of local configurations and DCLICs of the form $(c, D)$, such that $c \models_D f_i$. For this, we need to be able to finitely represent potentially infinite sets of such pairs. To this aim, we use a kind of finite automata. Then, we perform a kind of reachability analysis on $\mathcal{BP}_i$ and construct a finite automaton $\mathcal{A}_i$, that accepts all pairs $(c, D)$ for a configuration $c$ and set of DCLICs $D$ spawned during the run of $\mathcal{P}_i$ from $c$ satisfying $f_i$, i.e. $c \models_D f_i$.

3. Using the automata $\mathcal{A}_i$, we compute the maximal set of DCLICs $\mathcal{D}_{fp}$, such that it contains only DCLICs for local configurations that satisfy their LTL formulas, and that the accepting runs on that configurations spawn only DCLICs in $\mathcal{D}_{fp}$.

4. For every local configuration $(\langle p, \omega \rangle, \theta) \in \mathcal{G}$, we use the automaton $\mathcal{A}_{\pi(p)}$ to check that there exists $D' \subseteq \mathcal{D}_{fp}$, such that $(\langle p, \omega \rangle, \theta) \models_{D'} f_{\pi(p)}$.

These different steps are detailed in the following sections.

### 3.1 Self-Modifying Büchi Dynamic Pushdown Systems

We compute a Self-Modifying Büchi Dynamic Pushdown Systems (SM-BDPDS) as a product of a SM-DPDS and a BA:
**Definition 6.** A Self-Modifying Büchi Dynamic Pushdown System is a SM-DPDS $\mathcal{BP} = (P, \Gamma, \Delta, \Delta^c, I, F)$ with extra elements $I \subseteq P$, which is a set of initial states, and $F \subseteq P$, which is a set of accepting states.

Let $\mathcal{BP} = (P, \Gamma, \Delta, \Delta^c, I, F)$ be a SM-BDPDS, $c_0 = (\langle p_0, \omega_0 \rangle, \theta_0)$ be a local configuration and $D$ be a set of DCLICs. ($c_0, D$) is accepted by $\mathcal{BP}$ iff $p_0 \in I$ and there is a local run $\sigma = c_0 c_1 c_2 \dots$ in $\mathcal{BP}$, such that $\mathcal{BP}$ spawns new processes with DCLICs $D$ during $\sigma$ and there is an infinite subsequence of configurations $c_{k_0} c_{k_1} \dots$, where $c_{k_j} = (\langle p_{k_j}, \omega_{k_j} \rangle, \theta_{k_j})$ for $j \ge 0$ and $p_{k_j} \in F$. We denote by $\mathcal{L}(\mathcal{BP})$ the pairs of all configurations and DCLICs in the form $(c, D)$ accepted by $\mathcal{BP}$, where $c$ is a configuration and $D$ is a set of DCLICs.

For a SM-DPDS $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$, a BA $\mathcal{B}_i = (G, 2^{AP_i}, T, g_0, F)$ that corresponds to an LTL formula $f_i$, and a labelling function $\lambda_i$, we can compute a SM-BDPDS $\mathcal{BP}_i = (P'_i, \Gamma'_i, \Delta'_i, \Delta_i^{c'}, I'_i, F'_i)$, where $P'_i = P_i \times G$, $I'_i = P_i \times \{g_0\}$, and $F'_i = P_i \times F$. Let $p, p_1, \in P_i$, $g_1, g_2 \in G_i$, $\gamma \in \Gamma$, $\omega_1 \in \Gamma^*$, $\rho_1, \rho_2 \subseteq \Delta_i \cup \Delta_i^c$, $p_2 \in P_j$, $\omega_2 \in \Gamma_j^*$, $\theta_2 \in 2^{\Delta_j \cup \Delta_j^c}$. Let $\text{prod}_{\mathcal{B}_i}(\delta)$ be a set of rules of $\mathcal{BP}_i$ obtained by applying the following procedure, where $\delta \subseteq \Delta_i \cup \Delta_i^c$:

1. $[p, g_1]\gamma \hookrightarrow [p_1, g_2]\omega_1 \in \text{prod}_{\mathcal{B}_i}(\delta)$ iff $p\gamma \hookrightarrow p_1\omega_1 \in \delta$ and $(g_1, \lambda_i(p), g_2) \in T_i$,

2. $[p, g_1]\gamma \hookrightarrow [p_1, g_2]\omega_1 \triangleright p_2\omega_2\theta_2 \in \text{prod}_{\mathcal{B}_i}(\delta)$ iff $p\gamma \hookrightarrow p_1\omega_1 \triangleright p_2\omega_2\theta_2 \in \delta$ and $(g_1, \lambda_i(p), g_2) \in T_i$,

3. $[p, g_1] \xrightarrow{(\sigma_1, \sigma_2)} [p_1, g_2] \in \text{prod}_{\mathcal{B}_i}(\delta)$ iff $p \xrightarrow{(\rho_1, \rho_2)} p_1 \in \delta$, $(g_1, \lambda_i(p), g_2) \in T_i$, $\sigma_1 = \text{prod}_{\mathcal{B}_i}(\rho_1)$, and $\sigma_2 = \text{prod}_{\mathcal{B}_i}(\rho_2)$.

We construct rules for $\mathcal{BP}_i$ as follows: $\Delta_i' = \text{prod}_{\mathcal{B}_i}(\Delta_i)$ and $\Delta_i^{c'} = \text{prod}_{\mathcal{B}_i}(\Delta_i^c)$. Intuitively, $\mathcal{BP}_i$ is a product of $\mathcal{P}_i$ and the BA $\mathcal{B}_i$. The behavior of the constructed SM-BDPDS $\mathcal{BP}_i$ is the same as of $\mathcal{P}_i$ synchronized with $\mathcal{B}_i$ for the LTL formula $f_i$. The intuition behind this construction is that if there is a run on the SM-BDPDS $\sigma = (\langle [p_0, g_0], \omega_0 \rangle, \theta_0)(\langle [p_1, g_1], \omega_1 \rangle, \theta_1)\dots$, then there should be a valid run $\sigma^{\mathcal{P}_i} = (\langle p_0, \omega_0 \rangle, \theta_0)(\langle p_1, \omega_1 \rangle, \theta_1)\dots$ spawning DCLICs $D$ on $\mathcal{P}_i$ and a valid run $\sigma^{\mathcal{B}_i} = g_0 g_1 \dots$ on $\mathcal{B}_i$. Therefore, $\sigma^{\mathcal{P}_i} \models_D f_i$ iff $((\langle p_0, g_0 \rangle, \omega_0), \theta_0), D) \in \mathcal{L}(\mathcal{BP}_i)$.

## 3.2 Characterizing $\mathcal{L}(\mathcal{BP}_i)$ Using Reachability

We show in this section how $\mathcal{L}(\mathcal{BP}_i)$ can be computed by performing a kind of reachability analysis.

**Theorem 2.** For a SM-BDPDS $\mathcal{BP}_i = (P'_i, \Gamma_i, \Delta'_i, \Delta_i^{c'}, I_i, F_i)$, a local configuration $(\langle p, \omega \rangle, \theta)$ and a set of DCLICs $D$, $((\langle p, \omega \rangle, \theta), D) \in \mathcal{L}(\mathcal{BP}_i)$ iff $p \in I_i$ and $\exists D_1, D_2, D_3 \subseteq D_i$, s.t. $D = D_1 \cup D_2 \cup D_3$ and the following conditions hold:

$$ \alpha_1 \left( \langle p, \omega \rangle, \theta \right) \underset{D_1}{\stackrel{D_1}{\Longrightarrow}}^* \left( \langle p', \gamma\omega' \rangle, \theta' \right) \text{ for some } p' \in P'_i, \theta, \theta' \subseteq (\Delta'_i \cup \Delta_i^{c'}), \gamma \in \Gamma_i, \\ \omega' \in \Gamma^*, \text{ and} $$

$$ \alpha_2 \left( \langle p', \gamma \rangle, \theta' \right) \underset{D_2}{\stackrel{D_2}{\Longrightarrow}}^+ \left( \langle g, u \rangle, \theta'' \right) \text{ and } \left( \langle g, u \rangle, \theta'' \right) \underset{D_3}{\stackrel{D_3}{\Longrightarrow}}^* \left( \langle p', \gamma v \rangle, \theta' \right) \text{ for some} \\ g \in F_i, \theta'' \subseteq (\Delta'_i \cup \Delta_i^{c'}), u, v \in \Gamma^*. $$
**Definition 7.** A Multi-Automaton is a tuple $\mathcal{A}_i = (Q_i, \Gamma_i, \delta_i, I_i, \text{Acc}_i)$, where $Q_i$ is a finite set of states, $\Gamma_i$ is the alphabet of $\mathcal{P}_i$, $\delta_i \subseteq Q_i \times (\Gamma_i \cup \{\varepsilon\}) \times 2^{\mathcal{D}_i} \times Q_i$ is a set of transitions, $I_i = P_i \times 2^{\Delta_i \cup \Delta_i^c} \subseteq Q_i$ is a set of initial states representing the control point and the phase of the configuration, and $\text{Acc}_i \subseteq Q_i$ is a set of accepting states. Transition $(q, \gamma, D, q') \in \delta_i$ can be denoted as $q \xrightarrow{\gamma/D}^* q'$.

The reflexive-transitive closure $q \xrightarrow{\omega/D}^* q'$ for transitions is defined as: (1) $q \xrightarrow{\varepsilon/\emptyset}^* q$, (2) if $q \xrightarrow{\gamma/D}^* q''$ and $q'' \xrightarrow{\omega/D'}^* q'$, then $q \xrightarrow{\gamma\omega/D \cup D'}^* q'$, where $\omega \in \Gamma_i^*$, $D' \subseteq D_i$.

For a local configuration $((p, \omega), \theta)$ and a set of DCLICs $D$, the MA accepts tuples $(( (p, \omega), \theta), D) \text{ iff there is a path } (p, \theta) \xrightarrow{\omega/D}^* q_f \text{ for some } q_f \in \text{Acc}_i$. From now on, we will omit the index $i$ for $\xrightarrow{\gamma/D}$ when it is understood from the context.

Let $\mathcal{L}(\mathcal{A}_i)$ be the set of configurations and DCLICs accepted by the MA $\mathcal{A}_i$. We say that a set of configurations and DCLICs $W$ is *regular* iff there exists a MA $\mathcal{A}_i$, such that $W = \mathcal{L}(\mathcal{A}_i)$.

## 3.4 Algorithm for pre\* Computation

We prove in this section that given a SM-DPDS $\mathcal{P}_i$ and a regular set of pairs of configurations and DCLICs $W$ accepted by a MA $\mathcal{A}_i$, we can compute a new MA $\mathcal{A}_i^{\text{pre}*}$ that accepts pre\*(W) using the following saturation procedure. Let $\mathcal{A}_i = (Q_i, \Gamma_i \cup \{\varepsilon\}, \delta_i, I_i, \text{Acc}_i)$ be the original MA that accepts configurations of a SM-DPDS $\mathcal{P}_i = (P_i, \Gamma_i, \Delta_i, \Delta_i^c)$.

Without loss of generality, we assume that the SM-DPDS has no rules that remove themselves. I.e., there are no rules of type $r = p \stackrel{(\rho_1, \rho_2)}{\longrightarrow} p' \in \Delta_i^c$, such that $r \in \rho_1$. This is not a restriction since we can substitute such rules with two rules: $r = p \stackrel{(\emptyset, \emptyset)}{\longrightarrow} p^r$ and $r' = p^r \stackrel{(\rho_1, \rho_2)}{\longrightarrow} p'$, where $r'$ is a new rule and $p^r$ is a new state. Moreover, we assume w.l.o.g. that $\delta_i$ has no transitions into initial states, i.e. there exists no transitions of the form $q \stackrel{\gamma/D}{\longrightarrow} (p, \theta)$ in $\delta_i$, for any $q \in Q_i$, $\gamma \in \Gamma_i$, $D \subseteq D_i$, $(p, \theta) \in I_i$.

Now, we can construct $\mathcal{A}_i^{\text{pre}*} = (Q_i, \Gamma_i, \delta'_i, I_i, \text{Acc}_i)$. Initially, $\delta'_i = \delta_i$. Then, we apply the following saturation rules:

$\mu_1$ If $r = p\gamma \leftrightarrow p'\omega \in \Delta_i$, then for every $\theta \in 2^{\Delta_i \cup \Delta_i^c}$, s.t. $r \in \theta$ and $(p', \theta) \xrightarrow{\omega/D}^*$
$q \in \delta'_i$, add transition $(p, \theta) \xrightarrow{\gamma/D} q$ to $\delta'_i$;

$\mu_2$ if $r = p\gamma \leftrightarrow p'\omega \triangleright p''\omega''\theta'' \in \Delta_i$, then for every $\theta \in 2^{\Delta_i \cup \Delta_i^c}$, s.t. $r \in \theta$ and
$(p', \theta) \xrightarrow{\omega/D}^* q \in \delta'_i$, add transition $(p, \theta) \xrightarrow{\gamma/D \cup \{p''\omega''\theta''\}} q$ to $\delta'_i$;

$\mu_3$ If $r = p \stackrel{(\rho_1, \rho_2)}{\longrightarrow} p' \in \Delta_i^c$, then for every $\theta' \in 2^{\Delta_i \cup \Delta_i^c}$ and $\gamma \in \Gamma_i$, s.t.
$r \in \theta'$, $\rho_2 \subseteq \theta'$ and $(p', \theta') \xrightarrow{\gamma/D} q$, then add $(p, \theta) \xrightarrow{\gamma/D} q$ to $\delta_i'$, such that
$\theta' = (\theta \setminus \rho_1) \cup \rho_2$.

This procedure terminates because there is a finite number of transitions we can add, which is $|(P_i \times 2^{\Delta_i \cup \Delta_i^c}) \cup Q_i|^2 |\Gamma \cup \{\varepsilon\}| 2^{\mathcal{D}_i}|$.
Let us explain the intuition behind the saturation rules. Rule $\mu_1$ adds predecessors obtained from standard pushdown rules. Consider a rule $r = p\gamma \leftrightarrow p'\omega \in \Delta_i$ and let us consider a path of $A_i^{pre*}$ of the form $(p', \theta) \xrightarrow{\omega/D} q \xrightarrow{\omega'/D'} q_f$ such that $q_f \in \text{Acc}_i$ and $r \in \theta$, which means $((\langle p', \omega\omega' \rangle, \theta), D \cup D') \in \mathcal{L}(A_i^{pre*})$. Since the phase $\theta$ contains $r$, then $(\langle p, \gamma\omega' \rangle, \theta)$ is a direct predecessor of $(\langle p', \omega\omega' \rangle, \theta)$. Since $r$ does not spawn new processes, there is no need to update the DCLICs $D$. Therefore, we add the new transition $(p, \theta) \xrightarrow{\gamma/D} q$ to $A_i^{pre*}$, so that $((\langle p, \gamma\omega' \rangle, \theta), D \cup D')$ will be accepted by the path $(p, \theta) \xrightarrow{\gamma/D} q \xrightarrow{\omega'/D'} q_f$ in $A_i^{pre*}$.

Similarly, rule $\mu_2$ adds predecessors that require a process to be spawned. In this case, consider a rule $r = p\gamma \leftrightarrow p'\omega \triangleright p''\omega''\theta'' \in \Delta_i$ and let there be a path of the form $(p', \theta) \xrightarrow{\omega/D} q \xrightarrow{\omega'/D'} q_f$ such that $q_f \in \text{Acc}_i$ and $r \in \theta$. Therefore, $((\langle p', \omega\omega' \rangle, \theta), D \cup D') \in \mathcal{L}(A_i^{pre*})$. Since the phase $\theta$ contains $r$, then $(\langle p, \gamma\omega' \rangle, \theta)$ is a direct predecessor of $(\langle p', \omega\omega' \rangle, \theta)$. Since $r$ spawns a new process with the DCLIC $p''\omega''\theta''$, we add $p''\omega''\theta''$ to the DCLICs $D$. Therefore, we add the new transition $(p, \theta) \xrightarrow{\gamma/D \cup \{p''\omega''\theta''\}} q$, so that $((\langle p, \gamma\omega' \rangle, \theta), D \cup D' \cup \{p''\omega''\theta''\})$ will be accepted by the path $(p, \theta) \xrightarrow{\gamma/D \cup \{p''\omega''\theta''\}} q \xrightarrow{\omega'/D'} q_f$.

The saturation rule $\mu_3$ adds the predecessors that are obtained by self-modifying rules. Consider a rule $r = p \xrightarrow{\langle \rho_1, \rho_2 \rangle} p' \in \Delta_i^c$ and a path in $A_i^{pre*}$ of the form $(p', \theta') \xrightarrow{\gamma/D} q \xrightarrow{\omega/D'} q_f$, such that $q_f \in \text{Acc}_i$, $r \in \theta'$, $\rho_2 \subseteq \theta'$. Therefore, $((\langle p', \gamma\omega \rangle, \theta'), D \cup D') \in \mathcal{L}(A_i^{pre*})$. Since the phase $\theta'$ contains $r$ and all rules in $\rho_2$, then $(\langle p, \gamma\omega \rangle, \theta)$ is a direct predecessor of $(\langle p', \gamma\omega \rangle, \theta')$, where $\theta = (\theta' \setminus \rho_2) \cup \rho_1$. Since this transition does not spawn any new processes, there is no need to update DCLICs $D$. Therefore, we add the new transition $(p, \theta) \xrightarrow{\gamma/D} q$ to $A_i^{pre*}$, so that $((\langle p, \gamma\omega \rangle, \theta), D \cup D')$ will be accepted by the path $(p, \theta) \xrightarrow{\gamma/D} q \xrightarrow{\omega/D'} q_f$ in $A_i^{pre*}$.

We can show that the saturation algorithm described above computes MA $A_i^{pre*}$ that accepts $pre^*(\mathcal{L}(A_i))$. The proof can be found in the full version of the paper [27].

**Lemma 1.** Given a regular set of configurations and DCLICs $W$ recognized by MA $A_i = (Q_i, \Gamma_i, \delta_i, I_i, \text{Acc}_i)$, we can effectively compute the Multi-Automaton $A_i^{pre*} = (Q_i, \Gamma_i, \delta'_i, I_i, \text{Acc}_i)$, such that $\mathcal{L}(A_i^{pre*}) = pre^*(W)$.

Thus, we get:

**Theorem 3.** For a regular set of local configurations and DCLICs $W \subseteq P_i \times \Gamma_i^* \times 2^{\Delta_i \cup \Delta_i^c} \times 2^{\mathcal{D}_i}$, the set $pre^*(W)$ is also regular and can be effectively computed.

## 3.5 Effective Algorithm for Model Checking SM-DPNs

Now, we are ready to tackle the main problem of this paper - effective LTL model checking of SM-DPNs. Using Corollary 1 and our saturation procedure,
we can compute $\mathcal{L}(\mathcal{BP}_i)$ for every $i$, $1 \le i \le n$, by constructing a MA $\mathcal{A}_i$, such
that $\mathcal{L}(\mathcal{A}_i) = \mathcal{L}(\mathcal{BP}_i)$. To construct $\mathcal{A}_i$, we iterate over possible $p' \in P', \gamma' \in$
$\Gamma$, and $\theta' \subseteq \Delta'_i \cup \Delta^{c'}_i$. For every such triple, we construct the MA $\mathcal{A}_1^1$, s.t.
$\mathcal{L}(\mathcal{A}_1^1) = \text{pre}^*(\{p'\} \times \{\theta'\} \times \gamma'\Gamma_i^* \times \{\emptyset\})$. Then, we compute the MA $\mathcal{A}_2^2$, s.t.
$\mathcal{L}(\mathcal{A}_2^2) = (F_i \times 2^{\Delta'_i \cup \Delta^{c'}_i} \times \Gamma_i^* \times 2^{\mathcal{D}_i})$. We compute then the product $\mathcal{A}_3^3$, s.t.
$\mathcal{L}(\mathcal{A}_3^3) = \mathcal{L}(\mathcal{A}_1^1) \cap \mathcal{L}(\mathcal{A}_2^2)$. After that, we construct the $\text{pre}^+$ of the intersection:
$\mathcal{L}(\mathcal{A}_4^4) = \text{pre}^+(\mathcal{L}(\mathcal{A}_3^3))$, and test whether $((\langle p', \gamma' \rangle, \theta'), D'_2) \in \mathcal{L}(\mathcal{A}_4^4)$ for a set of
DCLICs $D'_2$. If the $\mathcal{A}_i^4$ automaton accepts $((\langle p', \gamma' \rangle, \theta'), D'_2)$, then we add the
transition $(p', \theta') \xrightarrow{\gamma'/D'_2} q_f$ to a MA $\mathcal{A}'_i$, where $q_f$ is a final state. Next, we
compute $\text{pre}^*$ of $\mathcal{A}'_i$ to get the final automaton $\mathcal{A}_i$, s.t. $\mathcal{L}(\mathcal{A}_i) = \text{pre}^*(\mathcal{L}(\mathcal{A}'_i))$.
From Corollary 1, this $\mathcal{A}_i$ is such that if $(c, D) \in \mathcal{L}(\mathcal{A}_i)$, then $c \models_D f_i$.

Now, we can use the constructed MAs $\mathcal{A}_i$ to model check $\mathcal{M}$. First, we need to compute the largest set of DCLICs that have an accepting run and spawn DCLICs that also have an accepting run. We call this set $\mathcal{D}_{fp}$. This set contains DCLICs that satisfy $f$. Let $D_I = \bigcup_{k=1}^n \mathcal{D}_k$ be the set of all DCLICs spawned in $\mathcal{M}$. Let $F: 2^{D_I} \rightarrow 2^{D_I}$ be defined as $F(D) = \{p\omega\theta \in D_I \mid \exists D' \subseteq D: (([p, g_{\pi(p)}^0], \omega), \theta) \in \mathcal{L}(\mathcal{A}_{\pi(i)})\}$. Let $D^0D^1D^2\dots$ be a sequence generated by the recursive application of $F$, such that $D^0 = D_I$, and $D^j = F(D^{j-1})$ for $j \ge 1$. We can show that $\mathcal{D}_{fp} = \bigcap_j D^j$ and can be effectively computed by finding the greatest fixpoint on $F$:

**Theorem 4.** We can effectively compute $\mathcal{D}_{fp}$, s.t. for every DCLIC $p\omega\theta \in \bigcup_{k=1}^n \mathcal{D}_k$, $(\langle p, \omega \rangle, \theta) \models_f f$ iff $p\omega\theta \in \mathcal{D}_{fp}$.

Intuitively, the function $F$ takes a set of DCLICs $D$ that *hypothetically* satisfy their corresponding LTL formulas. The function returns a smaller set of DCLICs $D'$, where for every DCLIC $p'\omega'\theta' \in D'$, there exists another set of DCLICs $D'' \subseteq D$, such that $(\langle p', \omega' \rangle, \theta') \models_{D''} f_{\pi(p')}$.
Initially, $D^0$ is the set of all DCLICs $D_I$. At the first step, we exclude DCLICs that cannot satisfy $f$ regardless of what DCLICs they generate. Then, every next iteration excludes such DCLICs that spawn unsatisfiable DCLICs during their accepting runs. At the end, the function should converge at a constant set of DCLICs that satisfy $f$. In other words, we can compute the greatest fixpoint $\mathcal{D}_{fp}$ on the recursion starting from $D_I$ because this function reduces a countable set of DCLICs for each step. Therefore, we can use Theorem 4 to find the set of valid DCLICs for a single-indexed LTL formula.

Now, for a global configuration $G = c_0c_1c_2...c_m$ and a single indexed formula
$f = \bigwedge_{i=1}^n f_i$, we can determine whether $G$ satisfies $f$ as follows: we check for
each local configuration $c_j = (\langle p_j, \omega_j \rangle, \theta_j)$, if there exists $D \subseteq \mathcal{D}_{fp}$, such that
$c_j \models_D f_{\pi(p_j)}$. $G \models f$ iff all configurations $c_j \in G$ satisfy their corresponding
$f_{\pi(p_j)}$ and spawn DCLICs $D \subseteq \mathcal{D}_{fp}$.

4 Experiments

4.1 Comparison with Model Checking DPNs

Since SM-DPNs are equivalent to normal DPNs, we compared our *direct* model
checking approach with the approach that consists of translating SM-DPN to
<table><caption>**Table 1.** Performance comparison of proposed algorithm to the algorithm of [25] on an equivalent DPN.</caption><thead><tr><th rowspan="2">|M|</th><th rowspan="2">|f<sub>i</sub>|</th><th rowspan="2">|Δ<sub>i</sub>| + |Δ<sub>i</sub><sup>o</sup>|</th><th colspan="2">Our approach</th><th colspan="2">SM-DPN to DPN</th></tr><tr><th>T, sec</th><th>mem, KiB</th><th>T, sec</th><th>mem, KiB</th></tr></thead><tbody><tr><td>1</td><td>5</td><td>10 + 3</td><td>0.01</td><td>63.57</td><td>0.4</td><td>1 153.93</td></tr><tr><td>1</td><td>6</td><td>10 + 3</td><td>3.98</td><td>236.29</td><td>2 927.27</td><td>2 017.56</td></tr><tr><td>1</td><td>7</td><td>10 + 3</td><td>2.87</td><td>325.34</td><td>815.80</td><td>1 232.78</td></tr><tr><td>1</td><td>8</td><td>10 + 3</td><td>5.29</td><td>674.29</td><td>8 894.93</td><td>2 420.37</td></tr><tr><td>1</td><td>5</td><td>10 + 1</td><td>0.30</td><td>63.57</td><td>7.23</td><td>134.47</td></tr><tr><td>1</td><td>6</td><td>10 + 1</td><td>0.10</td><td>63.57</td><td>3.11</td><td>116.18</td></tr><tr><td><b>1</b></td><td><b>7</b></td><td><b>10 + 1</b></td><td><b>2.12</b></td><td><b>642.30</b></td><td><b>389.87</b></td><td><b>1 045.70</b></td></tr><tr><td>2</td><td>1</td><td>12 + 2</td><td>1.24</td><td>71.24</td><td>21.76</td><td>561.31</td></tr><tr><td>2</td><td>1</td><td>22 + 2</td><td>1.53</td><td>78.41</td><td>39.49</td><td>706.41</td></tr><tr><td><b>2</b></td><td><b>1</b></td><td><b>32 + 2</b></td><td><b>10.04</b></td><td><b>179.01</b></td><td><b>1 473.41</b></td><td><b>1 542.21</b></td></tr><tr><td>2</td><td>12</td><td>32 + 2</td><td>114.78</td><td>1 433.08</td><td>timeout</td><td>timeout</td></tr><tr><td>3</td><td>4</td><td>31 + 3</td><td>29.19</td><td>483.58</td><td>3 586.07</td><td>10 920.32</td></tr><tr><td>3</td><td>5</td><td>32 + 5</td><td>0.02</td><td>72.42</td><td>4.21</td><td>41 818.15</td></tr><tr><td>3</td><td>5</td><td>42 + 5</td><td>1401.31</td><td>3 661.34</td><td>timeout</td><td>timeout</td></tr><tr><td>2</td><td>7</td><td>32 + 4</td><td>253.80</td><td>1 347.30</td><td>timeout</td><td>timeout</td></tr><tr><td>3</td><td>8</td><td>50 + 4</td><td>607.18</td><td>1 717.22</td><td>timeout</td><td>timeout</td></tr><tr><td>2</td><td>9</td><td>34 + 5</td><td>904.25</td><td>2 924.89</td><td>timeout</td><td>timeout</td></tr><tr><td>2</td><td>13</td><td>40 + 3</td><td>0.02</td><td>72.50</td><td>1.09</td><td>5 212.05</td></tr><tr><td><b>4</b></td><td><b>1</b></td><td><b>22 + 2</b></td><td><b>31.92</b></td><td><b>476.02</b></td><td><b>4 644.77</b></td><td><b>2 492.78</b></td></tr><tr><td>3</td><td>14</td><td>37 + 2</td><td>32.93</td><td>585.57</td><td>1 824.50</td><td>8 695.83</td></tr><tr><td>3</td><td>41</td><td>43 + 2</td><td>275.18</td><td>5 206.40</td><td>timeout</td><td>timeout</td></tr><tr><td>4</td><td>1</td><td>52 + 2</td><td>47.35</td><td>919.43</td><td>timeout</td><td>timeout</td></tr><tr><td>4</td><td>1</td><td>62 + 2</td><td>60.15</td><td>920.29</td><td>timeout</td><td>timeout</td></tr><tr><td>5</td><td>1</td><td>12 + 2</td><td>5.03</td><td>167.78</td><td>232.47</td><td>1 341.30</td></tr><tr><td>5</td><td>1</td><td>22 + 2</td><td>13.99</td><td>291.78</td><td>1 804.86</td><td>2 088.73</td></tr><tr><td><b>5</b></td><td><b>2</b></td><td><b>102 + 2</b></td><td><b>151.66</b></td><td><b>587.85</b></td><td><b>10 392.94</b></td><td><b>3 288.55</b></td></tr><tr><td>2</td><td>2</td><td>28 + 3</td><td>18.21</td><td>246.90</td><td>866.46</td><td>7 962.37</td></tr><tr><td><b>3</b></td><td><b>1</b></td><td><b>33 + 5</b></td><td><b>54.72</b></td><td><b>400.27</b></td><td><b>14 310.20</b></td><td><b>23 819.53</b></td></tr><tr><td>2</td><td>1</td><td>48 + 4</td><td>251.91</td><td>560.40</td><td>timeout</td><td>timeout</td></tr><tr><td>4</td><td>1</td><td>38 + 7</td><td>7 548.30</td><td>12 901.00</td><td>OOM</td><td>OOM</td></tr><tr><td>1</td><td>2</td><td>81 + 8</td><td>56 501.63</td><td>11 606.98</td><td>OOM</td><td>OOM</td></tr><tr><td>2</td><td>2</td><td>134 + 4</td><td>2 878.35</td><td>2 131.24</td><td>timeout</td><td>timeout</td></tr><tr><td>4</td><td>2</td><td>42 + 9</td><td>26 804.35</td><td>19 890.16</td><td>OOM</td><td>OOM</td></tr><tr><td>1</td><td>3</td><td>59 + 4</td><td>184.98</td><td>545.51</td><td>timeout</td><td>timeout</td></tr><tr><td>1</td><td>3</td><td>66 + 1</td><td>77.44</td><td>1 325.73</td><td>1 442.53</td><td>10 312.03</td></tr><tr><td>2</td><td>3</td><td>149 + 4</td><td>7 467.28</td><td>3 901.95</td><td>timeout</td><td>timeout</td></tr><tr><td><b>3</b></td><td><b>1</b></td><td><b>129 + 2</b></td><td><b>769.27</b></td><td><b>3 005.60</b></td><td><b>151 403.08</b></td><td><b>52 682.78</b></td></tr><tr><td>3</td><td>3</td><td>63 + 3</td><td>105.41</td><td>621.27</td><td>81 637.13</td><td>41 098.79</td></tr><tr><td>3</td><td>3</td><td>197 + 1</td><td>1 115.17</td><td>6 529.34</td><td>26 151.43</td><td>55 853.34</td></tr><tr><td>3</td><td>3</td><td>127 + 4</td><td>8 154.62</td><td>8 112.27</td><td>timeout</td><td>timeout</td></tr><tr><td>4</td><td>3</td><td>134 + 3</td><td>4 002.69</td><td>9 294.60</td><td>timeout</td><td>timeout</td></tr><tr><td>3</td><td>10</td><td>161 + 2</td><td>981.33</td><td>4 854.11</td><td>timeout</td><td>timeout</td></tr><tr><td>4</td><td>6</td><td>90 + 7</td><td>14 090.17</td><td>5 948.56</td><td>OOM</td><td>OOM</td></tr><tr><td>4</td><td>11</td><td>20 + 7</td><td>2 436.91</td><td>13 873.57</td><td>OOM</td><td>OOM</td></tr><tr><td>3</td><td>21</td><td>34 + 5</td><td>343.70</td><td>1 555.08</td><td>timeout</td><td>timeout</td></tr></tbody></table>
the equivalent DPN and applying the algorithm proposed by [25]. We implemented both algorithms using Python and tested them on random SM-DPNs. We summarized our results in Table 1. The column $|M|$ specifies the number of SM-DPDSs in a SM-DPN, $|f_i|$ is the number of transitions in a BA corresponding to the $i$-th LTL formula, $|\Delta_i|$ is the number of non self-modifying rules in each SM-DPDS, $|\Delta_i^c|$ is the number of self-modifying rules in each SM-DPDS, T is the time taken for the algorithm and mem is the amount of memory used during the computation. We put timeout for executions longer than 10 hours, and OOM (out-of-memory) if the computer ran out of memory resource for the computations. The experiments were conducted on a laptop with a CPU AMD Ryzen 7 8845HS and 10 GB of available memory (8 GB RAM and 2 GB swap pages).

From Table 1, we can see that our algorithm performs consistently better in terms of time and memory than translating SM-DPNs into standard DPNs and applying the LTL algorithm for standard DPNs from [25]. We highlighted some cases where our algorithm performed significantly better. For example, when a SM-DPN contains 3 processes, 129 standard rules and 2 self-modifying rules, our direct LTL model checking took 769.27 seconds (~13 minutes), while the naive approach took almost 2 days. The DPN approach timed out and required too much memory in a lot of cases, taking more than 10 hours to complete. Whereas our approach could finish model checking in a few minutes for most cases.

## 4.2 Specifying Malicious Behaviour as Single-Indexed LTL Formulas

We evaluated the applicability of our approach for malware detection. We have collected reported malware from malware databases, such as Virus Share [10] and Malware Bazaar [1]. We consider a variant of Mirai malware and a variant of Gozi malware that are both concurrent and self-modifying. We also considered a self-modifying version of a concurrent generic backdoor.

In what follows, we describe the malicious behaviour of the mentioned malware as single-indexed LTL formulas of the form $f = \bigwedge_i f_i$. For readability, we write $[f_i]_i$ to denote that $f_i$ describes the malicious behavior related to process $i$.

Mirai malware is a botnet virus that targets IoT devices running on Linux. It has two parallel processes. One process communicates with a Command and Control (C2) server. The other process evades detection and maintains persistence on the host machine. The single-indexed LTL formula for Mirai can be described as:

$$f_{Mirai} = [\mathbf{F}(accept \land \mathbf{F}fork)]_1 \land [\mathbf{F}(setsid \land \mathbf{F}kill)]_2$$

Intuitively, the first process waits for a command from the C2 server using the accept syscall and then creates a parallel process to perform malicious activity using the fork syscall. The second process disguises itself as a legitimate software. First, it calls setsid to move itself to a new group of processes and kills the parent process by calling kill to avoid detection.
**Gozi malware** is a Windows virus that targets banking field and steals credentials to critical systems such as banking software. The first thread tries to hide the presence of the malware by manipulating the filesystem. The second avoids automatic detection by antivirus software and connects to the C2 server or executes an external program. The third thread steals credentials from browsers. Here is the single-indexed formula for such behaviour:

$$f_{Gozi} = [\mathbf{F}(\mathit{FindFirstFileW} \land \mathbf{F}(\mathit{DeleteFileW} \lor \mathit{SetFileAttributesW}))]_1 \land \\ [\mathbf{F}(\mathit{Sleep} \land \mathbf{F}(\mathit{CreateProcessW} \lor \mathit{connect}))]_2 \land \\ [\mathbf{G}(\mathit{GetWindowTextW} \implies \mathbf{F}\mathit{CreateFileW})]_3$$

The first thread finds the file of itself using `FindFirstFileW` and hides it by either deleting it with `DeleteFileW`, or modifying its visibility with the `SetFileAttributesW` syscall. The second thread waits until antivirus software marks the program as safe by calling `Sleep` and then, establishes connection with C2 using `connect` or calls another malicious process using `CreateProcessW`. The third thread performs credential stealing by calling `GetWindowTextW` on a browser, and saving the credentials into a new file created by the syscall `CreateFileW`.

**Generic Backdoor** is a group of different malware that obtains a full access to the infected machine. Its first thread modifies the system registry to execute the malware at the startup of the system. The second thread establishes connection with a C2 server. The third thread sends data to the C2. And the fourth thread waits for commands from the C2. The behaviour is described using the following formula:

$$f_{Backdoor} = [\mathbf{F}(\mathit{GetModuleFileNameA} \land \mathbf{F}\mathit{RegSetValueExA})]_1 \land \\ [\mathbf{F}(\mathit{gethostbyname} \land \mathbf{F}\mathit{recv})]_2 \land [\mathbf{F}\mathit{send}]_3 \land [\mathbf{GF}(\mathit{accept} \land \mathbf{F}\mathit{CreateThread})]_4$$

The first thread gets its own filename using `GetModuleFileNameA`, and puts it into registry for automatic execution on system startup using the system call `RegSetValueExA`. The second formula finds the C2 server using `gethostbyname` and configures a socket to receive incoming messages with `recv`. The third thread sends data using `send` syscall. And the fourth thread waits for incoming messages using `accept` and, on receiving the message, spawns a new thread using `CreateThread` to perform malicious activities.

## 4.3 Applying Our Approach for Malware Detection

We applied our tool to detect malicious behaviour of the malware mentioned above. We translated the binary code of the malware into SM-DPNs using the method described in Section 2.4. We obtained the CFGs of malware using the ANGR analyzer [23]. We made use of its symbolic execution to resolve system
calls as control points, identify self-modifying instructions, and compute states
of spawned processes. Then, we model checked the obtained SM-DPNs against
single-indexed LTL formulas $f_{Mirai}$, $f_{Gozi}$, and $f_{Backdoor}$ describing the mali-
cious behaviors. We used system calls as atomic propositions AP. Our labelling
function $\lambda$ is that if there is a system call $x$ at a control point $p$, then $\lambda(p) = \{x\}$
and otherwise, $\lambda(p) = \emptyset$.

Our tool successfully detected the malicious behaviours specified by the above
single-indexed LTL formulas, by checking that the corresponding SM-DPN of
each program satisfies the corresponding malicious single-indexed LTL formula.
Thus, our tool was able to check that these programs are malicious in a few
minutes (e.g., the analysis of the backdoor malware took only 2 minutes).

## 5 Conclusion

In this work, we tackle the problem of LTL model checking of concurrent self-
modifying code. We propose a *direct* and *efficient* algorithm for model checking
of SM-DPNs over single-indexed LTL formulas. First, we show an algorithm
for reducing model checking SM-DPDS to the reachability analysis of Self-
Modifying Büchi Dynamic Pushdown Systems using Multi-Automata. Then, we
give an algorithm for single-indexed LTL model checking by computing fixpoint
of DCLICs. During the experiments, we compared our algorithm with an ap-
proach of translating SM-DPN into standard DPN and performing LTL model
checking on DPN, and the results show the efficiency of our approach. Finally,
we show how our model checking approach can be applied for detecting self-
modifying and concurrent malware.

## References

1. abuse.ch: Malwarebazaar (2025), https://bazaar.abuse.ch/about/

2. Álvarez, S.: The Official Radare2 Book. https://book.rada.re/credits/credits.html, accessed: 2025-01-15

3. Anckaert, B., Madou, M., De Bosschere, K.: A model for self-modifying code. In: IH 2006. pp. 232–248. Springer (2007)

4. Balakrishnan, G., Reps, T., Kidd, N., Lal, A., Lim, J., Melski, D., Gruian, R., Yong, S., Chen, C.H., Teitelbaum, T.: Model checking x86 executables with codesurfer/x86 and wpds++. In: CAV 2005. pp. 158–163. Springer (2005)

5. Bergeron, J., Debbabi, M., Desharnais, J., Erhioui, M.M., Lavoie, Y., Tawbi, N., et al.: Static detection of malicious code in executable programs. Int. J. of Req. Eng **2001**(184-189), 79 (2001)

6. Blazy, S., Laporte, V., Pichardie, D.: Verified abstract interpretation techniques for disassembling low-level self-modifying code. Journal of Automated Reasoning **56**, 283–308 (2016)

7. Bonfante, G., Marion, J.Y., Reynaud-Plantey, D.: A computability perspective on self-modifying programs. In: SEFM 2009. pp. 231–239. IEEE (2009)

8. Bouajjani, A., Müller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: CONCUR 2005. pp. 473–487. Springer (2005)
9. Cai, H., Shao, Z., Vaynberg, A.: Certified self-modifying code. In: ACM SIGPLAN PLDI'07. pp. 66–77 (2007)

10. Corvus Forensics: Virus share, https://virusshare.com/about

11. Dawei, S., Delong, L., Zhibin, Y.: Dynamic self-modifying code detection based on backward analysis. In: Proceedings of the 2018 10th International Conference on Computer and Automation Engineering. pp. 199–204 (2018)

12. Debray, S.K., Coogan, K.P., Townsend, G.M.: On the semantics of self-unpacking malware code. Citeseer, Tech. Rep. (2008)

13. Diaz, M., Touili, T.: Model checking dynamic pushdown networks with locks and priorities. In: NETYS 2018. pp. 240–251. Springer (2019)

14. Esparza, J., Kučera, A., Schwoon, S.: Model checking ltl with regular valuations for pushdown systems. Information and Computation 186(2), 355–376 (2003)

15. Hex-Rays: Ida pro. https://hex-rays.com/ida-pro, accessed: 2025-01-15

16. Kahlon, V., Gupta, A.: An automata-theoretic approach for model checking threads for ltl propert. In: LICS'06. pp. 101–110. IEEE (2006)

17. Kidd, N., Lammich, P., Touili, T., Reps, T.: A decision procedure for detecting atomicity violations for communicating processes with locks. International Journal on Software Tools for Technology Transfer 13(1), 37–60 (2011)

18. Kinder, J., Veith, H.: Jakstab: a static analysis platform for binaries: tool paper. In: CAV 2008. pp. 423–427. Springer (2008)

19. Messahel, W., Touili, T.: Reachability analysis of concurrent self-modifying code. In: International Conference on Engineering of Complex Computer Systems. pp. 257–271. Springer (2024)

20. Nguyen, H.V., Touili, T.: Caret analysis of multithreaded programs. In: LOPSTR 2017. pp. 73–90. Springer (2018)

21. Pommellet, A., Touili, T.: Ltl model checking for communicating concurrent programs. Innovations in Systems and Software Engineering 16(2), 161–179 (2020)

22. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: International conference on tools and algorithms for the construction and analysis of systems. pp. 93–107. Springer (2005)

23. Shoshitaishvili, Y., Wang, R., Salls, C., Stephens, N., Polino, M., Dutcher, A., Grosen, J., Feng, S., Hauser, C., Kruegel, C., et al.: Sok:(state of) the art of war: Offensive techniques in binary analysis. In: 2016 IEEE symposium on security and privacy (SP). pp. 138–157. IEEE (2016)

24. Song, F., Touili, T.: Efficient malware detection using model-checking. In: International Symposium on Formal Methods. pp. 418–433. Springer (2012)

25. Song, F., Touili, T.: Model checking dynamic pushdown networks. Formal Aspects of Computing 27, 397–421 (2015)

26. Touili, T., Ye, X.: Ltl model checking of self modifying code. Formal Methods in System Design 60(2), 195–227 (2022)

27. Touili, T., Zhangeldinov, O.: Ltl model checking of concurrent self modifying code (2025), https://www.irif.fr/_media/en/users/zhangeldinov/ltl_model_checking_smdpn.pdf

28. Ugarte-Pedrero, X., Balzarotti, D., Santos, I., Bringas, P.G.: Sok: Deep packer inspection: A longitudinal study of the complexity of run-time packers. In: 2015 IEEE Symposium on Security and Privacy. pp. 659–673. IEEE (2015)

29. Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs. In: ACM STOC'84. pp. 446–456 (1984)