Xin Par

Ye

Guillaume Bonfante

Jean-Marc Talbot

: Professeur

Valérie Viet

Model Checking Self Modifying Code

Keywords: Self-modifying Code, Model-checking, Pushdown System, Malware Detection, LTL, CTL, Reachability Analysis, Binary Code auto-modifiant, Vérification, Pushdown System, Détection de Malware, l'analyse de l

A Self modifying code is code that modifies its own instructions during execution time. It is nowadays widely used, especially in malware to make the code hard to analyse and to detect by anti-viruses. Thus, the analysis of such self modifying programs is a big challenge. Pushdown Systems (PDSs) is a natural model that is extensively used for the analysis of sequential programs because it allows to accurately model procedure calls and mimic the program's stack. In this thesis, we propose to extend the PushDown System model with self-modifying rules. We call the new model Self-Modifying PushDown System (SM-PDS). A SM-PDS is a PDS that can modify its own set of transitions during execution. First, we show how SM-PDSs can be used to naturally represent self-modifying programs and provide efficient algorithms to compute the backward and forward reachable configurations of SM-PDSs. Then, we consider the LTL model-checking problem of selfmodifying code. We reduce this problem to the emptiness problem of Self-modifying Büchi Pushdown Systems (SM-BPDSs). We also consider the CTL model-checking problem of selfmodifying code. We reduce this problem to the emptiness problem of Self-modifying Alternating Büchi Pushdown Systems (SM-ABPDSs). We implement our techniques in a tool called SMODIC. We obtained encouraging results. In particular, our tool was able to detect several self-modifying malwares; it could even detect several malwares that well-known anti-viruses such as McAfee, Norman, BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Avast and Symantec failed to detect.

système d'exploitation en utilisant des pushs et des sauts. Il est donc important de pouvoir suivre la pile pour détecter de tels appels obscurs. C'est pourquoi les systèmes PushDown ont été utilisés pour modéliser des programmes binaires afin de détecter les malwares. Cependant, ces travaux ne tiennent pas compte des malwares qui utilisent du code auto-modifiant, car les systèmes PushDown ne sont pas capables de modéliser des instructions auto-modifiantes.

Pour surmonter cette limitation, nous proposons dans cette thèse d'étendre le modéle du système PushDown avec des règles auto-modifiantes. Nous appelons ce nouveau modèle le système SM-PDS (Self-Modifying PushDown System). En gros, un SM-PDS est un PDS qui peut modifier son propre ensemble de transitions pendant l'exécution. Nous montrons comment les SM-PDS peuvent être utilisés pour représenter naturellement des programmes auto-modifiants. Il s'avère que les SM-PDS sont équivalents aux PDS standards. Nous montrons comment traduire un SM-PDS en PDS standard. Cette traduction est exponentielle. Par conséquent, il n'est pas efficace d'effectuer l'analyse de vérification du modèle sur le PDS équivalent. Nous proposons donc dans cette thèse des algorithmes directs pour les SM-PDS.

Analyse de l'accessibilité du code auto-modifiant

Tout d'abord, nous considérons le problème de l'accessibilité. Nous proposons des algorithmes directs pour calculer les ensembles d'accessibilité avant (post * ) et arrière (pre * ) pour les SM-PDS. Ceci permet d'effectuer efficacement l'analyse d'accessibilité pour les programmes auto-modifiants. Nos algorithmes sont basés sur (1) la représentation d'ensembles réguliers (potentiellement infinis) de configurations de SM-PDS en utilisant des automates à états finis, et (2) l'application de procédures de saturation sur les automates à états finis afin de prendre en compte l'effet de l'application des règles du SM-PDS. Ces résultats ont été publiés dans ICECCS 2017.

It has been an unforgettable and extraordinary experience of my Ph.D. years at LIPN, not only from the scientific perspective, but also from personal willpower. Here, I would like to take the opportunity to sincerely acknowledge all the people who helped and supported me in different ways. I would not have done it without them. First of all, I sincerely thank my two supervisors, Prof. Tayssir Touili and Prof. Jifeng He for giving me the opportunity to write this thesis. Prof. Tayssir Touili is also an excellent teacher. Thanks so much for her excellent and patient support and supervision throughout these four-year Ph.D. study. Without her detailed comments, this thesis cannot be completed. I would like to thank Prof. Jifeng He, my supervisor in China. His attitude in research inspired me a lot. Without his support, I cannot finish my thesis. Their attitude and devotion to the science encourages me all the time, and will continue inspiring me and be a role model for me in the rest of our lives.

My special thanks go to Prof. Guillaume Bonfante and Prof. Jean-Marc Talbot who kindly agreed to be my thesis referees. I would like to thank them for the valuable remarks.

I would like to thank Prof. Laure Petrucci and Prof. Valérie Viet Triem Tong who kindly agreed to be the members of my jury. My special thanks to Prof. Mihaela Sighireanu. I would like to thank her not only for accepting to be a member of my defense jury, but also for her help when I arrived in Paris to start my Ph.D study. Without her help, I might have no place to stay for my first year in Paris.

I am very grateful to many staff members of the Laboratoire d'Informatique de Paris Nord (LIPN) for their logistics help. I would like to thank Ms. Amina Hariti, the secretary of the doctoral school for the help with the paper work.

Many thanks to all my labmates both in LIPN and Shanghai for being there, for sharing good and bad times, for the encouragements.

I also would like to take it as an honor to express my thanks to my friends for their supportive influences in my life all the way. I thank them very much for coming to my life and helping me in any way.

Finally I would like to express my deep sense of gratitude to my ever loving big family. My parents, aunts, uncles and cousins have given me numerous encouragement and support. I would like to thank my dearest mother Yuying and father Jinshou, who give me unconditional support, love, and encouragement in my life. Thank you so much, my dearest families.

Introduction

Self-modifying code is code that modifies its own instructions during execution time. It is nowadays widely used, mainly to make programs hard to understand. For example, self-modifying code is extensively used to protect software intellectual property, since it makes reverse code engineering harder. It is also abundantly used by malware writers in order to obfuscate their malicious code and make it hard to analyse by static analysers and anti-viruses.

There are several kinds of implementations for self-modifying codes. Packing [START_REF] Debray | On the semantics of self-unpacking malware code[END_REF] consists in applying compression techniques to make the size of the executable file smaller. This converts the executable file to a form where the executable content is hidden. Then, the code is "unpacked" at runtime before execution. Such packed code is self-modifying. Encryption is another technique to hide the code. It uses some kind of invertible operations to hide the executable code with an encryption key. Then, the code is "decrypted" at runtime prior to execution. Encrypted programs are self-modifying. These two forms of self-modifying codes have been well studied in the litterature and could be handled by several unpacking tools such as [START_REF]Self-modifying code unpacking tool using dynamorio[END_REF][START_REF]Automated unpacking: A behaviour based approach[END_REF].

In this thesis, we consider another kind of self-modifying code, caused by selfmodifying instructions, where code is treated as data that can thus be read and written by self-modifying instructions. These self-modifying instructions are usually mov instructions, since mov can access memory, and read and write to it. For example, consider the program shown in Figure 1.1. For simplification matters, we suppose that the addresses' length is 1 byte. The binary code is given in the left side, while in the right side, we give its corresponding assembly code obtained by translating syntactically the binary code at each address. For example, ff is the binary code of the instruction push, thus, the first line is translated to push 0x3, the second line to push 0b, etc. Let us execute this code. First, we execute push 0x3, then push 0b, then mov 0x2 0xc. This last instruction will replace the first byte at address 0x2 by 0xc. Thus, at address 0x2, ff 0b is replaced by 0c 0b. Since 0c is the binary code of jmp, this means the instruction push 0b is replaced by jmp 0xb. Therefore, this code is selfmodifying. If we treat it blindly, without looking at the semantics of the different instructions, we will extract from it the Control Flow Graph CFG a, whereas its correct Control Flow Graph is CFG b. You can see that the mov instruction was able to modify the instructions of the program successfully via its ability to read and write the memory.

In this thesis, we consider the analysis of self-modifying programs where the code is modified by mov instructions. To this aim, we first need to find an adequate model for such programs. PushDown Systems (PDSs) is known to be a natural model for sequential programs [START_REF] Schwoon | Model-checking pushdown systems[END_REF], as it allows to track the contexts of the different calls in the program. Moreover, PushDown Systems allow to record and mimic the program's stack, which is very important for malware detection. Indeed, to check whether a program is malicious, anti-viruses start by identifying the calls it makes to the API functions. To evade these checks, malware writers try to obfuscate the calls they make to the Operating System by using pushes and jumps. Thus, it is important to be able to track the stack to detect such 1.1 Reachability Analysis of Self Modifying Code obfuscated calls. This is why PushDown Systems were used in [START_REF] Song | Efficient malware detection using model-checking[END_REF][START_REF] Song | Ltl model-checking for malware detection[END_REF] to model binary programs in order to perform malware detection. However, these works do not consider malwares that use self-modifying code, as PushDown Systems are not able to model self-modifying instructions.

To overcome this limitation, we propose in this thesis to extend the PushDown System model with self-modifying rules. We call the new model Self-Modifying PushDown System (SM-PDS). Roughly speaking, a SM-PDS is a PDS that can modify its own set of transitions during execution. We show how SM-PDSs can be used to naturally represent self-modifying programs. It turns out that SM-PDSs are equivalent to standard PDSs. We show how to translate a SM-PDS to a standard PDS. This translation is exponential. Thus, performing the modelchecking analysis on the equivalent PDS is not efficient. We propose then in this thesis direct model-checking algorithms for SM-PDSs.

Reachability Analysis of Self Modifying Code

First, we consider the reachability problem. We propose direct algorithms to compute the forward (post * ) and backward (pre * ) reachability sets for SM-PDSs. This allows to efficiently perform reachability analysis for self-modifying programs. Our algorithms are based on [START_REF] Bertrand | A model for self-modifying code[END_REF] representing regular (potentially infinite) sets of configurations of SM-PDSs using finite state automata, and (2) applying saturation procedures on the finite state automata in order to take into account the effect of applying the rules of the SM-PDS. These results were published in [START_REF] Touili | Reachability analysis of self modifying code[END_REF]. They are described in Chapter 2.

LTL Model Checking of Self Modifying Code

In Chapter 3, 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 a SM-BPDS by computing its repeating heads. This computation is

INTRODUCTION

based on computing labelled pre * configurations by applying a saturation procedure on labelled finite automata. These results are published in [START_REF] Touili | Ltl model checking for self modifying code[END_REF].

CTL Model Checking of Self Modifying Code

In Chapter 4, we consider the CTL model-checking problem for SM-PDSs. This allows to detect CTL-like malicious behaviors on self-modifying code. We reduce this problem to the emptiness checking problem of Self-modifying Alternating Büchi Pushdown Systems (SM-ABPDSs), and we propose an algorithm that computes a finite automaton that characterizes the set of configurations accepted by the SM-ABPDS.

SMODIC: A Model Checker for Self Modifying Code

We implemented our techniques in a tool for self-modifying code analysis called SMODIC. We successfully used SMODIC to model-check more than 900 selfmodifying binary codes. In particular, we applied SMODIC for malware detection, since malwares usually use self-modifying instructions, and since malicious behaviors can be described by LTL or CTL formulas. In our experiments, SMODIC was able to detect 895 malwares and to prove that 19 benign programs were benign. SMODIC 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. SMODIC can be found in https://lipn.univ-paris13.fr/ ~xin/smodic/index.html.

Related Works

Reachability analysis and LTL/CTL model-checking of pushdown systems was considered e.g. in [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][START_REF] Song | Efficient CTL model-checking for pushdown systems[END_REF][START_REF] Schwoon | Model-checking pushdown systems[END_REF]. Our algorithms are extensions of these works.

Model checking and static analysis approaches have been widely used to analyze binary programs, for instance, in [START_REF] Bozzelli | Complexity results on branching-time pushdown model checking[END_REF][START_REF] Esparza | Model-checking ltl with regular valuations for pushdown systems[END_REF][START_REF] Song | Ltl model-checking for malware detection[END_REF][START_REF] Balakrishnan | Model checking x86 executables with codesurfer/x86 and WPDS++[END_REF][START_REF] Bergeron | Static detection of malicious code in executable programs[END_REF][START_REF] Kinder | Detecting malicious code by model checking[END_REF][START_REF] Christodorescu | Semantics-aware malware detection[END_REF][START_REF] Christodorescu | Semantics-aware malware detection[END_REF][START_REF] Singh | Static verification of worm and virus behavior in binary executables using model checking[END_REF]. These works cannot handle self-modifying code.

Related Works

Cai et al. [START_REF] Cai | Certified self-modifying code[END_REF] use a Hoare-logic-style framework to describe self-modifying code by applying local reasoning and separation logic, and treating program code uniformly as regular data structure. However, [START_REF] Cai | Certified self-modifying code[END_REF] requires programs to be manually annotated with invariants. In [START_REF] Debray | On the semantics of self-unpacking malware code[END_REF], the authors describe a formal semantics for self-modifying codes, and use that semantics to represent self-unpacking code. This work only deals with packing and unpacking behaviours, it cannot capture self-modifying instructions as we do. In [START_REF] Bonfante | A computability perspective on self-modifying programs[END_REF], Bonfante et al. provide an operational semantics for self-modifying programs and show that they can be constructively rewritten to a non-modifying program. All these specifications [START_REF] Bonfante | A computability perspective on self-modifying programs[END_REF][START_REF] Cai | Certified self-modifying code[END_REF][START_REF] Debray | On the semantics of self-unpacking malware code[END_REF] are too abstract to be used in practice.

In [START_REF] Bertrand | A model for self-modifying code[END_REF], the authors propose a new representation of self-modifying code named State Enhanced-Control Flow Graph (SE-CFG). SE-CFG extends standard control flow graphs with a new data structure, keeping track of the possible states programs can reach, and with edges that can be conditional on the state of the target memory location. It is not easy to analyse a binary program only using its SE-CFG, especially that this representation does not allow to take into account the stack of the program. [START_REF] Blazy | Verified abstract interpretation techniques for disassembling low-level self-modifying code[END_REF] propose abstract interpretation techniques to compute an over-approximation of the set of reachable states of a self-modifying program, where for each control point of the program, an over-approximation of the memory state at this control point is provided. [START_REF] Roundy | Hybrid analysis and control of malware[END_REF] combine static and dynamic analysis techniques to analyse self-modifying programs. Unlike our self-modifying pushdown systems, these techniques [START_REF] Roundy | Hybrid analysis and control of malware[END_REF][START_REF] Blazy | Verified abstract interpretation techniques for disassembling low-level self-modifying code[END_REF] cannot handle the program's stack.

Unpacking binary code is 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.

There are a lot of tools that can deal with binary code analysis [START_REF] Balakrishnan | Codesurfer/x86-a platform for analyzing x86 executables*[END_REF][START_REF] Bardin | The bincoa framework for binary code analysis[END_REF][START_REF] Bergeron | Static detection of malicious code in executable programs[END_REF][START_REF] Brumley | Bitscope: Automatically dissecting malicious binaries[END_REF][START_REF] Brumley | Bap: A binary analysis platform[END_REF][START_REF] Bruschi | Detecting selfmutating malware using control-flow graph matching[END_REF][START_REF] David | Binsec/se: A dynamic symbolic execution toolkit for binary-level analysis[END_REF][START_REF] Song | Efficient malware detection using model-checking[END_REF][START_REF] Song | Ltl model-checking for malware detection[END_REF][START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF][START_REF] Dam | Malware detection based on graph classification[END_REF][START_REF] Dam | Learning malware using generalized graph kernels[END_REF][START_REF] Dam | Precise extraction of malicious behaviors[END_REF][START_REF] Simon | The gdsl toolkit: Generating frontends for the analysis of machine code[END_REF][START_REF] Song | Bitblaze: A new approach to computer security via binary analysis[END_REF][START_REF] Thakur | Directed proof generation for machine code[END_REF]. POMMADE [START_REF] Song | Efficient malware detection using model-checking[END_REF][START_REF] Song | Ltl model-checking for malware detection[END_REF] is a malware detector based on LTL and CTL model-checking of PDSs. STAMAD [START_REF] Dam | Malware detection based on graph classification[END_REF][START_REF] Dam | Learning malware using generalized graph kernels[END_REF][START_REF] Dam | Precise extraction of malicious behaviors[END_REF] is a malware detector based on PDSs and machine learning. However, all these tools cannot handle self-modifying code. The only tools that we know of and that can deal with self-modifying code are BE-PUM [START_REF] Nguyen | Pushdown model generation of malware[END_REF] and CoDisasm [5].

INTRODUCTION

determine the precise destinations of branches for indirect jumps. This tool can deal with self-modifying code caused by modifying the destinations of indirect jumps, including overwriting the return address of a function (in the stack). But it cannot handle self-modifying instructions.

CoDisasm [5] is a tool that focuses on the disassembly of x86 code that includes self-modifying instructions and code overlapping. CoDisasm deals only with disassembling the code. It does not consider model-checking problems of code. Currently, we use Jakstab [START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF] to disassemble binary code. CoDisasm might help our disassembly process and make it more precise. We plan to use CoDisasm in the future (instead of Jakstab) and see whether it will improve the precision of our extracted CFGs.

Thesis Organization

In Chapter 2, we give the definition of SM-PDS and show how a SM-PDS can describe self-modifying codes. We also present our direct algorithms for reachability analysis of SM-PDSs. Chapter 3 shows how to reduce the LTL model checking problem of SM-PDSs to the emptiness problem of self-modifying büchi pushdown systems. We tackle the CTL model checking problem on SM-PDSs in Chapter 4. Chapter 5 presents the tool SMODIC that implements our algorithms.

Reachability Analysis of Self Modifying Code

A Self modifying code is code that modifies its own instructions during execution time. It is nowadays widely used, especially in malware to make the code hard to analyse and to detect by anti-viruses. Thus, the analysis of such self modifying programs is a big challenge. Pushdown Systems (PDSs) is a natural model that is extensively used for the analysis of sequential programs because it allows to accurately model procedure calls and mimic the program's stack. In this chapter, we propose to extend the PushDown System model with self-modifying rules. We call the new model Self-Modifying PushDown System (SM-PDS). A SM-PDS is a PDS that can modify its own set of transitions during execution. We show how SM-PDSs can be used to naturally represent self-modifying programs and provide efficient algorithms to compute the backward and forward reachable configurations of SM-PDSs. We implemented our techniques in a tool and obtained encouraging results. In particular, we successfully applied our tool for the detection of self-modifying malware.

2.1

An Example of A Self-modifying Code

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

of the mov instruction. It copies the data item referred to by its second operand (register or memory location) into its first operand. In Fig. 2.1, in the box on the left, 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, ff is the binary code of the instruction push. Thus, the first line is translated to push 0b. The second instruction mov 0x2 0xc will replace the first byte at address 0x2 by 0xc. Thus, at address 0x2, ff 0b is replaced by 0c 0b, i.e., the instruction push 0b is replaced by jmp 0b. If we analyse this code without taking into account the fact that mov 0x2 0xc is a self-modifying instruction, then, we will obtain the Control Flow Graph "CFG a", and we will reach the conclusion that the Bagle malicious behaviour implemented at address 0b by the API functions RegCreateKeyA, RegDeleteVal-ueA, and RegCloseKey is not reachable. However, the actual CFG is "CFG b", where the malicious fragment of the malware Bagle.J that starts at address 0b is reached and will be executed.

It can be seen from this example that self-modifying codes can make malware detection harder, and that the mov instruction is able to modify instructions of the program successfully via its ability to read and write the memory. Thus, it is crucial to be able to analyse this kind of self-modifying code. We introduce in this section our new model: Self-modifying Pushdown Systems.

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

∆ c ⊆ P × (∆ ∪ ∆ c ) × (∆ ∪ ∆ c ) × P is 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 (r 1 ,r 2 ) ֒----→ p ′ ∈ ∆ c . A Pushdown System (PDS) is a SM-PDS where ∆ c = ∅.
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 (r 1 ,r 2 ) ֒----→ 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 . 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 (r 1 ,r 2 ) ֒----→ 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.

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

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 . We define i ⇒ as follows:

c i ⇒ c ′ iff there exists a sequence of configurations c 0 ⇒ P c 1 ⇒ P ... ⇒ P c i s.t. c 0 = c and c i = c ′ 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 omit the subscript P when it is understood from the context.

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 (r 1 ,r 3 ) ֒----→ 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 ).

From SM-PDSs to PDSs

A SM-PDS can be described by a PDS. This is due to the fact that the number of phases is finite, thus, we can encode phases in the control points of the PDS: Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS, we compute the PDS P ′ = (P ′ , Γ, ∆ ′ ) as follows: P ′ = P × 2 ∆∪∆c . Initially, ∆ ′ = ∅. For every θ ∈ 2 ∆∪∆c , r ∈ θ:

1. If r = p, γ ֒→ p ′ , w ∈ ∆ ∩ θ, we add (p, θ), γ ֒→ (p ′ , θ), w to ∆ ′ 2. if r = p (r 1 ,r 2 ) ֒----→ p ′ ∈ ∆ c ∩ θ, then for every γ ∈ Γ, we add (p, θ), γ ֒→ (p ′ , θ ′ ), γ to ∆ ′ , where θ ′ = (θ \ {r 1 }) ∪ {r 2 }.
It is easy to see that:

2.2 Self Modifying Pushdown Systems Proposition 1 ( p, w , θ) ⇒ P ( p ′ , w ′ , θ ′ ) iff (p, θ), w ⇒ P ′ (p ′ , θ ′ ), w ′ .
Proof: ⇒: We will show that if ( p, w , θ) ⇒ P ( p ′ , w ′ , θ ′ ), then we have (p, θ), w ⇒ P ′ (p ′ , θ ′ ), w ′ . There are two cases depending on the form of the rule that led to this transition.

• Case θ = θ ′ : it means that the transition does not correspond to a selfmodifying transition rule. Thus there is a rule r ∈ θ of the form r = p, γ ֒→ p ′ , u ′ that led to this transition. Let u be such that w = γu, w ′ = u ′ u. By the construction rule of the PDS P ′ , we have (p, θ), γ ֒→ (p ′ , θ), u ′ ∈ ∆ ′ . Therefore, (p, θ), γu ⇒ P ′ (p ′ , θ), u ′ u holds. This implies that (p, θ), w ⇒ P ′ (p ′ , θ), w ′ .

• Case θ = θ ′ : it means that the transition corresponds to a self-modifying transition rule. Thus there is a rule r ∈ θ of the form p (r 1 ,r 2 ) ֒----→ p ′ that led to this transition. Let u be such that w = γu, w ′ = γu. By the construction rule of the PDS P ′ , we have (p, θ), γ ֒→ (p ′ , θ ′ ), γ ∈ ∆ ′ where θ ′ = (θ\{r 1 }) ∪ {r 2 }. Therefore, (p, θ), γu ⇒ P ′ (p ′ , θ ′ ), γu holds. This implies that (p, θ), w ⇒ P ′ (p ′ , θ ′ ), w ′ . ⇐: We will show that if (p, θ), w ⇒ P ′ (p ′ , θ ′ ), w ′ , then ( p, w , θ) ⇒ P ( p ′ , w ′ , θ ′ ). Let γ ∈ Γ, u, u ′ ∈ Γ * be such that w = γu, w ′ = u ′ u. There are two cases.

• Case θ = θ ′ . Let r = (p, θ), γ ֒→ (p ′ , θ), u ′ ∈ ∆ ′ be the rule that led to the transition. By the construction of PDS P ′ , there must exist a rule r ∈ θ such that r = p, γ ֒→ p ′ , u ′ . Therefore, ( p, γu , θ) ⇒ P ( p, u ′ u , θ) holds. This implies that ( p, w , θ) ⇒ P ( p, w ′ , θ ′ ).

