Tayssir Touili

Xin Ye

LTL Model Checking of Self Modifying Code

Keywords: malware detection, model checking, automata

Self modifying code is code that can modify its own instructions during the execution of the program. It is extensively used by malware writers to obfuscate their malicious code. Thus, analysing self modifying code is nowadays a big challenge. In this paper, we consider the LTL model-checking problem of self modifying code. We model such programs using self-modifying pushdown systems (SM-PDS), an extension of pushdown systems that can modify its own set of transitions during execution. We reduce the LTL model-checking problem to the emptiness problem of self-modifying Büchi pushdown systems (SM-BPDS). We implemented our techniques in a tool that we successfully applied for the detection of several self-modifying malware. Our tool was also able to detect several malwares that well-known antiviruses such as BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Baidu, Avast, and Symantec failed to detect.

Introduction

Binary code presents several complex aspects that cannot be encountred in source code. One of these aspects is self-modifying code, i.e., code that can modify its own instructions during the execution of the program. Self-modifying code makes reverse code engineering harder. Thus, it is extensively used to protect software intellectual property. It is also heavily used by malware writers in order to make their malwares hard to analyse and detect by static analysers and anti-viruses. Thus, it is crucial to be able to analyse self-modifying code.

There are several kinds of self-modifying code. In this work, we consider self-modifying code caused by self-modifying instructions. These kind of instructions treat code as data. This allows them to read and write into code, leading to self-modifying instructions. These self-modifying instructions are usually mov instructions, since mov allows to access memory and read and write into it. Let us consider the example shown in Figure 1. For simplicity, the addresses' length is assumed to be 1 byte. In the right box, we give, respectively, the binary code, the addresses of the different instructions, and the corresponding assembly code, obtained by translating syntactically the binary code at each address. For example, 0c is the binary code of the jump jmp. Thus, 0c 02 is translated to jmp 0x2 (jump to address 0x2). The second line is translated to push 0x9, since ff is the binary code of the instruction push. The third instruction mov 0x2 0xc will replace the first byte at address 0x2 by 0xc. Thus, at address 0x2, ff 09 is replaced by 0c 09. This means the instruction push 0x9 is replaced by the jump instruction jmp 0x9 (jump to address 0x9), etc. Therefore, this code is self-modifying: the mov instruction was able to modify the instructions of the program via its ability to read and write the memory. If we study this code without looking at the semantics of the self-modifying instructions, we will extract from it the Control Flow Graph CFG a that is in the left of the figure, and we will reach the conclusion that the call to the API function CopyFileA at address 0x9 cannot be made. However, you can see that the correct CFG is the one on the right hand side CFG b, where the call to the API function CopyFileA at address 0x9 can be reached. Thus, it is very important to be able to take into account the semantics of the self-modifying instructions in binary code. In this paper, we consider the LTL model-checking problem of self-modifying code. To this aim, we use Self-Modifying Pushdown Systems (SM-PDSs) [START_REF] Touili | Reachability analysis of self modifying code[END_REF] to model self-modifying code. Indeed, SM-PDSs were shown in [START_REF] Touili | Reachability analysis of self modifying code[END_REF] to be an adequate model for self-modifying code since they allow to mimic the program's stack while taking into account the self-modifying semantics of the transitions. This is very important for binary code analysis and malware detection, since malwares are based on calls to API functions of the operating system. Thus, antiviruses check the API calls to determine whether a program is malicious or not. Therefore, to evade from these antiviruses, malware writers try to hide the API calls they make by replacing calls by push and jump instructions. Thus, to be able to analyse such malwares, it is crucial to be able to analyse the program's stack. Hence the need to a model like pushdown systems and selfmodifying pushdown systems for this purpose, since they allow to mimic the program's stack.

Intuitively, a SM-PDS is a pushdown system (PDS) with self-modifying rules, i.e., with rules that allow to modify the current set of transitions during execution. This model was introduced in [START_REF] Touili | Reachability analysis of self modifying code[END_REF] in order to represent self-modifying code. In [START_REF] Touili | Reachability analysis of self modifying code[END_REF], the authors have proposed algrithms to compute finite automata that accept the forward and backward reachability sets of SM-PDSs. In this work, we tackle the problem of LTL model-checking of SM-PDSs. Since SM-PDSs are equivalent to PDSs [START_REF] Touili | Reachability analysis of self modifying code[END_REF], one possible approach for LTL model checking of SM-PDS is to translate the SM-PDS to a standard PDS and then run the LTL model checking algorithm on the equivalent PDS [START_REF] Bouajjani | Reachability Analysis of Pushdown Automata: Application to Model Checking[END_REF][START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF]. But translation approach, these techniques [START_REF] Blazy | Verified abstract interpretation techniques for disassembling low-level self-modifying code[END_REF][START_REF] Roundy | Hybrid analysis and control of malware[END_REF] cannot handle the program's stack.

Unpacking binary code is also considered in [START_REF] Coogan | Automatic static unpacking of malware binaries[END_REF][START_REF] Gyung | Renovo: A hidden code extractor for packed executables[END_REF][START_REF] Royal | Polyunpack: Automating the hidden-code extraction of unpack-executing malware[END_REF][START_REF] Debray | On the semantics of self-unpacking malware code[END_REF]. These works do not consider self-modifying mov instructions.

Outline. The rest of the paper is structured as follows: Section 2 recalls the definition of Self Modifying pushdown systems. LTL model checking and SM-BPDSs are defined in Section 3. Section 4 solves the emptiness problem of SM-BPDS. Finally, the experiments are reported in Section 5.

Self-Modifying Pushdown Systems

Definition

We recall in this section the definition of Self-modifying Pushdown Systems [START_REF] Touili | Reachability analysis of self modifying code[END_REF].

Definition 1. A Self-modifying Pushdown System (SM-PDS) is a tuple P = (P, Γ, ∆, ∆ c ), where P is a finite set of control points, Γ is a finite set of stack symbols, ∆ ⊆ (P × Γ) × (P × Γ * ) is a finite set of transition rules, and Intuitively, a Self-modifying Pushdown System is a Pushdown System that can dynamically modify its set of rules during the execution time: rules ∆ are standard PDS transition rules, while rules ∆ c modify the current set of transition rules: ⟨p, γ⟩ → ⟨p ′ , w⟩ ∈ ∆ expresses that if the SM-PDS is in control point p and has γ on top of its stack, then it can move to control point p ′ , pop γ and push w onto the stack, while p (r1,r2) ----→ p ′ ∈ ∆ c expresses that when the PDS is in control point p, then it can move to control point p ′ , remove the rule r 1 from its current set of transition rules, and add the rule r 2 .

∆ c ⊆ P × (∆ ∪ ∆ c ) × (∆ ∪ ∆ c ) × P is
Formally, a configuration of a SM-PDS is a tuple c = (⟨p, w⟩, θ) where p ∈ P is the control point, w ∈ Γ * is the stack content, and θ ⊆ ∆ ∪ ∆ c is the current set of transition rules of the SM-PDS. θ is called the current phase of the SM-PDS. When the SM-PDS is a PDS, i.e., when ∆ c = ∅, a configuration is a tuple c = (⟨p, w⟩, ∆), since there is no changing rule, so there is only one possible phase. In this case, we can also write c = ⟨p, w⟩. Let C be the set of configurations of a SM-PDS. A SM-PDS defines a transition relation ⇒ P between configurations as follows: Let c = (⟨p, w⟩, θ) be a configuration, and let r be a rule in θ, then:

1. if r ∈ ∆ c is of the form r = p (r1,r2)
----→ p ′ , such that r 1 ∈ θ, then (⟨p, w⟩, θ) ⇒ P (⟨p ′ , w⟩, θ ′ ), where θ ′ = (θ\{r 1 })∪{r 2 }. In other words, the transition rule r updates the current set of transition rules θ by removing r 1 from it and adding r 2 to it. 2. if r ∈ ∆ is of the form r = ⟨p, γ⟩ → ⟨p ′ , w ′ ⟩ ∈ ∆, then (⟨p, γw⟩, θ) ⇒ P (⟨p ′ , w ′ w⟩, θ). In other words, the transition rule r moves the control point from p to p ′ , pops γ from the stack and pushes w ′ onto the stack. This transition keeps the current set of transition rules θ unchanged.

Let ⇒ * P be the transitive, reflexive closure of ⇒ P and ⇒ + P be its transitive closure. An execution (a run) of P is a sequence of configurations π = c 0 c 1 ... s.t. c i ⇒ P c i+1 for every i ≥ 0. Given a configuration c, the set of immediate predecessors (resp. successors) of c is pre P (c) = {c ′ ∈ C : c ′ ⇒ P c} (resp. post P (c) = {c ′ ∈ C : c ⇒ P c ′ }). These notations can be generalized straightforwardly to sets of configurations. Let pre * P (resp. post * P ) denote the reflexive-transitive closure of pre P (resp. post P ). We remove the subscript P when it is clear from the context. We suppose w.l.o.g. that rules in ∆ are of the form ⟨p, γ⟩ → ⟨p ′ , w⟩ such that |w| ≤ 2, and that the self-modifying rules r = p (r1,r2) ----→ p ′ in ∆ c are such that r ̸ = r 1 . Note that this is not a restriction, since for a given SM-PDS, one can compute an equivalent SM-PDS that satisfies these conditions [START_REF] Touili | Reachability analysis of self modifying code[END_REF] .

Example 1. Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS where

P = {p 1 , p 2 , p 3 , p 4 }, Γ = {γ 1 , γ 2 , γ 3 }, ∆ = {r 1 : ⟨p 1 , γ 1 ⟩ → ⟨p 2 , γ 2 γ 1 ⟩, r 2 : ⟨p 2 , γ 2 ⟩ → ⟨p 3 , ϵ⟩, r 3 : ⟨p 4 , γ 1 ⟩ → ⟨p 2 , γ 2 γ 3 ⟩}, ∆ c = {r ′ : p 3 (r1,r3) ----→ p 4 }. Let c 0 = (⟨p 1 , γ 1 γ 1 ⟩, θ 0 ) where θ 0 = {r 1 , r 2 , r ′ }. Applying rule r 1 , we get (⟨p 1 , γ 1 γ 1 ⟩, θ 0 ) ⇒ P (⟨p 2 , γ 2 γ 1 γ 1 ⟩, θ 0 ). Then, applying rule r 2 , we get (⟨p 2 , γ 2 γ 1 γ 1 ⟩, θ 0 ) ⇒ P (⟨p 3 , γ 1 γ 1 ⟩, θ 0 ). Then, applying rule r ′ , we get (⟨p 3 , γ 1 γ 1 ⟩, θ 0 ) ⇒ P (⟨p 4 , γ 1 γ 1 ⟩, θ 1 ) where r ′ is self- modifying, thus, it leads the SM-PDS from phase θ 0 = {r 1 , r 2 , r ′ } to phase θ 1 = θ 0 \ {r 1 } ∪ {r 3 } = {r 2 , r 3 , r ′ }. Then, applying rule r 3 , we get (⟨p 4 , γ 1 γ 1 ⟩, θ 1 ) ⇒ P (⟨p 2 , γ 2 γ 3 γ 1 ⟩, θ 1 ). Then, applying rule r 2 again, we get (⟨p 2 , γ 2 γ 3 γ 1 ⟩, θ 1 ) ⇒ P (⟨p 3 , γ 3 γ 1 ⟩, θ 1 ).

SM-PDS vs. PDS

Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS. It was shown in [START_REF] Touili | Reachability analysis of self modifying code[END_REF] that:

1. P can be described by an equivalent pushdown system (PDS). Indeed, since the number of phases is finite, we can encode phases in the control point of the PDS. However, this translation is not efficient since the number of control points of the equivalent PDS is |P | • 2 O(|∆|+|∆c|) . 2. P can also be described by an equivalent Symbolic pushdown system [START_REF] Schwoon | Model-checking pushdown systems[END_REF],

where each SM-PDS rule is represented by a single, symbolic transition, where the different values of the phases are encoded in a symbolic way using relations between phases. This translation is not efficient neither since the size of the relations used in the symbolic transitions is 2 O(|∆|+|∆c|) .

Modeling self-modifying code with SM-PDSs 2.3.1. Self-modifying instructions

There are different techniques to implement self-modifying code. We consider in this work code that uses self-modifying instructions. These are instructions that can access the memory locations and write onto them, thus changing the instructions that are in these memory locations. In assembly, the only instructions that can do this are the mov instructions. In this case, the self-modifying instructions are of the form mov l v, where l is a location of the program that stores executable data and v is a value. This instruction replaces the value at location l (in the binary code) with the value v. This means if at location l there is a binary value v ′ that is involved in an assembly instruction i 1 , and if by replacing v ′ by v, we obtain a new assembly instruction i 2 , then the instruction i 1 is replaced by i 2 . E.g., ff is the binary code of push, 40 is the binary code of inc, 0c is the binary code of jmp, c6 is the binary code of mov, etc. Thus, if we have mov l ff, and if at location l there was initially the value 40 01 (which corresponds to the assembly instruction inc %edx), then 40 is replaced by ff, which means the instruction inc %edx is replaced by push 01. If at location l there was initially the value c6 01 02 (which corresponds to the assembly instruction mov edx 0x2), then c6 is replaced by ff, which means the instruction mov edx 0x2 is replaced by push 02.