• Case θ = θ ′ . Let r = (p, θ), γ ֒→ (p ′ , θ ′ ), γ ∈ ∆ ′ be the rule leading to the transition and u ′ = γ. By the construction of PDS P ′ , there must exist

a rule r ∈ θ such that r = p (r 1 ,r 2 )
֒----→ p ′ where θ ′ = (θ\{r 1 }) ∪ {r 2 }. Therefore, ( p, γu , θ) ⇒ P ( p ′ , γu , θ ′ ) holds. This implies that ( p, w , θ) ⇒ P ( p, w ′ , θ ′ ). ✷ Thus, we get:

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

Theorem 2.2.1 Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS, we can compute an equivalent PDS

P ′ = (P ′ , Γ, ∆ ′ ) such that |∆ ′ | = |∆| + |∆ c | • |Γ| • 2 O(|∆|+|∆c|) and |P ′ | = |P | • 2 O(|∆|+|∆c|) .

From SM-PDSs to Symbolic PDSs

Instead of recording the phases θ of the SM-PDS in the control points of the equivalent PDS, we can have a more compact translation from SM-PDSs to symbolic PDSs [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: Definition 2 A symbolic pushdown system is a tuple P = (P, Γ, δ), where P is a set of control points, Γ is the stack alphabet, and δ is a set of symbolic rules of the form:

p, γ R ֒----→ p ′ , w , where R ⊆ 2 ∆∪∆c × 2 ∆∪∆c is a relation.
A symbolic PDS defines a transition relation ❀ P between SM-PDS configurations as follows: Let c = ( p, γw ′ , θ) be a configuration and let p, γ R ֒----→ p ′ , w be a rule in δ, then: ( p, γw ′ , θ) ❀ P ( p ′ , ww ′ , θ ′ ) for (θ, θ ′ ) ∈ R. Let ❀ * P be the transitive, reflexive closure of ❀ P . Then, given a SM-PDS P = (P, Γ, ∆, ∆ c ), we can compute an equivalent symbolic PDS P ′ = (P, Γ, ∆ ′ ) such that: Initially, ∆ ′ = ∅;

• For every p, γ ֒→ p ′ , w ∈ ∆, add p, γ R id ֒----→ p ′ , w to ∆ ′ , where R id is the identity relation.

• For every r = p (r 1 ,r 2 ) ֒----→ p ′ ∈ ∆ c and every γ ∈ Γ, add p, γ R ֒----→ p ′ , γ to ∆ ′ , where R = {(θ 1 , θ 2 ) ∈ 2 ∆∪∆c × 2 ∆∪∆c | r ∈ θ 1 and θ 2 = (θ 1 \ {r 1 }) ∪ {r 2 }}.
It is easy to see that:

Proposition 2 ( p, w , θ) ⇒ P ( p ′ , w ′ , θ ′ ) iff ( p, w , θ) ❀ P ′ ( p ′ , w ′ , θ ′ ).
Proof: ⇒: we will show that if ( p, w , θ) ⇒ P ( p ′ , w ′ , θ ′ ), then ( p, w , θ) ❀ P ′ ( p ′ , w ′ , θ ′ ). There are two cases depending on the form of the rule that led to this transition.

• Case θ = θ ′ , it means that the transition does not correspond to a selfmodifying transition rule. Thus there is a rule r ∈ θ of the form r = p, γ ֒→ p ′ , u ′ that led to this transition. Let u be such that w = γu, w ′ = u ′ u. By construction of the symbolic pushdown system P ′ , p, γ

R id ֒----→ p ′ , u ′ ∈ ∆ ′ , therefore, ( p, γu , θ) ❀ P ′ ( p ′ , u ′ u , θ) holds. This implies that ( p, w , θ) ❀ P ′ ( p ′ , w ′ , θ ′ ).
• Case θ = θ ′ , it means that the transition corresponds to a self-modifying transition rule. Thus there is a rule r ∈ θ of the form r = p (r 1 ,r 2 ) ֒----→ p ′ that led to this transition and θ ′ = (θ\{r 1 }) ∪ {r 2 }. Let u be such that w = γu, w ′ = γu. By construction of the symbolic pushdown system

P ′ , p, γ R ֒----→ p ′ , γ ∈ ∆ ′ and R = {(θ, θ ′ ) ∈ 2 ∆∪∆c × 2 ∆∪∆c | r ∈ θ and θ ′ = (θ \ {r 1 }) ∪ {r 2 }}, therefore, ( p, γu , θ) ❀ P ′ ( p ′ , γu , θ ′ ) holds. This implies that ( p, w , θ) ❀ P ′ ( p ′ , w ′ , θ ′ ). ⇐: we will show that if ( p, w , θ) ❀ P ′ ( p ′ , w ′ , θ ′ ), then ( p, w , θ) ⇒ P ( p ′ , w ′ , θ ′ ). Let γ ∈ Γ, u, u ′ ∈ Γ * be such that w = γu, w ′ = u ′ u.
There are two cases.

• Case θ = θ ′ . Let p, γ R id ֒----→ p ′ , u ′ ∈ ∆ ′ be
the rule applied to this transition. By the construction of the symbolic pushdown system P ′ , there must exist a rule r ∈ θ s.t. r = p, γ ֒→ p ′ , u ′ ∈ ∆. Therefore, ( p, γu , θ) ⇒ P ( p ′ , u ′ u , θ) holds. This implies that ( p, w , θ) ⇒ P ( p ′ , w ′ , θ ′ ).

• Case θ = θ ′ . Let p, γ R ֒----→ p ′ , γ ∈ ∆ ′ be
the rule applied to this transition with w ′ = γu. By the construction of the symbolic pushdown system P ′ , there must exist a rule r ∈ θ of the form r = p

(r 1 ,r 2 ) ֒----→ p ′ ∈ ∆ c s.t. R = {(θ 1 , θ 2 ) ∈ 2 ∆∪∆c × 2 ∆∪∆c | r ∈ θ 1 and θ 2 = (θ 1 \ {r 1 }) ∪ {r 2 }}. Therefore, θ ′ = (θ\{r 1 }) ∪ {r 2 } and ( p, γu , θ) ❀ P ′ ( p ′ , γu , θ ′ ) hold. This implies that ( p, w , θ) ❀ P ′ ( p ′ , w ′ , θ ′ ).
✷ Thus, we get: Theorem 2.2.2 Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS, we can compute an equivalent symbolic PDS

P ′ = (P ′ , Γ, ∆ ′ ) such that |P ′ | = |P |, |∆ ′ | = |∆| + |∆ c | • |Γ|,
and the size of the relations used in the symbolic transitions is 2 O(|∆|+|∆c|) .

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

2.3 Modeling Self-modifying Code with SM-PDSs

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. 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] Veith | 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 mimics 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 (r 1 ,r 2 ) ֒----→ n ′ to ∆ c . This is the SM-PDS rule corresponding to the instruction mov l v at control point n.

Representing Infinite Sets of Configurations of a SM-PDS

Multi-automata were introduced in [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] to finitely represent regular infinite sets of configurations of a PDS. A configuration c = ( p, w , θ) of a SM-PDS involves a PDS configuration p, w , together with the current set of transition rules (phase) θ. To finitely represent regular infinite sets of such configurations, we extend multi-automata in order to take into account the phases θ:

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

Definition 3 Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS. A P-automaton is a tuple A = (Q, Γ, T, P, F ) where Γ is the automaton alphabet, Q is a finite set of states, P × 2 ∆∪∆c ⊆ Q is the set of initial states, T ⊂ Q × (Γ ∪ {ǫ}) × Q is the set of transitions and F ⊆ Q is the set of final states.

If q, γ, q ′ ∈ T , we write q γ -→ T q ′ . We extend this notation in the obvious manner to sequences of symbols: (1) ∀q ∈ Q, q ǫ -→ T q, and (2) ∀q,

q ′ ∈ Q, ∀γ ∈ Γ∪ {ǫ}, ∀w ∈ Γ * for w = γ 0 γ 1 • • • γ n , q γw --→ T q ′ iff ∃q ′′ ∈ Q, q γ -→ T q ′′ and q ′′ w -→ T q ′ . If q w -→ T q ′ holds, we say that q w -→ T q ′ is a path of A. A configuration ( p, w , θ) is accepted by A iff A contains a path (p, θ) γ 0 --→ T q 1 γ 1 --→ T q 2 • • • q n γn
--→ T q where q ∈ F . Let L(A) be the set of configurations accepted by A. Let C be a set of configurations of the SM-PDS P. C is regular if there exists a P-automaton A such that C = L(A).

Efficient Computation of pre * images

Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS, and let A = (Q, Γ, T, P, F ) be a Pautomaton that represents a regular set of configurations C ( C = L(A)). To compute pre * (C), one can use the translation of Section 2.2.2 to compute an equivalent PDS, and then apply the algorithms of [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]. This procedure is too complex since the size of the obtained PDS is huge. One can also use the translation of Section 2.2.3 to compute an equivalent symbolic PDS, and then use the algorihms of [START_REF] Schwoon | Model-checking pushdown systems[END_REF]. However, this procedure is not optimal neither since the number of elements of the relations considered in the rules of the symbolic PDSs are huge. We present in this section a direct and more efficient algorithm that computes pre * (C) without any need to translate the SM-PDS to an equivalent PDS or symbolic PDS. We assume w.l.o.g. that A has no transitions leading to an initial state. We also assume that the self-modifying rules

r = p (r 1 ,r 2 )
֒----→ p ′ in ∆ c are such that r = r 1 . This is not a restriction since a rule of the form r = p (r,r 2 ) ֒----→ p ′ can be replaced by these rules that meet this constraint: r = p (r ⊥ ,r ⊥ ) ֒----→ p i and p i (r,r 2 ) ֒----→ p ′ , where r ⊥ is a new fake rule that we can add to all phases.

The construction of A pre * follows the same idea as for standard pushdown systems (see [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]). It consists in adding iteratively new transitions to the 2.5 Efficient Computation of pre * images automaton A according to saturation rules (reflecting the backward application of the transition rules in the system), while the set of states remains unchanged. Therefore, let A pre * be the P-automaton (Q, Γ, T ′ , P, F ), where T ′ is computed using the following saturation rules: initially T ′ = T .

α 1 : If r = p, γ ֒→ p 1 , w ∈ ∆, where w ∈ Γ * . For every θ ⊆ ∆ ∪ ∆ c s.t. r ∈ θ,
if there exists in T ′ a path π = (p 1 , θ) w -→ T q, then add ((p, θ), γ, q) to T ′ .

α 2 : if r = p (r 1 ,r 2 )
֒----→ p 1 ∈ ∆ c for every θ ⊆ ∆ ∪ ∆ c s.t. r ∈ θ, r 2 ∈ θ and for every γ ∈ Γ, if there exists in T ′ a transition t = (p 1 , θ) γ -→ T q, then add ((p, θ ′ ), γ, q) to T ′ where θ = (θ ′ \ {r 1 }) ∪ {r 2 }.

The procedure above terminates since there is a finite number of states and phases. Let us explain intuitively the role of the saturation rule (α 1 ). Let r = p, γ ֒→ p ′ , w ∈ ∆. Consider a path in the automaton of the form (p ′ , θ ′ ) w -→ T ′ q w ′ --→ T ′ q F , where q F ∈ F . This means, by definition of P-automata, that the configuration c = ( p ′ , ww ′ , θ ′ ) is accepted by A pre * . If r is in θ ′ , then the configuration c ′ = ( p, γw ′ , θ ′ ) is a predecessor of c. Therefore, it should be added to A pre * . This configuration is accepted by the run (p, θ ′ ) γ -→ T ′ q w ′ --→ T ′ q F added by rules (α 1 ).

Rule (α 2 ) deals with modifying rules: Let r = p (r 1 ,r 2 ) ֒----→ p ′ ∈ ∆ c . Consider a path in the automaton of the form (p ′ , θ ′ ) γ -→ T ′ q w ′ --→ T ′ q F , where q F ∈ F . This means, by definition of P-automata, that the configuration c = ( p ′ , γw ′ , θ ′ ) is accepted by A pre * . If r and r 2 are in θ ′ , then the configuration c ′ = ( p, γw ′ , θ) is a predecessor of c, where θ ′ = (θ \ {r 1 }) ∪ {r 2 }. Therefore, it should be added to A pre * . This configuration is accepted by the run π ′ = (p, θ) γ -→ T ′ q w ′ --→ T ′ q F added by rules (α 2 ). Thus, we can show that: Example 2 Let us illustrate the procedure by an example. Consider the SM-PDS with control points P = {p 0 , p 1 , p 2 , p 3 , p 4 , p 5 } and ∆, ∆ c as shown in the left half

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

Δ : Δ : of Fig. 2.2. Let A be the automaton that accepts the set C = {( p 0 , γ 0 γ 0 , θ 0 )}, also shown on the left where (p 0 , θ 0 ) is the initial state and s 2 is the final state. The result of the algorithm is shown in the right half of Fig. 2.2. The result is obtained through the following steps:

r 1 : ⟨p 0 , γ 0 ⟩ ↪ ⟨p 1 , γ 1 γ 0 ⟩ r 1 : ⟨p 0 , γ 0 ⟩ ↪ ⟨p 1 , γ 1 γ 0 ⟩ r 2 : ⟨p 5 , γ 1 ⟩ ↪ ⟨p 2 , γ 2 γ 0 ⟩ r 2 : ⟨p 5 , γ 1 ⟩ ↪ ⟨p 2 , γ 2 γ 0 ⟩ r 3 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 3 , ϵ⟩ r 3 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 3 , ϵ⟩ r 4 : ⟨p 4 , γ 0 ⟩ ↪ ⟨p 0 , ϵ⟩ r 4 : ⟨p 4 , γ 0 ⟩ ↪ ⟨p 0 , ϵ⟩ r 5 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 4 , γ 0 ⟩ r 5 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 4 , γ 0 ⟩ Δ c : Δ c : r′! : p 3 r′! : p 3 θ 0 = {r 5 , r 2 , r 3 , r 4 , r′!} θ 0 = {r 5 , r 2 , r 3 , r 4 , r′!} p 0 , θ 0 p 0 , θ 0 s 1 s 1 s 2 s 2 γ 0 γ 0 γ 0 γ 0 p 0 , θ 0 p 0 , θ 0 s 1 s 1 s 2 s 2 γ 0 γ 0 γ 0 γ 0 γ 2 p 4 , θ 0 p 4 , θ 0 γ 0 p 1 , θ 0 p 1 , θ 0 γ 1 p 3 , θ 1 p 3 , θ 1 γ 0 p 2 , θ 1 p 2 , θ 1 p 5 , θ 1 p 5 , θ 1 γ 1 ↪ p 4 (r 1 , r 5 )
1. First, we note that (p 0 , θ 0 ) ǫ -→ T ′ (p 0 , θ 0 ) holds. Since p 0 , ǫ occurs on the right hand side of rule r 4 and r 4 ∈ θ 0 , then Rule (α 1 ) adds the transition (p 4 , θ 0 )

γ 0 -→ (p 0 , θ 0 ) to T ′ .
2. Now that we have (p 4 , θ 0 )

γ 0 -→ T ′ (p 0 , θ 0 ), since r 5 ∈ θ 0 , Rule (α 1 ) adds (p 1 , θ 0 ) γ 1 -→ (p 0 , θ 0 ) to T ′ . 3. Since we have (p 4 , θ 0 ) γ 0 -→ T ′ (p 0 , θ 0 ), the self-modifying transition r ′ ∈ θ 0 can be applied. Thus, Rule (α 2 ) adds (p 3 , θ 1 ) γ 0 -→ (p 0 , θ 0 ) to T ′ where θ 1 = (θ 0 \ {r 5 }) ∪ {r 1 } = {r 1 , r 2 , r 3 , r 4 , r ′ }. 4. Since (p 3 , θ 1 ) ǫ - → (p 3 , θ 1 ) and r 3 ∈ θ 1 , Rule (α 1 ) adds (p 2 , θ 1 ) γ 2 -→ (p 3 , θ 1 ) to T ′ . 5. Then, there is a path (p 2 , θ 1 ) γ 2 -→ T ′ (p 3 , θ 1 ) γ 0 -→ T ′ (
p 0 , θ 0 ). Since p 2 , γ 2 γ 0 occurs on the right hand side of r 2 and r 2 ∈ θ 1 , then Rule (α 1 ) adds the transition (p 5 , θ 1 )

γ 1 -→ (p 0 , θ 0 ) to T ′ .
2.5 Efficient Computation of pre * images 6. No further additions are possible. Thus, the procedure terminates.

p 0 , θ 0 p 0 , θ 0 s 1 s 1 s 2 s 2 γ 0 γ 0 γ 0 γ 0 Δ : Δ : r 1 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 0 , γ 0 ⟩ r 1 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 0 , γ 0 ⟩ r 2 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 1 , γ 1 ⟩ r 2 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 1 , γ 1 ⟩ r 3 : ⟨p 3 , γ 0 ⟩ ↪ ⟨p 2 , ϵ⟩ r 3 : ⟨p 3 , γ 0 ⟩ ↪ ⟨p 2 , ϵ⟩ r 4 : ⟨p 4 , γ 1 ⟩ ↪ ⟨p 3 , γ 0 γ 2 ⟩ r 4 : ⟨p 4 , γ 1 ⟩ ↪ ⟨p 3 , γ 0 γ 2 ⟩ r 5 : ⟨p 0 , γ 0 ⟩ ↪ ⟨p 4 , ϵ⟩ r 5 : ⟨p 0 , γ 0 ⟩ ↪ ⟨p
θ 0 = {r 1 , r 2 , r 3 , r 4 , r 5 , r 1 c , r 2 c , r 3 c , r 4 c } θ 0 = {r 1 , r 2 , r 3 , r 4 , r 5 , r 1 c , r 2 c , r 3 c , r 4 c } p 0 , θ 0 p 0 , θ 0 s 1 s 1 s 2 s 2 p 1 , θ 0 p 1 , θ 0 γ 1 p 4 , θ 0 p 4 , θ 0 γ 1 γ 0 p 5 , θ 1 p 5 , θ 1 γ 1 p 5 , θ 2 p 5 , θ 2 γ 0 γ 0 θ 1 = {r 1 , r 3 , r 4 , r 5 , r 6 , r 1 c , r 2 c , r 3 c , r 4 c } θ 0 = {r 1 , r 2 , r 3 , r 4 , r 5 , r 1 c , r 2 c , r 3 c , r 4 c } θ 2 = {r 2 , r 3 , r 4 , r 5 , r 7 , r 1 c , r 2 c , r 3 c , r 4 c } p 2 , θ 1 p 2 , θ 1 γ 0 γ 0 γ 2 p 3 , θ 1 p 3 , θ 1 γ 0 p 4 , θ 1 p 4 , θ 1 p 0 , θ 1 p 0 , θ 1 γ 0 γ 1 p 2 , θ 0 p 2 , θ 0 γ 2 p 3 , θ 0 p 3 , θ 0 γ 0 γ 2 γ 1 γ 1 γ 2 γ 1 θ 3 = {r 3 , r 4 , r 5 , r 6 , r 7 , r 1 c , r 2 c , r 3 c , r 4 c } p 5 , θ 3 p 5 , θ 3 γ 0 p 2 , θ 3 p 2 , θ 3 γ 2 γ 0 p 3 , θ 3 p 3 , θ 3 γ 0 p 4 , θ 3 p 4 , θ 3 γ 1 p 0 , θ 3 p 0 , θ 3 γ 0 p 2 , θ 2 p 2 , θ 2 γ 0 γ 2 p 3 , θ 2 p 3 , θ 2 γ 0 p 4 , θ 2 p 4 , θ 2 γ 1 p 0 , θ 2 p 0 , θ 2 γ 0 γ 1 γ 2 γ 2 γ 0 γ 1 γ 2 ↪ ↪ p 2 ↪ ↪ (r 6 , r 2 ) (r 7 , r 1 ) (r 2 , r 6 ) (r 1 , r 7 ) p 3 p 0 p 4

Let

A be the automaton that accepts the set C = {( p 0 , γ 0 γ 0 , θ 0 )} where (p 0 , θ 0 ) is the initial state and s 2 is the final state as shown on the left. The result A pre * of the algorithm is on the right half of Fig. 2.3. The result is obtained through the following steps:

1. Since (p 0 , θ 0 ) γ - → T ′ s 1 and r 1 ∈ θ 0 , then Rule (α 1 ) adds (p 1 , θ 0 ) γ 1 -→ s 1 to T ′ . 2. Since (p 1 , θ 0 ) γ 1 -→ T ′ s 1 and r 2 ∈ θ 0 , Rule (α 1 ) adds the transition (p 2 , θ 0 ) γ 2 -→ s 1 to T ′ . 3. Since (p 2 , θ 0 ) ǫ - → T ′ (p 2 , θ 0 ) and r 3 ∈ θ 0 , Rule (α 1 ) adds the transition (p 3 , θ 0 ) γ 0 -→ (p 2 , θ 0 ) to T ′ . 4. Then, there is a path (p 3 , θ 0 ) γ 0 -→ T ′ (p 2 , θ 0 ) γ 2 -→ T ′ s 1 and r 4 ∈ θ 0 , Rule α 1 adds the transition (p 4 , θ 0 ) γ 1 -→ s 1 to T ′ . 5. Because (p 4 , θ 0 ) ǫ - → T ′ (p 4 , θ 0 ) and r 5 ∈ θ 0 , Rule (α 1 ) adds the transition (p 0 , θ 0 ) γ 0 -→ (p 4 , θ 0 ) to T ′ .

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

6. Since (p 0 , θ 0 ) γ 0 -→ T ′ (p 4 , θ 0 ) and r 1 ∈ θ 0 , Rule (α 1 ) adds the transition (p 1 , θ 0 ) γ 1 -→ (p 4 , θ 0 ) to T ′ . Then, since r 2 ∈ θ 0 , Rule (α 1 ) adds the transition (p 2 , θ 0 )

γ 2 -→ (p 4 , θ 0 ) to T ′ . 7. Since there is a path (p 3 , θ 0 ) γ 0 -→ T ′ (p 2 , θ 0 ) γ 2 -→ T ′ (p 4 , θ 0 ) and r 4 ∈ θ 0 , Rule (α 1 ) adds (p 4 , θ 0 ) γ 1 -→ (p 4 , θ 0 ) to T ′ . 8. Since (p 4 , θ 0 ) γ 1 -→ T ′ s 1 , (p 4 , θ 0 ) γ 1 -→ T ′ (p 4 , θ 0 ) and r 1 c , r 2 ∈ θ 0 , Rule (α 2 ) adds (p 5 , θ 1 ) γ 1 -→ s 1 and (p 5 , θ 1 ) γ 1 -→ (p 4 , θ 0 ) to T ′ where θ 1 = (θ 0 \ {r 2 }) ∪ r 6 = {r 1 , r 3 , r 4 , r 5 , r 6 , r 1 c , r 2 c , r 3 c , r 4 c }.
For the same reason, since (p 0 , θ 0 )

γ 0 -→ T ′ (p 4 , θ 0 ), (p 0 , θ 0 ) γ - → T ′ s 1 and r 1 , ∈ θ 1 , r 2 c ∈ θ 0 , Rule (α 2 ) adds the transitions (p 5 , θ 2 ) γ 0 -→ (p 4 , θ 0 ) and (p 5 , θ 2 ) γ 0 -→ s 1 to T ′ where θ 2 = (θ 0 \ {r 1 }) ∪ {r 7 } = {r 2 , r 3 , r 4 , r 5 , r 7 , r 1 c , r 2 c , r 3 c , r 4 c }.
9. Since (p 5 , θ 1 )