Note that if the instructions i 1 and i 2 do not have the same number of operands, then mov l v will, in addition to replacing i 1 by i 2 , change several other instructions that follow i 1 . Currently, we cannot handle this case, thus we assume that i 1 and i 2 have the same number of operands.

Note also that mov l v is self-modifying only if l is a location of the program that stores executable data, otherwise, it is not; e.g., mov eax v does not change the instructions of the program, it just writes the value v to the register eax. Thus, from now on, by self-modifying instruction, we mean an instruction of the form mov l v, where l is a location of the program that stores executable data.

Moreover, to ensure that only one instruction is modified, we assume that the corresponding instructions i 1 and i 2 have the same number of operands.

From self-modifying code to SM-PDS

We show in what follows how to build a SM-PDS from a binary program. We suppose we are given an oracle O that extracts from the binary code a corresponding assembly program, together with informations about the values of the registers and the memory locations at each control point of the program. In our implementation, we use Jakstab [START_REF] Kinder | Jakstab: A static analysis platform for binaries[END_REF] to get this oracle. We translate the assembly program into a self-modifying pushdown system where the control locations store the control points of the binary program and the stack memics the program's stack. The non self-modifying instructions of the program define the rules ∆ of the SM-PDS (which are standard PDS rules), and can be obtained following the translation of [START_REF] Song | Efficient malware detection using model-checking[END_REF] that models non self-modifying instructions of the program by a PDS.

As for the self-modifying instructions of the program, they define the set of changing rules ∆ c . As explained above, these are instructions of the form mov l v, where l is a location of the program that stores executable data. This instruction replaces the value at location l (in the binary code) with the value v. Let i 1 be the initial instruction involving the location l, and let i 2 be the new instruction involving the location l, after applying the mov l v instruction.

As mentioned previously, we assume that i 1 and i 2 have the same number of operands (to ensure that only one instruction is modified). Let r 1 (resp. r 2 ) be the SM-PDS rule corresponding to the instruction i 1 (resp. i 2 ). Suppose from control point n to n ′ , we have this mov l v instruction, then we add n (r1,r2)

----→ n ′ to ∆ c . This is the SM-PDS rule corresponding to the instruction mov l v at control point n.

LTL Model-Checking of SM-PDSs

The linear-time temporal logic LTL

Let At be a finite set of atomic propositions. LTL formulas are defined as follows (where A ∈ At):

φ := A | ¬φ | φ 1 ∨ φ 2 | Xφ | φ 1 U φ 2
Formulae are interpreted on infinite words over 2 At . Let ω = ω 0 ω 1 ... be an infinite word over 2 At . We write ω i for the suffix of ω starting at ω i . We denote ω |= φ to express that ω satisfies a formula φ:

ω |= A ⇐⇒ A ∈ ω 0 ω |= ¬φ ⇐⇒ ω ⊭ φ ω |= φ 1 ∨φ 2 ⇐⇒ ω |= φ 1 or ω |= φ 2 ω |= Xφ ⇐⇒ ω 1 |= φ ω |= φ 1 U φ 2 ⇐⇒ ∃i ≥ 0, ω i |= φ 2 and ∀0 ≤ j < i, ω j |= φ 1
The temporal operators G (globally) and F (eventually) are defined as follows: F φ = (A ∨ ¬A)U φ and Gφ = ¬F ¬φ. Let W (φ) be the set of infinite words that satisfy an LTL formula φ. It is well known that W (φ) can be accepted by Büchi automata:

Definition 2. A Büchi automaton B is a quintuple (Q, Γ, η, q 0 , F ) where Q is a finite set of states, Γ is a finite input alphabet, η ⊆ (Q × Γ × Q) is a set of transitions, q 0 ∈
Q is the initial state and F ⊆ Q is the set of accepting states. A run of B on a word γ 0 γ 1 ... ∈ Γ ω is a sequence of states q 0 q 1 q 2 ... s.t. ∀i ≥ 0, (q i , γ i , q i+1 ) ∈ η. An infinite word ω is accepted by B if B has a run on ω that starts at q 0 and visits accepting states from F infinitely often.

Theorem. [START_REF] Vardi | Reasoning about infinite computations[END_REF] Given an LTL formula φ, one can effectively construct a Büchi automaton B φ which accepts W (φ).

Self Modifying Büchi Pushdown Systems Definition 3. A Self Modifying Büchi Pushdown Systems (SM-BPDS) is a

tuple BP = (P, Γ, ∆, ∆ c , G) where P is a set of control locations, G ⊆ P is a set of accepting control locations, ∆ ⊆ (P × Γ) × (P × Γ * ) is a finite set of transition rules, and ∆ c ⊆ P × 2 ∆∪∆c × 2 ∆∪∆c × P is a finite set of modifying transition rules of the form p

(σ,σ ′ ) ----→ p ′ where σ, σ ′ ⊆ ∆ ∪ ∆ c .
Let ⇒ BP be the transition relation between configurations as follows: Let

θ ⊆ ∆ ∪ ∆ c , γ ∈ Γ, w ∈ Γ * , and p ∈ P , then 1. If r : ⟨p, γ⟩ → ⟨p ′ , w ′ ⟩ ∈ ∆ and r ∈ θ, then (⟨p, γw⟩, θ) ⇒ BP (⟨p ′ , w ′ w⟩, θ). 2. If r : p (σ,σ ′ ) ----→ p ′ ∈ ∆ c , σ ∩ θ ̸ = ∅ and r ∈ θ, then (⟨p, γw⟩, θ) ⇒ BP (⟨p ′ , γw⟩, θ ′ ) where θ ′ = θ\σ ∪ σ ′ . A run π of BP is a sequence of configurations π = c 0 c 1 ... s.t. c i ⇒ BP c i+1
for every i ≥ 0. π is accepting iff it infinitely often visits configurations having control locations in G.

Let c and c ′ be two configurations of the SM-BPDS BP. We assume w.l.o.g. that for every rule in ∆ c of the form r : p

(σ,σ ′ ) ----→ p ′ , r /
∈ σ. Note that this is not a restriction since a rule of the form r = p

(σ,σ ′ )
----→ p ′ where r ∈ σ can be simulated by a set of rules that satisfy the above condition.

From LTL Model-Checking of SM-PDSs to the emptiness problem of SM-BPDSs

Let P = (P, Γ, ∆, ∆ c ) be a self modifying pushdown system. Let At be a set of atomic propositions. Let ν : P → 2 At be a labelling function. Let π = (⟨p 0 , w 0 ⟩, θ 0 )(⟨p 1 , w 1 ⟩, θ 1 )... be an execution of the SM-PDS P. Let φ be an LTL formula over the set of atomic propositions At. We say that

π |= ν φ iff ν(p 0 )ν(p 1 ) • • • |= φ
Let (⟨p, w⟩, θ) be a configuration of P. We say that (⟨p, w⟩, θ) |= ν φ iff P has an execution π starting at (⟨p, w⟩, θ) such that π |= ν φ.

Our goal in this paper is to perform LTL model-checking for self-modifying pushdown systems. Since SM-PDSs can be translated to standard (symbolic) pushdown systems, one way to solve this LTL model-checking problem is to compute the (symbolic) pushdown system that is equivalent to the SM-PDS (see section 2.2), and then apply the standard LTL model-checking algorithms on standard PDSs [START_REF] Schwoon | Model-checking pushdown systems[END_REF]. However, this approach is not efficient (as will be witnessed later in the experiments). Thus, we need a direct approach that performs LTL model-checking on the SM-PDS, without translating it to an equivalent PDS. Let B φ = (Q, 2 At , η, q 0 , F ) be a Büchi automaton that accepts W (φ). We compute the SM-BPDS BP φ = (P × Q, Γ, ∆ ′ , ∆ ′ c , G) by performing a kind of product between the SM-PDS P and the Büchi automaton B φ as follows:

1. if r = ⟨p, γ⟩ → ⟨p ′ , w⟩ ∈ ∆ and (q, ν(p), q ′ ) ∈ η, then ⟨(p, q), γ⟩ → ⟨(p ′ , q ′ ), w⟩ ∈ ∆ ′ . Let prod(r) be the set of rules of ∆ ′ obtained from the rule r, i.e., rules of ∆ ′ of the form ⟨(p, q), γ⟩ → ⟨(p ′ , q ′ ), w⟩.

2. if a rule r = p (r1,r2) ----→ p ′ ∈ ∆ c and (q, ν(p), q ′ ) ∈ η, then (p, q) (σ,σ ′ ) ----→ (p ′ , q ′ ) ∈ ∆ ′
c where σ = prod(r 1 ), σ ′ = prod(r 2 ). Let prod(r) be the set of rules of ∆ ′ obtained from the rule r, i.e., rules of ∆ ′ c of the form

(p, q) (σ,σ ′ ) ----→ (p ′ , q ′ ). 3. G = P × F . Remark. Note that a rule r = p (r1,r2) ----→ p ′ ∈ ∆ c generates rules of the form (p, q) (σ,σ ′ ) ----→ (p ′ , q ′ ) ∈ ∆ ′ c
, where σ = prod(r 1 ) and σ ′ = prod(r 2 ) are sets of rules. This is why we require that a Self Modifying Büchi Pushdown System has modifying transition rules of the form p (σ,σ ′ ) ----→ p ′ where σ, σ ′ ⊆ ∆ ∪ ∆ c are sets of rules.

We can show that: Theorem 3.1. Let (⟨p, w⟩, θ) be a configuration of the SM-PDS P. (⟨p, w⟩, θ) |= ν φ iff BP φ has an accepting run from (⟨(p, q 0 ), w⟩, prod(θ)) where prod(θ) is the set of rules of ∆ ∪ ∆ c obtained from the rules of θ as described above.

Thus, LTL model-checking for SM-PDSs can be reduced to checking whether a SM-BPDS has an accepting run. The rest of the paper is devoted to this problem.

The Emptiness Problem of SM-BPDSs

From now on, we fix a SM-BPDS BP = (P, Γ, ∆, ∆ c , G). Following [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF], we can show that BP has an accepting run starting from a configuration c if and only if from c, it can reach a configuration with a repeating head: Proposition 1. A SM-BPDS BP has an accepting run starting from a configuration c if and only if there exists a repeating head ((p, γ), θ) such that c ⇒ * BP (⟨p, γw⟩, θ) for some w ∈ Γ * . Proof: " ⇒ ": Let σ = c 0 c 1 ... be an accepting run starting at configuration c where c 0 = c and c i = (⟨p i , w i ⟩, θ i ). We construct an increasing sequence of indices i 0 , i 1 ... with a property that once any of the configurations c i k is reached, the rest of the run never changes the bottom |w i k |-1 elements of the stack anymore. This property can be written as follows:

|w i0 |= min{|w j | | j ≥ 0} |w i k |= min{|w j | | j > i k-1 }, k ≥ 1
Because BP has only finitely many different heads, there must be a head (⟨p, γ⟩, θ) which occurs infinitely often as a head in the sequence c i0 c i1 .... Moreover, as some g ∈ G becomes a control location infinitely often, we can find a subsequence of indices i j0 , i j1 , ... with the following property: for every k

≥ 1, there exist v, w ∈ Γ * c ij k = (⟨p, γw⟩, θ) ⇒ r (⟨p, γvw⟩, θ) = c ij k+1
Because w is never looked at or changed in this path, we can have (⟨p, γ⟩, θ) ⇒ r (⟨p, γv⟩, θ). This proves this direction of the proposition.

" ⇐ ": Because (⟨p, γ⟩, θ) is a repeating head, we can construct the following run for some u, v, w

∈ Γ * , θ ′ ⊆ (∆ ∪ ∆ c ) and g ∈ G: c ⇒ * (⟨p, γw⟩, θ) ⇒ * (⟨g, uw⟩, θ ′ ) ⇒ + (⟨p, γvw⟩, θ) ⇒ * (⟨g, uvw⟩, θ ′ ) ⇒ + (⟨p, γvvw⟩, θ) ⇒ * ...
Since g occurs infinitely often, the run is accepting. 2

Thus, since there exists an efficient algorithm to compute the pre * of SM-PDSs [START_REF] Touili | Reachability analysis of self modifying code[END_REF], the emptiness problem of a SM-BPDS can be reduced to computing its repeating heads.

The Head Reachability Graph G

Our goal is to compute the set of repeating heads Rep BP , i.e., the set of heads (⟨p, γ⟩, θ) such that there exists v ∈ Γ * , (⟨p, γ⟩, θ) ⇒ r (⟨p, γv⟩, θ). I.e., (⟨p, γ⟩, θ) ⇒ * (⟨p, γv⟩, θ) s.t. this path goes through an accepting location in G.

To this aim, we will compute a finite graph G whose nodes are the heads of BP of the form ((p, γ), θ), where p ∈ P , γ ∈ Γ and θ ⊆ ∆ ∪ ∆ c ; and whose edges encode the reachability relation between these heads. More precisely, given two heads ((p, γ), θ) and ((p

′ , γ ′ ), θ ′ ), ((p, γ), θ) b -→ ((p ′ , γ ′ ), θ ′
) is an edge of the graph G means that the configuration (⟨p, γ⟩, θ) can reach a configuration having (⟨p ′ , γ ′ ⟩, θ ′ ) as head, i.e., it means that there exists v ∈ Γ * s.t. (⟨p, γ⟩, θ) ⇒ * (⟨p ′ , γ ′ v⟩, θ ′ ). Moreover, we need to keep the information whether this path visits an accepting location in G or not. This information is recorded in the label of the edge b: b = 1 means that the path visits an accepting location in G, i.e. that (⟨p, γ⟩, θ) ⇒ r (⟨p ′ , γ ′ v⟩, θ ′ ). Otherwise, b = 0. Therefore, if the graph G contains a loop from a head ((p, γ), θ) to itself such that this loop goes through an edge labelled by 1, then ((p, γ), θ) is a repeating head. Thus, computing Rep BP can be reduced to computing the graph G and finding 1-labelled loops in this graph.

More precisely, we define the head reachability graph G as follows:

Definition 4. The head reachability graph G is a tuple (P ×Γ×2 ∆∪∆c , {0, 1}, δ) such that ((p, γ), θ) b - → ((p ′ , γ ′ ), θ ′ ) is an edge of δ iff:
1. there exists a transition r c : p

(σ,σ ′ ) ----→ p ′ ∈ θ ∩ ∆ c , γ = γ ′ , θ ′ = θ \ σ ∪ σ ′ , and b = 1 iff p ∈ G; 2. there exists a transition ⟨p, γ⟩ → ⟨p ′ , γ ′ ⟩ ∈ θ ∩ ∆, θ = θ ′ and b = 1 iff p ∈ G; 3. there exists a transition ⟨p, γ⟩ → ⟨p ′′ , γ 1 γ ′ ⟩ ∈ θ ∩ ∆, for γ 1 ∈ Γ, p ′′ ∈ P , s.t. (⟨p ′′ , γ 1 ⟩, θ) ⇒ * BP (⟨p ′ , ϵ⟩, θ ′ ), and b = 1 iff p ∈ G or (⟨p ′′ , γ 1 ⟩, θ) ⇒ r BP (⟨p ′ , ϵ⟩, θ ′ )
Let G be the head reachability graph. We define -→ i as follows: let ((p, γ), θ) and ((p ′ , γ ′ ), θ ′ ) be two heads of BP. We write

((p, γ), θ) - → i ((p ′ , γ ′ ), θ ′ ) iff ∃ booleans b 1 , b 2 ...b i ∈ {0, 1}, ∃ heads ((p j , γ j ), θ j ), 0 ≤ j ≤ i s.t. G contains the path ((p 0 , γ 0 ), θ 0 ) b1 -→ ((p 1 , γ 1 ), θ 1 ) b2 -→ ... bi -→ ((p i , γ i ), θ i ) where ((p 0 , γ 0 ), θ 0 ) = ((p, γ), θ) and ((p i , γ i ), θ i ) = ((p ′ , γ ′ ), θ ′ ).
Let → * be the reflexive transitive closure of the graph relation b -→, and let → r be defined as follows: Given two heads ((p, γ), θ) and

((p ′ , γ ′ ), θ ′ ), ((p, γ), θ) → r ((p ′ , γ ′ ), θ ′ ) iff there is in G a path between ((p, γ), θ) and ((p ′ , γ ′ ), θ ′ ) that goes through a 1-labelled edge, i.e., iff there exist heads ((p 1 , γ 1 ), θ 1 ) and ((p 2 , γ 2 ), θ 2 ) s.t. ((p, γ), θ) → * ((p 1 , γ 1 ), θ 1 ) 1 -→ ((p 2 , γ 2 ), θ 2 ) → * ((p ′ , γ ′ ), θ ′ ).
We can show that: Theorem 4.1. Let BP = (P, Γ, ∆, ∆ c , G) be a self-modifying Büchi pushdown system, and let G be its corresponding head reachability graph. A head ((p, γ), θ) of BP is repeating iff G has a loop on the node ((p, γ), θ) that goes through a 1-labeled edge.

To prove this theorem, we first need to prove the following lemma: Lemma 1. The relations → * and → r have the following properties: For any heads ((p, γ), θ 1 ) and ((p ′ , γ ′ ), θ 2 ):

(a) ((p, γ), θ 1 ) → * ((p ′ , γ ′ ), θ 2 ) iff (⟨p, γ⟩, θ 1 ) ⇒ * (⟨p ′ , γ ′ v⟩, θ 2 ) for some v ∈ Γ * . (b) ((p, γ), θ 1 ) → r ((p ′ , γ ′ ), θ 2 ) iff (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ) for some v ∈ Γ * . Proof: "⇒": Assume ((p, γ), θ 1 ) -→ i ((p ′ , γ ′ ), θ 2 )
. We proceed by induction on i.

(a) Basis. i = 0. In this case, ((p, γ), θ 1 ) = ((p ′ , γ ′ ), θ 2 ), then we can get (⟨p, γ⟩, θ 1 ) ⇒ * (⟨p, γ⟩, θ 1 ) = (⟨p ′ , γ ′ ⟩, θ 2 )
Step. i > 0. Then there exist

p 1 ∈ P, γ ′′ ∈ Γ * and θ ′ ⊆ ∆ ∪ ∆ c such that ((p, γ), θ 1 ) -→ 1 ((p 1 , γ ′′ ), θ ′ ) --→ i-1 ((p ′ , γ ′ ), θ 2 ). From the induction hypothesis, there exists u ∈ Γ * such that (⟨p 1 , γ ′′ ⟩, θ ′ ) ⇒ * (⟨p ′ , γ ′ u⟩, θ 2 ) Since ((p, γ), θ 1 ) → ((p 1 , γ ′′ ), θ ′ ), we have (⟨p, γ⟩, θ 1 ) ⇒ * (⟨p 1 , γ ′′ w⟩, θ ′ ) for w ∈ Γ * , hence (⟨p, γ⟩, θ 1 ) ⇒ * (⟨p ′ , γ ′ uw⟩, θ 2 ).
The property holds.

(b) ((p, γ), θ 1 ) → r ((p, γ), θ 1 ) cannot hold for the case i = 0.

Basis. i = 1. In this case, ((p, γ), θ 1 ) → r ((p ′ , γ ′ ), θ 2 ), then we can get p ∈ G and (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p ′ , γ ′ ⟩, θ 2 )
. The property holds.

Step. i > 0. As done in the proof of part (a) of this lemma, there exists

p 1 , γ ′′ ∈ Γ, θ ′′ ⊆ ∆ ∪ ∆ c s.t. ((p, γ), θ 1 ) -→ 1 ((p 1 , γ ′′ ), θ ′ ) --→ i-1 ((p ′ , γ ′ ), θ 2 ). Then if ((p, γ), θ 1 ) → r ((p ′ , γ ′ ), θ 2 ), either ((p 1 , γ ′′ ), θ ′ ) → r ((p ′ , γ ′ ), θ 2 ) or ((p, γ), θ 1 ) 1 -→ ((p 1 , γ ′′ ), θ ′ ) holds. In the first case i.e. ((p 1 , γ ′′ ), θ ′ ) → r ((p ′ , γ ′ ), θ 2 )
, by the induction hypothesis, we can have (⟨p

1 , γ ′′ ⟩, θ ′ ) ⇒ r (⟨p ′ , γ ′ u⟩, θ 2 ), hence, (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p ′ , γ ′ u⟩, θ 2 ) holds
The second case depends on the rule applied to get ((p, γ), θ 1 )

1 -→ ((p 1 , γ ′′ ), θ ′ ) according to Definition 4.
-If this edge corresponds to a transition r c : p

(σ,σ ′ ) ----→ p 1 ∈ θ 1 , then γ = γ ′′ , θ ′ = θ 1 \σ ∪ σ ′ and p ∈ G. Since we can obtain (⟨p, γ⟩, θ 1 ) ⇒ BP (⟨p 1 , γ⟩, θ ′ ) ⇒ * (⟨p ′ , γ ′ uw⟩, θ 2 ) from part (a) and p ∈ G, then (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p 1 , γ⟩, θ ′ ) ⇒ * (⟨p ′ , γ ′ uw⟩, θ 2 ). This implies that (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ) for some v ∈ Γ * .
-If this edge corresponds to a transition r :

⟨p, γ⟩ → ⟨p 1 , γ ′′ ⟩ ∈ θ 1 ∩ ∆, then θ ′ = θ 1 and p ∈ G. Since we can obtain (⟨p, γ⟩, θ 1 ) ⇒ BP (⟨p 1 , γ ′′ ⟩, θ 1 ) ⇒ * (⟨p ′ , γ ′ uw⟩, θ 2 ) from part (a) and p ∈ G, then (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p 1 , γ ′′ ⟩, θ 1 ) ⇒ * (⟨p ′ , γ ′ uw⟩, θ 2 ). This implies that (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ) for some v ∈ Γ * .
-If this edge corresponds to a transition r : ⟨p, γ⟩ → ⟨p ′′

, γ 1 γ ′′ ⟩ ∈ θ 1 , then either p ∈ G or (⟨p ′′ , γ 1 ⟩, θ 1 ) ⇒ r (⟨p 1 , ϵ⟩, θ ′ ) holds. If p ∈ G, then we have (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p ′′ , γ 1 γ ′′ ⟩, θ 1 ). Otherwise, (⟨p ′′ , v 1 γ ′′ w⟩, θ 1 ) ⇒ r (⟨p 1 , γ ′′ w⟩, θ ′ ). Since we can obtain (⟨p 1 , γ ′′ ⟩, θ ′ ) ⇒ * (⟨p ′ , γ ′ u⟩, θ 2 ) from part (a). Therefore, (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p 1 , γ ′′ ⟩, θ ′ ) ⇒ * (⟨p ′ , γ ′ u⟩, θ 2 ). This implies that (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ) for some v ∈ Γ * . '⇐": Assume (⟨p, γ⟩, θ 1 ) i ⇒ (⟨p ′ , γ ′ v⟩, θ 2 )
. We proceed by induction on i.

(a) Basis. i = 0. In this case, v = ϵ and (⟨p, γ⟩, θ 1 ) = (⟨p ′ , γ ′ ⟩, θ 2 ), then ((p, γ), θ 1 ) → * ((p ′ , γ ′ ), θ 2 ) holds.
Step. i > 0. Then there exist

p 1 ∈ P, u ∈ Γ * and θ ′ ⊆ ∆ ∪ ∆ c such that (⟨p, γ⟩, θ 1 ) 1 ⇒ (⟨p 1 , u⟩, θ ′ ) i-1 ⇒ (⟨p ′ , γ ′ v⟩, θ 2 ).
There are 2 cases:

1. Case θ ′ = θ 1 : There must exist a rule r : ⟨p, γ⟩ → ⟨p 1 , u⟩ ∈ ∆ such that r ∈ θ ′ and |u| ≥ 1. Let l denote the minimal length of the stack on the path from (⟨p 1 , u⟩, θ 1 ) to (⟨p ′ , γ ′ v⟩, θ 2 ). Then u can be written as u ′′ γ 1 u ′ where |u ′ | = l -1 (that means u ′ will remain on the stack for the path). Furthermore, there exists p ′′′ such that (⟨p

1 , u ′′ ⟩, θ 1 ) ⇒ * (⟨p ′′′ , ϵ⟩, θ ′′ ) for some θ ′′ ⊆ (∆ c ∪ ∆). We have (⟨p, γ⟩, θ 1 ) k ⇒ (⟨p ′′′ , γ 1 u ′ ⟩, θ ′′ ) for k < i.
By the induction on i, we have ((p, γ), θ 1 ) → * ((p ′′′ , γ 1 ), θ ′′ ). Because u ′ has to remain on the stack for the rest of the path, v is of the form