γ 1 -→ T ′ s 1 , (p 5 , θ 1 ) γ 1 -→ T ′ (p 4 , θ 0 ) and r 6 ∈ θ 1 , Rule (α 1 ) adds the transitions (p 2 , θ 1 ) γ 2 -→ s 1 and (p 2 , θ 1 ) γ 2 -→ (p 4 , θ 0 ) to T ′ . 10. Since (p 2 , θ 1 ) ǫ - → T ′ (p 2 , θ 1 ) and r 3 ∈ θ 1 , Rule (α 1 ) adds (p 3 , θ 1 ) γ 0 -→ (p 2 , θ 1 ).
11. Because there are paths (p 3 , θ 1 )

γ 0 -→ T ′ (p 2 , θ 1 ) γ 2 -→ T ′ (p 4 , θ 0 ) and (p 3 , θ 1 ) γ 0 -→ T ′ (p 2 , θ 1 ) γ 2 -→ T ′ s 1 , Rule (α 1 ) adds the transitions (p 4 , θ 1 ) γ 1 -→ (p 4 , θ 0 ) and (p 4 , θ 1 ) γ 1 -→ s 1 to T ′ . 12. Since (p 4 , θ 0 ) ǫ - → T ′ (p 4 , θ 0 ) and r 5 ∈ θ 1 , Rule (α 1 ) adds (p 0 , θ 1 ) γ 0 -→ (p 4 , θ 1 ).
13. Now we have (p 0 , θ 1 )

γ 0 -→ T ′ (p 4 , θ 1 ) and r 2 c , r 1 ∈ θ 1 , Rule (α 2 ) adds the transition (p 5 , θ 3 ) γ 0 -→ (p 4 , θ 1 ) to T ′ where θ 3 = {r 3 , r 4 , r 5 , r 6 , r 7 , r 1 c , r 2 c , r 3 c , r 4 c }. For the same reason, since (p 3 , θ 1 ) γ 0 -→ (p 2 , θ 1 ) and r 3 c , r 6 ∈ θ 1 , Rule α 2 adds the transition (p 2 , θ 0 ) γ 0 -→ (p 2 , θ 1 ) to T ′ because θ 0 = (θ 1 \ {r 6 }) ∪ {r 2 }. 14. Since (p 5 , θ 3 ) ǫ - → T ′ (p 5 , θ 3 ) and r 7 ∈ θ 3 , Rule (α 1 ) adds the transition (p 2 , θ 3 ) γ 2 -→ (p 5 , θ 3 ) to T ′ . 15. Because (p 2 , θ 3 ) ǫ - → T ′ (p 2 , θ 3 ) and r 3 ∈ θ 3 , Rule (α 1 ) adds the transition (p 3 , θ 3 ) γ 0 -→ (p 2 , θ 3 ) to T ′ . Then, since there is a path (p 3 , θ 3 ) γ 0 -→ T ′ (p 2 , θ 3 ) γ 2 -→ T ′ (p 5 , θ 3 ) and r 4 ∈ θ 3 , Rule (α 1 ) adds the transition (p 4 , θ 3 ) γ 1 -→ (p 5 , θ 3 ) to T ′ . Then, since r 5 ∈ θ 3 , Rule (α 1 ) adds the transition (p 0 , θ 3 ) γ 0 -→ (p 4 , θ 3 ) to T ′ . 20 2.5 Efficient Computation of pre * images 16. Since (p 3 , θ 3 ) γ 0 -→ T ′ (p 2 , θ 3 ) and r 3 c ∈ θ 3 , Rule (α 2 ) adds the transition (p 2 , θ 2 ) γ 0 -→ T ′ (p 2 , θ 3 ) to T ′ where (θ 3 \ {r 6 }) ∪ {r 2 } = θ 2 . Meanwhile, since (p 2 , θ 3 ) γ 2 -→ (p 5 , θ 3 ) and r 4 c , r 7 ∈ θ 3 , Rule (α 2 ) adds the transition (p 4 , θ 1 ) γ 2 -→ (p 5 , θ 3 ) to T ′ where (θ 3 \ {r 7 }) ∪ {r 1 } = θ 1 . 17. Because r 7 ∈ θ 2 and (p 5 , θ 2 ) ǫ - → T ′ (p 5 , θ 2 ), Rule (α 1 ) adds the transition (p 2 , θ 2 ) γ 2 -→ (p 5 , θ 2 ) to T ′ . 18. Since (p 2 , θ 2 ) ǫ - → T ′ (p 2 , θ 2 ) and r 3 ∈ θ 2 , Rule (α 1 ) adds (p 3 , θ 2 ) γ 0 -→ T ′ (p 2 , θ 2 ) to T ′ . Then, there is a path (p 3 , θ 2 ) γ 0 γ 2 --→ * T ′ (p 5 , θ 2 ), since r 4 ∈ θ 2 , Rule (α 1 ) adds the transition (p 4 , θ 2 ) γ 1 -→ T ′ (p 5 , θ 2 ) to T ′ . Then, since (p 5 , θ 2 ) ǫ - → T ′ (p 5 , θ 2 ) and r 5 ∈ θ 2 , Rule (α 1 ) adds the transition (p 0 , θ 2 ) γ 0 -→ (p 4 , θ 2 ) to T ′ . 19. Now we have (p 2 , θ 2 ) γ 2 -→ T ′ (p 5 , θ 2 ) and (p 2 , θ 2 ) γ 0 -→ T ′ (p 2 , θ 3 ), since r 4 c , r 7 ∈ θ 2 , Rule α 2 adds the transitions (p 4 , θ 0 ) γ 2 -→ (p 5 , θ 2 ) and (p 4 , θ 0 ) γ 0 -→ (p 2 , θ 3 ) to T ′ where (θ 2 \ {r 7 }∪){r 1 } = θ 0 . 20. Since (p 4 , θ 2 ) γ 1 -→ T ′ (p 5 , θ 2 ) and r 2 , r 1 c ∈ θ 2 , Rule (α 2 ) adds the transition (p 5 , θ 3 ) γ 1 -→ (p 5 , θ 2 ) to T ′ where (θ 2 \ {r 2 }) ∪ {r 6 } = θ 3 . 21. Since (p 5 , θ 3 ) γ 1 -→ T ′ (p 5 , θ 2 ) and r 6 ∈ θ 3 , Rule (α 1 ) adds the transition (p 2 , θ 3 ) γ 2 -→ (p 5 , θ 2 ) to T ′ .
22. No further additions are possible, so the procedure terminates.

Proof of Theorem 2.5.1

Let us now prove Theorem 2.5.1. To prove this theorem, we first introduce the following lemma.

Lemma 1 For every configuration ( p, w , θ 0 ) ∈ L(A), if ( p ′ , w ′ , θ) ⇒ * P ( p, w , θ 0 ), then (p ′ , θ) w ′ -→ T ′ q for some final state q of A pre * . Proof: Assume ( p ′ , w ′ , θ) i ⇒ P ( p,
w , θ 0 ). We proceed by induction on i.

Basis. i = 0. Then θ = θ 0 , p ′ = p and w = w ′ . Since ( p, w , θ 0 ) ∈ L(A), we have (p, θ 0 ) w -→ T ′ q always holds for some final state q i.e. (p ′ , θ)

w ′ -→ T ′ q holds.
Step. i > 0. Then there exists a configuration ( p ′′ , u , θ ′′ ) such that

( p ′ , w ′ , θ) ⇒ P ( p ′′ , u , θ ′′ ) i-1 ⇒ P ( p, w , θ 0 )

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

We apply the induction hypothesis to ( p ′′ , u , θ ′′ ) i-1 ⇒ ( p, w , θ 0 ), and obtain

(p ′′ , θ ′′ ) u -→ T ′ q for q ∈ F . Let w 1 , u 1 ∈ Γ * , γ ′ ∈ Γ be such that w ′ = γ ′ w 1 , u = u 1 w 1 . Let q ′ be a state of A pre * s.t. (p ′′ , θ ′′ ) u 1 --→ T ′ q ′ w 1 --→ T ′ q (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 ′ , θ ′′ ) γ ′ --→ T ′ q ′ (2)
Putting ( 1) and ( 2) together, we can obtain that

π = (p ′ , θ ′′ ) γ ′ --→ T ′ q ′ w 1 --→ T ′ q (3)
Thus, (p ′ , θ ′′ ) γ ′ w 1 ---→ T ′ q i.e. (p ′ , θ) w ′ --→ q for some final state q ∈ F .

2. Case ( p ′ , w ′ , θ) ⇒ ( p ′′ , u , θ ′′ ) is obtained by a rule of the form p ′ (r 1 ,r 2 ) ֒----→ p ′′ ∈ ∆ c . I.e θ ′′ = θ. In this case, u 1 = γ ′ . By the saturation rule α 2 , we obtain that

(p ′ , θ) γ ′ --→ T ′ q ′ where θ ′′ = θ\{r 1 } ∪ {r 2 }. (4)
Putting ( 1) and ( 4) together, we have the following path

(p ′ , θ) γ ′ --→ T ′ q ′ w 1 --→ T ′ q. I.e. (p ′ , θ) w ′ --→ T ′ q for q ∈ F (5) ✷ Lemma 2 If a path π = (p, θ) w -→ T ′ q for θ ⊆ ∆ ∪ ∆ c is in A pre * , then (I) ( p, w , θ) ⇒ * ( p ′ , w ′ , θ 0 ) holds for a configuration ( p ′ , w ′ , θ 0 ) s.t.
(p ′ , θ 0 ) w ′ --→ T q in the initial P-automaton A;

(II) Moreover, if q is an initial state i.e. in the form (p, θ), then w ′ = ǫ. to denote the transition relation of A pre * obtained after adding i-transitions using the saturation procedure. In particular, since initially A pre * = A, A pre * contains the path (p ′ , θ 0 )

w ′ - -→ T q where ( p ′ , w ′ , θ 0 ) ∈ L(A), then we write (p ′ , θ 0 ) w ′ - -→ 0 T q. Let i be an index such that π = (p, θ) w - -→ i T ′
q holds. We shall prove (I) by induction on i. Statement (II) then follows immediately from the fact that initial states have no incoming transitions in A.

Basis. i = 0. Since ( p, w , θ) ⇒ * ( p, w , θ) always holds, take then p = p ′ , w = w ′ and θ 0 = θ.

Step. i > 0. Let t = ((p 1 , θ 1 ), γ, q ′ ) 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 - -→ i T ′ q. The proof is by induction on j. If j = 0, then we have (p, θ) w --→ i-1 T ′
q in the automaton, and we apply the induction hypothesis (induction on i) then we obtain ( p, w , θ)