v ′ u ′ for some v ′ ∈ Γ * . That means (⟨p ′′′ , γ 1 ⟩, θ ′′ ) j ⇒ (⟨p ′ , γ ′ v ′ ⟩, θ 2 ) for j < i.
By the induction hypothesis, ((p ′′′ , γ 1 ), θ ′′ ) → * ((p ′ , γ ′ ), θ 2 ) holds. Moreover, we have ((p, γ), θ 1 ) → * ((p ′′′ , γ 1 ), θ ′′ ), hence ((p, γ), θ 1 ) → * ((p ′ , γ ′ ), θ 2 ).

2. Case θ ′ ̸ = θ 1 : There must be a rule r c : p

(σ,σ ′ ) ----→ p 1 ∈ ∆ c such that r c ∈ θ 1 and σ ∩ θ 1 ̸ = ∅, then θ ′ = θ 1 \ σ ∪ σ ′ .
After the execution of r c , the content of the stack will remain the same, thus, u = γ. Then (⟨p, γ⟩, θ 1 )

1 ⇒ (⟨p 1 , γ⟩, θ ′ ) i-1 ⇒ (⟨p ′ , γ ′ v⟩, θ 2 ). By the induction hypothesis to (⟨p 1 , γ⟩, θ ′ ) i-1 ⇒ (⟨p ′ , γ ′ v⟩, θ 2 ), we can obtain that ((p 1 , γ), θ ′ ) → * ((p ′ , γ ′ ), θ 2 ). Since (⟨p, γ⟩, θ 1 ) 1 ⇒ (⟨p 1 , γ⟩, θ ′ ), then we can have a path ((p, γ), θ 1 ) → ((p 1 , γ), θ ′ ) → * ((p ′ , γ ′ ), θ 2 ) that implies ((p, γ), θ 1 ) → * ((p ′ , γ ′ ), θ 2 ). The property holds. (b) (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p, γ ′ v⟩, θ 1 ) is impossible in 0 steps. Basis. i = 1. (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p, γ⟩, θ 1 ), then p ∈ G. Thus, ((p, γ), θ 1 ) → r ((p, γ), θ 1 ) holds.
Step. i > 1. (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ) holds, then there exist

p 1 ∈ P, u ∈ Γ * and θ ′ ⊆ ∆ ∪ ∆ c such that (⟨p, γ⟩, θ 1 ) 1 ⇒ (⟨p 1 , u⟩, θ ′ ) i-1 ⇒ (⟨p ′ , γ ′ v⟩, θ 2 ). Thus, either (⟨p, γ⟩, θ 1 ) ⇒ r (⟨p 1 , u⟩, θ ′ ) or (⟨p 1 , u⟩, θ ′ ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ) holds.
The first case implies p ∈ G. There are 2 cases:

1. Case θ ′ = θ 1 : then as in the previous proof of part (a), we can have a path ((p, γ), θ 1 ) → * ((p ′′′ , γ 1 ), θ ′′ ) → * ((p ′ , γ ′ ), θ 2 ). Since p ∈ G, we get by Definition 4 ((p, γ), θ 1 ) → * ((p ′′′ , γ 1 ), θ ′′ ) → * ((p ′ , γ ′ ), θ 2 ). Thus, we have that ((p, γ), θ 1 ) → r ((p ′ , γ ′ ), θ 2 ). The property holds. 2. Case θ ′ ̸ = θ 1 : then as in the previous proof of part (a), we can have

a path ((p, γ), θ 1 ) → ((p 1 , γ), θ ′ ) → * ((p ′ , γ ′ ), θ 2 ). Since p ∈ G, we get ((p, γ), θ 1 ) 1 -→ ((p 1 , γ), θ ′ ) → * ((p ′ , γ ′ ), θ 2 )
. Thus, we have that ((p, γ), θ 1 ) → r ((p ′ , γ ′ ), θ 2 ). The property holds.

In the second case, (⟨p 1 , u⟩, θ ′ ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ) holds. As previously, there are 2 cases:

1. Case θ ′ = θ 1 : then as in case (a) we have (⟨p 1 , u⟩, θ 1 ) ⇒ * (⟨p ′′′ , γ 1 u ′ ⟩, θ ′′ ) and (⟨p ′′′ , γ 1 ⟩, θ ′′ ) ⇒ * (⟨p ′ , γ ′ v ′ ⟩, θ 2 ). If (⟨p 1 , u⟩, θ 1 ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ), then either (⟨p 1 , u⟩, θ 1 ) ⇒ r (⟨p ′′′ , γ 1 u ′ ⟩, θ ′′ ) or (⟨p ′′′ , γ 1 ⟩, θ ′′ ) ⇒ r (⟨p ′ , γ ′ v ′ ⟩, θ 2 ). -If (⟨p 1 , u⟩, θ 1 ) ⇒ r (⟨p ′′′ , γ 1 u ′ ⟩, θ ′′ ), let u ′′ ∈ Γ * s.t. u = u ′′ γ 1 u ′ and (⟨p 1 , u ′′ ⟩, θ 1 ) ⇒ r (⟨p ′′′ , ϵ⟩, θ ′′ ), then, we have ((p, γ), θ 1 ) → r ((p ′′′ , γ 1 ), θ ′′ ). We have (⟨p, γ⟩, θ 1 ) k ⇒ (⟨p ′′′ , γ 1 u ′ ⟩, θ ′′ ) for k < i.
By the induction on i, we have ((p, γ), θ 1 ) → * ((p ′′′ , γ 1 ), θ ′′ ). Because u ′ has to remain on the stack for the rest of the path, v

is of the form v ′ u ′ for some v ′ ∈ Γ * . That means (⟨p ′′′ , γ 1 ⟩, θ ′′ ) j ⇒ (⟨p ′ , γ ′ v ′ ⟩, θ 2 ) for j < i. By the induction hypothesis, ((p ′′′ , γ 1 ), θ ′′ ) → * ((p ′ , γ ′ ), θ 2 ) holds. Moreover, we have ((p, γ), θ 1 ) → * ((p ′′′ , γ 1 ), θ ′′ ), hence ((p, γ), θ 1 ) → * ((p ′ , γ ′ ), θ 2 ). So we can have a path ((p, γ), θ 1 ) → * ((p ′′′ , γ 1 ), θ ′′ ) → * ((p ′ , γ ′ ), θ 2 ), thus we have that ((p, γ), θ 1 ) → r ((p ′ , γ ′ ), θ 2 ); -If (⟨p ′′′ , γ 1 ⟩, θ ′′ ) ⇒ r (⟨p ′ , γ ′ v ′ ⟩, θ 2 )
, then by the induction hypothesis we have ((p ′′′ , γ 1 ), θ ′′ ) → r ((p ′ , γ ′ ), θ 2 ). Thus, we can have a path ((p, γ), θ 1 ) → * ((p ′′′ , γ 1 ), θ ′′ ) → * ((p ′ , γ ′ ), θ 2 ), then we have that ((p, γ), θ 1 ) → r ((p ′ , γ ′ ), θ 2 ); 2. Case θ ′ ̸ = θ 1 : then (⟨p 1 , γ⟩, θ ′ ) ⇒ r (⟨p ′ , γ ′ v⟩, θ 2 ). By the induction hypothesis we have ((p 1 , γ), θ ′ ) → r ((p ′ , γ ′ ), θ 2 ). Since (⟨p, γ⟩, θ 1 )

1 ⇒ (⟨p 1 , γ⟩, θ ′ ) i-1 ⇒ (⟨p ′ , γ ′ v⟩, θ 2 ). By the induction hypothesis to (⟨p 1 , γ⟩, θ ′ ) i-1 ⇒ (⟨p ′ , γ ′ v⟩, θ 2 ), we can obtain that ((p 1 , γ), θ ′ ) → * ((p ′ , γ ′ ), θ 2 ). Since (⟨p, γ⟩, θ 1 ) 1 ⇒ (⟨p 1 , γ⟩, θ ′ ), then we can have a path ((p, γ), θ 1 ) → ((p 1 , γ), θ ′ ) → * ((p ′ , γ ′ ), θ 2 ).
Thus, we have that ((p, γ), θ 1 ) → r ((p ′ , γ ′ ), θ 2 ); Thus, the property holds.

Proof of Theorem 4.1

We can now prove Theorem 4.1. Proof: Let ((p, γ), θ) be a repeating head, then there exists some v ∈ Γ * , θ ⊆ ∆ c ∪ ∆ such that (⟨p, γ⟩, θ) ⇒ r (⟨p, γv⟩, θ). By Lemma 1, this is the case if and only if ((p, γ), θ) → r ((p, γ), θ). From the definition of → r , that means that there exist heads ((p 1 , γ 1 ), θ ′ ) and ((p 2 , γ 2 ), θ ′′ ) such that ((p, γ), θ)

→ * ((p 1 , γ 1 ), θ ′ ) 1 -→ ((p 2 , γ 2 ), θ ′′ ) → * ((p, γ), θ
). Then ((p, γ), θ), ((p 1 , γ 1 ), θ ′ ) and ((p 2 , γ 2 ), θ ′′ ) are all in the same loop with a 1-labelled edge. Conversely, whenever ((p, γ), θ) is in a component with such an edge, ((p, γ), θ) → r ((p, γ), θ) holds, then Lemma 1 implies that (⟨p, γ⟩, θ) ⇒ r (⟨p, γv⟩, θ) which means that ((p, γ), θ) is a repeating head. 2

Labelled configurations and labelled BP-automata

To compute G, we need to be able to compute predecessors of configurations of the form (⟨p ′ , ϵ⟩, θ ′ ), and to determine whether these predecessors were backward-reachable using some control points in G (item 3 in Definition 4). To solve this question, we will label configurations (⟨p ′′ , w⟩, θ) s.t.

(⟨p ′′ , w⟩, θ) ⇒ * (⟨p ′ , ϵ⟩, θ ′ ) by 1 if this path went through an accepting location in G, i.e., if (⟨p ′′ , w⟩, θ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ), and by 0 if not. To this aim, we define a labelled configuration as a tuple [(⟨p, w⟩, θ) of a SM-PDS involves a PDS configuration ⟨p, w⟩, together with the current set of transition rules (phase) θ, and a boolean b, in order to take into account the phases θ, and these new 0/1-labels in configurations, we extend multi-automata to labelled BP-automata as follows:

Definition 5. Let BP = (P, Γ, ∆, ∆ c , G) be a SM-BPDS. A labelled BP-automaton is a tuple A = (Q, Γ, T, I, F ) where Γ is the automaton alphabet, Q is a fi- nite set of states, I ⊆ P × 2 ∆∪∆c ⊆ Q is the set of initial states, T ⊂ Q × ( (Γ ∪ {ϵ}) × {0, 1} ) × Q is the set of transitions, F ⊆ Q is the set of final states. If ( q, [γ, b], q ′ ) ∈ T , we write q [γ,b]
---→ T q ′ . We extend this notation in the obvious way to sequences of symbols: (1) ∀q ∈ Q, q

[ϵ,0]
---→ T q, and (2) ∀q,

q ′ ∈ Q, ∀b ∈ {0, 1}, ∀w ∈ Γ * for w = γ 0 ...γ n+1 , q [w,b] ---→ T q ′ iff ∃q 0 , ..., q n ∈ Q, b 0 , ..., b n+1 ∈ {0, 1}, b = b 0 ∨b 1 ∨...∨b n+1 and q [γ0,b0] -----→ T q 0 [γ1,b1] -----→ T q 1 • • • q n [γn+1,bn+1] --------→ T q ′ . If q [w,b]
---→ T q ′ holds, we say that q

[w,b] ---→ T q ′ and q [γ0,b0] -----→ T q 0 [γ1,b1] -----→ T q 1 • • • q n [γn+1,bn+1] --------→ T q ′ is a path of A.
A labelled configuration [(⟨p, w⟩, θ), b] is accepted by the automaton A iff there exists a path (p, θ)

[γ0,b0] -----→ T q 1 [γ1,b1] -----→ T q 2 • • • q n [γn,bn] -----→ T q n+1 in A such that w = γ 0 γ 1 • • • γ n , b = b 0 ∨ b 1 ∨ ... ∨ b n , (p, θ) ∈ I, and q n+1 ∈ F . Let L(A)
be the set of labelled configurations accepted by A. ---→ T q (in case |w| = 0, we have w = ϵ) with r ∈ θ. Then, add (p, θ) to I, and

( (p, θ), [γ, B(p) ∨ b], q ) to T . α 2 : if r = p (σ,σ ′ )
----→ p 1 ∈ ∆ c and there exists in T a transition (p 1 , θ)

[γ,b]
---→ T q with r ∈ θ, where γ ∈ Γ. Then add (p, θ ′ ) to I, and

( (p, θ ′ ), [γ, B(p)∨b], q ) to T , for θ ′ such that θ = θ ′ \ σ ∪ σ ′ .
The procedure above terminates since there is a finite number of states and phases. Note that by construction, F = {(p ′ , θ ′ )}, and, since initially

Q = {(p ′ , θ ′ )}, states of A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) )
are all of the form (p, θ) for p ∈ P and θ ⊆ ∆ ∪ ∆ c . Let us explain the intuition behind rule (α 1 ). Let r = ⟨p, γ⟩ → ⟨p 1 , w⟩ ∈ ∆.

Let c = (⟨p 1 , ww ′ ⟩, θ) and c ′ = (⟨p, γw ′ ⟩, θ). Then, if c ⇒ * (⟨p ′ , ϵ⟩, θ ′ ), then necessarily, c ′ ⇒ * (⟨p ′ , ϵ⟩, θ ′ ). Moreover, c ′ ⇒ r (⟨p ′ , ϵ⟩, θ ′ ) iff either c ⇒ r (⟨p ′ , ϵ⟩, θ ′ ) or p ∈ G (i.e. B(p) = 1
). Thus, we would like that if the automaton

A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) accepts the labelled configuration [c, b] (where b = 1 means c ⇒ r (⟨p ′ , ϵ⟩, θ ′ )), then it should also accept the labelled configuration [c ′ , b ∨ B(p)] (b ∨ B(p) = 1 means c ′ ⇒ r (⟨p ′ , ϵ⟩, θ ′ )). Thus, if the automaton A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) contains a path of the form π = (p 1 , θ) [w,b1] ----→ T q [w ′ ,b2] ----→ T q f where q f ∈ F that
[γ,B(p)∨b1] --------→ T q [w ′ ,b2]
-----→ T q f added by rule (α 1 ).

Rule (α 2 ) deals with modifying rules: Let r = p

(r1,r2) ----→ p 1 ∈ ∆ c . Let c = (⟨p 1 , γw ′ ⟩, θ) and c ′ = (⟨p, γw ′ ⟩, θ ′′ ) s.t. θ = θ ′′ \{r 1 } ∪ {r 2 }. Then, if c ⇒ * (⟨p ′ ,
ϵ⟩, θ ′ ), then necessarily, c ′ ⇒ * (⟨p ′ , ϵ⟩, θ ′ ). Moreover, c ′ ⇒ r (⟨p ′ , ϵ⟩, θ ′ ) iff either c ⇒ r (⟨p ′ , ϵ⟩, θ ′ ) or p ∈ G (i.e. B(p) = 1). Thus, we need to impose that if the automaton A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) contains a path of the form

(p 1 , θ) [γ,b1] ---→ T q [w ′ ,b2]
----→ T q f (where q f ∈ F ) that accepts the labelled configuration

-------→ T q [w ′ ,b2]
----→ T q f added by rule (α 2 ).

Example

Let us illustrate the procedure by an example. Consider the SM-BPDS BP = (P, Γ, ∆, ∆ c , G) shown in the left (i.e. part a) of Fig. 2 where P = {p 1 , p 2 , p 3 , p ′ }, ∆ = {r 1 , r 2 , r 3 , r 4 , r 5 , r 6 , r 7 }, ∆ c = {r ′ } and G = {p 2 }. We show how to compute a BP-automaton A pre * ((⟨p ′ , ϵ⟩, θ ′ )). Let A be the automaton that accepts the set {(⟨p ′ , ϵ⟩, θ ′ )} with Q = I = F = {(p ′ , θ ′ )}. Initially, T is empty. The result is obtained through the following steps:

1. First we note that (p ′ , θ ′ )

(p 1 , θ ′ ) [γ1,b1] ----→ T (p ′ , θ ′ ) with b 1 = B(p 1 ) ∨ b = 0 and (p ′ , θ ′ ) [γ ′ ,b2] ----→ T (p ′ , θ ′ ) with b 2 = B(p ′ ) ∨ b = 0. pre* ((⟨p′ , ϵ⟩, θ′ )) p′ , θ′ p′ , θ′ Δ : Δ : r 1 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p′ , ϵ⟩ r 1 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p′ , ϵ⟩ r 2 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 1 , γ 1 γ′ ⟩ r 2 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 1 ,
G = {p 2 } G = {p 2 } , Γ = {γ 1 , γ 2 , γ′ } Γ = {γ 1 , γ 2 , γ′ } ↪ p 2 p 1 , θ′ p 1 , θ′ p 2 , θ′ p 2 , θ′ p 3 , θ 1 p 3 , θ 1 p 2 , θ 1 p 2 , θ 1 a b p′ , θ 1 p′ , θ 1 p 1 , θ 1 p 1 , θ 1 [γ′ ,0] [γ 1 ,0] [ γ ′ ,1 ] [ γ 2 , 1 ] [γ ′ ,1 ] [ γ ′ , 1 ] [γ 1 ,0] ({r 4 }, {r 3 }) [γ 2 ,1 ] [ γ ′ , 1 ] [ γ 2 , 1 ] [γ′ ,1] [γ 1 ,1] [γ′ ,1] [ γ 1 , 1 ]

Now that we have the path (p

1 , θ ′ ) [γ1,b1] ----→ T (p ′ , θ ′ ) [γ ′ ,b2] ----→ T (p ′ , θ ′ ), b 1 = 0 and b 2 = 0, since r 2 ∈ θ ′ , moreover, p 2 ∈ G i.e. B(p 2 ) = 1 then Rule (α 1 ) adds (p 2 , θ ′ ) [γ2,b] ---→ T (p ′ , θ ′ ) with b = B(p 2 ) ∨ b 1 ∨ b 2 = 1.

Since we have (p

1 , θ ′ ) [γ1,b1] ----→ T (p ′ , θ ′ ), b 1 = 0 and r 6 ∈ θ ′ ,

Now we have (p

2 , θ ′ ) [γ ′ ,b1] ----→ T (p ′ , θ ′ ), b 1 = 1 and r 5 ∈ θ ′ , moreover, p ′ / ∈ G i.e. B(p ′ ) = 0, then Rule (α 1 ) adds the transition (p ′ , θ ′ ) [γ ′ ,b] ---→ T (p ′ , θ ′ ) with b = B(p ′ ) ∨ b 1 = 1. 6. Since we have (p 2 , θ ′ ) [γ ′ ,b1] ----→ T (p ′ , θ ′ ) and (p 2 , θ ′ ) [γ2,b2] ----→ T (p ′ , θ ′ ), b 1 = 1, b 2 = 1, the self-modifying rule r ′ ∈ θ ′ can be applied. Moreover, p 3 / ∈ G i.e. B(p 3 ) = 0 Thus, Rule (α 2 ) adds (p 3 , θ 1 ) [γ2,b] ---→ T (p ′ , θ ′ ) and (p 3 , θ 1 ) [γ ′ ,b ′ ] ----→ T (p ′ , θ ′ ) where θ 1 = (θ ′ \ {r 3 }) ∪ {r 4 } with b = B(p 3 ) ∨ b 1 = 1, b ′ = B(p 3 ) ∨ b 2 = 1.
7. Now we have (p 3 , θ 1 )

[γ2,b1] ----→ T (p ′ , θ ′ ), b 1 = 1 and r 4 ∈ θ 1 , moreover, p 2 ∈ G i.e. B(p 2 ) = 1, then Rule (α 1 ) adds the transition (p 2 , θ 1 ) [γ ′ ,b] ---→ T (p ′ , θ ′ ) with b = B(p 2 ) ∨ b 1 = 1. 8. Since (p 2 , θ 1 ) [γ ′ ,b1] ----→ T (p ′ , θ ′ ), b 1 = 1 and r 5 ∈ θ 1 , moreover, p 2 ∈ G i.e.
B(p 2 ) = 1, then Rule (α 1 ) adds the transition (p ′ , θ 1 )

[γ ′ ,b] ---→ T (p ′ , θ ′ ) with b = B(p 2 ) ∨ b 1 = 1.
[γ ′ ,b] ---→ T (p ′ , θ 1 ) with b = B(p 2 ) ∨ b 1 = 1.
11. Now that we have the path (p 1 , θ 1 )

[γ1,b1] ----→ T (p ′ , θ 1 ) [γ ′ ,b2] ----→ T (p ′ , θ ′ ), since r 2 ∈ θ 1 , b 1 = 0, b 2 = 1, moreover, p 2 ∈ G i.e. B(p 2 ) = 1 then Rule (α 1 ) adds (p 2 , θ 1 ) [γ2,b] ---→ T (p ′ , θ ′ ) with b = B(p 2 ) ∨ b 1 ∨ b 2 = 1.
12. Since we have (p 2 , θ 1 )

[γ2,b1] ----→ T (p ′ , θ ′ ), b 1 = 1 and r 7 ∈ θ 1 , Rule (α 1 ) adds the transition (p 1 , θ 1 ) [γ1,b] ---→ T (p ′ , θ ′ ) with b = B(p 1 ) ∨ b 1 = 1.
13. No further additions are possible. Thus, the procedure terminates.

The result is depicted in the right side of Fig. 2

Proof

Before proving that our construction is correct, we introduce the following definition:

Definition 6. Let A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) )
= (Q, Γ, T, P, F ) be the labelled P-automaton computed by the saturation procedure above. In this section, we use -→ i T to denote the transition relation of A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) obtained after adding i transitions using the saturation procedure above. Let us notice that due to the fact that initially Q = {(p ′ , θ ′ )} and due to rules (α 1 ) and (α 2 ) that at step i add only transitions of the form (p, θ) γ -→ T q for a state q that is already in the automaton at step i -1, then, states of A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) are all of the form (p, θ) for p ∈ P and θ ⊆ ∆ ∪ ∆ c .

We can show that:

Lemma 2. Let p, p ′′ ∈ P and θ, θ ′′ ⊆ ∆ ∪ ∆ c . Let w ∈ Γ * and b ∈ {0, 1}. If a path (p, θ) [w,b] ---→ T (p ′′ , θ ′′ ) is in A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) )
, then (⟨p, w⟩, θ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ). Moreover, if b = 1, then (⟨p, w⟩, θ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ).

Proof: Initially, the automaton contains no transitions. Let i be an index such that (p, θ)

[w,b] ---→ i T
(p ′′ , θ ′′ ) holds. We proceed by induction on i.

Basis. i = 0, then (p ′′ , θ ′′ ) [ϵ,0] ---→ 0 T (p ′′ , θ ′′ ). This means p ′′ = p ′ , θ ′′ = θ ′ . Since initially Q = {(p ′ , θ ′ )}, then (⟨p ′′ , ϵ⟩, θ ′′ ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ) always holds. Step. i > 0. Let t = ( (p 1 , θ 1 ), [γ, b 1 ], (p 0 , θ 0 )
) be the i-th transition added to A pre * and j be the number of times that t is used in the path (p, θ)

[w,b] ---→ i T (p ′′ , θ ′′ ).
The proof is by induction on j. If j = 0, then we have

(p, θ) [w,b] ---→ i-1 T
(p ′′ , θ ′′ ) in the automaton, and we apply the induction hypothesis (induction on i) then we obtain (⟨p, w⟩, θ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ). So assume that j > 0. Then, there exist

u, v ∈ Γ * , b ′ , b ′′ ∈ {0, 1} such that w = uγv, b = b ′ ∨ b 1 ∨ b ′′ and (p, θ) [u,b ′ ] ---→ i-1 T (p 1 , θ 1 ) [γ,b1] ---→ i T (p 0 , θ 0 ) [v,b ′′ ] ----→ i T (p ′′ , θ ′′ ) (1)
The application of the induction hypothesis (induction on i) to (p, θ)

[u,b ′ ] ---→ i-1 T (p 1 , θ 1 ) gives that (⟨p, u⟩, θ) ⇒ * (⟨p 1 , ϵ⟩, θ 1 ), moreover, if b ′ = 1, (⟨p, u⟩, θ) ⇒ r (⟨p 1 , ϵ⟩, θ 1 ) (2)
There are 2 cases depending on whether transition t was added by saturation rule α 1 or α 2 .

1. Case t was added by rule α 1 : There exist p 2 ∈ P and w 2 ∈ Γ * such that

r = ⟨p 1 , γ⟩ → ⟨p 2 , w 2 ⟩ ∈ ∆ ∩ θ 1 (3)
and A pre * contains the following path:

π ′ = (p 2 , θ 1 ) [w2,b2] ----→ i-1 T (p 0 , θ 0 ) [v,b ′′ ] ----→ i T (p ′′ , θ ′′ ), b 1 = b 2 ∨ B(p 1 ) (4)
Applying the transition rule r, we get that

(⟨p 1 , γv⟩, θ 1 ) ⇒ (⟨p 2 , w 2 v⟩, θ 1 ) (5)
By induction on j (since transition t is used j -1 times in π ′ ), we get from (4) that (⟨p 2 , w 2 v⟩, θ 1 ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ) moreover, if b 2 ∨b ′′ = 1, (⟨p 2 , w 2 v⟩, θ 1 ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ) (6) Putting ( 2), ( 5) and ( 6) together, we can obtain that