⇒ * ( p ′ , w ′ , θ 0 ) for a configuration ( p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′
--→ T q in the initial Pautomaton A. So assume that j > 0. Then, there exist u and v such that w = uγv and (p, θ)

u --→ i-1 T ′ (p 1 , θ 1 ) γ - -→ i T ′ q ′ v - -→ i T ′ q (1)
The application of the induction hypothesis (induction on i) to (p, θ)

u --→ i-1 T ′ (p 1 , θ 1 ) (notice that (p 1 , θ 1 ) is an initial state) gives that ( p, u , θ) ⇒ * ( 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 ) w 2 --→ i-1 T ′ q ′ v - -→ i T ′ q (4)

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

Applying the transition rule r gets 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 ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′ --→ T ′ q in the initial P-automaton A (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 ′ , w ′ , θ 0 ) such that (p ′ , θ 0 ) w ′ --→ T q in the initial P-automaton A 2.
Case t was added by rule α 2 : there exist p 2 ∈ P and θ ′′ ⊆ ∆ ∪ ∆ c such that

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

(p 2 , θ ′′ ) γ --→ i-1 T ′ q ′ v - -→ i T ′ q (8)
Applying the transition rule, we can get from ( 7) that

( p 1 , γv , θ 1 ) ⇒ ( p 2 , γv , θ ′′ ) (9)
We can apply the induction hypothesis (on j) to ( 8), and obtain

( p 2 , γv , θ ′′ ) ⇒ * ( p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′ --→ T q in the initial P-automaton A (10)
From ( 2),( 9) and ( 10), we get

( p, w , θ) = ( p, uγv , θ) ⇒ * ( p 1 , γv , θ 1 ) ⇒ ( p 2 , γv , θ ′′ ) ⇒ * ( p ′ , w ′ , θ 0 )
such that (p ′ , θ 0 ) w ′ --→ T q in the initial P-automaton A.

Efficient Computation of post * Images

✷

Then, we can prove Theorem 2.5.1:

Proof: Let ( p, w , θ) be a configuration of pre * (L(A)). Then ( p, w , θ) ⇒ * ( p ′ , w ′ , θ 0 ) for a configuration ( p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′ --→ T ′ q is a path in A for q ∈ F .
By lemma 1, we can obtain that there exists a path (p, θ) w -→ T ′ q for some final state q of A pre * . So ( p, w , θ) is recognized by A pre * .

Conversely, let ( p, w , θ) be a configuration accepted by A pre * i.e. there exists a path (p, θ) w -→ T ′ q in A pre * for some final state q ∈ F . By Lemma 2, there exists a configuration ( p ′ , w ′ , θ 0 ) s.t. there exist a path (p ′ , θ 0 )

w ′ -→ T q in the initial automaton A and ( p, w , θ) ⇒ * ( p ′ , w ′ , θ 0 ). Because q is a final state, we have ( p ′ , w ′ , θ 0 ) ∈ L(A) i.e. ( p, w , θ) ∈ pre * (L(A)). ✷ 2.

Efficient Computation of post * Images

Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS, and let A = (Q, Γ, T, P, F ) be a Pautomaton that represents a regular set of configurations C ( C = L(A)). Similarly, it is not optimal to compute post * (C) using the translations of Sections 2.2.2 and 2.2.3 to compute equivalent PDSs or symbolic PDSs, and then apply the algorithms of [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF][START_REF] Schwoon | Model-checking pushdown systems[END_REF]. We present in this section a direct and efficient algorithm that computes post * (C). We assume w.l.o.g. that A has no transitions leading to an initial state. Moreover, we assume that the rules of ∆ are of the form p, γ ֒→ p ′ , w , where |w| ≤ 2. This is not a restriction, indeed, a rule of the form p, γ ֒→ p ′ , γ 1 • • • γ n , n > 2 can be replaced by the following rules:

• p, γ ֒→ p 1 , a 1 γ n • p 1 , a 1 ֒→ p 2 , a 2 γ n-1 • p 2 , a 2 ֒→ p 3 , a 3 γ n-2 • • • • , • p n-2 , a n-2 ֒→ p ′ , γ 1 γ 2
As previously, the construction of A post * consists in adding iteratively new transitions to the automaton A according to saturation rules (reflecting the forward application of the transition rules in the system). We define A post * to be the P-automaton (Q ′ , Γ, T ′ , P, F ), where T ′ is computed using the following saturation rules and

Q ′ is the smallest set s.t. Q ⊆ Q ′ and for every r = p, γ ֒→ p ′ , γ 1 γ 2 ∈ ∆, q θ p ′ γ 1 ∈ Q ′ where q θ p ′ γ 1
is the new state labelled with p ′ , γ 1 and θ: initially T ′ = T ;

β 1 : If r = p, γ ֒→ p ′ , ǫ ∈ ∆ and there exists in T ′ a path π = (p, θ) γ -→ T ′ q with r ∈ θ, then add ((p ′ , θ), ǫ, q) to T ′ . β 2 : If r = p, γ ֒→ p ′ , γ ′ ∈ ∆ and there exists in T ′ a path π = (p, θ) γ -→ T ′ q with r ∈ θ, then add ((p ′ , θ), γ ′ , q) to T ′ . β 3 : If r = p, γ ֒→ p ′ , γ 1 γ 2 ∈ ∆ and there exists in T ′ a path π = (p, θ) γ -→ T ′ q with r ∈ θ. Add t ′ = ((p ′ , θ), γ 1 , q θ p ′ γ 1 ) and t ′′ = (q θ p ′ γ 1 , γ 2 , q) to T ′ . β 4 : if r = p (r 1 ,r 2 )
֒----→ p ′ ∈ ∆ c and there exists in T ′ a path π = (p, θ) γ -→ T ′ q, where γ ∈ Γ with r ∈ θ, and r 1 ∈ θ, then add t ′ = ((p ′ , θ ′ ), γ, q) where θ ′ = (θ \ {r 1 }) ∪ {r 2 }}.

The procedure above terminates since there is a finite number of states and phases.

Let us explain intuitively the role of the saturation rules above. Consider a path in the automaton of the form (p, θ) γ -→ T ′ q w ′ --→ T ′ q F , where q F ∈ F . This means, by definition of P-automata, that the configuration c = ( p, γw ′ , θ) is accepted by

A post * . Let r = p, γ ֒→ p ′ , ǫ ∈ ∆. If r is in θ, then the configuration c ′ = ( p ′ , w ′ , θ) is a successor of c. Therefore, it should be added to A post * . This configuration is accepted by the run (p ′ , θ) ǫ -→ T ′ q w ′ --→ T ′ q F added by rules (β 1 ). If θ contains the rule r = p, γ ֒→ p ′ , γ ′ ∈ ∆, then the configuration c ′ = ( p ′ , γ ′ w ′ , θ) is a successor of c. Therefore, it should be added to A post * . This configuration is accepted by the run (p ′ , θ) γ ′ --→ T ′ q w ′ --→ T ′ q F added by rules (β 2 ). If r = p, γ ֒→ p ′ , γ 1 γ 2 ∈ ∆ is in θ, then the configuration c ′ = ( p ′ , γ 1 γ 2 w ′ , θ)
is a successor of c. Therefore, it should be added to A post * . This configuration is accepted by the run (p ′ , θ)

γ 1 --→ T ′ q θ p ′ γ 1 γ 2 --→ T ′ q w ′ --→ T ′ q F added
by rules (β 3 ).

Efficient Computation of post * Images

Rule (β 4 ) deals with modifying rules: Let r = p

(r 1 ,r 2 ) ֒----→ p ′ ∈ ∆ c . If r and r 1 are in θ, then the configuration c ′ = ( p ′ , γw ′ , θ ′ ) is a successor of c, where θ ′ = (θ \ {r 1 }) ∪ {r 2 }.
Therefore, it should be added to A post * . This configuration is accepted by the run (p ′ , θ ′ ) γ -→ T ′ q w ′ --→ T ′ q F added by rules (β 4 ).

Thus, we can show that:

Theorem 2.6.1 A post * recognizes the set post * (L(A)).
Before proving this theorem, let us illustrate the construction on 2 examples. 1. First, since (p 0 , θ 0 ) γ 0 -→ T ′ s 1 and r 1 ∈ θ 0 , Rule (β 3 ) generates a new state q θ 0 p 1 γ 1 and adds the two transitions:

p 0 , θ 0 p 0 , θ 0 s 1 s 1 s 2 s 2 γ 0 γ 0 γ 0 γ 0 Δ : Δ : r 1 : ⟨p 0 , γ 0 ⟩ ↪ ⟨p 1 , γ 1 γ 0 ⟩ r 1 : ⟨p 0 , γ 0 ⟩ ↪ ⟨p 1 , γ 1 γ 0 ⟩ r 2 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 2 , γ 2 γ 1 ⟩ r 2 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 2 , γ 2 γ 1 ⟩ r 3 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 3 , γ 0 ⟩ r 3 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 3 , γ 0 ⟩ r 4 : ⟨p 4 , γ 0 ⟩ ↪ ⟨p 1 , ϵ⟩ r 4 : ⟨p 4 , γ 0 ⟩ ↪ ⟨p 1 , ϵ⟩ r 5 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 4 , γ 1 ⟩ r 5 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 4 , γ 1 ⟩ Δ c : Δ c : r′! : p 3 r′! : p 3 θ 0 = {r 1 , r 2 , r 3 , r 4 , r′!} θ 0 = {r 1 , r 2 , r 3 , r 4 , r′!} p 0 , θ 0 p 0 , θ 0 s 1 s 1 s 2 s 2 γ 0 γ 0 γ 0 γ 0 p 1 , θ 0 p 1 , θ 0 q θ 0 p 1 γ 1 q θ 0 p 1 γ 1 γ 1 γ 0 p 2 , θ 0 p 2 , θ 0 q θ 0 p 2 γ 2 q θ 0 p 2 γ 2 γ 2 γ 1 p 3 , θ 0 p 3 , θ 0 γ 0 p 4 , θ 1 p 4 , θ 1 γ 0 p 1 , θ 1 p 1 , θ 1 ϵ p 2 , θ 1 p 2 , θ 1 q θ 1 p 2 γ 2 q θ 1 p 2 γ 2 γ 2 γ 1 γ 1 (r 3 , r 5 ) ↪ p 4
(p 1 , θ 0 ) γ 1 -→ q θ 0 p 1 γ 1 and q θ 0 p 1 γ 1 γ 0 -→ s 1 to T ′ . 2. Since (p 1 , θ 0 ) γ 1 -→ T ′ q θ 0 p 1 γ 1 and r 2 ∈ θ 0 , Rule (β 3 ) generates a new state q θ 0 p 2 γ 2
and adds two transitions : (p 2 , θ 0 )

γ 2 -→ q θ 0 p 2 γ 2 and q θ 0 p 2 γ 2 γ 1 -→ q θ 0 p 1 γ 1 to T ′ .

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

3. Because (p 2 , θ 0 ) γ 2 -→ T ′ q θ 0 p 2 γ 2 and r 3 ∈ θ 0 , Rule (β 1 ) adds the transition (p 3 , θ 0 ) γ 0 -→ q θ 0 p 2 γ 2 to T ′ . 4. Since (p 3 , θ 0 ) γ 0 -→ T ′ q θ 0 p 2 γ 2 and r ′ ∈ θ 0 , Rule (β 4 ) adds the transition (p 4 , θ 1 ) γ 0 -→ q θ 0 p 2 γ 2 to T ′ where θ 1 = (θ 0 \ {r 3 }) ∪ {r 5 } = {r 1 , r 2 , r 4 , r 5 , r ′ }. 5. Since (p 4 , θ 1 ) γ 0 -→ T ′ q θ 0 p 2 γ 2 and r 4 ∈ θ 1 , Rule (β 1 ) adds the transition (p 1 , θ 1 ) ǫ - → q θ 0 p 2 γ 2 to T ′ .
6. Then, since there is a path (p 1 , θ 1 )

γ 1 -→ * T ′ q θ 0 p 1 γ 1 and r 2 ∈ θ 1 , Rule (β 3 ) generates new state q θ 1
p 2 ,γ 2 and adds two transitions (p 2 , θ 1 )

γ 2 -→ q θ 1 p 2 ,γ 2 and q θ 1 p 2 ,γ 2 γ 1 -→ q θ 0 p 1 γ 1 to T ′ . 7. Since (p 2 , θ 1 ) γ 2 -→ T ′ q θ 1 p 2 ,γ 2 and r 5 ∈ θ 1 , Rule (β 2 ) adds the transition (p 4 , θ 1 ) γ 1 -→ q θ 1 p 2 ,γ 2 to T ′ . 8.
No unprocessed matches remain. The procedure terminates. -→ T ′ s 1 and r 1 ∈ θ 0 , Rule (β 3 ) generates a new state q θ 0 p 1 γ 1 and adds two transitions: (p 1 , θ 0 )

p 0 , θ 0 p 0 , θ 0 s 1 s 1 s 2 s 2 γ 0 γ 0 γ 0 γ 0 Δ : Δ : r 1 : ⟨p 0 , γ 0 ⟩ ↪ ⟨p 1 , γ 1 γ 0 ⟩ r 1 : ⟨p 0 , γ 0 ⟩ ↪ ⟨p 1 , γ 1 γ 0 ⟩ r 2 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 2 , γ 2 γ 1 ⟩ r 2 : ⟨p 1 , γ 1 ⟩ ↪ ⟨p 2 , γ 2 γ 1 ⟩ r 3 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 3 , γ 1 ⟩ r 3 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 3 , γ 1 ⟩ r 4 : ⟨p 4 , γ 1 ⟩ ↪ ⟨p 0 , ϵ⟩ r 4 : ⟨p 4 , γ 1 ⟩ ↪ ⟨p 0 , ϵ⟩ r 5 : ⟨p 0 , γ 1 ⟩ ↪ ⟨p 5 , γ 0 ⟩ r 5 : ⟨p 0 , γ 1 ⟩ ↪ ⟨p 5 , γ 0 ⟩ r 6 : ⟨p 2 , γ 1 ⟩ ↪ ⟨p 4 , γ 0 ⟩ r 6 : ⟨p 2 , γ 1 ⟩ ↪ ⟨p 4 , γ 0 ⟩ Δ c : Δ c : r 1 c : p 3 r 1 c : p 3 r 2 c : p 4 r 2 c : p 4 r 3 c : p 4 r 3 c : p 4 r 4 c : p 5 r 4 c : p 5 θ 0 = {r 1 , r 2 , r 3 . r 4 , r 1 c , r 2 c , r 3 c , r 4 c } θ 0 = {r 1 , r 2 , r 3 . r 4 , r 1 c , r 2 c , r 3 c , r 4 c } p 0 , θ 0 p 0 , θ 0 s 1 s 1 s 2 s 2 γ 0 γ 0 γ 0 γ 0 p 1 , θ 0 p 1 , θ 0 q θ 0 p1γ1 q θ 0 p1γ1 γ 1 γ 0 p 2 , θ 0 p 2 , θ 0 q θ 0 p2γ2 q θ 0 p2γ2 γ 1 γ 2 p 3 , θ 0 p 3 , θ 0 γ 1 p 4 , θ 1 p 4 , θ 1 γ 1 p 0 , θ 1 p 0 , θ 1 ϵ p 5 , θ 1 p 5 , θ 1 γ 0 θ 0 = {r 1 , r 2 , r 3 , r 4 , r 1 c , r 2 c , r 3 c , r 4 c } θ 1 = {r 2 , r 3 , r 4 , r 5 , r 1 c , r 2 c , r 3 c , r 4 c } θ 2 = {r 2 , r 4 , r 5 , r 6 , r 1 c , r 2 c , r 3 c , r 4 c } p 2 , θ 2 p 2 , θ 2 γ 1 p 4 , θ 2 p 4 , θ 2 γ 0 γ 0 γ 0 γ 0 γ 0 γ 0 p 4 p 2 p 5 p 0 ↪ ↪ ↪ ↪ (r 1 , r 5 ) (r 3 , r 6 ) (r 6 , r 3 ) (r 5 , r 1 )
γ 1 -→ q θ 0 p 1 γ 1 and q θ 0 p 1 γ 1 γ 0 -→ s 1 to T ′ . 2. Since (p 1 , θ 0 ) γ 1 -→ T ′ q θ 0 p 1 γ 1 and r 2 ∈ θ 0 , Rule (β 3 ) generates a new state q θ 0 p 2 γ 2
and adds two transitions: (p 2 , θ 0 )

γ 2 -→ q θ 0 p 2 γ 2 and q θ 0 p 2 γ 2 γ 1 -→ q θ 0 p 1 γ 1 to T ′ . 3. Because (p 2 , θ 0 ) γ 2 -→ T ′ q θ 0 p 2 γ 2 and r 3 ∈ θ 0 , Rule (β 2 ) adds (p 3 , θ 0 ) γ 1 -→ q θ 0 p 2 γ 2 to T ′ . 4. Since (p 3 , θ 0 ) γ 1 -→ T ′ q θ 0 p 2 γ 2 and r 1 c , r 1 ∈ θ 0 , Rule (β 4 ) adds the transition (p 4 , θ 1 ) γ 1 -→ q θ 0 p 2 γ 2 to T ′ where θ 1 = (θ 0 \ {r 1 }) ∪ {r 5 }. 5. Since (p 4 , θ 1 ) γ 1 -→ T ′ q θ 0 p 2 γ 2 and r 4 ∈ θ 1 , Rule (β 1 ) adds the transition (p 0 , θ 1 ) ǫ - → q θ 0 p 2 γ 2 to T ′ .
Then there is a path (p 0 , θ 1 )

γ 1 -→ * T ′ q θ 0 p 1 γ 1 , since r 5 ∈ θ 1 , Rule (β 2 ) adds the transition (p 5 , θ 1 ) γ 0 -→ q θ 0 p 1 γ 1 to T ′ . 6. Since (p 5 , θ 1 ) γ 0 -→ T ′ q θ 0 p 1 γ 1 and r 4 c , r 5 ∈ θ 1 , Rule (β 4 ) adds the transition (p 0 , θ 0 ) γ 0 -→ q θ 0 p 1 γ 1 to T ′ where (θ 1 \ {r 5 }) ∪ {r 1 } = θ 0 . 7. Since (p 0 , θ 0 ) γ 0 -→ T ′ q θ 0 p 1 γ 1 and r 1 ∈ θ 0 , Rule (β 3 ) adds the transitions (p 1 , θ 0 ) γ 1 -→ q θ 0 p 1 γ 1 and q θ 0 p 1 γ 1 γ 0 -→ q θ 0 p 1 γ 1 to T ′ . 8. Because (p 4 , θ 1 ) γ 1 -→ T ′ q θ 0 p 2 γ 2 and r 2 c ∈ θ 1 , Rule (β 4 ) adds the transition (p 2 , θ 2 ) γ 1 -→ q θ 0 p 2 γ 2 to T ′ . 9. Since (p 2 , θ 2 ) γ 1 -→ T ′ q θ 0 p 2 γ 2 and r 6 ∈ θ 2 , Rule (β 2 ) adds the transition (p 4 , θ 2 ) γ 0 -→ q θ 0 p 2 γ 2 to T ′ . 10. Since p 4 , θ 2 γ 0 -→ T ′ q θ 0 p 2 γ 2 holds and r 6 , r 3 c ∈ θ 2 , Rule (β 4 ) adds the transition (p 5 , θ 1 ) γ 0 -→ q θ 0 p 2 γ 2 to T ′ .
11. Then, since (p 5 , θ 1 )

γ 0 -→ T ′ q θ 0 p 2 γ 2 and r 4 c ∈ θ 1 , Rule (β 4 ) adds the transition (p 0 , θ 0 ) γ 0 -→ q θ 0 p 2 γ 2 to T ′ .
12. Since r 1 ∈ θ 0 and (p 0 , θ 0 )

γ 0 -→ T ′ q θ 0 p 2 γ 2 , Rule (β 3 ) adds two transitions: (p 1 , θ 0 ) γ 1 -→ q θ 0 p 1 γ 1 and q θ 0 p 1 γ 1 γ 0 -→ q θ 0 p 2 γ 2 to T ′ .
13. No more rules can be applied. Thus, the procedure terminates. Let us now prove Theorem 2.6.1. To prove this theorem, we first show the following lemma:

Lemma 3 For every configuration ( p, w , θ 0 ) ∈ L(A), if ( p, w , θ 0 ) ⇒ * ( p ′ , w ′ , θ) then we have a path π = (p ′ , θ) w ′ - -→ T ′ q for some final state q of A post * .
Proof:

Let i be the index s.t. ( p, w , θ 0 ) i ⇒ ( p ′ , w ′ , θ) holds.
We proceed by induction on i.

Basis. i = 0. Then p ′ = p, w = w ′ and θ 0 = θ. Since ( p, w , θ 0 ) ∈ L(A), we have (p, θ 0 ) w --→ T ′ q for some final state q that implies π = (p ′ , θ)

w ′ - -→ T ′ q is a path of A post * .
Step. i > 0. Then there exists a configuration ( p ′′ , u , θ ′′ ) with

( p, w , θ 0 ) i-1 ⇒ ( p ′′ , u , θ ′′ ) ⇒ ( p ′ , w ′ , θ)
By applying the induction hypothesis (induction on i), we can get that

(p ′′ , θ ′′ ) u - -→ T ′ q for some q ∈ F (1)
Then, let γ ∈ Γ, u 1 , w 1 ∈ Γ * be such that u = γu 1 , w ′ = w 1 u 1 . Let q 1 be a state of A post * s.t. we have the following path in A post * :

(p ′′ , θ ′′ ) γ - → T ′ q 1 u 1 --→ T ′ q (2)
There are two cases depending on whether ( p ′′ , u , θ ′′ ) ⇒ ( p ′ , w ′ , θ) is corresponding to a self-modifying transition (i.e. (θ ′′ = θ)) or not.

1. Case: θ ′′ = θ. Then there exists a transition rule r : p ′′ , γ ֒→ p ′ , w 1 ∈ ∆ s.t. r ∈ θ. There are three possible cases depending on the length of w 1 :

-Case |w 1 | = 0 i.e. w 1 = ǫ, by applying the saturation rule

β 1 , we can get (p ′ , θ) ǫ - → T ′ q 1 (3)
Putting ( 2) and (3) together, we can have (p ′ , θ)

ǫ - → T ′ q 1 u 1 --→ T ′ q i.e. (p ′ , θ) w ′
-→ T ′ q for some final state q of A post * .

Efficient Computation of post

* Images -Case |w 1 | = 1, then let γ ′ ∈ Γ s.t. w 1 = γ ′ . By applying the saturation rule α 2 , we can get (p ′ , θ) γ ′ -→ T ′ q 1 (4)
Putting ( 2) and ( 4) together, we can have (p ′ , θ)

γ ′ -→ T ′ q 1 u 1 --→ T ′ q i.e. (p ′ , θ) w ′ -→ T ′ q for some final state q of A post * . -Case |w 1 | = 2, let γ ′ 0 , γ ′ 1 ∈ Γ be such that w 1 = γ ′ 0 γ ′ 1 .
By applying the saturation rule α 3 , we can get

(p ′ , θ) γ ′ 0 --→ T ′ q θ p ′ γ ′ 0 γ ′ 1 --→ T ′ q 1 (5)
Putting ( 2) and ( 5) together, then we have a path (p ′ , θ)

γ ′ 0 -→ T ′ q θ p ′ γ ′ 0 γ ′ 1 -→ T ′ q 1 u 1 -→ T ′ q i.e. (p ′ , θ) w ′
-→ T ′ q for some final state q of A post * .

2. Case θ ′′ = θ. Then there exists a self-modifying transition rule s.t. r :

p ′′ (r 1 ,r 2 ) ֒----→ p ′ ∈ ∆ c ∩ θ ′′ and γ = w 1 and θ = (θ ′′ \{r 1 }) ∪ {r 2 }.
By applying rule β 4 to (2), we have the following path in the automaton:

(p ′ , θ) γ - → T ′ q 1 u 1 -→ T ′ q (5)
i.e. (p ′ , θ)

w ′ -→ T ′ q for some final state q of A post * . ✷ Lemma 4 If a path π = (p, θ) w -→ T ′ q is in A post * , then the following holds: (I) if q is a state of A, then ( p ′ , w ′ , θ 0 ) ⇒ * ( p, w , θ) for a configuration ( p ′ , w ′ , θ 0 ) such that (p ′ , θ 0 ) w ′ -→ T q is a path in the initial P-automaton A; (II) if q is a new state of the form q = q θ 1 p 1 γ 1 , then ( p 1 , γ 1 , θ 1 ) ⇒ * ( p, w , θ).
Proof: Let A post * = (Q ′ , Γ, T ′ , P, F ) be the P-automaton computed by the saturation procedure. In this proof, we use --→ i T ′ to denote the transition relation → T ′ of A post * obtained after adding i transitions using the saturation procedure.

Let i be an index such that (p, θ) w --→ i T ′ q holds. We prove both parts of the lemma by induction on i.

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

Basis. i = 0. Only (I) applies. Thus, p ′ = p, θ 0 = θ and w = w ′ . ( p ′ , w ′ , θ) ⇒ * ( p ′ , w ′ , θ) always holds.

Step. i > 1. Let t be the i-th transition added to the automaton. Let j be the number of times that t is used in (p, θ)

w - -→ i T ′ q.
A has no transitions leading to initial states, and the algorithm does not add any such transitions; therefore, if t starts in an initial state, t can only be used at the start of the path.

The proof is by induction on j. If j = 0, then we have (p, θ)

w --→ i-1 T ′ q.
We apply the induction hypothesis (induction on i) then we obtain that there exists a configuration (

p ′ , w ′ , θ 0 ) s.t. ( p ′ , w ′ , θ 0 ) ⇒ * ( p, w , θ) and (p ′ , θ 0 ) w ′
-→ T q is a path of initial P-automaton A. So assume that j > 0. We distinguish three possible cases:

1. If t was added by the rule β 1 , β 2 or β 3 , then t = ((p 1 , θ 1 ), v, q 1 ), where v = ǫ or v = γ 1 . Then, necessarily, j = 1 and there exists the following path in the current automaton:

(p, θ) = (p 1 , θ 1 ) v - -→ i T ′ q 1 w 1 --→ i-1 T ′ q (1)
There are 2 cases depending on whether transition t was added by rule β 4 or not.

-Case t was added by rule β 4 : there exists a self-modifying transition rule such that r = p 2 (r 1 ,r 2 )

֒----→ p 1 ∈ ∆ c , and there exists the following path in the current automaton:

(p 2 , θ 2 ) v --→ i-1 T ′ q 1 w 1 --→ i-1 T ′ q, θ 1 = θ 2 \{r 1 } ∪ {r 2 } (2)
By induction on (i), we get from (2) that there exists a configuration

( p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′
-→ T q is a path in the initial P-automaton A:

( p ′ , w ′ , θ 0 ) ⇒ * ( p 2 , vw 1 , θ 2 ) (3)
By applying the rule p 2 (r 1 ,r 2 )

֒----→ p 1 , we get that

( p 2 , vw 1 , θ 2 ) ⇒ ( p 1 , vw 1 , θ 1 ) (4)
2.6 Efficient Computation of post * Images Thus, putting (3) and ( 4) together, we get that there exists a configuration ( p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′ -→ T q is a path in the initial P-automaton A and:

( p ′ , w ′ , θ 0 ) ⇒ * ( p 2 , vw 1 , θ 2 ) ⇒ ( p 1 , w , θ 1 ) = ( p, w , θ) (5)
-Case t is added by β 1 or β 2 : then there exists

p 2 ∈ P , γ 2 ∈ Γ such that r = p 2 , γ 2 ֒→ p 1 , v ∈ ∆ (6)
and A post * contains the following path:

(p 2 , θ 1 ) γ 2 --→ i-1 T ′ q 1 w 1 --→ i-1 T ′ q (7)
By induction on (i), We can get from ( 7) that there exists a configura-

tion ( p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′ -→ T q is a path in the initial P-automaton A and: ( p ′ , w ′ , θ 0 ) ⇒ * ( p 2 , γ 2 w 1 , θ 1 ) (8)
Thus, putting ( 6) and ( 8) together, we have that there exists a configuration ( p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′ -→ T q is a path in the initial Pautomaton A and:

( p ′ , w ′ , θ 0 ) ⇒ * ( p 2 , γ 2 w 1 , θ 1 ) ⇒ ( p 1 , w , θ 1 ) = ( p, w , θ) (9)
2. If t is the first transition added by rule β 3 i.e. t is in the form of ((p 1 , θ ′′ ), γ 1 , q θ 1 p 1 γ 1 ). If this transition is new, then there are no transitions outgoing from q θ 1 p 1 γ 1 . So the only path using t is (p 1 , θ ′′ )

γ 1 - -→ i T ′ q θ 1 p 1 γ 1 .
For this path, we only need to prove part (II), and ( p 1 , γ 1 , θ 1 ) ⇒ * ( p 1 , γ 1 , θ 1 ) holds trivially.

3. Let t = (q θ 1 p 1 γ 1 , γ ′′ , q ′ ) be the second transition added by saturation rule β 3 . Then there exist u, v ∈ Γ * s.t. w = uγ ′′ v and the current automaton contains the following path:

(p, θ) u --→ i-1 T ′ q θ 1 p 1 γ 1 γ ′′ - -→ i T ′ q ′ v - -→ i T ′ q ( 10
)
Because t was added via the saturation rule, then there exist p 2 ∈ P , γ 2 ∈ Γ and a rule of the form

p 2 , γ 2 ֒→ p 1 , γ 1 γ ′′ ∈ ∆ ∩ θ 1 (11)

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

and A post * contains the following path:

(p 2 , θ 1 ) γ 2 --→ i-1 T ′ q ′ v - -→ i T ′ q (12)
We apply the induction hypothesis on i and obtain that

( p 1 , γ 1 , θ 1 ) ⇒ * ( p, u , θ) (13)
We apply the induction hypothesis on i to obtain that there exists a config-

uration ( p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′
-→ T q is a path in the initial P-automaton A and:

( p ′ , w ′ , θ 0 ) ⇒ * ( p 2 , γ 2 v , θ 1 ) (14)
Thus, putting (11) ( 13) and ( 14) together, we have that there exists a configuration (

p ′ , w ′ , θ 0 ) s.t. (p ′ , θ 0 ) w ′
-→ T q is a path in the initial Pautomaton A and:

( p ′ , w ′ , θ 0 ) ⇒ * ( p 2 , γ 2 v , θ 1 ) ⇒ ( p 1 , γ 1 γ ′′ v , θ 1 ) ⇒ * ( p, uγ ′′ v , θ) = ( p, w , θ) (15)

✷

Then we continue to prove Theorem 2.6.1:

Proof: Let ( p ′ , w ′ , θ) be a configuration of post * (L(A)). Then there exists a configuration ( p, w , θ 0 ) such that there exists a path (p, θ 0 ) w -→ T q in the initial automaton A and ( p, w , θ 0 ) ⇒ * ( p ′ , w ′ , θ). By Lemma 3, we can have (p ′ , θ)

w ′ -→ T ′ q for q is a final state of A post * . So ( p ′ , w ′ , θ) is recognized by A post * .
Conversely, let ( p ′ , w ′ , θ) be a configuration recognized by A post * . Then there exists a path (p ′ , θ) w ′ -→ T ′ q in A post * for some final state q. By Lemma 4, since q is a final state, we have ( p, w , θ 0 ) We implemented our algorithms in a tool. To compare the performance of our algorithms against the approach that consists in translating the SM-PDS into an equivalent PDS or symbolic PDS and then apply the standard post * and pre * algorithms for PDSs and symbolic PDSs [START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF][START_REF] Schwoon | Model-checking pushdown systems[END_REF], we first applied our tool on randomly generated SM-PDSs of various sizes. The results of the comparision using the pre * (resp. post * ) algorithms are reported in Table 2.1 (resp. Table 2.

⇒ * P ( p ′ , w ′ , θ) s.t. there exists a configuration ( p, w , θ 0 ) s.t. (p, θ 0 ) w -→ T ′ q is a path in the initial automaton A i.e. ( p, w , θ 0 ) ∈ L(A). Therefore, ( p ′ , w ′ , θ) ∈ post * (L(A)) ✷ 2.

2).

In Table 2.1, Column |∆| + |∆ c | is the number of transitions of the SM-PDS (changing and non changing rules). Column SM-PDS gives the cost it takes to apply our direct algorithm to compute the pre * for the given SM-PDS.

Column PDS shows the cost it takes to get the equivalent PDS from the SM-PDS. Column Symbolic PDS reports the cost it takes to get the equivalent Symbolic PDS from the SM-PDS. Column Result1 reports the cost it takes to get the pre * analysis of Moped [START_REF] Schwoon | Model-checking pushdown systems[END_REF] for the PDS we got. Column Total1 is the total cost it takes to translate the SM-PDS into a PDS and then apply the standard pre * algorithm of Moped (Total1=PDS+Result1). Column Result2 reports the cost it takes to get the pre * analysis of Moped for the symbolic PDS we got. Column Total2 is the total cost it takes to translate the SM-PDS into a symbolic PDS and then apply the standard pre * algorithm of Moped (Total2=Symbolic PDS+Result2). "error" in the table means failure of Moped, because the size of the relations involved in the symbolic transitions is huge. Hence, we markfor the total execution time. You can see that our direct algorithm (Column SM-PDS) is much more efficient.

Table 2.2 shows the performance of our post * algorithm. The meaning of the columns are exactly the same as for the pre * case, but using the post * algorithms instead. You can see from this table that applying our direct post * algorithm on the SM-PDS is much better than translating the SM-PDS to an equivalent PDS or symbolic PDS, and then applying the standard post * algorithms of Moped. Going through PDSs or symbolic PDSs is less efficient and leads to memory out in several cases. We consider self-modifying versions of 13 well known malwares. In these versions, the malicious behaviors are unreachable if one does not take into account that the self-modifying piece of code will change the malware code: if the code does not change, the part that contains the malicious behavior cannot be reached; after executing the self-modifying code, the control point will jump to the part containing the malicious behavior.

REACHABILITY ANALYSIS OF SELF MODIFYING CODE

We model such malwares in two ways: (1) first, we take into account the self-modifying piece of code and use SM-PDSs to represent these programs as discussed in Section 2.3.2, (2) second, we don't take into account that this part of the code is self-modifying and we treat it as all the other instructions of the program. In this case, we model these programs by a standard PDS following the translation of [START_REF] Song | Efficient malware detection using model-checking[END_REF].

The results are reported in Table 2.3, Column Example reports the name of the worm. Column SM-PDS shows the result obtained by applying our method

Experiments

to check the reachability of the entry point of the malicious block. Column PDS gives the result if we apply the traditional PDS translation of programs (without taking into account the semantics of self modifying code) method to check the reachability of the entry point of the malicious block. Y stands for yes (the program is malicious) and N stands for no (the program is benign). As it can be seen, our techniques that go through SM-PDS to model self modifying code is able to conclude that the entry point of the malicious block is reachable, whereas the standard PDS translation from programs fails to reach this conclusion.

LTL Model-Checking of Self-modifying Code

In this chapter, we consider the LTL model-checking problem of SM-PDSs. We reduce this problem to the emptiness problem of Self-modifying Büchi PushDown Systems (SM-BPDSs).

3.1

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

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

satisfy an LTL formula ϕ. It is well known that W (ϕ) can be accepted by Büchi automata:

Definition 4 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 3.1.1 [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

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. The relation ⇒ r

BP

is defined as follows: c ⇒ r BP c ′ iff there exists a configuration ( g, u , θ), g ∈ G s.t. c ⇒ * BP ( g, u , θ) ⇒ + BP c ′ . We remove the subscript BP when it is clear from the context. We define i ⇒ as follows:

c i ⇒ c ′ 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 ′ .

LTL Model-Checking of SM-PDSs

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 .

We assume w.l.o.g. that for every rule in ∆ c of the form r : p

(σ,σ ′ ) ֒----→ p ′ , r / ∈ σ.
3.1.3 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 a path π starting at ( p, w , θ) such that π |= ν ϕ.

Our goal in this chapter 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, 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 .

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

2. if a rule r = p (r 1 ,r 2 )

֒----→ 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 .
We can show that: Theorem 3.1.2 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 chapter is devoted to this problem.

The Emptiness Problem of SM-BPDSs

From now on, we fix a SM-BPDS BP = (P, Γ, ∆, ∆ c , G). 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 3 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 i 0 |= min{|w j | | j ≥ 0} |w i k |= min{|w j | | j > i k-1 }, k ≥ 1

The Emptiness Problem of SM-BPDSs

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 i 0 c i 1 .... Moreover, as some g ∈ G becomes a control location infinitely often, we can find a subsequence of indices i j 0 , i j 1 , ... with the following property: for every k ≥ 1, there exist v, w ∈ Γ *

c i j k = ( p, γw , θ) ⇒ r ( p, γvw , θ) = c i j 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. ✷ 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, γ), θ)

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

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 6 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 following path ((p 0 , γ 0 ), θ 0 ) b 1 -→ ((p 1 , γ 1 ), θ 1 ) b 2 -→ ... b i -→ ((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 3.2.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 5 The relations → * and → r have the following properties: For any heads ((p, γ), θ 1 ) and ((p ′ , γ ′ ), θ 2 ):

The Emptiness Problem of SM-BPDSs

(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 6.
-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 ∈ Γ * .

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

-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 ).

The Emptiness Problem of SM-BPDSs

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 in- duction 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 6 ((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 ob- tain 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 3.2.1

We can now prove Theorem 3.2.1. Proof: Let ((p, γ), θ) be a repeating head, then there exists some v ∈ Γ * , θ ⊆ ∆ c ∪ ∆ such that ( p, γ , θ) ⇒ r ( p, γv , θ). By Lemma 5, 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 50

The Emptiness Problem of SM-BPDSs

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 5 implies that ( p, γ , θ) ⇒ r ( p, γv , θ) which means that ((p, γ), θ) is a repeating head.

✷

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 backwardreachable using some control points in G (item 3 in Definition 6). 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 , θ), b], s.t. ( p, w , θ) is a configuration and b ∈ {0, 1}.

Multi-automata were introduced in [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] to finitely represent regular infinite sets of configurations of a PDS. Since a labelled configuration c = [( p, w , θ), b] 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 7 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 finite 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 ,b 0 ] ----→ T q 0 [γ 1 ,b 1 ] ----→ T q 1 • • • q n [γ n+1 ,b n+1 ] -------→ T q ′ . If q [w,b] --→ T q ′ holds, we say that q [w,b] --→ T q ′ and q [γ 0 ,b 0 ] ----→ T q 0 [γ 1 ,b 1 ] ----→ T q 1 • • • q n [γ n+1 ,b n+1 ] -------→ T q ′ is a path of A.

The Emptiness Problem of SM-BPDSs

path of the form π = (p 1 , θ) [w,b 1 ] ---→ T q [w ′ ,b 2 ]
---→ T q f where q f ∈ F that 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, θ)

[γ,B(p)∨b 1 ] -------→ T q [w ′ ,b 2 ]
----→ T q f added by rule (α 1 ).

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

(σ,σ ′ ) ֒----→ p 1 ∈ ∆ c . Let c = ( p 1 , γw ′ , θ) and c ′ = ( p, γw ′ , θ ′′ ) s.t. θ = θ ′′ \σ ∪ σ ′ . 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 , θ)

[γ,b 1 ] ---→ T q [w ′ ,b 2 ] ---→ T q f (where q f ∈ F ) that accepts the labelled configuration [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)∨b 1 ] ------→ T q [w ′ ,b 2 ]
---→ T q f added by rule (α 2 ).

Before proving that our construction is correct, we introduce the following definition: Definition 8 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 6 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.

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

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 ) [γ,b 1 ] ---→ 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 ) [w 2 ,b 2 ] ----→ 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

The Emptiness Problem of SM-BPDSs

( 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 , θ 6)). Therefore, ( p, w , θ 1 ) ⇒ r ( p ′′ , ǫ , θ ′′ ).

) ⇒ r ( p 1 , γv , θ 1 ) ⇒ * ( p ′′ , ǫ , θ ′′ ) i.e. ( p, w , θ) ⇒ 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