(⟨p, w⟩, θ) = (⟨p, uγv⟩, θ) ⇒ * (⟨p 1 , γv⟩, θ 1 ) ⇒ (⟨p 2 , w 2 v⟩, θ 1 ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ) Furthermore, if b = b ′ ∨ b 1 ∨ b ′′ = 1, then b ′ = 1 or b 1 ∨ b ′′ = 1.
For the first case, b ′ = 1, then we can have (⟨p, u⟩, θ) ⇒ r (⟨p 1 , ϵ⟩, θ 1 ) from ( 2). Thus, we can obtain that (⟨p, uγv⟩, θ) ⇒ r (⟨p 1 , γv⟩, θ 1 ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ) i.e. (⟨p, w⟩, θ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ). 6)). Therefore, (⟨p, w⟩, θ 1 ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ).

The second case b

1 ∨ b ′′ = 1 i.e. B(p 1 ) ∨ b 2 ∨ b ′′ = 1 implies that B(p 1 ) = 1 (that means p 1 ∈ G and (⟨p 1 , γv⟩, θ 1 ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ )) or b 2 ∨ b ′′ = 1 (that implies (⟨p 2 , w 2 v⟩, θ 1 ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ) from (
2. Case t was added by rule α 2 : there exist p 2 ∈ P and

θ 2 ⊆ ∆ ∪ ∆ c such that r = p 1 (σ,σ ′ ) ----→ p 2 ∈ ∆ c ∩ θ 2 , θ 2 = (θ 1 \σ) ∪ σ ′ (7)
and the following path in the current automaton ( self-modifying rule won't change the stack) with r ∈ θ 2 :

(p 2 , θ 2 ) [γ,b ′ 1 ] ---→ i-1 T (p 0 , θ 0 ) [v,b ′′ ] ----→ i T (p ′′ , θ ′′ ), b 1 = B(p 1 ) ∨ b ′ 1 (8)
Applying the transition rule, we can get from ( 7) that

(⟨p 1 , γv⟩, θ 1 ) ⇒ (⟨p 2 , γv⟩, θ 2 ) ( 9
)
We can apply the induction hypothesis (on j) to ( 8), and obtain 2),( 9) and ( 10), we get

(⟨p 2 , γv⟩, θ 2 ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ), moreover, if b ′ 1 ∨b ′′ = 1, (⟨p 2 , γv⟩, θ 2 ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ) (10) From (
(⟨p, w⟩, θ) = (⟨p, uγv⟩, θ) ⇒ * (⟨p 1 , γv⟩, θ 1 ) ⇒ (⟨p 2 , γv⟩, θ 2 ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ) Furthermore, if b = b ′ ∨ b 1 ∨ b ′′ = 1 , then b ′ = 1 or b 1 ∨ b ′′ = 1.
For the first case, b ′ = 1, then we can have (⟨p, u⟩, θ) ⇒ r (⟨p 1 , ϵ⟩, θ 1 ) from ( 2). Thus, we can obtain that (⟨p, uγv⟩, θ) ⇒ r (⟨p 1 , γv⟩, θ 1 ) ⇒ * (⟨p ′′ , ϵ⟩, θ ′′ ) i.e. (⟨p, w⟩, θ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ). The second case b 10)) i.e. (⟨p, w⟩, θ 1 ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ). Therefore, we can get that if b = 1, then (⟨p, w⟩, θ 1 ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ).

1 ∨ b ′′ = 1 i.e. B(p 1 ) ∨ b ′ 1 ∨ b ′′ = 1 implies that B(p 1 ) = 1 (that means p 1 ∈ G and (⟨p 1 , γv⟩, θ 1 ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ )) or b ′ 1 ∨ b ′′ = 1 (that implies (⟨p 2 , γv⟩, θ 2 ) ⇒ r (⟨p ′′ , ϵ⟩, θ ′′ ) from (
---→ T (p ′ , θ ′ ) in A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) )
. Moreover, if (⟨p, w⟩, θ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ), then b = 1.

Proof: Assume (⟨p, w⟩, θ) i ⇒ (⟨p ′ , ϵ⟩, θ ′ ). We proceed by induction on i.

Basis. i = 0. Then θ = θ ′ , p ′ = p and w = ϵ. Initially, we have that Q = {(p ′ , θ ′ )}, therefore, by the definition of → T , we have (p

′ , θ ′ ) ϵ - → T (p ′ , θ ′ ). We cannot have (⟨p ′ , ϵ⟩, θ ′ ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ) in 0-step.
Step. i > 0. Then there exists a configuration (⟨p ′′ , u⟩, θ ′′ ) such that

(⟨p, w⟩, θ) ⇒ (⟨p ′′ , u⟩, θ ′′ ) i-1 ⇒ (⟨p ′ , ϵ⟩, θ ′ )
We apply the induction hypothesis to (⟨p ′′ , u⟩, θ ′′ ) i-1 ⇒ (⟨p ′ , ϵ⟩, θ ′ ), and obtain that there exists in

A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) a path (p ′′ , θ ′′ ) [u,b ′′ ] ----→ T (p ′ , θ ′ ). If (⟨p ′′ , u⟩, θ ′′ ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ), b ′′ = 1.
Let (p 0 , θ 0 ) be a state of

A pre * . Let w 1 , u 1 ∈ Γ * , γ ∈ Γ, b ′′ 0 , b ′′ 1 ∈ {0, 1} be such that w = γw 1 , u = u 1 w 1 , b ′′ = b ′′ 0 ∨ b ′′ 1 and (p ′′ , θ ′′ ) [u1,b ′′ 0 ] -----→ T (p 0 , θ 0 ) [w1,b ′′ 1 ] -----→ T (p ′ , θ ′ ) (1)
There are two cases depending on which rule is applied to get (⟨p, w⟩, θ) ⇒ (⟨p ′′ , u⟩, θ ′′ ).

1. Case (⟨p, w⟩, θ) ⇒ (⟨p ′′ , u⟩, θ ′′ ) is obtained by a rule of the form: ⟨p, γ⟩ → ⟨p ′′ , u 1 ⟩ ∈ ∆. In this case, θ ′′ = θ. By the saturation rule α 1 , we have

(p, θ ′′ ) [γ,b0] ----→ T (p 0 , θ 0 ), b 0 = B(p) ∨ b ′′ 0 (2)
Putting ( 1) and ( 2) together, we can obtain that

π = (p, θ ′′ ) [γ,b0] ----→ T (p 0 , θ 0 ) [w1,b ′′ 1 ] -----→ T (p ′ , θ ′ ) (3) Thus, (p, θ ′′ ) [γw1,b0∨b ′′ 1 ] --------→ T (p ′ , θ ′ ) i.e. (p, θ) [w,b] ---→ T (p ′ , θ ′ ) where b = b 0 ∨ b ′′ 1 . 2. Case (⟨p, w⟩, θ) ⇒ (⟨p ′′ , u⟩, θ ′′ ) is obtained by a rule of the form p (σ,σ ′ ) ----→ p ′′ ∈ ∆ c i.e θ ′′ ̸ = θ. In this case, u 1 = γ. By the saturation rule β 2 , we obtain that (p, θ) [γ,b0] ----→ T (p 0 , θ 0 ) where θ ′′ = θ\{r 1 } ∪ {r 2 }, b 0 = B(p) ∨ b ′′ 0 . (4)
Putting ( 1) and ( 4) together, we have the following path (p, θ)

[γ,b0] ----→ T (p 0 , θ 0 ) [w1,b ′′ 1 ] -----→ T (p ′ , θ ′ ) i.e. (p, θ) [w,b] ---→ T (p ′ , θ ′ ) where b = b 0 ∨b ′′ 1 (5) Furthermore, if (⟨p, w⟩, θ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ), then (⟨p, w⟩, θ) ⇒ r (⟨p ′′ , u⟩, θ ′′ ) or (⟨p ′′ , u⟩, θ ′′ ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ).
For the first case, (⟨p, w⟩, θ) ⇒ r (⟨p ′′ , u⟩, θ ′′ ), then p ∈ G i.e. B(p) = 1. For the second case, (⟨p ′′ , u⟩, θ ′′ ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ), we can get b ′′ = 1 (from induction hypothesis).

Thus, b = b 0 ∨ b ′′ 1 = B(p) ∨ b ′′ 0 ∨ b ′′ 1 = B(p) ∨ b ′′ = 1.
Therefore, if (⟨p, w⟩, θ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ), then we can obtain b = 1.

2

From these two lemmas, we get:

Theorem 4.2. Let [c, b] be a labelled configuration. Then [c, b] is in L(A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) iff c ∈ pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) . Moreover, c ⇒ r (⟨p ′ , ϵ⟩, θ ′ ) iff b = 1. Proof: Let [(⟨p, w⟩, θ), b] be a labelled configuration of pre * ( (⟨p ′ , ϵ⟩, θ ′ ) )
). Then (⟨p, w⟩, θ) ⇒ * (⟨p ′ , ϵ⟩, θ ′ ). By Lemma 2, we can obtain that there exists a path (p, θ)

[w,b] ---→ T (p ′ , θ ′ ) in A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) . So [(⟨p, w⟩, θ), b] is in L(A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) ). Moreover, if (⟨p, w⟩, θ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ), then b = 1.

Conversely, let [(⟨p, w⟩, θ), b] be a labelled configuration accepted by

A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) )
i.e. there exists a path (p, θ)

[w,b] ---→ T (p ′ , θ ′ ) in A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) . By Lemma 3, (⟨p, w⟩, θ) ⇒ * (⟨p ′ , ϵ⟩, θ ′ ) i.e. (⟨p, w⟩, θ) ∈ pre * (L(A)). Moreover, if b = 1, (⟨p, w⟩, θ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ). 2

Computing the Head Reachability Graph G

Based on the definition of the Head Reachability Graph G, and on Theorem 4.2, we can compute G as follows. Initially, G has no edges.

α ′ 1 : if r c : p (σ,σ ′ )
----→ p ′ ∈ ∆ c , then for every phase θ such that r c ∈ θ and every γ ∈ Γ, we add the edge ((p, γ), θ)

B(p) ---→ ((p ′ , γ), θ 0 ) to the graph G, where θ 0 = θ \ σ ∪ σ ′ .
α ′ 2 : if r : ⟨p, γ⟩ → ⟨p 0 , γ 0 ⟩ ∈ ∆, then for every phase θ such that r ∈ θ, we add the edge ((p, γ), θ)

B(p) ---→ ((p 0 , γ 0 ), θ) to the graph G. α ′ 3 : if r : ⟨p, γ⟩ → ⟨p 0 , γ 0 γ ′ ⟩ ∈ ∆,
then for every phase θ such that r ∈ θ, we add to the graph G the edge ((p, γ), θ)

B(p)
---→ ((p 0 , γ 0 ), θ). Moreover, for every control point p ′ ∈ P and phase θ ′ such that

A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) )
contains a transition of the form t = (p 0 , θ)

[γ0,b] ----→ T (p ′ , θ ′ ), we add to the graph G the edge ((p, γ), θ) b∨B(p) ----→ ((p ′ , γ ′ ), θ ′ ).
pre* ((⟨p′ , ϵ⟩, θ′ ))

p′ , θ 1 p′ , θ 1 pre* ((⟨p′ , ϵ⟩, θ 1 )) p 1 , θ 1 p 1 , θ 1 b p′ , θ′ p′ , θ′ p 1 , θ′ p 1 , θ′ p 2 , θ′ p 2 , θ′ p 3 , θ 1 p 3 , θ 1 p 2 , θ 1 p 2 , θ 1 a p′ , θ 1 p′ , θ 1 p 1 , θ 1 p 1 , θ 1 [γ′ ,0] [γ 1 ,0] [ γ ′ ,1 ] [ γ 2 , 1 ] [γ ′ ,1 ] [ γ ′ ,1 ] [γ 1 ,0] [γ 1 ,0] p 2 , θ 1 p 2 , θ 1 [γ′ ,0] ((p 2 , γ′ ), θ 1 ) ((p 2 , γ′ ), θ 1 ) ((p 3 , γ 2 ), θ 1 ) ((p 3 , γ 2 ), θ 1 ) 1
((p 1 , γ 1 ), θ 1 ) ((p 1 , γ 1 ), θ 1 ) 1 ((p′ , γ′ ), θ 1 ) ((p′ , γ′ ), θ 1 ) 0 ((p 2 , γ 2 ), θ′ ) ((p 2 , γ 2 ), θ′ ) ((p 1 , γ 1 ), θ′ ) ((p 1 , γ 1 ), θ′ ) ((p′ , γ′ ), θ′ ) ((p′ , γ′ ), θ′ ) 1 [γ 2,1] ((p 2 , γ 2 ), θ 1 ) ((p 2 , γ 2 ), θ 1 ) ((p 1 , γ′ ), θ 1 ) ((p 1 , γ′ ), θ 1 ) 0
((p 2 , γ′ ), θ′ ) ((p 2 , γ′ ), θ′ ) 0 1 ((p 3 , γ′ ), θ 1 ) ((p 3 , γ′ ), θ 1 ) 0 0 [γ 1 ,0] [ γ ′ , 1 ] [ γ 2 , 1 ] [ γ ′ ,1 ] [ γ 2 , 1 ] [γ′ ,1] 1 0 C [γ 1 ,1] [γ 1 ,1] 1 1
((p 3 , γ 1 ), θ 1 ) ((p 3 , γ 1 ), θ 1 ) ((p 2 , γ 1 ), θ′ ) ((p 2 , γ 1 ), θ′ ) 0 0 [γ′ ,1] [ γ 1 , 1 ]
{((p 2 , γ 2 ), θ ′ ), ((p ′ , γ ′ ), θ ′ ), ((p 2 , γ ′ ), θ ′ ), ((p 1 , γ 1 ), θ ′ )}.