( p 2 , γv , θ 2 ) ⇒ * ( p ′′ , ǫ , θ ′′ , ) moreover, if b ′ 1 ∨ b ′′ = 1, ( p 2 , γv , θ 2 ) ⇒ r ( p ′′ , ǫ , θ ′′ ) ( 10
)
From ( 2),( 9) and ( 10), we get

( 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.

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

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

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 ( 10
)) i.e. ( p, w , θ 1 ) ⇒ r ( p ′ , ǫ , θ ′ ). Therefore, we can get that if b = 1, then ( p, w , θ 1 ) ⇒ r ( p ′′ , ǫ , θ ′′ ). ✷ Lemma 7 If there is a labelled configuration [( p, w , θ), b] such that ( p, w , θ) ⇒ * ( p ′ , ǫ , θ ′ ), then there is a path (p, θ) [w,b] ---→ T (p ′ , θ ′ ) in A pre * ( p ′ , ǫ , θ ′ ) . More- over, 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 ′′ , θ ′′ ) [u 1 ,b ′′ 0 ] ----→ T (p 0 , θ 0 ) [w 1 ,b ′′ 1 ] ----→ T (p ′ , θ ′ ) ( 6
)
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, θ ′′ ) [γ,b 0 ] ---→ T (p 0 , θ 0 ), b 0 = B(p) ∨ b ′′ 0 (7) 56

The Emptiness Problem of SM-BPDSs

Putting ( 1) and ( 2) together, we can obtain that

π = (p, θ ′′ ) [γ,b 0 ] ---→ T (p 0 , θ 0 ) [w 1 ,b ′′ 1 ] ----→ T (p ′ , θ ′ ) (8)
Thus, (p, θ ′′ )

[γw 1 ,b 0 ∨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, θ) [γ,b 0 ] ---→ T (p 0 , θ 0 ) where θ ′′ = θ\{r 1 } ∪ {r 2 }, b 0 = B(p) ∨ b ′′ 0 . (9)
Putting ( 1) and ( 4) together, we have the following path

(p, θ) [γ,b 0 ] ---→ T (p 0 , θ 0 ) [w 1 ,b ′′ 1 ] ----→ T (p ′ , θ ′ ) i.e. (p, θ) [w,b] ---→ T (p ′ , θ ′ ) where b = b 0 ∨ b ′′ 1 (10) 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.

✷

From these two lemmas, we get:

Theorem 3.2.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 configuration of pre * ( p ′ , ǫ , θ ′ ) ).
Then ( p, w , θ) ⇒ * ( p ′ , ǫ , θ ′ ). By Lemma 6, 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.

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

Conversely, let [( p, w , θ), b] be a configuration accepted by A pre * ( p ′ , ǫ , θ ′ ) i.e. there exists a path (p, θ)

[w,b] --→ T (p ′ , θ ′ ) in A pre * ( p ′ , ǫ , θ ′ ) . By Lemma 7, ( p, w , θ) ⇒ * ( p ′ , ǫ , θ ′ ) i.e. ( p, w , θ) ∈ pre * (L(A)). Moreover, if b = 1, ( p, w , θ) ⇒ r ( p ′ , ǫ , θ ′ ). ✷

Computing the Head Reachability Graph G

Based on the definition of the Head Reachability Graph G, and on Theorem 3.2.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 ′ , γ ′ ), θ ′ ).

Items α ′

1 and α ′ 2 are obvious. They respectively correspond to item 1 and item 2 of Definition 6 (since

B(p) = 1 iff p ∈ G). Item α ′
3 is based on Lemma 5 and on item 3 of Definition 6. Indeed, it follows from Lemma 5 that A pre * ( p ′ , ǫ , θ ′ ) contains a transition of the form (p 0 , θ)

[γ 0 ,b] ---→ 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 6) since p, γ ֒→ p 0 , γ 0 γ ′ ∈ ∆.

Experiments

Experiments

Our approach vs. standard LTL for PDSs

We implemented our approach in a tool 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. The results (CPU Execution time) are shown in Table 3.1 and 3.2. 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 thesis. 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. 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 GetModuleHan-dleA 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.

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

Then the API functions CreateFileMappingA and MapViewOfFile 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

Experiments

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]Automated unpacking: A behaviour based approach[END_REF] to handle packers like UPX, and we use Jakstab [START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF] as disassembler. We consider 160 malwares from the malware library VirusShare [49], 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 19 benign samples from Windows XP system. We consider selfmodifying versions of these programs. 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.2. 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 Tables 3.5, 3.6, 3.7 and 3.8 the results we obtained. 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 described above.

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

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 Tables 3.5, 3.6, 3.7 and 3.8 , using selfmodifying PDSs as models, and applying our LTL model-checking algorithm allowed to detect all the 892 malwares that we considered.

Note that checking the formulas φ rk , φ ds , and φ sw could be done using multiple pre * queries on SM-PDSs using the pre * algorithm of Section 2.5. However, this would be less efficient than performing our direct LTL model-checking algorithm, as shown in Tables 3.3, 3.4, 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 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.

Experiments

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

CTL Model-Checking of Self-modifying Code

In this chapter, we reduce the CTL model-checking problem of self-modifying code to the emptiness problem of Self-Modifying Alternating Büchi Pushdown Systems (SM-ABPDSs).

4.1

CTL Model-Checking of SM-PDSs

The Computation Tree Logic CTL

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

ϕ ::= A | ¬A | ϕ ∨ ϕ| ϕ ∧ ϕ | AXϕ | EXϕ | A[ϕU ϕ] |E[ϕU ϕ] | A[ϕ U ϕ] |E[ϕ U ϕ].
Given a CTL formula ϕ, the closure cl(ϕ) is the set of all the subformulae of ϕ, including ϕ. Let P = (P, Γ, ∆, ∆ c ) be a SM-PDS, ν : P → 2 At be a labelling function mapping to each control location p ∈ P a set of atomic propositions. The satisfiability relation of a CTL formula ϕ at a configuration ( p 0 , w 0 , θ 0 ) (denoted by ( p 0 , w 0 , θ 0 ) |= ν ϕ) is defined as follows:

• ( p 0 , w 0 , θ 0 ) |= ν A iff A ∈ ν(p 0 ), • ( p 0 , w 0 , θ 0 ) |= ν ¬A iff A / ∈ ν(p 0 ), • ( p 0 , w 0 , θ 0 ) |= ν ϕ 1 ∨ ϕ 2 iff ( p 0 , w 0 , θ 0 ) |= ν ϕ 1 or ( p 0 , w 0 , θ 0 ) |= ν ϕ 2 ,
• ( p 0 , w 0 , θ 0 ) |= ν ϕ 1 ∧ ϕ 2 iff ( p 0 , w 0 , θ 0 ) |= ν ϕ 1 and ( p 0 , w 0 , θ 0 ) |= ν ϕ 2 ,

4.1 CTL Model-Checking of SM-PDSs

2. If r : p ֒ (σ,σ ′ ) ---→ p ′ is a rule in ∆ c ∩ θ , then ( p, w , θ) ⇒ BP {( p ′ , w , θ ′ )}, θ ′ = θ\σ ∪ σ ′ . Intuitively, [σ 1 , • • • , σ m ] in the transition r : p, γ ֒ [σ 1 ,••• ,σm] ------→ { p 1 , w 1 , • • • , p m , w m }
ensures that for a given configuration ( p, γw , θ), for every 1 ≤ i ≤ n, ( p i , w i w , θ) is in the set of immediate successor iff -either for every 1 ≤ j ≤ n, σ j = -;

-or σ i = -and ∃j = i, 1 ≤ j ≤ n s.t. σ j ∩ θ = ∅ -or σ i ∩ θ = ∅
Note thatmeans that there is no constraint on whether θ contains a rule in σ i or not.

For every c ∈ P × Γ * × 2 A run ρ of BP starting from an initial configuration c 0 is a tree whose root is labelled by c 0 and whose other nodes are labelled by configurations of P × Γ * × 2 ∆×∆c . A node of ρ labelled by configuration c has n children labelled by c 1 , . . . , c n , respectively, iff c ⇒ BP {c 1 , ...c n }. A path c 0 c 1 • • • of a run ρ is an infinite sequence of configurations s.t. c 0 is the root of ρ and c i+1 is one child of c i . A path is accepting iff it visits some configurations with control locations in F infinitely often. A run is accepting iff all its paths are accepting. A configuration c is accepted by BP iff it is the root of a run accepted by BP. The language of BP, L(BP), is the set of configurations accepted by BP.

We assume w.l.o.g. that for every rule in ∆ c of the form r : p ֒

(σ,σ ′ ) ---→ p ′ , r / ∈ σ.
Representing potentially infinite sets of configurations of SM-ABPDSs.

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

Alternating Multi-Automata (AMA) were introduced in [START_REF] Bouajjani | Reachability Analysis of Pushdown Automata: Application to Model Checking[END_REF] to finitely represent regular sets of configurations of an alternating PDS. In order to adapt AMA to represent regular sets of SM-ABPDS, we extend this notion taking phases into account as follows:

Definition 10 Let BP = (P, Γ, ∆, ∆ c , F ) be a SM-ABPDS. An Extended Alternating Multi-Automaton (EAMA) is a tuple A = (Q, Γ, T, I, Q F ) where

I ⊆ P × 2 ∆∪∆c ⊆ Q is the set of initial states, T ⊆ Q × (Γ ∪ {ǫ}) × 2 Q is the set of transitions, Q F ⊆ Q is a finite set of final states.
Let → T be the transition relation defined as follows: (1) ∀q ∈ Q, q ǫ -→ T {q} where ǫ is the empty word; ( 2

) if (q, γ, {q 1 , • • • , q n }) ∈ T, q γ - → T {q 1 , • • • , q n }; and (3) if q γ - → T {q 1 , • • • , q n } and q i w -→ T Q i for every 1 ≤ i ≤ n, then q γw -→ T n i=1 Q i . A configuration ( p, w , θ) is accepted by the EAMA A iff (p, θ) ∈ I and ∃ Q ′ ⊆ Q F such that (p, θ) w -→ T Q ′ . Let L(A)
be the set of configurations accepted by A. Let C be a set of configurations of the SM-ABPDS BP. C is regular if there exists an EAMA A such that C = L(A).

From CTL Model-Checking of SM-PDSs to the emptiness problem of SM-ABPDSs

Let P = (P, Γ, ∆, ∆ c ) be a Self Modifying Pushdown System with an initial configuration c 0 = ( p 0 , w 0 , θ 0 ). We suppose w.l.o.g. that P has a bottom stack symbol ♯ ∈ Γ that is never popped from the stack i.e. there is no transition rule of the from p, ♯ ֒→ p ′ , w ∈ ∆. Given a set of atomic propositions At, let ν : P → 2 At be a labeling function that associates each control location to a set of atomic propositions. Let ϕ be a CTL formula over At. Our goal is to check whether c 0 |= ν ϕ. This can be done by translating the SM-PDS into an equivalent PDS as described in Chapter 2, and then applying the standard CTL model-checking algorithm for PDSs [START_REF] Song | Pumoc: a ctl model-checker for sequential programs[END_REF]. However, as will be shown in the experiments section (Section 4.3), this approach is not efficient. Thus, we need a direct algorithm that operates directly on the SM-PDS without translating it into a PDS. We provide in this section a direct algorithm that performs CTL model-checking on SM-PDSs. To this aim, we will compute a kind of product of the SM-PDS with ϕ: we construct a Self Modifying Alternating Büchi Pushdown

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

handles the case ψ = ψ 1 ∧ ψ 2 where ( p, w , θ) satisfies ψ iff it satisfies both ψ 1 and ψ 2 .

If ψ = EXψ 1 , then ∀w ∈ Γ * , θ ⊆ ∆ ∪ ∆ c , ( p, w , θ) |= ν ψ iff an immediate successor ( p ′ , w ′ , θ ′ ) of ( p, w , θ) satisfies ψ 1 . Thus, BP ϕ has an accepting run from ( [p, ψ], w , β(θ)) iff it can accept a run from ( [p ′ , ψ 1 ], w ′ , β(θ ′ )) . There are two cases depending on whether p ∈ P N or p ∈ P c , because the form of the rules of the SM-PDS depends on whether p ∈ P N or p ∈ P c : if p ∈ P N , then necessarily, the rules that can be applied from p are of the form p, γ ֒→ p ′ , w ∈ ∆, whereas if p ∈ P c , then necessarily, the rules that can be applied from p are of the form

r : p (r 1 ,r 2 )
֒----→ p ′ ∈ ∆ c . Thus, if p ∈ P N , then BP ϕ has an accepting run from ( [p, ψ], γu , β(θ)) iff there exists a rule p, γ ֒→ p ′ , w ∈ ∆ such that BP ϕ has an accepting run from ( [p ′ , ψ 1 ], wu , β(θ)). This is ensured by Item 5(a). If p ∈ P c , then BP ϕ has an accepting run from ( [p, ψ], γu , β(θ)) iff there exists a rule r : p (r 1 ,r 2 ) ֒----→ p ′ ∈ ∆ c ∩ θ such that BP ϕ has an accepting run from ( [p ′ , ψ 1 ], γu , β(θ ′ )), where θ ′ = (θ\{r 1 }) ∪ {r 2 }. This is ensured by Item 5(b).

If ψ = AXψ 1 , then ∀w ∈ Γ * , θ ⊆ ∆ ∪ ∆ c , ( p, w , θ) |= ν ψ iff every immediate successor ( p ′ , w ′ , θ ′ ) of ( p, w , θ) satisfies ψ 1 . Thus, BP ϕ has an accepting run from ( [p, ψ], w , β(θ)) iff it can accept a run from all its immediate successors ( [p ′ , ψ 1 ], w ′ , β(θ ′ )). As previously, there are two cases depending on whether p ∈ P N or p ∈ P c : if p ∈ P N , let γ ∈ Γ and u ∈ Γ * such that w = γu. Let then { p, γ ֒→ p 1 , w 1 , • • • , p, γ ֒→ p m , w m } be the set of all the rules of ∆ ∩ θ that have p, γ in the left-hand-side. Then, BP ϕ has an accepting run from ( [p, ψ], γu , β(θ)) iff BP ϕ has an accepting run from every ( [p i , ψ 1 ], w i u , β(θ)), 1 ≤ i ≤ m. This is ensured by Item 6(a). Note that Item 6(a) considers all the rules R i : p, γ ֒→ p i , w i that are in ∆ (even those that are not in θ), then the constraints [σ 1 , • • • , σ n ] of the rule R ′ of Item 6(a) ensures that only the R i 's that are in θ are applied. Note also that in

R ′ , σ i = prod E (R i ) ensures that σ i ∩ β(θ) = ∅ iff R i ∩ θ = ∅.
Here taking σ i = prod(R i ) is not correct because R ′ ∈ prod(R i ) and so in this case, σ i ∩ β(θ) would always be nonempty. On the other hand, if p ∈ P c , let {p

֒ (r 1 ,r ′ 1 ) ---→ p 1 , • • • , p (rm,r ′ m )
֒----→ p m } be the set of all the rules of ∆ c ∩ θ that have p in the left-hand-side. Then BP ϕ has an accepting run from ( [p, ψ], γu , β(θ)) iff BP ϕ has an accepting run from ( [p i , ψ 1 ], γu , β(θ i )), for every 1 ≤ i ≤ m, where θ i = (θ\{r i }) ∪ {r i ′ }. This is ensured by Item 6(b). As previously, Item 6(b) considers all the rules R i : p

(r i ,r ′ i )
֒----→ p i that 4.1 CTL Model-Checking of SM-PDSs are in ∆ c (even those that are not in θ), then the constraints

[σ 1 , • • • , σ n ] of the rule R ′ ⊥ = [p, ψ], γ ֒ [σ 1 ,••• ,σn] -----→ { p ψ 1 , γ , • • • , p ψ n , γ } of Item 6(b) ensures that only the R i 's that are in θ are applied. Then R ′ i : p ψ i ֒ (σ,σ ′ )
---→ [p i , ψ 1 ] ensures BP ϕ has an accepting run from ( p ψ i , γu , β(θ)) iff BP ϕ has an accepting run from ( [p i , ψ 1 ], γu , β(θ i )) where

θ i = (θ\{r i }) ∪ {r i ′ } for 1 ≤ i ≤ n. Note that σ ′ = prod(r i ) and σ ′ = prod(r ′ i ), then β(θ i ) = β(θ) \ σ ∪ σ ′ .
Thus, BP ϕ has an accepting run from ( [p, ψ], γu , β(θ)) iff BP ϕ has an accepting run from ( [p i , ψ 1 ], γu , β(θ i )) for every 1 ≤ i ≤ n.

If ψ = E[ψ 1 U ψ 2 ], then ∀w ∈ Γ * , θ ⊆ ∆ ∪ ∆ c , ( p
, w , θ) |= ν ψ iff either it satisfies ψ 2 or it satisfies ψ 1 and there exists an immediate successor satisfying ψ. Thus, BP ϕ has an accepting run from ( [p, ψ], w , β(θ)) iff:

1. BP ϕ has an accepting run from ( [p, ψ 2 ], w , β(θ)). This is handled by the

rules [p, ψ], γ ֒ [-,-] ---→{ [p, ψ 2 ], γ , [p, ψ 1 ], γ } introduced by Item 7.
2. or BP ϕ has an accepting run from both ( [p, ψ 1 ], w , β(θ)) and ( [p ′ , ψ], w ′ , β(θ ′ )) where ( p ′ , w ′ , θ ′ ) is an immediate successor of ( p, w , θ)). There are two cases depending on whether p ∈ P N or p ∈ P C : the case p ∈ P N is handled by Item 7(a). Its intuition is similar to the intuition behind the previous items. Let then p ∈ P C . Then there exists a rule

r : p (r 1 ,r ′ 1 )
֒----→ p ′ ∈ θ ∩ ∆ c such that BP ϕ has an accepting run from both ( [p, ψ 1 ], w , β(θ)) and ( [p ′ , ψ], w , β(θ ′ )), where θ ′ = θ\{r 1 ) ∪ {r 1 ′ }. This is ensured by the rule

R ⊥ = [p, ψ], γ [-,-] ֒----→ { [p, ψ 2 ], γ , p ψ , γ } ∈ ∆ ′ and R ′ : p ψ ֒ (σ,σ ′ ) ---→ [p ′ , ψ] ∈ ∆ ′ c added by Item 7(b). The case ψ = A[ψ 1 U ψ 2 ]
is handled in a similar way using Items 8. ( p,w ,θ) |= ν ψ iff it satisfies ψ 2 and either it satisfies also ψ 1 , or it has a successor ( p ′ , w ′ , θ ′ ) that satisfies ψ. Then, BP ϕ has an accepting run from ( [p, ψ], w , θ) iff BP ϕ has an accepting run from both (( [p, ψ 2 ], w , β(θ)) and ( [p, ψ 1 ], w , β(θ))), or it has an accepting run from both (( [p, ψ 2 ], w , β(θ)) and ( [p ′ , ψ], w ′ , β(θ ′ ))). This case is handled by Items 9. To ensure that the runs on which ψ 2 always holds are accepted, we add [p, ψ] in F . The case where ψ = A[ψ 1 U ψ 2 ] is handled similarly by Items 10.

If ψ = E[ψ 1 U ψ 2 ], then ∀w ∈ Γ * , θ ⊆ ∆ ∪ ∆ c ,
We can show that:

4. CTL MODEL-CHECKING OF SELF-MODIFYING CODE prod(R i ). Let {R i 1 = p (r i 1 ,r ′ i 1 ) ֒----→ p i 1 , • • • , R i k = p (r i k ,r ′ i k
)

֒----→ p i k } be the set of rules of S ∩ θ. Then {( p i 1 , γu , θ i 1 ), • • • , ( p i k , γu , θ i k )} is an immediate successor of ( p, w , θ) where θ i j = (θ \{r i j })∪{r ′ i j }. Since ( p, w , θ) |= ν ψ, then ( p i j , γu , θ i j ) |= ν ψ 1 for every j, 1 ≤ j ≤ k. By applying the induction hypothesis, BP ϕ has an accepting run from ( [p i j , ψ 1 ], γu , β(θ i j )). Since

prod(θ) = {r ′ ∈ ∆ ′ ∪ ∆ ′ c | ∃r ∈ θ, r ′ ∈ prod(r)} and R i ∈ θ, then R ′ i , R ′ ⊥ ∈ β(θ). Since σ l = prod E (R l ) , σ l ∩β(θ) = ∅ if l ∈ {i 1 , • • • , i k } and σ l ∩β(θ) = ∅ if l / ∈ {i 1 , • • • , i k }, then using R ′ ⊥ , we get that ( [p, ψ], w , β(θ)) ⇒ BP {( p ψ i 1 , w , β(θ)), • • • , ( p ψ i k , w , β(θ))}. For every j, 1 ≤ j ≤ k, using R ′ i j , we get that ( p ψ i 1 , w , β(θ)) ⇒ BP ( [p i j , ψ 1 ], γu , β(θ) \ σ ∪ σ ′ ). Since β(θ i j ) = prod(θ i j ) ∪ δ = (prod(θ\{r i j } ∪ {r ′ i j }) ∪ δ, then β(θ i j ) = β(θ)\σ ∪ σ ′
for every σ = prod(r i j ) and σ ′ = prod(r ′ i j ). Thus, we can obtain that

( [p, ψ], w , β(θ)) ⇒ * BP {( [p i 1 , ψ i 1 ], w , β(θ i 1 )), • • • , ( [p i k , ψ 1 ], w , β(θ i k ))}.
Since BP ϕ has an accepting run from ( [p i j , ψ 1 ], w i j , β(θ)), then, BP ϕ has an accepting run from ( [p, ψ], w , β(θ)).

Case ψ = E[ψ 1 U ψ 2 ] : Since ( p, w , θ) |= ν ψ, then there exists a path ρ : ( p 0 , w 0 , θ 0 ), ( p 1 , w 1 , θ 1 ), ( p 2 , w 2 , θ 2 ) • • • from ( p, w , θ) (i.e. ( p 0 , w 0 , θ 0 ) = ( p, w , θ)) such that there exists i ≥ 0, ( p i , w i , θ i ) |= ν ψ 2 and for every 0 ≤ j < i, ( p j , w j , θ j ) |= ν ψ 1 . Thus, by applying the induction hypothesis, we obtain that BP ϕ has an accepting run from ( [p i , ψ 2 ], w i , β(θ i )) and for every 0 ≤ j < i, BP ϕ has an accepting run from the configuration ( [p j , ψ 1 ], w j , β(θ j )). We first show that BP ϕ has an accepting run from ( [p i , ψ], w i , β(θ i )).

By the construction Item 7,

r ′ = [p i , ψ], γ ֒ [-] -→ [p i , ψ 2 ], γ ∈ ∆ ′ s.t. r ′ ∈ δ (since it is not constructed from ∆ nor ∆ c ). Then, r ′ ∈ β(θ i ). Thus, we have that ( [p i , ψ], w i , β(θ i )) ⇒ BP ( [p i , ψ 2 ], w i , β(θ i ))
. Hence, BP ϕ has an accepting run from ( [p i , ψ], w i , β(θ i )). If i = 0, then ( [p, ψ], w , β(θ)) = ( [p i , ψ], w i , β(θ i )) and BP ϕ has an accepting run from ( [p, ψ], w , β(θ)). Otherwise if i > 0, we show that BP ϕ has an accepting run from ( [p j , ψ], w j , β(θ j )), 1 ≤ j < i, by induction on l = ij. (Note that ( [p, ψ], w , β(θ)) = ( [p 0 , ψ], w 0 , β(θ 0 ))).

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

Indeed, let c ∈ X 1 . Then c has a successor C ⊆ F × Γ * × 2 ∆∪∆c (since X 1 = P re + BP (X 0 ∩(F ×Γ * ×2 ∆∪∆c ))). Therefore, BP has a run starting from c that visits some configuration p ∈ F at least once. X 2 = P re + BP X 1 ∩(F ×Γ * ×2 ∆∪∆c ) , thus ∀c ′ ∈ X 2 , a run starting from c ′ will visit configurations in X 1 ∩ (F × Γ * × 2 ∆∪∆c ) at least once; and thus, it visits configurations with control locations in F at least twice. Thus, we can get by induction that ∀k ≥ 1, for every configuration c in X k , BP has a run that visits configurations with control locations in F at least k times. Proof: (⇒) : We proceed by induction on k.

Basis. k = 0. In this case, we can directly obtain that ( p, w , θ) ∈ X 0 .

Step

. k ≥ 1. Let ( p 1 , w 1 , θ 1 ), • • • , ( p n , w n , θ n ) be the first nodes of ρ that are visited in each path of ρ such that p i ∈ F . Then we get (1) ( p, w ), θ) ⇒ BP {( p 1 , w 1 ), θ 1 ), • • • , ( p n , w n , θ n )}. (2) for every 1 ≤ i ≤ n, p i ∈ F. ( 3
) for every 1 ≤ i ≤ n, BP has a run ρ i from the configuration ( p i , w i , θ i ) s.t. all the paths of ρ i can visit some configurations with control locations in F at least k -1 times.

By applying the induction hypothesis to (3), we can get that ( p i , w i , θ i ) ∈ X k-1 for each 1 ≤ i ≤ n. Since p i ∈ F , then ( p i , w i , θ i ) ∈ X k-1 ∩F ×Γ * ×2 ∆∪∆c . Moreover, since X k = P re + (X k-1 ∩F ×Γ * ×2 ∆∪∆c ), we have that ( p, w , θ) ∈ X k .

(⇐) : In this direction, let's proceed by induction on k. It is obvious when k = 0. we only need to prove that BP has a run ρ from the configuration ( p, w , θ) such that each path of ρ can visit some configurations with control locations in F and least k times for k ≥ 1.

Since

( p, w , θ) ∈ X k for X k = P re + (X k-1 ∩ F × Γ * × 2 ∆∪∆c ), we obtain that ( p, w ), θ) ⇒ BP {( p 1 , w 1 ), θ 1 ), • • • , ( p n , w n , θ n )} and ( p i , w i , θ i ) ∈ X k-1 ∩F × Γ * × 2 ∆∪∆c for every 1 ≤ i ≤ n.
By applying the induction hypothesis, we can get that BP has a run ρ i starting from ( p i , w i , θ i ) s.t. every path of ρ i can visit some configurations with control locations in F at least k -1 times. Thus, BP has a run ρ from the configuration ( p, w , θ) such that each path of ρ can visit some configuration with the control location in F at least k times. ✷

Then we can prove Theorem 4.2.1:

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

different X i 's iteratively. Each iteration step i computes an EAMA A i . States of A i are of the form (p, θ) i , where p ∈ P and θ ⊆ ∆ ∪ ∆ c . There are two loops in the algorithm: the outer loop (loop 1 ) and the inner loop (loop 2 ). As will be explained later, if the sequence (X i ) is strictly decreasing, the outer loop won't terminate. So we introduce two projections to force termination as follows: for every S ⊆ P × 2 ∆∪∆c × N ∪ {q f }:

π -1 (S) =    {q i |q i+1 ∈ S} ∪ {q f } if q f ∈ S or ∃q 1 ∈ S {q i |q i+1 ∈ S} else. π i (S) = {q i |∃1 ≤ j ≤ i s.t. q j ∈ S} ∪ {q f |q f ∈ S} Algorithm 1 Computation of Y BP 1: Initially: i = 0, T = {(q f , γ, {q f })}, ∀γ ∈ Γ, p ∈ P, θ ⊆ ∆ ∪ ∆ c , (p, θ) 0 = q f . 2:
Repeat (we call this loop loop 1 )

3: i := i + 1; 4: ∀(p, θ) i-1 in the current automaton s.t. p ∈ F , add (p, θ) i ǫ - → (p, θ) i-1 to T 5:

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

(a) for every accepting run ρ of BP from ( p, w , θ) ∈ P × Γ * × 2 ∆∪∆c , there exists a path (p, θ) i w -→ T {q f } in A i and for every decomposition

(p, θ) i u - → T Q v - → T {q f } of the path (p, θ) i w -→ T {q f }, if Q = {q f }, then for all (p ′ , θ ′ ) i or (p ′ , θ ′ ) i-1 in Q\{q f }, some path of the run ρ will reach ( p ′ , v , θ ′ ) i.e. ( p, w , θ) ⇒ * ( p ′ , v , θ ′ ) (b) Y BP ⊆ L(A i
) after substitution at line 14.

Proof: We proceed by induction on i.

Basis. i = 0. The statement (a) holds directly from the fact that for every configuration ( p, w , θ) ∈ P × Γ * × 2 ∆∪∆c , there exists a path (p, θ) 0 w -→ T {q f } in the initial automaton A 0 and for every decomposition (p, θ)

0 u - → T Q v - → T {q f }, Q = {q f }. Then, statement (b) holds from the fact that Y BP ⊆ P ×Γ * ×2 ∆∪∆c = L(A 0 ).
Step. i ≥ 1. For the statement (a). Let H(ρ) be the maximum number of steps required by the paths of ρ from root (( p, w , θ)) to reach some configuration with control locations in F . We apply a nested induction on H(ρ).

-Basis. H(ρ) = 0. Since the root of ρ is ( p, w , θ), we can obtain that ( p, w , θ) ∈ F × Γ * × 2 ∆∪∆c . By the transition rule added to the automaton during the i-th iteration by line 4, we can get that (p, θ) i ǫ -→ {(p, θ) i-1 } is a transition rule of A i . Then, by applying the induction hypothesis on i, the result immediately follows.

-

Step. H(ρ) ≥ 1. Let ρ 1 , • • • , ρ n be the sub-trees of ρ whose root is the children of the root ( p, w , θ). Let p 1 , • • • , p n ∈ P , w 1 , • • • , w n ∈ Γ * , γ ∈ Γ and θ 1 ⊆ ∆ ∪ ∆ c be such that w = γw ′ and the roots of the sub-trees of ρ are ( p 1 , w 1 w ′ , θ 1 ), • • • , ( p n , w n w ′ , θ n ).
There are 2 cases depending on whether (θ = θ j ) for every j : 1 ≤ j ≤ n or not.

-Case θ j = θ for every j : 1 ≤ j ≤ n. Then ρ 1 , • • • , ρ n are the accepting runs of BP from configurations ( p 1 , w 1 w ′ , θ), • • • , ( p n , w n w ′ , θ) and there exists r : p, γ ֒

[σ j 1 ,••• ,σ jm ] -------→{ p j 1 , w j 1 , • • • , p jm , w jm } ∈ ∆ s.t. r ∈ θ, {1, • • • , n} ⊆ {j 1 , • • • , j m } and for every 1 ≤ j ≤ n, σ j ∩θ = ∅ or σ j = -. Note that for the constraint [σ j 1 , • • • , σ jm ], either ∃1 ≤ l ≤ m, σ j l ∩ θ = ∅ or ∀1 ≤ l ≤ m, σ j l = -. Since H(ρ) ≥ 1 (p /
∈ F ), we can get H(ρ j ) < H(ρ) for 1 ≤ j ≤ n. Thus we apply the nested induction 4.2 Computing the language of a SM-ABPDS hypothesis on H(ρ j ), we can get that there exists a path (p j , θ) i w j w ′ ---→ T {q f } in A i and for every decomposition (p j , θ)

i u - → T Q v - → T {q f } of the path (p j , θ) i w j w ′ ---→ T {q f }, if Q = {q f }, then for all (p ′ , θ ′ ) k ∈ Q\{q f } with k ∈ {i, i-1},
some path of the run ρ j will reach the configuration ( p ′ , v , θ ′ ).

Moreover, there exists a path (p j , θ) i w j -→ T Q j w ′ -→ T {q f } in A i for every j : 1 ≤ j ≤ n and by applying the saturation procedure, we get that (p, θ)

i γ - → n j=1 Q j w ′ -→ T {q f } in A i . Then for every decom- position (p, θ) i u - → T Q v - → T {q f } of the path ((p, θ) i γw ′ --→ T {q f }), if Q = {q f }, then for all (p ′ , θ ′ ) k ∈ Q\{q f } with k ∈ {i, i -1},
some path of the run ρ will reach the configuration ( p ′ , v , θ ′ ). Thus, we can have ( p, w , θ) ⇒ * ( p ′ , v , θ ′ ).

-Case θ j = θ, then there exists a transition rule r in θ, r : p ֒ (σ,σ ′ ) ---→ p j ∈ ∆ c and θ j = θ\σ ∪ σ ′ . In this case, w j = γ and j = 1. Thus, the root of ρ j is ( p j , w j w ′ , θ j ). Since H(ρ) ≥ 1 (p / ∈ F ), we can get H(ρ j ) < H(ρ). Thus we apply the induction hypothesis on H(ρ j ), we can get that there exists a path (p j , θ j ) i w j w ′ ---→ T {q f } in A i and for every

decomposition (p j , θ j ) i u - → T Q v - → T {q f } of the path (p j , θ j ) i w j w ′ ---→ T {q f } where uv = w j w ′ , if Q = {q f }, then for all (p ′ , θ ′ ) k ∈ Q\{q f } with k ∈ {i, i -1},
some path of the run ρ j will reach the configuration ( p ′ , v , θ ′ ).

Moreover, there exists a path (p j , θ j ) i w j -→ T Q j w ′ -→ T {q f } in A i and by applying the saturation procedure, we get that (p, θ)

i γ - → Q j w ′ -→ T {q f } in A i . Thus, for every decomposition (p, θ) i u - → T Q v - → T {q f } of the path (p, θ) i γw ′ --→ T {q f }, if Q = {q f }, then for all (p ′ , θ ′ ) k ∈ Q\{q f } with k ∈ {i, i -1}, some path of the run ρ will reach the configuration ( p ′ , v , θ ′ ) i.e. ( p, w , θ) ⇒ * ( p ′ , v , θ ′ ).
For the statement (b). Since Y BP = P re + (Y BP ∩ F × Γ * × 2 ∆∪∆c ) and by the induction hypothesis Y BP ⊆ L(A i-1 ), we get that

Y BP ⊆ P re + (L(A i-1 ) ∩ F × Γ * × 2 ∆∪∆c ) (1)
By Lemma 11, we get that just before the substitution at Line 14, A i accepts

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

P re + (L(A i-1 ) ∩ F × Γ * × 2 ∆∪∆c
). Thus, it is sufficient to prove that for every configuration ( p, w , θ) ∈ Y BP , A i accepts ( p, w , θ) after the substitution at Line 14. Let n be the number of transition rules substituted at Line 14. For all m ≤ n, let A m i be the automaton obtained by substituting m transition rules. We show that Y BP ⊆ L(A m i ) by induction on m.

• Basis. m = 0. We directly get that Y BP ⊆ L(A 0 i ).

•

Step. m ≥ 1. By applying the induction hypothesis, we can get that

Y BP ⊆ L(A m-1 i ). If L(A m-1 i ) ⊆ L(A m i ), the result follows from the fact that Y BP ⊆ L(A m-1 i ). Otherwise, if L(A m-1 i )\L(A m i ) = ∅, let ( p, w , θ) ∈ L(A m-1 i )\L(A m i ) be some configuration s.t. |w| is the minimum of {|w ′ | | ( p ′ , w ′ , θ ′ ) ∈ L(A m-1 i )\L(A m i )} s.t. ( p, w , θ) ∈ Y BP .
Then we prove by contradiction that ( p, w , θ) should not be in Y BP .

For every path of the form (p, θ)

i w -→ T {q f } in A m-1 i , there exist u ∈ Γ + , v ∈ Γ * and q ∈ P such that w = uv and (p, θ) i u - → T Q ∪ { (q, θ ′ ) i-1 } v - → T {q f } in A m-1 i and A m i doesn't have {(q, θ ′ ) i } v - → T {q f }. (Otherwise, ( p, w , θ) ∈ L(A m i ))
. By the statement(a), for each accepting run ρ of BP starting from ( p, w , θ), one path of this run ρ will reach such a configuration ( q, v , θ ′ ). It is sufficient to show that ( q, v , θ

′ ) / ∈ Y BP . Now let us show that ( q, v , θ ′ ) / ∈ Y BP . If ( q, v , θ ′ ) / ∈ L(A m-1 i
), by applying the induction hypothesis on m, we get that ( q, v , θ

′ ) / ∈ Y BP . If ( q, v , θ ′ ) ∈ L(A m-1 i ), then ( q, v , θ ′ ) ∈ L(A m-1 i )\L(A m i ). If ( q, v , θ ′ ) ∈ Y BP , then |v| < |w| which contradicts the fact that |w| is the minimum of {|w ′ | | ( p ′ , w ′ , θ ′ ) ∈ L(A m-1 i )\L(A m i )} s.t. ( p, w , θ) ∈ Y BP . Thus, we can obtain that ( q, v , θ ′ ) / ∈ Y BP .
✷ Then, we can prove Theorem 4.2.2: Proof: We prove termination and correctness.

Termination: There are two loops in Algorithm 1. Thus, we will prove those two loops both terminate.

Experiments

to a standard PDS may take more than 24 days, whereas our direct algorithm takes only a few seconds.

Malicious

Behavior Detection on Self-Modifying Code 4.3.2.1 Specifying malicious behaviors using CTL.

We applied our tool to detect several self-modifying malwares. Indeed, as shown in [START_REF] Song | Pumoc: a ctl model-checker for sequential programs[END_REF], several malicious behaviors can be described by CTL formulas. We give in what follows an example of such a malicious behavior.

Spyware (Scanning the Disk). The aim of a spyware is to steal information from the host. To do this, it has to scan the disk of the host in order to find the interesting file that he wants to steal. If a file is found, it will run a payload to steal it, then continues searching the next file. If a directory is found, it will enter this path and continues scanning. This malicious behaviour is present e.g. in the notorious spyware Flame: It first calls the function FindFirstFileW to search the first object in the given path, then, it will check whether the function call succeeds or not. If the function call fails, it will call the function GetLastError. Otherwise it will call either the function FindFirstFileW again if it finds a directory or the function FindNextFileW to search for the next object. We can specify this behavior in CTL as follows:

φ spy = EF call F indF irstF ileW ∧ AF call GetLastError ∨call F indF irstF ileW ∨ call F indN extF ileW
This formula states that there exists a path where the function F indF irstF ileW is called, then, in all the future paths, the program either calls GetLastError (if F indF irstF ileW failed) or calls F indF irstF ileW (if a directory is found) or calls F indN extF ileW (to search for the next file). Scanning a disk can be a behavior of a benign program. To avoid false alarms, we can combine this CTL formula with other formulas describing other malicious behaviors expressing the payload (such as sending a file) to determine whether the binary code is a malware or not. Note that, the formula is branching time and cannot be described as a LTL formula. In this chapter, we present SMODIC, a model checker for self-modifying binary code that use self-modifying mov instructions. In SMODIC, such binary code is modeled using Self Modifying Pushdown Systems (SM-PDS). SMODIC takes as input either a self-modifying binary code or a self modifying pushdown system. It can then perform reachability analysis and LTL/CTL model-checking for these models. SMODIC first adapts the tool Jakstab [START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF] to get the Control Flow Graph from the binary code. Then, it translates this CFG into a SM-PDS. It then implements the algorithms presented in the previous chapters to perform reachability analysis and LTL/CTL model-checking for this model.

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

We successfully used SMODIC to model-check more than 900 self-modifying binary codes. In particular, we applied SMODIC for malware detection. In our experiments, SMODIC was able to detect 895 malwares and to prove that 19 benign programs were benign. SMODIC 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. SMODIC can be found in https://lipn.univ-paris13.fr/ ~xin/smodic/index.html.

Comparison with Well-known Anti-viruses

We also compare our tool against well-known and widely used antiviruses. In order to have a fair comparision, we need to consider new malwares, since the anti-viruses know the signatures of all the known malwares. Thus, the challenge for the anti-viruses is to detect new malwares. To this aim, we use the sophisticated malware generator NGVCK available at VX Heavens [START_REF] Heaven | [END_REF] to generate new malwares. Then we obfuscate these malwares with self-modifying code. Then, we feed these malwares to SMODIC and to well-known antiviruses such as Bit-Defender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Avast, and Symantec to detect them. 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 5.1 reports the detection rates of our tool and the well-known anti-viruses. The model file can be either a binary program or a SM-PDS (.smpds file). The output have three files: one for the Control Flow Graph, one for assembly codes, and one for the generated SM-PDS. A SM-PDS consists of four parts: a finite set of standard PDS transition rules, a finite set of self-modifying transition rules, an initial phase (the initial set of transition rules) and an initial configuration (initial control location equipped with the stack contents). In order to show this, we will use the following command to check whether the program cmd.exe can eventually call the API function GetModuleA or not. For this case, we execute the following command: ./SMODIC B malware/cmd.exe L <> (getasynckeystate|| getrawinputdata)&& <> (sendto||send) . The result is shown in Figure 5.11. The result of the computation is that there is no accepting run. The output of the tool is No, i.e. cmd.exe is not a spyware.

Description of SMODIC

Conclusion 6.1 Summary

In this thesis, we propose a new formal model for self-modifying code called Self Modifying Pushdown System(SM-PDS). It is an extension of standard Pushdown Systems (PDS) with self-modifying transition rules that modify the set of the rules of the PDS during the execution. This allows to represent the self-modifying instructions of the program. We also proposed several corresponding modelchecking algorithms for this SM-PDS model and implemented them in a tool: SMODIC to perform the analysis of self-modifying code and malware detection.

Modeling Self-modifying Code: In Chapter 2, we introduce our new model: SM-PDS. This new model allows us to present the self-modifying code by selfmodifying transition rules. A SM-PDS is a Pushdown System that can dynamically modify its set of rules during the execution time: rules that are not selfmodifying rules are standard PDS transition rules, while self-modifying rules modify the current set of transition rules. We show how SM-PDSs can be used to naturally represent self-modifying programs. It turns out that SM-PDSs are equivalent to standard PDSs. We show how to translate a SM-PDS to a standard PDS. This translation is exponential. Thus, performing the model-checking analysis on the equivalent PDS is not efficient. We propose then in this thesis direct algorithms to perform reachability and LTL/CTL model checking on SM-PDSs.

Rechability Analysis of Self-Modifying Code: In Chapter 2, we propose direct algorithms to compute the forward (post * ) and backward (pre * ) reachabil-

Future Work

Precise Model for Self-modifying Code: As described in Section 2.3, during the construction of the SM-PDS, we need to assume that instructions i 1 and i 2 have the same number of operands where i 1 is replaced by i 2 because of some selfmodifying instructions. If instructions i 1 and i 2 do not have the same number of operands, then the corresponding self-modifying instruction, in addition to replacing i 1 by i 2 , changes several other instructions that follow i 1 . As mentioned in Section 2.3, our translation from a self-modifying binary program to a SM-PDS can only handle the case where i 1 and i 2 have the same number of operands. In the future, we plan to improve our SM-PDS model so that it can handle the case where i 1 and i 2 do not have the same number of operands.

Precise Control Flow Reconstruction: In our implementation, the control flow reconstruction is not very precise. This step is based on the tool Jakstab [START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF] as disassembler. But Jakstab will sometimes ran into some situations where the value set analysis cannot be processed and the reconstruction of the control flow will stop. This holds, in many cases such as: (1) some values of the registers and possible values of memory addresses are unknown and are represented by any possible values (the ⊤ value); or (2) the destination of some indirect jumps cannot be computed. In the future, we plan to come up with new approaches to construct more precise control flow graphs from binary code to make the procedure of disassembling more precise.

Precise Malicious Behavior Description: In our experiments, we use standard LTL/CTL formulas to describe malicious behaviors. It was shown in [START_REF] Song | Efficient malware detection using model-checking[END_REF][START_REF] Song | Ltl model-checking for malware detection[END_REF] that SCTPL and SLTPL are more precise and concise to represent malicious behaviors. SCTPL and SLTPL are logics that extend LTL and CTL with variables, quantifiers and predicates over the stack. In the future, we plan to propose SCTPL/SLTPL model checking algorithms for SM-PDS. This would allow to have more precise and concise algorithms for self-modifying code analysis and malware detection.