Experiments

Our approach vs. standard LTL for PDSs

We implemented our approach in a tool1 and we compared its performance against the approaches that consist in translating the SM-PDS to an equivalent standard (or symbolic) PDS, and then applying the standard LTL model checking algorithms implemented in the PDS model-checker tool Moped [START_REF] Schwoon | Model-checking pushdown systems[END_REF].

All our experiments were run on Ubuntu 16.04 with a 2.7 GHz CPU, 2GB of memory. To perform the comparison, we randomly generate several SM-PDSs and LTL formulas of different sizes. For this, we use the function int rand(void) several times to randomly generate states and transitions. The results (CPU Execution time) are shown in Table 1. Column Size is the size of SM-PDS (S 1 for non-modifying transitions ∆ and S 2 for modifying transitions ∆ c ). Column LTL gives the size of the transitions of the Büchi automaton generated from the LTL formula (using the tool LTL2BA [START_REF] Gastin | Fast ltl to büchi automata translation[END_REF]). Column SM-PDS gives the cost of our direct algorithm presented in this paper. Column PDS shows the cost it takes to get the equivalent PDS from the SM-PDS. Column Result reports the cost it takes to run the LTL PDS model-checker Moped [START_REF] Schwoon | Model-checking pushdown systems[END_REF] for the PDS we got. Column Total is the total cost it takes to translate the SM-PDS into a PDS and then apply the standard LTL model checking algorithm of Moped (Total=PDS+Result). Column Symbolic PDS reports the cost it takes to get the equivalent Symbolic PDS from the SM-PDS. Column Result 1 is the cost to run the Symbolic PDS LTL model-checker Moped. Column T otal 1 is the total cost it takes to translate the SM-PDS into a symbolic PDS and then apply the standard LTL model checking algorithm of Moped. You can see that our direct algorithm (Column SM-PDS ) is much more efficient than translating the SM-PDS to an equivalent (symbolic) PDS, and then run the standard LTL model-checker Moped. Translating the SM-PDS to a standard PDS may take more than 20 days, whereas our direct algorithm takes only a few seconds. Moreover, since the obtained standard (symbolic) PDS is huge, Moped failed to handle several cases (the time limit that we set for Moped is 20 minutes), whereas our tool was able to deal with all the cases in only a few seconds.

Malicious Behavior Detection on Self-Modifying Code 5.2.1. Specifying Malicious Behaviors using LTL.

As described in [START_REF] Song | Ltl model-checking for malware detection[END_REF], several malicious behaviors can be described by LTL formulas. We give in what follows four examples of such malicious behaviors and show how they can be described by LTL formulas:

Registry Key Injecting: In order to get started at boot time, many malwares add themselves into the registry key listing. This behavior is typically implemented by first calling the API function GetModuleFileNameA to retrieve the path of the malware's executable file. Then, the API function RegSetVal-ueExA is called to add the file path into the registry key listing. This malicious behavior can be described in LTL as follows:

ϕ rk = F ( call GetM oduleF ileN ameA ∧ F( call RegSetV alueExA) )
This formula expresses that if a call to the API function GetModuleFile-NameA is followed by a call to the API function RegSetValueExA, then probably a malware is trying to add itself into the registry key listing.

Data-Stealing:

Stealing data from the host is a popular malicious behavior that intend to steal any valuable information including passwords, software codes, bank information, etc. To do this, the malware needs to scan the disk to find the interesting file that he wants to steal. After finding the file, the malware needs to locate it. To this aim, the malware first calls the API function Get-ModuleHandleA to get a base address to search for a location of the file. Then the malware starts looking for the interesting file by calling the API function FindFirstFileA. Then the API functions CreateFileMappingA and MapViewOf-File are called to access the file. Finally, the specific file can be copied by calling the API function CopyFileA. Thus, this data-stealing malicious behavior can be described by the following LTL formula as follows:

ϕ ds = F(call GetM oduleHandleA ∧F(call F indF irstF ileA∧F (call CreateF ileM appingA ∧ F (call M apV iewof F ile ∧ F call CopyF ileA))))
Spy-Worm: A spy worm is a malware that can record data and send it using the Socket API functions. For example, Keylogger is a spy worm that can record the keyboard states by calling the API functions GetAsyKeyState and GetKeyState and send that to the specific server by calling the socket function sendto. Another spy worm can also spy on the I/O device rather than the keyboard. For this, it can use the API function GetRawInputData to obtain input from the specified device, and then send this input by calling the socket functions send or sendto. Thus, this malicious behavior can be described by the following LTL formula:

ϕsw = F ( (call GetAsyncKeyState ∨ call GetRawInputData) ∧ F(call sendto ∨ call send) )
Appending virus: An appending virus is a virus that inserts a copy of its code at the end of the target file. To achieve this, since the real OFFSET of the virus' variables depends on the size of the infected file, the virus has to first compute its real absolute address in the memory. To perform this, the virus has to call the sequence of instructions: l 1 : call f ; l 2 : ....; f : pop eax;. The instruction call f will push the return address l 2 onto the stack. Then, the pop instruction in f will put the value of this address into the register eax. Thus, the virus can get its real absolute address from the register eax. This malicious behavior can be described by the following LTL formula:

ϕav = ∨ F ( call ∧ X(top-of-stack = a) ∧ G¬ ( ret ∧ (top-of-stack = a) ) )
where the ∨ is taken over all possible return addresses a, and top-of-stack=a is a predicate that indicates that the top of the stack is a. The subformula call ∧ X(top-of-stack = a) means that there exists a procedure call having a as return address. Indeed, when a procedure call is made, the program pushes its corresponding return address a to the stack. Thus, at the next step, a will be on the top of the stack. Therefore, the formula above expresses that there exists a procedure call having a as return address, such that there is no ret instruction which will return to a.

Note that this formula uses predicates that indicate that the top of the stack is a. Our techniques work for this case as well: it suffices to encode the top of the stack in the control points of the SM-PDS. Our implementation works for this case as well and can handle appending viruses.

Applying our tool for malware detection.

We applied our tool to detect several malwares. We use the unpack tool unpacker [START_REF] Tool | Automated unpacking: A behaviour based approach[END_REF] to handle packers like UPX, and we use Jakstab [START_REF] Kinder | Jakstab: A static analysis platform for binaries[END_REF] as disassembler. We consider 160 malwares from the malware library VirusShare [START_REF] Virusshare | [END_REF], 184 malwares from the malware library MalShare [START_REF] Cutler | malshare[END_REF], 288 email-worms from VX heaven [START_REF] Heaven | [END_REF] and 260 new malwares generated by NGVCK, one of the best malware generators. We also choose 200 benign samples from Windows programs. We consider self-modifying versions of these programs2 . In these versions, the malicious behaviors are unreachable if the semantics of the self-modifying instructions are not taken into account, i.e., if the self-modifying instructions are considered as "standard" instructions that do not modify the code, then the malicious behaviors cannot be reached. To check this, we model such programs in two ways:

1. First, we take into account the self-modifying instructions and model these programs using SM-PDSs as described in Section 2.3. Then, we check whether these SM-PDSs satisfy at least one of the malicious LTL formulas presented above. If yes, the program is declared as malicious, if not, it is declared as benign. Our tool was able to detect all the 892 self-modifying malwares as malicious, and to determine that benign programs are benign. We report in Table 3 2. Second, we abstract away the self-modifying instructions and proceed as if these instructions were not self-modifying. In this case, we translate the binary codes to standard pushdown systems as described in [START_REF] Song | Efficient malware detection using model-checking[END_REF]. By using PDSs as models, none of the malwares that we consider was detected as malicious, whereas, as reported in Table 3, using self-modifying PDSs as models, and applying our LTL model-checking algorithm allowed to detect all the 892 malwares that we considered.

Remark. Note that checking the formulas ϕ rk , ϕ ds , and ϕ sw could be done using multiple pre * queries on SM-PDSs using the pre * algorithm of [START_REF] Touili | Reachability analysis of self modifying code[END_REF]. However, this would be less efficient than performing our direct LTL model-checking algorithm, as shown in SM-PDSs to check the properties ϕ rk , ϕ ds , and ϕ sw . It can be seen that applying our direct LTL model checking algortihm is more efficient. Furthermore, the appending virus formula ϕ av cannot be solved using multiple pre * queries. Our direct LTL model-checking algorithm is needed in this case. Note that some of the malwares we considered in our experiments are appending viruses. Thus, our algorithm and our implementation are crucial to be able to detect these malwares.

Comparison with well-known antiviruses.

We compare our tool against well-known and widely used antiviruses. Since known antiviruses update their signature database as soon as a new malware is known, in order to have a fair comparision with these antiviruses, we need to consider new malwares. We use the sophisticated malware generator NGVCK available at VX Heavens [START_REF] Heaven | [END_REF] to generate 205 malwares. We obfuscate these malwares with self-modifying code, and we fed them to our tool and to well known antiviruses such as BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Baidu, Avast, and Symantec. Our tool was able to detect all these programs as malicious, whereas none of the well-known antiviruses was able to detect all these malwares. Table 4 reports the detection rates of our tool and the well-known anti-viruses.

Conclusion and discussion

In this paper, we propose a direct LTL model checking algorithm for SM-PDSs. Our algorithm is based on reducing the LTL model checking problem to the emptiness problem of Self Modifying Büchi Pushdown Systems (SM-BPDSs). Intuitively, we obtain this SM-BPDS by taking the product of the SM-PDS with a Büchi automaton accepting an LTL formula φ. Then, we solve the emptiness problem of an SM-BPDS by computing its repeating heads. This computation is based on computing labelled pre * configurations by applying a saturation procedure on labelled finite automata.

We implemented our techniques in a tool for self-modifying code analysis. We successfully used our tool to model-check more than 900 self-modifying binary codes. In particular, we applied our tool for malware detection, since malwares usually use self-modifying instructions, and since malicious behaviors can be described by LTL formulas. In our experiments, our tool was able to detect 895 malwares and to prove that 200 benign programs were benign. It was also able to detect several malwares that well-known antiviruses such as Bit-Defender, Kinsoft, Avira, eScan, Kaspersky, Avast, and Symantec failed to detect.

Malware detection is nowadays a big challenge. This work brings just a stone to the building, and helps dealing with self-modifying code. However, a lot of work remains to be done in order to have a robust tool for malware detection. Indeed, as mentionned in Section 2.3.1, this work assumes that if instruction i 1 is replaced by i 2 , then i 1 and i 2 must have the same number of operands. This of course does not hold for all malicious programs. Moreover, to disassemble programs, we use Jakstab [START_REF] Kinder | Jakstab: A static analysis platform for binaries[END_REF]. This tool has a lot of limitations and offers sometimes rough translations, as discussed in [START_REF] Kinder | Jakstab: A static analysis platform for binaries[END_REF]. Another limitation of our tool is that currently it considers only the four malicious behaviors described in Section 5.2.1. Several other malicious behaviors can be found in malwares.

Thus, we need to study these behaviors and specify them as LTL formulas. To this aim, we plan to apply machine learning techniques in order to extract the maximum number of malicious behaviors from malwares.

Figure 1 :

 1 Figure 1: An Example of a Self-modifying Code

  a finite set of modifying transition rules. If((p, γ), (p ′ , w)) ∈ ∆, we also write ⟨p, γ⟩ → ⟨p ′ , w⟩ ∈ ∆. If (p, r 1 , r 2 , p ′ ) ∈ ∆ c , we also write p (r1,r2) ----→ p ′ ∈ ∆ c . A Pushdown System (PDS) is a SM-PDS where ∆ c = ∅.

  , b], s.t. (⟨p, w⟩, θ) is a configuration and b ∈ {0, 1}. Multi-automata were introduced in [2, 3] to finitely represent regular infinite sets of configurations of a PDS. Since a labelled configuration c = [(⟨p, w⟩, θ), b]