Figure 1 . 1 :

 11 Figure 1.1: A Simple Example of Self-modifying Codes

Fig. 2 .

 2 Fig. 2.1 shows how malware can use self-modifying instructions to evade from static analysis techniques. This figure shows a fragment of the malware Bagle.J equipped with such self-modifying instructions. First let us recall the semantics

2. 4

 4 Representing Infinite Sets of Configurations of a SM-PDS 2.3.2 From Self-modifying Code to SM-PDS

Theorem 2 . 5 . 1 A

 251 pre * recognizes pre * (L(A)). Before proving this theorem, let us illustrate the construction on 2 examples.

Figure 2 . 2 :

 22 Figure 2.2: The automata A (left) and A pre * (right)

Figure 2 . 3 :Example 3

 233 Figure 2.3: The automata A (left) and A pre * (right)

22 2. 5

 225 Efficient Computation of pre * images Proof: Let A pre * = (Q, Γ, T, P, F ) be the P-automaton computed by the saturation procedure. In this proof, we use --→ i T ′

Figure 2 . 4 :Example 4

 244 Figure 2.4: The automata A (left) and A post * (right)

Figure 2 . 5 :Example 5

 255 Figure 2.5: The automata A (left) and A post * (right)

29 2 .

 2 REACHABILITY ANALYSIS OF SELF MODIFYING CODE 2.6.1 Proof of Theorem 2.6.1

Definition 5 A

 5 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 in 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 , θ).

3 :Table 3 . 4 :

 334 Multiple pre * v.s. our direct LTL model-checking algorithm (part 1) Multiple pre * v.s. our direct LTL model-checking algorithm (part 2)

  ∆∪∆c and C ⊆ P × Γ * × 2 ∆∪∆c , if c ⇒ BP C then c is an immediate predecessor of C and C is an immediate successor of c. Let ⇒ * BP ⊆ (P × Γ * × 2 ∆∪∆c ) × 2 (P ×Γ * ×2 ∆∪∆c ) be the reflexive transitive closure of ⇒ BP defined as follows: (1) ∀c ∈ P × Γ * × 2 ∆∪∆c , c ⇒ * BP {c}, (2) if c ⇒ BP C, then c ⇒ * BP C, and (3) if c ⇒ BP {c 1 , ...c n } and c i ⇒ * BP C i for every 1 ≤ i ≤ n, then c ⇒ * BP n i=1 C i . Given a set of configurations C, we define the sets pre BP (C), pre * BP (C) and pre + BP (C) as follows: pre BP(C) = {c ∈ P × Γ * × 2 ∆∪∆c |∃C ′ ⊆ C s.t. C ′ is an immediate successor of c}, pre * BP (C) = {c ∈ P × Γ * × 2 ∆∪∆c , ∃C ′ ⊆ C s.t. c ⇒ * BP C ′ } and pre + BP (C) = pre BP • pre * BP(C). We omit the subscript BP when it is clear from the context.

  Let us show how to use SMODIC. The commands to launch the tool are as follows: -SMODIC <option1> < modelfile> < option2 > <formula> Option1 specifies the input file of SMODIC: 113 5. SMODIC: A MODEL CHECKER FOR SELF MODIFYING CODE -M: the input is a SM-PDS model. -B: the input is a binary program Option2 specifies the model checking strategy: -L: use the LTL model checking algorithm -C: use the CTL model checking algorithm -R1: perform the Reachability Analysis using pre * -R2: perform the Reachability Analysis using post *

Figure 5 . 2 :

 52 Figure 5.2: The Output of SMODIC

Figure 5 . 3 :

 53 Figure 5.3: A Segment of Disassembly Codes

5. 4

 4 Applying SMODIC for Malware Detection function in lowercase string. The operators are in spin syntax. Thus, formula φ sw is rewritten as: <> (getasynckeystate||getrawinputdata)&& <> (sendto||send)

Figure 5 . 10 :

 510 Figure 5.10: Command for LTL Model Checking

Figure 5 . 11 :

 511 Figure 5.11: Result of LTL Model Checking

  4 , ϵ⟩ r 6 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 5 , γ 1 ⟩ r 6 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 5 , γ 1 ⟩ r 7 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 5 , ϵ⟩ r 7 : ⟨p 2 , γ 2 ⟩ ↪ ⟨p 5 , ϵ⟩

	Δ c : Δ c :
	r 1 c : p 5 r 1 c : p 5
	r 2 c : p 5 r 2 c : p 5
	r 3 c : p 2 r 3 c : p 2
	r 4 c : p 4 r 4 c : p 4

  Our Algorithms vs. Standard pre * and post * Algorithms of PDSs

	7 Experiments
	2.7 Experiments
	2.7.1

Table 2 . 1 :

 21 Our direct pre * algorithm vs. standard pre * algorithms of PDSs

	36

Table 2 . 2 :

 22 Our direct post * algorithm vs. standard post * Self-modifying code is widely used as an obfuscation technique for malware writers. Thus, we applied our tool for malware detection.

	algorithms of PDSs

Table 2 .

 2

3: Malware Detection

Table 3 .

 3

	Experimental Results (part 1)
	5:

Table 3 . 6 :

 36 Experimental Results (part2)

Table 3 .

 3

	Experimental Results (part 3)
	7:

Table 3 . 8 :

 38 Experimental Results (part 4)

Table 4 .

 4

	Bagle.ab 5690	Atak.f 2005	Newapt.C 11730	Bagle.m 5111	LdPinch.aaz 4145	LdPinch.v 7235	LdPinch.bb 8145	Newapt.F 11785	LDPinch.400 1783	Generic.12861 30183	LdPinch.by 970	Mydoom.ACQ 19210	Sramota.avf 240	Mydoom.R 230	Mydoom.M 5965	klez.e 27	Kelino.g 470	Kelino.l 495	Netsky.d 45	Repah.b 221	klez.c 30	Mydoom.y 26902	Netsky.r 230	Netsky.gen 5508	Netsky.x 55	Netsky.a 45	game.exe 34325	ipv4.exe 968	sort.exe 8529	notepad.exe 10529	shutdown.exe 2529	calculation.exe 9952	Example Size
	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	No	No	No	No	No	No	Result
	89.42s	11.35s	924.92s	39.92s	41.05s	51.69s	63.13s	211.24s	54.93s	188.94s	42.92s	439.57s	11.01s	30.22s	75.19s	3.94s	22.08s	21.01s	1.87s	12.76s	2.79s	452.77s	8.83s	59.24s	21.85s	19.12s	234.14s	24.43s	74.12s	68.77s	23.52s	76.34s	cost
	Bagle.ef 995	Atak.g 2498	Krynos.b 18370	Bagle.k 35	LdPinch.c0 8230	LdPinch.fk 4906	LdPinch.br 3645	Newapt.A 11715	PSW.LdPinch.plt 1808	Generic.18017273 267	Generic.2026199 433	Mydoom.ba 19423	Mydoom 238	Mydoom.dlnpqi 235	MyDoom.54464 5935	Magistr.b 4670	Plage.b 395	Kipis.t 20378	Ardurk.d 1913	Gibe.b 5358	Mydoom.v 5965	Mydoom.j 22355	Netsky.k 6115	Netsky.p 6015	Netsky.y 68	Mydoom.c 155	cycle.tex 9014	TextWrangler.exe 14675	bibDesk.exe 32800	java.exe 800	loop.exe 529	cisvc.exe 4105	Example Size
	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	No	No	No	No	No	No	Result
	54.11s Bagle.eg 380	16.69s Atak.l 1914	893.45s Jeans.a 6490	1.92s Bagle.t 3345	65.17s LdPinch.ee 6501	47.11s LdPinch.awp 195	33.52s LdPinch.hb 1645	205.79s Newapt.E 11797	55.88s PSW.Pinch.1 1905	9.19s LdPinch.mg 5957	32.83s LdPinch.arr 1250	238.77s Mydoom.ftde 19495	2.01s Mydoom.288 248	1.99s Mydoom.o 235	45.78s Mydoom.e 138	231.97s Magistr.a.poly 36989	1.96s Urbe.a 123	121.11s klez.d 31	12.08s klez.f 27	37.01s Magistr.b 4670	283.11s Netsky.b 45	211.93s klez-N 6281	79.79s Netsky.e 6245	76.32s Netsky.m 6805	29.06s Netsky.z 115	4.14s MyDoom-N 16980	75.44s calender.exe 892	65.09s sogou.exe 45219	243.79s interface.exe 1005	19.17s java.exe 21324	11.78s cmd.exe 1324	31.22s simple.exe 52	cost Example Size
	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	Yes	No	No	No	No	No	No	Result
	25.49s	10.37s	188.36s	45.64s	71.30s	17.97s	21.08s	252.49s	57.07s	69.77s	49.84s	339.29s	3.12s	2.01s	46.53s	469.63s	9.17s	0.95s	0.73s	43.59s	29.51s	63.07s	79.44s	73.77s	43.37s	343.93s	25.39s	301.14s	18.25s	122.07s	19.36s	3.17s	cost

1: Our approach vs. standard algorithms for PDSs for CTL model checking

4. CTL MODEL-CHECKING OF SELF-MODIFYING CODE

Table 4 . 2 :

 42 Experimental Results (part 1)

	108

Table 4 .

 4

	Experimental Results(part 2)
	3:

Table 4 . 4 :

 44 Experimental Results(part 3)

	110

Table 5 . 1 :

 51 SMODIC vs. Well-known Anti-viruses 5.2 Experiments 5.2.1 Analysing Self-modifying Binary Code We successfully applied SMODIC to perform reachability analysis and LTL/CTL model-checking for binary code and for Self-Modifying Pushdown systems. The results are summarized in Tables 2.1, 2.2, 3.1, 3.2 and 4.1. SMODIC was also able to detect 895 malwares and to prove that 19 benign programs are benign. The experimental results are summarized in Tables 3.5, 3.6, 3.7, 3.8, 4.2, 4.3 and 4.4.

S 1 : 2059, S 2 : 9 |δ|:8 1.49s 19784.7s 79.12s 19863.32

Acknowledgements

LTL MODEL-CHECKING OF SELF-MODIFYING CODE

A labelled configuration [( p, w , θ), b] is accepted by the automaton A iff there exists a path (p, θ)

(p, θ) ∈ I, and q n+1 ∈ F . Let L(A) be the set of labelled configurations accepted by A.

Computing pre

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: ---→ 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 128.12s error - 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 RegSetValueExA is called to add the file path into the registry key listing. This malicious behavior can be described in LTL as follows:

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

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

Standard CTL operators can be expressed by the above operators:

Self-modifying Alternating Büchi Pushdown Systems

Definition 9 A Self Modifying Alternating Büchi Pushdown System (SM-ABPDS) is a tuple BP = (P, Γ, ∆, ∆ c , F ), where P is a finite set of control points, Γ is a finite set of stack symbols, F is the set of final states, ∆ ⊆ (P × Γ) ×

A configuration of a SM-ABPDS is a tuple of the form ( p, w , θ) where p ∈ P , w ∈ Γ * and θ ⊆ ∆ ∪ ∆ c is the current phase.

BP defines the transition relation ⇒ BP ⊆ (P ×Γ * ×2 ∆∪∆c )×2 (P ×Γ * ×2 ∆∪∆c ) between configurations as follows: Let θ ⊆ ∆ ∪ ∆ c , γ ∈ Γ, w ∈ Γ * , and p ∈ P , then:

CTL Model-Checking of SM-PDSs

System BP ϕ s.t. BP ϕ accepts a configuration c iff c |= ν ϕ. Thus, determining whether c 0 |= ν ϕ can be reduced to checking whether c 0 ∈ L(BP ϕ ).

Let BP ϕ = (P ′ , Γ, ∆ ′ , ∆ ′ c , F ) be the SM-ABPDS defined as follows: ϕ) , where P cl(ϕ) is the set of control locations in the form p ψ where p ∈ P and

we call this set of rules prod(r). Moreover, let prod E (r) ⊆ prod(r) be the set of rules generated from r using subformulas of the form EXψ

( see below for more details about prod(r) and prod E (r)).

The transition relations ∆ ′ and ∆ ′ c (resp. the sets prod(r) and prod E (r), for every r ∈ ∆ ∪ ∆ c ) are the smallest sets of transitions (resp. of sets of rules) defined as follows:

and ∀γ ∈ Γ, we have:

the set of all the rules of ∆ that have p, γ in the left-hand-side. Then,

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

֒----→ p n } be the set of all the rules of ∆ c that have p in the left-hand-side. Then, for every γ ∈ Γ,

, and for every 1

γ ֒→ p n , w n } be the set of all the rules of ∆ that have p, γ in the left-hand-side. Then,

where for every 1 ≤ i ≤ n, σ i = prod E (R i ), and

֒----→ p n } be the set of all the rules of ∆ c that have p in the left-hand-side. Then, ∀1 ≤ i ≤ n, for every

be the set of all the rules of ∆ that have p, γ in the left-hand-side.

Then for every 1

֒----→ p n } be the set of all the rules of ∆ c that have p in the left-hand-side. Then, for every γ ∈

Let prod(∆) = {r ′ ∈ ∆ ′ | ∃r ∈ ∆, r ′ ∈ prod(r)} be the set of rules of ∆ ′ that are generated from ∆. Let δ = ∆ ′ \ prod(∆) be the set of rules of ∆ ′ that are not generated from any rule of ∆ nor ∆ c (e.g., the rules computed by items 1, 2, 3 and 4 are in δ). These rules δ are independent of ∆ and ∆ c . They are introduced by the structure of ϕ. Thus, they need to be present in all the phases of BP ϕ . Let then θ ⊆ ∆ ∪ ∆ c be a phase of P. Its corresponding phase in BP ϕ is β(θ) = prod(θ) ∪ δ, where prod(θ) = {r ′ ∈ ∆ ′ ∪ ∆ ′ c | ∃r ∈ θ, r ′ ∈ prod(r)}. Let us explain the above construction intuitively. The above automaton BP ϕ can be seen as a kind of product of the SM-PDS P with the formula ϕ. For ψ ∈ cl(ϕ), ( p, w , θ) |= ν ψ iff BP ϕ accepts a configuration [p, ψ], w , β(θ) . We give in what follows the intuition behind all the items above:

Hence, the automaton BP ϕ should accept a run starting from ( [p, a], w , β(θ)) iff a ∈ ν(p). [p, a] ∈ F iff a ∈ ν(p). Thus, the loop added in ( [p, a], w , β(θ)) by Item 1 makes sure that BP ϕ accepts this run.

If -→ [p, ¬a], γ ∈ ∆ ′ and r ∈ δ (since it is not from ∆ nor ∆ c ). Then, r ∈ β(θ) and there is a loop in ( [p, ψ], w , β(θ)). Hence, BP ϕ has an accepting run from ( [p, ψ], w , β(θ)).

By applying the induction hypothesis, BP ϕ has an accepting run from the configuration ( [p,

Case ψ = EXψ 1 : Since ( p, w , θ) |= ν ψ, then there exists an immediate successor ( p 1 , w 1 , θ 1 ) of ( p, w , θ) s.t. ( p 1 , w 1 , θ 1 ) |= ν ψ 1 . By applying the induction hypothesis, BP ϕ has an accepting run from ( [p 1 , ψ 1 ], w 1 , β(θ 1 )). There are two cases depending on whether p ∈ P N or not.

By the construction Item 5, we can obtain

). Hence, BP ϕ has an accepting run from ( [p, ψ], w , β(θ)).

Case ψ = AXψ 1 : there are 2 cases depending on whether p ∈ P N or not.

-Case p ∈ P N . Let then γ ∈ Γ and u ∈ Γ * be such that w = γu.

be the set of all the rules of ∆ that have p, γ on the left hand-side. Then, by Item 6(a), we ob-

} is an immediate successor of ( p, w , θ). Since ( p, w , θ) |= ν ψ, then ( p i j , w i j , θ) |= ν ψ 1 for every j, 1 ≤ j ≤ k. By applying the induction hypothesis, BP ϕ has an accepting run from ( [

Since BP ϕ has an accepting run from ( [p i j , ψ 1 ], w i j , β(θ)), then, BP ϕ has an accepting run from ( [p, ψ], w , β(θ)).

-Case p ∈ P C . Let then γ ∈ Γ and u ∈ Γ * be such that w = γu. Let

֒----→ p n } be the set of all the rules of ∆ c that have p on the left hand-side. Then, by Item 6(b), we obtain that

) is an immediate successor of ( p j , w j , θ j ).

If p j ∈ P N , then there exists

Hence, BP ϕ has an accepting run from the configuration ( [p j , ψ], w j , β(θ j )).

Then, we can obtain that:

Hence, BP ϕ has an accepting run from the configuration ( [p j , ψ], w j , β(θ j )).

-

Step. l > 1. Then there exists ( p j+1 , w j+1 , θ j+1 ) s.t. ( p j , w j , θ j ) ⇒ P ( p j+1 , w j+1 , θ j+1 ) ⇒ * P ( p i , w i , θ i ). By applying the induction hypothesis (induction on l), we can obtain that BP ϕ has an accepting run from ( [p j+1 , ψ], w j+1 , β(θ j+1 )). Since ( p j , w j , θ j ) |= ν ψ 1 , by applying the induction hypothesis (induction on the structure of ψ), BP ϕ has an accepting run from ( [p j , ψ 1 ], w j , β(θ j )). There are two cases depending on whether p j ∈ P N or not.

-Case p j ∈ P N , then there exists

So, BP ϕ has an accepting run from the configuration ( [p j , ψ], w j , β(θ j )).

Hence, BP ϕ has an accepting run from the configuration ( [p j , ψ], w j , β(θ j )).

Thus, BP ϕ has an accepting run from ( [p, ψ], w , β(θ)).

, then there exists a path ( p 0 , w 0 , θ 0 ), ( p 1 , w First let us consider item 2, it can be proved that BP ϕ has an accepting run from ( [p, ψ], w , β(θ)) by applying the induction on ij similar to the case

Let's consider item 1, we will show that BP ϕ has an accepting run from ( [p, ψ], w , β(θ)). Let us construct an accepting run ρ of BP ϕ as follows. (Note that ( [p, ψ], w , β(θ)) = ( [p 0 , ψ], w 0 , β(θ 0 ))).

Let ( [p 0 , ψ], w 0 , θ 0 ) be the root of ρ. For every k ≥ 0,

• if p k ∈ P N , then we have that

CTL Model-Checking of SM-PDSs

In this case, we let ( [p k , ψ 2 ], w k , β(θ k )) and ( [p k+1 , ψ], w k+1 , β(θ k+1 )) be the children of ( [p k , ψ], w k , β(θ k )). By applying the induction hypothesis to ( p k , w k , θ k ) |= ν ψ 2 , we obtain that BP ϕ has an accepting run

We replace the child ( [p k , ψ 2 ], w k , β(θ k )) in ρ by the run ρ k . By the above construction, we obtain an infinite run ρ of BP ϕ s.t. ρ has an infinite path

and all the other paths infinitely often visit some accepting control locations. Since for every k ≥ 0, [p k , ψ] ∈ F , we obtain that each path of ρ infinitely often visits some accepting control locations i.e. BP ϕ has an accepting run from ( [p, ψ], w , β(θ)).

. By applying the induction hypothesis to ( p k , w k , θ k ) |= ν ψ 2 , we obtain that BP ϕ has an accepting run ρ k from ( [p k , ψ 2 ], w k , β(θ k )). We replace the child ( [p k , ψ 2 ], w k , β(θ k )) in ρ by the run ρ k . By the above construction, we obtain an infinite run ρ of BP ϕ s.t. ρ has an infinite path

and all the other paths infinitely often visit some accepting control locations. Since for every k ≥ 0, [p k , ψ] ∈ F , we obtain that each path of ρ infinitely often visits some accepting control locations i.e. BP ϕ has an accepting run from ( [p, ψ], w , β(θ)).

(⇐) : Suppose BP ϕ has an accepting run from the configuration ( [p, ψ], w , β(θ)), we show that ( p, w , θ) |= ν ψ by induction on the structure of ψ.

Case ψ = a: Since BP ϕ has an accepting run from ( [p, ψ], w , β(θ)), then ∀γ ∈ Γ,

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

Case ψ = ¬a: Since BP ϕ has an accepting run from ( [p, ¬a], w , β(θ)), then

Since BP ϕ has an accepting run from ( [p, ψ], w , β(θ)), then BP ϕ has an accepting run from ( [p, ψ 1 ], w , β(θ)) or BP ϕ has an accepting run from ( [p, ψ 2 ], w , β(θ)). By applying the induction hypothesis, we get that ( p, w , θ) |= ν ψ 1 or ( p, w , θ) |= ν ψ 2 . This implies that ( p, w , θ) |= ν ψ.

Case ψ = EXψ 1 : it is similar to the case ψ = AXψ 1 .

Case ψ = AXψ 1 : Since BP ϕ has an accepting run from ( [p, ψ], w , β(θ)). There are two cases depending on whether p ∈ P N or not.

-Case p ∈ P N . Then suppose there exists an immediate successor

By applying the induction hypothesis, we get that ( p i , w i , θ i ) |= ν ψ 1 for 1 ≤ i ≤ n. By the construction, the immediate successors in P of ( p, w , θ) are ( p 1 , w 1 , θ), • • • , ( p n , w n , θ). Thus, we obtain that ( p, w , θ) |= ν ψ.

-Case p ∈ P C . Then suppose there exists a successor

Then BP ϕ has an accepting run from ( [p i , ψ 1 ], w i , β(θ i )) for each i : 1 ≤ i ≤ n. By applying the induction hypothesis, we get that ( p i , w i , θ i ) |= ν ψ 1 for 1 ≤ i ≤ n. By the construction of Item 6(b), there exists

where σ = prod(r i ) and σ ′ = prod(r ′ i ) ensuring that θ i = (θ \ {r i }) ∪ {r ′ i }. Thus, we can obtain that the set of all transition rules of the SM-PDS in ∆ c ∩ θ that have p in the left-hand side are

Then, the immediate successors of ( p, w , θ) in P are ( p 1 , w , θ 1 ), • • • , ( p n , w , θ n ). Thus we obtain that ( p, w , θ) |= ν ψ.

Case ψ = E[ψ 1 U ψ 2 ] : Let ρ be the accepting run from ( [p, ψ], w , β(θ)). By the construction, every configuration ( [p i , ψ], w i , β(θ i )) in ρ has

Since ρ is an accepting run, there exists a configuration ( [p n , ψ], w n , β(θ n )) in ρ s.t. ( [p n , ψ], w n , β(θ n )) has only one child ( [p n , ψ 2 ], w n , β(θ n )). In particular, there exists a path of ρ of the form ( q 0 , w q 0 , β(θ 0 )), • • • , ( q n , w qn , β(θ n )) • • • where ( q 0 , w q 0 , β(θ 0 )) = ( [p, ψ], w , β(θ)) and ( q n , w qn , β(θ i )) = ( [p n , ψ], w n , β(θ n )). Then, BP ϕ has an accepting run from ( q i , w q i , β(θ i )) of the form ( [p i , ψ], w i , β(θ i )) for every i : 0 ≤ i < n.

and

and ( p ψ i , w i , β(θ i )) whose child is ( [p i+1 , ψ], w i+1 , β(θ i+1 )) or has only one child ( [p i , ψ 2 ], w i , β(θ i )). Since BP ϕ has an accepting run from ( [p n , ψ], w n , β(θ n ))

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

))}. Thus, BP ϕ has an accepting run from ( [p i , ψ 1 ], w i , β(θ i )).