4. 3 .

 3 Computing pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) Given a configuration of the form (⟨p ′ , ϵ⟩, θ ′ ), our goal is to compute a labelled BP-automaton A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) that accepts labelled configurations of the form [c, b] where c is a configuration and b ∈ {0, 1} such that c ⇒ * (⟨p ′ , ϵ⟩, θ ′ ) (i.e., c ∈ pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) ) and b = 1 iff this path went through final control points, i.e., c ⇒ r (⟨p ′ , ϵ⟩, θ ′ ). Otherwise, b = 0. Let p ∈ P , we define B(p) = 1 if p ∈ G and B(p) = 0 otherwise. A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) = (Q, Γ, T, I, F ) is computed as follows: Initially, Q = I = F = {(p ′ , θ ′ )} and T = ∅. We add to T transitions as follows: α 1 : If r = ⟨p, γ⟩ → ⟨p 1 , w⟩ ∈ ∆. If there exists in T a path (p 1 , θ) [w,b]

  accepts the labelled configuration [c, b], then the automaton should also accept the labelled configuration [c ′ , b ∨ B(p)]. This configuration is accepted by the run (p, θ)

  [c, b], b = b 1 ∨ b 2 (b = 1 means c ⇒ r (⟨p ′ , ϵ⟩, θ ′ )), then necessarily, the automaton A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) should also accept the labelled configuration [c ′ , b ∨ B(p)]. This configuration is accepted by the run (p, θ ′′ ) [γ,B(p)∨b1]

  T (p ′ , θ ′ ), b = 0 holds. Since ⟨p ′ , ϵ⟩ occurs on the right hand side of rule r 1 ∈ θ ′ and r 3 ∈ θ ′ , moreover, p 1 / ∈ G i.e. B(p 1 ) = 0 and p ′ / ∈ G i.e. B(p ′ ) = 0, then Rule (α 1 ) adds the transition

Figure 2 :

 2 Figure 2: BP-automaton A pre * ((⟨p ′ , ϵ⟩, θ ′ ))

  moreover, p 2 ∈ G i.e. B(p 2 ) = 1, then Rule (α 1 ) adds the transition (p 2 , θ ′ ) [γ ′ ,b] ---→ T (p ′ , θ ′ ) with b = B(p 2 ) ∨ b 1 = 1. 4. Now we have (p 2 , θ ′ ) [γ2,b1] ----→ T (p ′ , θ ′ ), b 1 = 1 and r 7 ∈ θ ′ , moreover, p 2 ∈ G i.e. B(p 2 ) = 1, then Rule (α 1 ) adds the transition (p 1 , θ ′ ) [γ1,b] ---→ T (p ′ , θ ′ ) with b = B(p 2 ) ∨ b 1 = 1.

9 .

 9 We note that (p ′ , θ 1 ) [ϵ,b1] ---→ T (p ′ , θ 1 ), b 1 = 0 holds. Since ⟨p ′ , ϵ⟩ occurs on the right hand side of rule r 1 ∈ θ 1 , moreover, p 1 / ∈ G i.e. B(p 1 ) = 0 and p ′ / ∈ G i.e. B(p ′ ) = 0, then Rule (α 1 ) adds the transition (p 1 , θ 1 ) [γ1,b] ---→ T (p ′ , θ ′ ) with b = B(p 1 ) ∨ b 1 = 0. 10. Now we have (p 1 , θ 1 ) [γ1,b1] ----→ T (p ′ , θ 1 ), b 1 = 0 and r 6 ∈ θ 1 , moreover, p 2 ∈ G i.e. B(p 2 ) = 1, then Rule (α 1 ) adds the transition (p 2 , θ 1 )

2 Lemma 3 .

 23 If there is a labelled configuration [(⟨p, w⟩, θ), b] such that (⟨p, w⟩, θ) ⇒ * (⟨p ′ , ϵ⟩, θ ′ ), then there is a path (p, θ)[w,b]

Figure 3 :

 3 Figure 3: An Example of the SM-BPDS and the graph G

  ′ iff there exists a sequence of configurations c 0 ⇒ BP c 1 ⇒ BP ... ⇒ BP c i s.t. c 0 = c and c i = c ′ .

	from the context. We define	i ⇒ as follows: c
	A head of SM-BPDS is a tuple (⟨p, γ⟩, θ) where p ∈ P , γ ∈ Γ and θ ⊆ ∆∪∆ c .
	A head ((p, γ), θ) is repeating if there exists v ∈ Γ * such that (⟨p, γ⟩, θ) ⇒ r BP
	(⟨p, γv⟩, θ). The set of repeating heads of SM-BPDS is called Rep BP .
	The relation ⇒ r BP BP c ′ iff there exists a configuration (⟨g, u⟩, θ), g ∈ G is defined as follows: c ⇒ r s.t. c ⇒ * BP (⟨g, u⟩, θ) ⇒ + BP c ′ . We remove the subscript BP when it is clear

i ⇒ c

  γ 1 γ′ ⟩ r 3 : ⟨p′ , γ′ ⟩ ↪ ⟨p′ , ϵ⟩ r 3 : ⟨p′ , γ′ ⟩ ↪ ⟨p′ , ϵ⟩ r 4 : ⟨p 2 , γ′ ⟩ ↪ ⟨p 3 , γ 2 ⟩ r 4 : ⟨p 2 , γ′ ⟩ ↪ ⟨p 3 , γ 2 ⟩ r 5 : ⟨p′ , γ′ ⟩ ↪ ⟨p 2 , γ′ ⟩ r 5 : ⟨p′ , γ′ ⟩ ↪ ⟨p 2 , γ′ ⟩ r 6 : ⟨p 2 , γ′ ⟩ ↪ ⟨p 1 , γ 1 ⟩ r 6 : ⟨p 2 , γ′ ⟩ ↪ ⟨p 1 , γ 1 ⟩ r 7 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 2 , γ 2 ⟩ r 7 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 2 , γ 2 ⟩ θ′ = {r 1 , r 2 , r 3 , r 5 ,r 6 , r 7 , r′ } θ′ = {r 1 , r 2 , r 3 , r 5 , r 6 , r 7 , r′ } , θ 1 = {r 1 , r 2 , r 4 , r 5 , r 6 , r 7 , r′ } θ 1 = {r 1 , r 2 , r 4 , r 5 , r 6 , r 7 , r′ }

	Δ c : Δ c :
	r′ : p 3 r′ : p 3

  some partial results of our experiments. Column Size is the number of control locations, Column Result gives the result of our algorithm: Yes means malicious and No means benign; and Column cost gives the cost to apply our LTL model-checker to check one of the LTL properties (Column Formula) described above. For every program, we consider all the formulas mentionned above. A program is declared malicious if it satisfes at least one of the formulas.

Table 2 ,

 2 where Column Size gives the number of control locations, Column LTL gives the time of applying our LTL model-checking algorithm; and Column Multiple pre * gives the cost of applying multiple pre * on

	Multiple pre *	0.092s	98.418s	0.183s	0.206s	83.988s	3.212s	159.195s	53.235s	4.088s	5.757s	0.392s	4.503s	8.981s	9.232s	3.392s	78.419s	111.617s	2.981s	5.946s	8.928s	9.968s	7.985s	2.983s	2.749s	298.047s	16.018s	15.452s	9.614s	4.097s	4.973s
	Example Size LTL	Netsky.c 45 0.002s	MyDoom-N 16980 30.231s	Netsky.b 45 0.057s	Mydoom.c 155 0.014s	Mydoom.v 5965 3.971s	Ardurk.d 1913 0.482s	Magistr.a.poly 36989 49.863s	Magistr.b 4670 3.987s	Adon.1559 37 0.255s	Alaul.c 355 0.109s	Alcaul.d 845 0.165s	fsAutoB.F026 245 1.698s	LdPinch.Win32.5558 2015 6.907s	LdPinch.fmye 1845 6.194s	LdPinch.e 578 1.185s	klez-N 6281 3.252s	Mydoom.j 22355 11.262s	Urbe.a 123 0.376s	Email.W32!c 220 0.249s	Mydoom.DN.worm 220 0.299s	Mydoom.cjdz 225 0.392s	Win32.Mydoom 235 0.296s	Win32.Mydoom.288 248 0.410s	Mydoom 238 0.278	Win32.Chur.A 51895 98.161s	Netsky.ah@MM 4480 6.991s	Skybag.A 4310 6.205s	Generic.20269 433 2.402s	LdPnch-Fam 195 1.440s	LdPinch.Gen.3 210 1.482s
	Multiple pre *	46.635s	0.075s	3.446s	0.085s	0.088s	0.123s	4.518s	0.482s	0.884s	4.894s	1.863s	4.318s	4.312s	8.128s	3.957s	3.978s	102.559s	3.138s	6.172s	6.452s	8.163s	9.086s	10.323s	2.691s	248.146s	245.452s	13.739s	11.327s	9.986s	6.154s
	Size LTL	12315 16.261s	23 0.042s	470 0.672s	45 0.047s	30 0.039s	45 0.083s	27 0.054s	27 0.094s	37 0.358s	487 0.924s	273 0.136s	210 1.462s	235 1.558s	2010 6.965s	580 1.008s	590 2.023s	26902 12.462s	395 0.291s	230 0.242s	235 0.288s	228 0.307s	230 0.322s	235 0.403s	240 0.383s	51678 92.692s	51095 94.952s	4180 6.891s	970 4.092s	1250 1.848s	205 2.529s
	Example	Tanatos.b	Win32.Happy	Kelino.g	Netsky.a	klez.c	Netsky.d	klez.f	klez.e	Adon.1703	Spam.Tedroo.AB	Akez	Haharin.A	Haharin.dr	LdPinch.bx.dll	LdPinch-15	Win32/Toga!rfn	Mydoom.y	Plage.b	Mydoom-EG	W32.Mydoom.L	Mydoom.5	Mydoom.R	Mydoom.o@MM!zip	Sramota.avf	Win32.Runouce	Win32.CNHacker	Win32.Skybag	LdPinch.by	LdPinch.arr	Troj.LdPinch.er

Table 2 :

 2 Multiple pre * v.s. our direct LTL model-checking algorithm

	Formula Result
	Size
	Example
	cost
	Formula Result
	Size
	Example
	cost
	Formula Result
	Size
	Example

Table 3 :

 3 Experimental results our tool McAfee Norman BitDefender Kinsoft Avira eScan Kaspersky Qihoo360 Baidu Avast Symantec

	100%	24.8%	19.5%	31.2%	9.7%	34.1% 21.9%	53.1%	51.7%	1.4% 68.3%	82.4%

Table 4 :

 4 Detection rate: Our tool vs. well known antiviruses

https://lipn.univ-paris13.fr/∼touili/smodic/

Table 1: Our approach vs. standard LTL for PDSs

Self-modifying instructions are embedded into these programs.

Items α ′

1 and α ′ 2 are obvious. They respectively correspond to item 1 and item 2 of Definition 4 (since B(p) = 1 iff p ∈ G).

Item α ′ 3 is based on Lemma 1 and on item 3 of Definition 4. Indeed, it follows from Lemma 1 that A pre * ( (⟨p ′ , ϵ⟩, θ ′ ) ) contains a transition of the form (p 0 , θ)

----→ T (p ′ , θ ′ ) implies that (⟨p 0 , γ 0 ⟩, θ) ⇒ * (⟨p ′ , ϵ⟩, θ ′ ), and if b = 1, then (⟨p 0 , γ 0 ⟩, θ) ⇒ r (⟨p ′ , ϵ⟩, θ ′ ). Thus, in this case, the edge ((p, γ), θ) b∨B(p) ----→ ((p ′ , γ ′ ), θ ′ ) is added to G (item 3 of Definition 4) since ⟨p, γ⟩ → ⟨p 0 , γ 0 γ ′ ⟩ ∈ ∆.

Example: Let us illustrate the procedure by an example. Consider the previous example shown in Fig. 2. A pre * ((⟨p ′ ,ϵ⟩,θ ′ )) is shown in Fig. 3 (a) and A pre * ((⟨p ′ ,ϵ⟩,θ1)) is shown in Fig. 3 (b). The result G shown in Fig. 3 (c) is obtained as follows:

5. Now we have r ′ ∈ θ 1 and r 4 ∈ θ 1 , for every γ ∈ Γ, Rule α ′ 1 adds edges

8. No further additions are possible. Thus, the procedure terminates.

The result is depicted in Fig. 3 (c). By finding 1-labelled loops in G, the repeating heads are {((p 2 , γ 2 ), θ 1 ), ((p ′ , γ ′ ), θ 1 ), ((p 2 , γ ′ ), θ 1 ), ((p 1 , γ 1 ), θ 1 )}