BP ϕ has an accepting run from ( [p n , ψ 2 ], w n , β(θ n )) and ( [p i , ψ 1 ], w i , β(θ i )) for i < n. By applying the induction hypothesis, we get that (

Case ψ = E[ψ 1 U ψ 2 ]: Let ρ be the accepting run from ( [p, ψ], w , β(θ)). By the construction, every configuration ( [p i , ψ], w i , β(θ i )) in ρ has two children:

1. either ( [p i , ψ 2 ], w i , β(θ i )) and ( q i , w q i , β(θ i )) where

or ( [p

First, we consider Case 1.

Since ρ is an accepting run, there exists an infinite path of ρ of the form

where ( q 0 , w q 0 , β(θ 0 )) = ( [p, ψ], w , β(θ)) and BP ϕ has an accepting run from ( [p i , ψ 2 ], w i , β(θ i )) for every i ≥ 0.

By applying the induction hypothesis ( the fact that BP ϕ has an accepting run from ( [p i , ψ 2 ], w i , β(θ i ))), we get that ( p i , w i , θ i ) |= ν ψ 2 for every i ≥ 0. By the construction, we get that ( p 0 , w 0 , θ 0 ),

4.2 Computing the language of a SM-ABPDS in this path has children ( [p i , ψ 2 ], w i , β(θ i )) and ( [p i+1 , ψ], w i+1 , β(θ i+1 )) or ( p ψ i , w i , β(θ i )) whose child is ( [p i+1 , ψ], w i+1 , β(θ i+1 )). So BP ϕ has an accepting run from ( [p n , ψ 1 ], w n , β(θ n )) and BP ϕ has an accepting run from ( [p i , ψ 2 ], w i , β(θ i )) for every 1 ≤ i ≤ n. By applying the induction hypothesis, (

is a run of P with ( p 0 , w 0 , θ 0 ) = ( p, w , θ). Thus, ( p, w , θ) |= ν ψ.

✷ Therefore, CTL model-checking for SM-PDSs can be reduced to the problem of determining whether a SM-ABPDS has an accepting run.

Computing the language of a SM-ABPDS

From now on, we fix a SM-ABPDS BP = (P, ∆, ∆ c , Γ, F ). We show in this section that the set of configurations accepted by BP is regular and can be effectively represented by an EAMA (extended Alternating Multi-automaton). To this aim, we first characterize the set of configurations L(BP) from which BP has an accepting run. Then we use this characterization to compute an EAMA that accepts it.

Characterizing L(BP)

Let (X i ) i≥0 be the following sequence: X 0 = P × Γ * × 2 ∆∪∆c , and for every i ≥ 0, Proving this theorem is based on the following lemma:

Lemma 8 BP has a run ρ starting from a configuration ( p, w , θ) s.t. each path of ρ visits configurations with control locations in F at least k times iff ( p, w , θ) ∈ X k .

Computing the language of a SM-ABPDS

Proof: (⇒) : In this direction, we show that if ( p, w , θ) / ∈ Y BP , then BP has no accepting run from ( p, w , θ).

Since ( p, w , θ) /

∈ Y BP and Y BP = i≥0 X i , there exists k ≥ 0 s.t. ( p, w , θ) / ∈ X k . Assume BP has an accepting run from ( p, w , θ). Then, by Lemma 8, all runs from the configuration ( p, w , θ) can visit configurations with control location in F at least k times, we can get that ( p, w , θ) ∈ X k which contradicts the fact that ( p, w , θ) / ∈ X k . Thus, BP has no accepting run from the configuration ( p, w , θ).

(⇐) : We prove that if ( p, w , θ) ∈ Y BP , then BP has an accepting run from ( p, w , θ). Since

Then we will construct a finite run (tree) ρ with root ( p, w , θ), the leaves of ρ are {( p 1 , w 1 , θ 1 ), • • • , ( p n , w n , θ n )} and the inner nodes are the successors during the derivation of ( p, w , θ) ⇒ BP {( p 1 , w 1 , θ 1 ), • • • , ( p n , w n , θ n )}. Every path of ρ can visit some configurations with control locations in F at least once.

Since ( p i , w i , θ i ) ∈ Y BP , we can repeatedly construct a corresponding tree ρ i for the configuration ( p i , w i , θ i ). Then the leaf ( p i , w i , θ i ) in ρ can be replaced by the tree ρ i and we can obtain a new tree whose every path can visit some configuration with control location in F at least twice. Then we can infinitely repeat this procedure to leaves of the latest tree. Then each path of the latest tree can visit some configurations with control locations in F infinitely often. Thus, BP has an accepting run ρ. ✷

Computing Y BP

In this section, our goal is to compute Y BP . We show that this set can be effectively represented by an EAMA A = (Q, Γ, T, I, Q f ), where Q ⊆ P × 2 ∆∪∆c × N ∪ {q f }, I ⊆ P × 2 ∆∪∆c × N is the set of initial states and q f is the final state (Q f = {q f }). Following [START_REF] Song | Efficient ctl model-checking for pushdown systems[END_REF], we propose a saturation procedure to compute A iteratively. Algorithm 1 below computes A. Intuitively, it computes the Repeat (we call this loop loop 2 )

Then, add (p, θ) i γ -→ Q to T .

12:

Until No new transition rule can be added.

13:

Remove from T the transition rules (p, θ) i ǫ -→ (p, θ) i-1 , for every p ∈ F.

14:

Replace every (p,

Until i > 1 and for every p

Intuitively, at each step i, every state (p, θ) is represented by state (p, θ) i in A i . For every (p, θ) ∈ I, A i recognizes a configuration ( p, w , θ) if (p, θ) i ω -→ T q f . A 0 is the automaton obtained by Line 1. It accepts X 0 = P × Γ * × 2 ∆∪∆c . At 4.2 Computing the language of a SM-ABPDS the beginning of each iteration, an ǫ-transition in the form (p, θ) i ǫ -→ T (p, θ) i-1 is added in Line 4 for every (p, θ) ∈ F × 2 ∆∪∆c in the current automaton. This allows to get L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ). Lines 5-12 (loop 2 ) is the saturation procedure that computes P re * BP L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) . They ensure that if θ is a phase such that p, γ ֒

T should contain the path (p, θ) i γw -→ T q f . This path is added thanks to Line 8.

Moreover, if θ is a phase such that p, γ ֒

, where θ ′ = θ\σ ∪ σ ′ ; then ( p, γw , θ) should also be in L(A i ) (since it is a predecessor of ( p ′ , γw , θ ′ )). I.e., T should contain the path (p, θ) i γw -→ T q f . This path is added thanks to Line 11. Line 13 removes the ǫ-transition added by Line 4. This leads to P re + BP L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) . Let Algorithm A be Algorithm 1 without Line 14. Then, if Algorithm A terminates, it computes Y BP . However, if the sequence X i is strictly decreasing, Algorithm A never terminates. Lines 14-15 are then used to force termination. Indeed, thanks to the substitution of Line 14, at the end of step i, states of the form (p, θ) j , for j < i become useless and can be removed. Line 15 checks then whether at step i, the transitions of A i are "the same" than those of A i-1 . If this is the case, the algorithm terminates. Termination of the algorithm then follows from the fact that step i adds less transitions than step i -1. Intuitively, this is due to the fact that L(A i ) ⊆ L(A i-1 ), because step i computes P re + BP L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) and A 0 accepts P × Γ * × 2 ∆∪∆c . Thus, we can show that: Theorem 4.2.2 Algorithm 1 always terminates and produces Y BP .

To prove Theorem 4.2.2, we need the following lemma: Lemma 9 In Algorithm 1, for every γ ∈ Γ, w ∈ Γ * , p ∈ P, S ⊆ Q; at each step i ≥ 1, the following holds:

CTL MODEL-CHECKING OF SELF-MODIFYING CODE

Proof: We proceed by induction on i.

Basis. i = 1. In this case, whenever a transition rule (p, θ) 1 γ -→ S is added to T by either the saturation procedure (Lines 2-12) or the substitution (Line 14), we can get that π -1 (π

). Therefore, the statement (a) holds. For statement (b). In this case, we can have that π

) Hence, the statement (b) holds.

Step. i > 1. Let k be the number of transition rules added at the step i. We proceed by induction on k.

-Basis. k = 0. there is no transition rule added in the form of (p, θ) i γ -→ S which implies that the statement (a) holds. For every (p, θ) i w -→ T S, we get that there is a path (p, θ) i ǫ -→ T (p, θ) i-1 w -→ T S in the automaton for some

). This implies the statement (b) holds.

-

For statement (a). Let t = (p, θ) i γ -→ S be the k-th transition rule added by the saturation procedure. Then there exist 1 ≤ j ≤ n and

There are 2 cases depending on whether t is added by Line 8 or not.

(I) if t is added by Line 8, then there exists a transition rule ---→ p j ∈ ∆ c ∩ θ in BP where θ j = θ\σ ∪ σ ′ . In this case, n = j = 1. Then, there exists (p j , θ j ) i γ -→ T S j s.t. S = S j . We rewrite (p j , θ j ) i γ -→ T S j of the form (p j l , θ j l ) i w j l --→ T S j l where j l = 1, θ j l = θ j and w j l = γ.

By applying the induction hypothesis on i to (p j l , θ j l ) i w j l --→ T S j l for each l : 1 ≤ l ≤ m, we can obtain that (p j l , θ j l ) i-1 w j l --→ T π -1 (π i (S j l )). Therefore, we only need to prove that there exists R j l s.t. π i-1 (R j l ) = π -1 (π i (S j l )) for every 1 ≤ l ≤ m and (p j l , θ j l ) i-1 w j l --→ T R j l exists in the current automaton during the (i -1)-th iteration of loop 1 . If the derivation of (p j l , θ j l ) i-1 w j l --→ T π -1 (π i (S j l )) does not use any transition rule added by the substitution at Line 14, then, (p j l , θ j l ) i-1 w j l --→ T π -1 (π i (S j l )) exists during the saturation procedure at the (i -1)th iteration. Otherwise, there is a transition rule

and is obtained by replacing q i-1 γ ′ -→ T R ′ at line 14 where R = π i-1 (R ′ ). Let us decompose (p j l , θ j l ) i-1 w j l --→ T π -1 (π i (S j l )) as follows:

-

By applying the induction hypothesis on

′′′ is obtained by applying the saturation procedure at the (i -1)th iteration and G ′′ = π i-1 (G ′′′ ). Thus, there must exist R j l s.t. π i-1 (R j l ) = π -1 (π i (S j l )) and the derivation of (p j l , θ j l ) i-1 w j l --→ T R j l uses transition rules added by the substitution at Line 14 less often than the derivation of (p j l , θ j l ) i-1 w j l --→ T S j l .

Similarly, we can apply the same reasoning to (p j l , θ j l ) i-1 w j l --→ T R j l to show that there exists R ′ j l s.t. (p j l , θ j l ) i-1 w j l --→ T R ′ j l holds during the saturation procedure at the (i -1)th iteration. Thus, the statement (a) holds. If a transition rule (p, θ) i γ -→ π i (S) is added by the substitution at line 14 due to the transition t = (p, θ) i γ -→ S, then the statement (a) still holds.

For statement (b). Let us consider the statement (b) where we show that if (p,

n+n ′ } be the k-th transition rule added by either the saturation procedure or the substitution (line 14). Let x be the number of times that t is used in the path (p, θ) i w -→ T S. We proceed by induction on x. In the basic case when x = 0, the property holds by applying the induction hypothesis on k. Let us consider the case where x > 0. Then, there exist u, v ∈ Γ * s.t. w = vγu and there exist the following path in the current automaton:

-q i j u -→ T S j for every j : 1 ≤ j ≤ n.

-q i-1 j u -→ T S j for every j :

By applying the induction hypothesis on k to (p,

). Thus, the statement (b) holds.

✷

Computing the language of a SM-ABPDS

In order to show that there exists a fix-point s.t. the termination condition of loop 1 is true, let Algorithm C be Algorithm 1 without Line 15 i.e. without the termination condition of loop 1 . We show that there exists a fix-point n such that

Lemma 10 Let n ≥ 1 be the first number in Algorithm C s.t. for every p ∈ P, γ ∈ Γ, S ⊆ (P ×

Proof: Since (p, θ) i+1 γ -→ S will be replaced by (p, θ) i+1 γ -→ π i+1 (S) by line 14, then each path (p, θ) i+1 w -→ T {q f } only uses states in the form of P × 2 ∆∪∆c × {i + 1} ∪ {q f }. It is sufficient to prove that for every (p, θ)

Basis. i = n. We can get directly from the condition of n that

Step. i > n. By applying the induction hypothesis (induction on i), then we obtain that for every (p, θ)

Since the result of (1), (p, θ)

Proof:

To prove this lemma, we first show that each configuration c accepted by A i after Line 13 is such that c ∈ P re + L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) , then we show that each configuration c ∈ P re + L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) is accepted by A i after Line 13.

(⇒:) Suppose ( p, w , θ) is a configuration accepted by A i after Line 13, we show that ( p, w , θ)

Since there is no path of the form (p, θ) i ǫ -→ T {q f } after Line 13, then we get that |w| ≥ 1. Then there

There are 2 cases depending on whether t is added by Line 8 or Line 11. Let r be the transition rule used to add t.

-Case t is added by Line 8: then there exists a rule

Thus, we get that ( p, γu , θ) ∈ P re + L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) . The property holds.

-Case t is added by Line 11: then there exists a rule r : p ֒

Thus, we get that ( p, γu , θ) ∈ P re + L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) . The property holds.

(⇐:) Suppose ( p, w , θ) ∈ P re + L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) , we show that ( p, w , θ) is accepted by A i after Line 13. Since P re + L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) = P re * P re L(A i-1 )∩(F ×Γ * ×2 ∆∪∆c ) , we obtain that P re + L(A i-1 )∩ (F × Γ * × 2 ∆∪∆c ) is the limit of the infinite sequence {C i } i≥0 given by C 0 = P re L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) and C j+1 = C j ∪ P re(C j ) for every j ≥ 0 (C j ⊆ C j+1 for j ≥ 0). Thus, we only need to show that for every j ≥ 0, ( p, w , θ) ∈ C j , there exists a path (p, θ) i w -→ T {q f } in A i whose derivation doesn't 98 4.2 Computing the language of a SM-ABPDS use any transition rule in the form of q i ǫ -→ {q i-1 }. We proceed by induction on j.

Basis. j = 0. By applying the saturation procedure (Lines 5-12), A i can accept C 0 if only the out-coming states in the form of (p, θ) i of the added transition rules are regarded as initial states. Moreover, these transition rules are in the form of (p, θ) i γ -→ Q for some Q ⊆ P × 2 ∆∪∆c × {i -1} ∪ {q f }. Thus, for every configuration ( p, w , θ) ∈ C 0 , A i has a path of the form (p, θ) i w -→ T {q f } whose derivation doesn't use any transition rule in the form of q i ǫ -→ {q i-1 }.

Step. j ≥ 1. For every configuration ( p, w , θ) ∈ C j , since C j = C j-1 ∪ P re(C j-1 ), we have ( p, w , θ) ∈ C j-1 or ( p, w , θ) ∈ P re(C j-1 ).

If ( p, w , θ) ∈ C j-1 , the result follows from the induction hypotheses.

If ( p, w , θ) ∈ P re(C j-1 ), there are 2 cases depending on whether it corresponds to a self-modifying rule or not.

-If there exists a transition rule r : p, γ ֒

Applying the saturation rule, we obtain that (p, θ) i γ -→ S Q where

T {q f } whose derivation doesn't use any transition rule in the form of q i ǫ -→ {q i-1 }. The property holds.

-If there exists a transition rule r : p ֒

. By applying the induction hypothesis, we obtain that A i has a path (p 1 , θ

whose derivation doesn't use any transition rule in the form of q i ǫ -→ {q i-1 }. The property holds.

Thus, A i accepts P re + L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) . ✷

Lemma 12

In Algorithm C (Algorithm 1 without Line 15), ∀i ≥ 0, 4.2 Computing the language of a SM-ABPDS Loop 2 : Suppose loop 2 is in the ith iteration of loop 1 . Since only states of the form (p, θ) i ∈ P × 2 ∆∪∆c × {i} can be added into A at the ith iteration, we obtain that Loop 2 only add a finite number of transition rules at the ith iteration. This implies that ∀i ≥ 1, loop 2 always terminates at the i-th iteration.

Loop 1 : Now we consider the termination of Loop 1 . For every i ≥ 1, Line 14 ensures that at the end of the ith iteration, every transition rule in the current automaton is in the form of (p, θ) j γ -→ S for every j ≤ i, S ⊆ (P × 2 ∆∪∆c × {j}) ∪ {q f }. Thus, by the Lemma 9(a), at (i + 1)th iteration with i ≥ 1, either the termination condition at Line 15 is satisfied or the number of transitions is strictly smaller than in the ith iteration. Therefore, Algorithm 1 terminates.

Correctness: Let n > 1 be the fix-point of Algorithm 1 s.t. for every p ∈

If we remove the termination condition of loop 1 i.e. if we consider Algorithm C, by Lemma 10 and Lemma 9(b) and the fact that L(A 0 ) = P × Γ * × 2 ∆∪∆c , we have that for all i ≥ n:

-Let us first show that L(A n ) ⊆ Y BP : Since Y BP = i≥0 X i and X i+1 = P re + X i ∩ (F × Γ * × 2 ∆∪∆c ) , then it is sufficient to prove that L(A i ) ⊆ X i for every i ≥ 0. We proceed by induction on i.

• Basis. i = 0. L(A 0 ) ⊆ X 0 always holds.

•

Step. i > 0. By applying the induction hypothesis (induction on i), we get that L(A i-1 ) ⊆ X i-1 . By the definition of

)), we can have that

By Lemma 11, ∀i ≥ 1, A i accepts P re + L(A i-1 ) ∩ (F × Γ * × 2 ∆∪∆c ) before Line 14 of the algorithm. By Lemma 9(b), Line 14 only removes configurations from A i ( Line 15 can only reduce the language of A i ), we can obtain that:

From ( 2) and (3), we can get that L(A i ) ⊆ X i .

- We applied our tool to detect several malwares. We consider 400 email-worms, 30 worms and 100 viruses from VX heaven [START_REF] Heaven | [END_REF] and 260 new malwares generated by NGVCK. We also choose 19 benign samples from Windows XP system (win32). We consider self-modifying versions of these programs. 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. As previously, first, we abstract away the semantics of the self-modifying instructions and model such programs as standard PDSs as described in [START_REF] Song | Pumoc: a ctl model-checker for sequential programs[END_REF], and perform CTL model-checking for PDSs to determine whether the programs contain any malicious behavior. In this case, none of the programs was declared as malicious. Then, we use SM-PDSs to model these programs, thus, taking self-modifying instructions into consideration. Then, we check whether these SM-PDSs satisfy any malicious CTL formula in our database. If yes, the program is declared as malicious. If not, it is declared as benign. In our experiments (we have 790 malwares), our tool was able to detect all these programs as malicious (whereas when we model these programs using standard PDSs and abstract away self-modifying instructions, none of these programs was detected as malicious). Our tool was also able to determine that benign programs are benign. We report in Tables 4 If the input of SMODIC is a binary program, it is passed to the component Oracle. This component is based on the disassembler Jakstab [START_REF] Veith | Jakstab: A static analysis platform for binaries[END_REF]. It takes as input a binary program, and outputs its corresponding assembly program, its corresponding Control Flow Graph (CFG) equipped with the assembly instruction corresponding to each edge, together with informations about the called API functions, and the different values of the registers and memory addresses at each control point (state). All these outputs are fed to the component Model Builder that will compute the corresponding SM-PDS.

The Reachability component takes as input a SM-PDS, and a sequence of API functions, and applies the reachability algorithms of Chapter 2 to check whether the SM-PDS has a run that calls these API functions in this order. For example, if we consider the sequence f 1 , f 2 , f 3 , then Reachability component checks whether the SM-PDS has a run that calls first f 1 , then f 2 , then f 3 .

The LTL component takes as input a SM-PDS and an LTL formula, and applies the algorithms of Chapter 3 to check whether the SM-PDS satisfies the LTL formula. Similarly, the CTL component takes as input a SM-PDS and a CTL formula, and applies the algorithms of Chapter 4 to check whether the SM-PDS satisfies the CTL formula. and self-modifying code. To start the reachability analysis, we need to specify the options. Let us consider Option1 B, and Option2 R2(or R1). We also need to specify the sequence of API functions. For example, to perform the reachability analysis on the sequence of API functions "Call GetModuleA", "Call CopyFile" , "call SendFile", we put the names of the functions in lowercase and use the symbol ";" to separate the names. To use the post * approach to check whether the above sequence of API functions can be reached or not, we use the following command (see Fig. 5.8):

-./SMODIC B malware/cmd.exe R2 getmodulea;copyfile;sendfile

The result is shown in Fig. 5.9.

We also can run reachability analysis on SM-PDSs. Then, we need to specify the options. We make Option1 M, and Option2 R2(or R1). We also need to specify the target configuration. For example, we can execute reachability analysis using the post * approach to check if configuration p 0 , r 0 can be reached or not by the following command:

-./SMODIC M input.smpds R2 p0:r0

The output of SMODIC is the automaton representing the set of reachable configurations. SMODIC also tells whether the target configuration is reached or not.

LTL and CTL in SMODIC

First, we will introduce the syntax of LTL/CTL used in SMODIC. To be able For LTL:

Description of SMODIC

-Propositional Symbols: true, false and any lowercase string.

-Boolean operators: !(negation), -> (implication), <->(equivalence), && (and), || (or).

-Temporal operators: []p(p always holds), <> p (eventually p holds), pU q ( p holds until q holds), and Xp (p holds next time). For CTL:

SMODIC: A MODEL CHECKER FOR SELF MODIFYING CODE

-Propositional Symbols: tt(true),ff(false) and any lowercase string.

-Boolean operators: !(negation), -> (implication), <->(equivalence), && (and), || (or).

-Path quantifiers: A (for all paths) and E (there exists a path).

-Temporal operators: Xp (p holds next time), pRq (p holds until q does't hold), pU q (p holds until q holds).

Applying SMODIC for Malware Detection

We show how to apply LTL/CTL model checking to malware detection. Let us take a spy worm as example. Such a worm 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 this to the specific server by calling the socket function sendto. This behavior can be specified by the following LTL formula:

To check whether the program cmd.exe satisfies this formula or not, first, we need to rewrite this formula to the form supported by our tool SMODIC. Because all the propositions are lowercase strings, we rewrite API function calls (like call GetAsyncKeyState) by removing the word "call" and changing the name of the 6. CONCLUSION ity sets for SM-PDSs. Our algorithms are based on representing regular sets of configurations of SM-PDSs using finite state automata, and applying saturation procedures on these automata.

LTL Model Checking of Self-modifying Code: In Chapter 3, 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.

CTL Model Checking of Self-modifying Code: In Chapter 4, we consider the CTL model-checking problem for SM-PDSs. This allows to detect CTLlike malicious behaviors on self-modifying code. We reduce this problem to the emptiness checking of Self-modifying Alternating Büchi Pushdown Systems (SM-ABPDS), and we propose an algorithm that computes a finite automaton that characterizes the set of configurations accepted by the SM-ABPDS. SMODIC: A Model Checker for Self-modifying Code: we implemented our techniques in a tool for self-modifying code analysis called SMODIC. We successfully used SMODIC to model-check more than 900 self-modifying binary codes. In particular, we applied SMODIC for malware detection, since malwares usually use self-modifying instructions, and since malicious behaviors can be described by LTL or CTL formulas. In our experiments, SMODIC was able to detect 895 malwares and to prove that 19 benign programs were benign. SMODIC 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. SMODIC can be found in https://lipn.univ-paris13.fr/ ~xin/smodic/index.html.

Future Work

The results presented in this thesis can be extended in several ways :

[49] VirusShare. vxshare. https://virusshare.com.