LTL Model Checking of Self Modifying Code
Tayssir Touili Xin Ye








LTL Model Checking of Self Modifying Code









Lecture Notes in Computer Science: Authors' Instructions




^1CNRS,LIPN and University Paris 13

^2East China Normal University, Shanghai, China











Lecture Notes in Computer Science
Authors' Instructions
LTL Model Checking of Self Modifying Code
    Tayssir Touili^1



Xin Ye^1^2
    December 30, 2023
=========================================





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






§ INTRODUCTION

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


There are several kinds of  self-modifying code. In this work, we consider    self-modifying code  caused by self-modifying instructions.
These kind of instructions treat code as data. This allows them to read and write into code, leading to self-modifying instructions.
 These  self-modifying instructions are usually mov instructions, since mov allows to access memory and read and write into it.


Let us consider the example shown in  <ref>.
For simplicity, the addresses' length   is assumed to be 1 byte.
In the right box, we give,  respectively, the binary code, the addresses of the different instructions, and the  corresponding assembly code, obtained  by translating 
syntactically the binary code at  each address. For example,  0c is the binary code of the jump jmp.
Thus, 0c 02 is translated to jmp  0x2 (jump to address  0x2). The second line is translated to  push 0x9,
since ff is the binary code of the instruction push.
The third instruction mov 0x2 0xc will replace the first byte at address 
0x2 by  0xc. Thus, at address 0x2, ff 09 is replaced by 0c 09.
This means the instruction    push 0x9 is replaced by the jump instruction jmp  0x9 (jump to address  0x9), etc.
Therefore, this code  is self-modifying: the mov instruction was able to modify the instructions of the program 
via its ability to read and write the memory.
If we study this code without  looking at the semantics of the  self-modifying instructions, we will  extract from it the Control Flow Graph CFG a  that is in the left of the figure,
and we will reach the conclusion that the call to the API function  CopyFileA at address 0x9 cannot be made.
However, you can see that the correct CFG is the one on the right hand side  CFG b, where   the call to the API function  CopyFileA at address 0x9 
can be reached. Thus, it is very important to be able to take into account  the semantics of the  self-modifying instructions in binary code.


 	 	
 	
 


In this paper, we consider the LTL model-checking problem of self-modifying code. 
To this aim, we use Self-Modifying Pushdown Systems (SM-PDSs) <cit.> to model self-modifying code.
Indeed, SM-PDSs were shown in <cit.> to be an adequate model for self-modifying code since they allow to mimic  the program's stack  
while taking into account the self-modifying semantics  of the transitions. This is very important for binary code analysis and malware detection, since malwares are based on calls to 
API functions of the operating system. Thus, antiviruses check the API calls to determine whether a program is malicious or not.
Therefore, to evade from these antiviruses, malware writers try to hide the API calls they make by replacing calls by push and jump instructions.
Thus, to be able to analyse such malwares, it is crucial to be able to analyse the program's stack. Hence the need to a model like pushdown systems and self-modifying pushdown systems for this purpose, since they  allow to mimic the program's stack.



Intuitively, a SM-PDS is a pushdown system (PDS) with self-modifying rules, i.e., with rules that allow to modify the current  set of transitions during execution.
This model was introduced in <cit.> in order to represent self-modifying code.  In <cit.>, the authors have proposed algrithms to compute 
finite automata that accept the forward and backward reachability sets of SM-PDSs.
In this work, we  tackle the problem of LTL model-checking of SM-PDSs. Since SM-PDSs are equivalent to PDSs <cit.>, one possible approach for LTL model checking
 of SM-PDS is to translate the SM-PDS to a standard PDS and then run the LTL model checking algorithm on the equivalent PDS   <cit.>. But translation from a SM-PDS to a standard PDS is exponential. Thus, performing 
 	the LTL model checking on the equivalent PDS is not efficient. 



 	 
 	To overcome this limitation, 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-BPDS).
Intuitively, we obtain this SM-BPDS  by taking the  product of the SM-PDS with a Büchi automaton accepting an  LTL formula φ. 
Then, we solve the emptiness problem of an SM-BPDS by computing its repeating heads. This computation is based on computing labelled pre^* configurations by applying a saturation procedure
 on  labelled finite automata. 


 	We implemented our algorithm in a tool. 
 	Our experiments show that our direct techniques are much more efficient than translating the SM-PDS to an equivalent PDS and then applying the standard 
 	LTL model checking for PDSs <cit.>.
 	Moreover, we  successfully applied our tool to the analysis of 892 self-modifying malwares. 
Our tool was also able to detect several self-modifying malwares that well-known antiviruses like BitDefender, Kinsoft, Avira, eScan, Kaspersky, Qihoo-360, Baidu, Avast, and Symantec 
were not able to detect.





	
 	Related Work.
 	Model checking and static analysis approaches have been widely used to analyze binary programs, for instance, 
 	in <cit.>.  Temporal Logics were  chosen to describe malicious   behaviors in <cit.>. 
 However, these works cannot deal with self-modifying code.


POMMADE <cit.> is a malware detector based on LTL and CTL model-checking of PDSs. STAMAD <cit.> is   a malware detector based on PDSs and machine learning.
However, POMMADE and STAMAD cannot deal with self-modifying code. 
 	
 	 Cai et al. <cit.> use  local reasoning and separation logic to describe  self-modifying  code 
 	 and   treat  program code uniformly as regular data structure.   However, <cit.>  requires programs to be manually annotated with invariants. 
 	In <cit.>, the authors  propose  a formal semantics for  self-modifying codes, and   use that to represent self-unpacking code. This work only deals with packing  and unpacking  behaviours.
 	Bonfante  et al. <cit.> provide an operational semantics for self-modifying programs and  show that they  can be constructively
 	rewritten to a non-modifying program. 
 	However, all these specifications <cit.> are  too abstract  to be used in practice. 
 	
In <cit.>, 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.

 	<cit.> 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.
 	<cit.> combine static and dynamic analysis techniques to analyse self-modifying programs.
 	Unlike our approach, these techniques <cit.> cannot handle the program's stack. 
 	
 	Unpacking binary code is also considered in <cit.>. These works do not consider self-modifying 
 	mov instructions. 
 




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


 	
 	
 	
 	
 	
 	
 	
 	
 	
  	
 	
   

§ SELF MODIFYING  PUSHDOWN SYSTEMS 

 
   

 §.§ Definition

We recall in this section the definition of Self-modifying Pushdown Systems <cit.>.
 
A  Self-modifying Pushdown System (SM-PDS) is a tuple 𝒫=(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 ×Δ×Δ× 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 𝒞 be the set of configurations of a SM-PDS.
A SM-PDS defines a transition relation ⇒_𝒫 between configurations as follows: Let c=(⟨ p,w⟩,θ) be a configuration,
and let r be a rule in θ,  then:



	
  * if r∈Δ_c is of the form r= p (r_1,r_2) p', such that r_1 ∈θ, then 
	(⟨ p, w ⟩, θ) ⇒_𝒫 (⟨ 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.
	
	
  * if r∈Δ is of the form r=⟨ p,γ⟩↪⟨ p',w'⟩∈Δ, then 
	(⟨ p, γ w ⟩, θ) ⇒_𝒫 (⟨ 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  ⇒_𝒫^* be the transitive, reflexive closure of ⇒_𝒫 and 
  ⇒_𝒫^+ be its  transitive  closure.
 An execution (a run)  of 𝒫 is a sequence of configurations π=c_0c_1...  s.t.  
c_i ⇒_𝒫 c_i+1 for every i≥ 0.
Given a configuration c, the set of immediate predecessors (resp. successors)
of c is pre_𝒫(c)={c'∈𝒞  :   c' ⇒_𝒫 c}
(resp. post_𝒫(c)={c'∈𝒞  :   c ⇒_𝒫 c'}). These notations
can be generalized straightforwardly to sets of configurations.
Let pre_𝒫^* (resp. post_𝒫^*) denote the reflexive-transitive closure of pre_𝒫 (resp.
post_𝒫). We remove the subscript 𝒫 when it is clear from the context.


We suppose w.l.o.g. that rules in Δ are of the form ⟨ p,γ⟩↪⟨ p',w ⟩ such that 
|w|≤ 2, and that the self-modifying rules r=p (r_1,r_2) p' in Δ_c are such that r≠ r_1. 
Note that this is not a restriction, since for a given SM-PDS, one can compute an equivalent SM-PDS that satisfies these conditions <cit.> .





 §.§ SM-PDS vs. PDS



Let 𝒫=(P,Γ,Δ,Δ_c) be a SM-PDS. 
It was shown in <cit.> that:




  * 𝒫 can be described by an equivalent pushdown system (PDS). Indeed, since the number of phases is finite, we can encode phases
in the control point of the  PDS.  However, this translation is not efficient since the  number of control points of the equivalent PDS is    
|P|· 2^𝒪(|Δ| +|Δ_c|).



  * 𝒫 can also be described by an equivalent Symbolic pushdown system <cit.>, where each SM-PDS rule is represented by a single, symbolic
transition, where the different values of the phases are encoded in a symbolic way using relations between phases. 
This translation is not efficient neither since the  size   of the relations used in the symbolic transitions is
	2^𝒪(|Δ|+|Δ_c|).








 §.§ From Self-modifying Code to SM-PDS 



It is shown in <cit.>  how to describe a self-modifying binary code using a SM-PDS.
The basic idea is that  the control locations of the SM-PDS store the control points of the binary program and
the stack  mimics the program's stack.  Our translation relies on the  disassembler Jakstab <cit.>
to disassemble binary code, construct the control flow graph (CFG), determine indirect jumps,
compute the possible values of used variables,  registers and the memory locations at each control point of program. After getting the control flow graph whose edges are equipped with disassembled instructions, we translate the CFG into a SM-PDS as described in <cit.>. 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 <cit.> that models non self-modifying instructions  of the program by a PDS.
Self-modifying instructions are represented using self-modifying transitions  Δ_c of the  SM-PDS.  
For more details, we refer the reader to  <cit.>.

 

§  LTL MODEL-CHECKING OF SM-PDSS





 §.§ The linear-time temporal logic LTL



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

    φ:= A | φ | φ_1 ∨φ_2 | X φ | φ_1 U φ_2


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




 
ω A  A ∈ω^0

ωφω⊭φ

ωφ_1   ∨φ_2 ωφ_1  or ωφ_2

ω X φω_1 φ

ωφ_1 U φ_2 ∃ i ≥0, ω_i φ_2  and ∀ 0 ≤ j < i, ω_j φ_1




 The  temporal operators  G (globally) and F (eventually) are defined as follows: F φ= (A ∨ A) U φ and G φ = F φ. 
Let  W(φ) be  the set of infinite words that satisfy  an LTL formula   φ.
It is well known that  W(φ) can be accepted by Büchi automata:



	A Büchi automaton ℬ 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 ℬ on a 
word γ_0γ_1... ∈Γ^ω is a sequence of states  q_0q_1q_2...  s.t. ∀ i≥ 0, (q_i,γ_i,q_i+1)∈η. An infinite word ω  is accepted by ℬ  if ℬ has a run on 
ω that starts at q_0 and visits accepting states from F infinitely often. 



<cit.>
Given an LTL formula φ, one can effectively construct a Büchi automaton ℬ_φ which accepts  W(φ).

	






 §.§ Self Modifying Büchi Pushdown Systems
 

 		A Self Modifying Büchi Pushdown Systems (SM-BPDS) is a tuple ℬ𝒫=(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 ⇒_ℬ𝒫 be the  transition relation between configurations as follows: Let θ⊆Δ∪Δ_c,γ∈Γ, w∈Γ^*, and p∈ P, then


	
  * If r: ⟨ p,γ⟩↪⟨ p',w' ⟩∈Δ and r∈θ, then (⟨ p,γ w ⟩, θ) ⇒_ℬ𝒫 (⟨ p',w' w ⟩,θ).
	
  * If r: p(σ,σ') p' ∈Δ_c,  σ∩θ≠∅ and r∈θ, then (⟨ p,γ w ⟩, θ)⇒_ℬ𝒫 (⟨ p',γ w ⟩, θ') where θ'=θ\σ∪σ'.


 A run π  of ℬ𝒫 is a sequence of configurations π=c_0c_1...  s.t.  
c_i ⇒_ℬ𝒫 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 ℬ𝒫. The relation ⇒_ℬ𝒫^r  is defined as follows: c ⇒_ℬ𝒫^r c' iff there exists a configuration (⟨ g, u⟩,θ), g∈ G s.t. 
c⇒_ℬ𝒫^* (⟨ g, u⟩,θ) ⇒_ℬ𝒫^+ c'. We remove the subscript ℬ𝒫 when it is clear from the context. We define i⇒ as follows: c i⇒ c' iff there exists  a sequence of configurations c_0⇒_ℬ𝒫 c_1 ⇒_ℬ𝒫...⇒_ℬ𝒫 c_i s.t. c_0=c and c_i=c'.


 	A head of SM-BPDS is a tuple (⟨ p, γ⟩,θ) where p∈ P, γ∈Γ and θ⊆Δ∪Δ_c. A head (( p,γ ),θ) is repeating if there exists v ∈Γ^* such that (⟨ p,γ⟩, θ) ⇒_ℬ𝒫^r (⟨ p,γ v ⟩,θ).
 The set of repeating heads of SM-BPDS is called  Rep_ℬ𝒫.
 	 

  We assume w.l.o.g. that for every rule in Δ_c of the form r:p(σ,σ') p', r ∉σ.


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

Let 𝒫=(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 𝒫. Let φ be an LTL formula over the set of atomic propositions At. We say that 

    π_νφν(p_0) ν(p_1)⋯φ



Let (⟨ p, w ⟩, θ) be a configuration of 𝒫. We say that (⟨ p, w ⟩, θ) _νφ iff 𝒫
has a path π starting at (⟨ p, w ⟩, θ) such that π_νφ.



Our goal in this paper is to perform LTL model-checking for self-modifying pushdown systems.
Since SM-PDSs can be translated to standard (symbolic) pushdown systems, one way to solve this LTL model-checking problem is to compute the (symbolic) pushdown system
that is  equivalent to the SM-PDS (see section <ref>), and then apply the standard LTL model-checking  algorithms on standard PDSs  <cit.>.
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   ℬ_φ =(Q,2^At, η, q_0,F)  be a Büchi automaton that accepts W(φ).
We compute the SM-BPDS ℬ𝒫_φ=(P × Q, Γ, Δ',Δ_c', G)  by performing a kind of product between the SM-PDS 𝒫 and 
the Büchi automaton ℬ_φ as follows:



  * 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 ⟩.

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

  * G=P× F.
 

We can show that:

Let  (⟨ p,w⟩,θ) be a configuration of the SM-PDS 𝒫.
(⟨ p,w⟩,θ) _νφ iff ℬ𝒫_φ has an accepting run from (⟨(p,q_0),w⟩,   prod(θ)) where prod(θ) is the set of rules of Δ∪Δ_c obtained from the rules of θ as described  above.
	 	


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



  



§ THE EMPTINESS PROBLEM OF SM-BPDSS
 

From now on, we fix a SM-BPDS ℬ𝒫=(P,Γ, Δ,Δ_c,G). 
We can show that  ℬ𝒫 has an accepting run starting from a configuration c if and only if from c, it can reach a configuration with a
repeating head:

  	 	
 	
 	
A  SM-BPDS ℬ𝒫 has an accepting run starting from a configuration c if and only if there exists a repeating head (( p,γ ), θ) such that c ⇒_ℬ𝒫^* (⟨ p,γ w ⟩, θ) for some w ∈Γ^*. 
 	

 		“⇒": Let σ=c_0c_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
 
 		Because  ℬ𝒫 has only finitely many different heads, there must be a head (⟨ p,γ⟩,θ) which  occurs infinitely often as a head in the sequence c_i_0c_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,γ v w⟩,θ)=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,γ v w ⟩,θ) ⇒^*(⟨ g,u v w ⟩,θ') ⇒^+(⟨ p,γ v v w ⟩,θ) ⇒^* ...

 		Since g occurs infinitely often, the run is accepting.
 	


Thus, since there exists an efficient algorithm to compute the pre^* of SM-PDSs <cit.>,
the emptiness problem of a SM-BPDS can be reduced to computing  its repeating heads.


 


 §.§ The Head Reachability Graph 𝒢


Our goal is to compute the set of repeating heads  Rep_ℬ𝒫, 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 𝒢 whose  nodes are the heads of ℬ𝒫 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,γ),θ)  ((p',γ' ),θ')  is an edge of the graph 𝒢 
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 𝒢 contains a loop from a head ((p,γ),θ) to itself such that this loop goes through an edge labelled by 1,
then ((p,γ),θ) is a  repeating head. Thus, computing  Rep_ℬ𝒫 can be reduced to computing the graph 𝒢 and finding 
1-labelled loops in this graph. 


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









The  head reachability graph 𝒢 is a tuple (P ×Γ× 2^Δ∪Δ_c,{0,1}, δ) such that 
((p,γ),θ)  ((p',γ'),θ') is an  edge of δ iff:



  * there exists a transition r_c: p  (σ,σ') p' ∈θ∩Δ_c,  γ=γ', θ'=θ∖σ∪σ', and 
b=1 iff p ∈ G; 


  * there exists a transition ⟨ p,γ⟩↪⟨ p',γ'⟩∈θ∩Δ,θ=θ' and b=1 iff p∈ G;


  * there exists a transition ⟨ p, γ⟩↪⟨ p”, γ_1 γ'  ⟩∈θ∩Δ, for γ_1∈Γ, p”∈ P, 
s.t. (⟨ p”,γ_1 ⟩,θ) ⇒_ℬ𝒫^* (⟨ p',ϵ⟩ ,θ'), and b=1 iff p ∈ G or 
(⟨ p”,γ_1 ⟩,θ) ⇒_ℬ𝒫^r (⟨ p',ϵ⟩ ,θ')

		Let 𝒢 be the head reachability graph. We define  as follows: let ((p,γ),θ) and ((p',γ'),θ') be two heads of ℬ𝒫. We write ((p,γ),θ)((p',γ'),θ') iff ∃ booleans b_1,b_2...b_i ∈{ 0,1}, ∃ heads ((p_j,γ_j),θ_j), 0≤ j≤ i s.t.  𝒢 contains the following path ((p_0,γ_0),θ_0) ((p_1,γ_1),θ_1) ...((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 , and let →^r be defined as follows: Given two heads
 ((p,γ),θ) and  ((p',γ'),θ'),
((p,γ),θ) →^r ((p',γ'),θ')  iff there is in 𝒢 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)  ((p_2,γ_2),θ_2) →^* ((p',γ'),θ').


We can show that:

		
		
 		Let ℬ𝒫=(P,Γ,Δ,Δ_c,G)  be  a self-modifying Büchi pushdown system, and let 𝒢 be its corresponding head reachability graph. A head (( p,γ),θ) of ℬ𝒫 is repeating iff 𝒢 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:
 	
 	
 		The relations →^* and →^r have the following properties: For any heads ((p,γ),θ_1) and ((p',γ'),θ_2):
 		
 			
  (a) ((p,γ),θ_1) →^* ((p',γ'),θ_2) iff (⟨ p,γ⟩,θ_1) ⇒^* (⟨ p',γ' v⟩,θ_2) for some v∈Γ^*.
 			
  (b) ((p,γ),θ_1) →^r ((p',γ'),θ_2)  iff (⟨ p,γ⟩,θ_1) ⇒^r (⟨ p',γ' v⟩,θ_2) for some v∈Γ^*. 
 		
 	
 	
 	“⇒": Assume ((p,γ),θ_1)  ((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) ((p_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) ((p_1,γ”),θ') ((p',γ'),θ_2). Then if ((p,γ),θ_1) →^r ((p',γ'),θ_2), either ((p_1,γ”),θ') →^r((p',γ'),θ_2)  or ((p,γ),θ_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) ((p_1,γ”),θ') according to Definition <ref>.
 			 
 			 
 			 	 			 	
  - If this edge corresponds to a transition r_c:p  (σ,σ') p_1∈θ_1, then  γ=γ”,θ' =θ_1 \σ∪σ' and p∈ G. Since we can obtain  (⟨ p,γ⟩ ,θ_1) ⇒_ℬ𝒫 (⟨ p_1,γ⟩ ,θ') ⇒^* (⟨ p',γ' uw ⟩,θ_2) from part (a) and p∈ G, then (⟨ p,γ⟩ ,θ_1) ⇒^r (⟨ p_1,γ⟩ ,θ') ⇒^* (⟨ p',γ' uw ⟩,θ_2). This implies that (⟨ p,γ⟩ ,θ_1) ⇒^r  (⟨ p',γ' v ⟩,θ_2) for some v∈Γ^*.
 	
 	
  - If this edge corresponds to a transition r:⟨ p,γ⟩↪⟨ p_1,γ”⟩∈θ_1 ∩Δ, then θ'=θ_1 and p∈ G.  Since we can obtain  (⟨ p,γ⟩ ,θ_1) ⇒_ℬ𝒫 (⟨ p_1,γ”⟩,θ_1) ⇒^* (⟨ p',γ' uw ⟩,θ_2) from part (a) and p∈ G,  then (⟨ p,γ⟩ ,θ_1) ⇒^r (⟨ p_1,γ”⟩,θ_1) ⇒^* (⟨ p',γ' uw ⟩,θ_2). This implies that   (⟨ p,γ⟩ ,θ_1) ⇒^r (⟨ p',γ' v ⟩,θ_2) for some v∈Γ^*.


  -  If this edge corresponds to a transition r:⟨ p,γ⟩↪⟨ p”, γ_1 γ”⟩∈θ_1, then either p∈ G or (⟨ p”,γ_1 ⟩,θ_1) ⇒^r (⟨ p_1,ϵ⟩,θ') holds. If p∈ G, then we have (⟨ p,γ⟩ ,θ_1) ⇒^r ( ⟨ p”,γ_1 γ”⟩, θ_1). Otherwise, ( ⟨ p”,v_1 γ” w ⟩, θ_1) ⇒^r (⟨ p_1, γ” w⟩, θ').  Since we can obtain (⟨ p_1,γ”⟩,θ') ⇒^* (⟨ p',γ' u⟩,θ_2) from part (a). Therefore,  (⟨ p,γ⟩ ,θ_1) ⇒^r( ⟨ p_1,γ”⟩, θ') ⇒^* (⟨ p',γ' u  ⟩,θ_2). This implies that  (⟨ p,γ⟩ ,θ_1) ⇒^r(⟨ p',γ' v  ⟩,θ_2) for some v∈Γ^*.

 			 

 		
 		
 		 `⇐": Assume (⟨ p,γ⟩,θ_1) i⇒ (⟨ p',γ'v⟩,θ_2). We proceed by induction on i. 
 	
 		
 			
  (a) Basis. i=0. 
 	In this case, v=ϵ and (⟨ p,γ⟩ ,θ_1)=(⟨ p',γ'⟩,θ_2), then ((p,γ),θ_1) →^*((p',γ'),θ_2) holds.
   Step. i>0. Then there exist p_1∈ P,u∈Γ^* and θ'⊆Δ∪Δ_c such that (⟨ p,γ⟩,θ_1) 1⇒ (⟨ p_1,u⟩,θ')i-1⇒ (⟨ p',γ' v⟩,θ_2). There are 2 cases:
 	
 	
 	 
  1. Case θ'=θ_1: There must exist a rule r: ⟨ p,γ⟩↪⟨  p_1,u⟩∈Δ such that r∈θ' and  |u|≥ 1. Let l denote the minimal length of the stack on the path from (⟨ p_1,u ⟩, θ_1) to (⟨ p',γ' v⟩,θ_2). Then u can be written as u”γ_1 u' where |u'|=l-1 (that means u' will remain on the stack for the path). Furthermore, there exists p”' such that (⟨ p_1,u”⟩,θ_1) ⇒^*(⟨ p”',ϵ⟩,θ”) for some θ”⊆ (Δ_c ∪Δ).  We have (⟨ p,γ⟩,θ_1)k⇒(⟨ p”',γ_1 u' ⟩,θ”) for k<i. By the induction on i, we have ((p,γ),θ_1) →^* ((p”',γ_1),θ”). Because u' has to remain on the stack for the rest of the path, v is of the form v'u' for some v'∈Γ^*. That means (⟨ p”',γ_1⟩, θ”)j⇒ (⟨  p',γ' v'⟩, θ_2) for j<i. By the induction hypothesis, ((p”',γ_1),θ”)→^* ((p',γ'),θ_2) holds. Moreover, we have ((p,γ),θ_1) →^* ((p”',γ_1),θ”), hence ((p,γ),θ_1) →^*((p',γ'),θ_2).
 	 
  2. Case θ'≠θ_1: There must be a rule r_c: p  (σ,σ')  p_1∈Δ_c such that r_c ∈θ_1 and σ∩θ_1 ≠∅, then θ'= θ_1 ∖σ∪σ'.  After the execution of r_c, the content of the stack will remain the same, thus, u=γ. Then  (⟨ p,γ⟩,θ_1) 1⇒ (⟨ p_1,γ⟩,θ')i-1⇒ (⟨ p',γ' v⟩,θ_2). By the induction hypothesis to (⟨ p_1,γ⟩,θ')i-1⇒ (⟨ p',γ' v⟩,θ_2), we can obtain that ((p_1,γ),θ')→^* ((p',γ'),θ_2). Since (⟨ p,γ⟩,θ_1) 1⇒ (⟨ p_1,γ⟩,θ'), then we can have a path (( p,γ),θ_1) → (( p_1,γ),θ')→^*((p',γ'),θ_2) that implies (( p,γ),θ_1) →^*((p',γ'),θ_2). The property holds.  	
 	
 			  
  (b) (⟨ p,γ⟩,θ_1) ⇒^r (⟨ p,γ' v⟩,θ_1) is impossible in 0 steps.
 	
 	Basis. i=1. (⟨ p,γ⟩,θ_1) ⇒^r (⟨ p,γ⟩,θ_1), then p∈ G. Thus, ((p,γ),θ_1) →^r ((p,γ),θ_1) holds.
 
       Step. i>1.  (⟨ p,γ⟩,θ_1) ⇒^r (⟨ p',γ' v⟩,θ_2) holds,   then there exist p_1∈ P,u∈Γ^* and θ'⊆Δ∪Δ_c such that (⟨ p,γ⟩,θ_1) 1⇒ (⟨ p_1,u⟩,θ')i-1⇒ (⟨ p',γ' v⟩,θ_2). Thus, either (⟨ p,γ⟩,θ_1) ⇒^r (⟨ p_1,u⟩,θ') or (⟨ p_1,u⟩,θ') ⇒^r (⟨ p',γ'v ⟩,θ_2) holds. 
 	The first case implies p∈ G. There are 2 cases:
 	 
 	 	
  1. Case θ'=θ_1: then as in the previous proof of part (a), we can have a path ((p,γ),θ_1) →^* ((p”',γ_1),θ”) →^* ((p',γ'),θ_2).   Since  p∈ G, we get  by Definition <ref> ((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)  (( 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”γ_1u' and (⟨ p_1,u”⟩,θ_1)⇒^r (⟨ p”',ϵ⟩,θ”), then, we have  ((p,γ),θ_1) →^r ((p”',γ_1),θ”). We have (⟨ p,γ⟩,θ_1)k⇒(⟨ p”',γ_1 u' ⟩,θ”) for k<i. By the induction on i, we have ((p,γ),θ_1) →^* ((p”',γ_1),θ”). Because u' has to remain on the stack for the rest of the path, v is of the form v'u' for some v'∈Γ^*. That means (⟨ p”',γ_1⟩, θ”)j⇒ (⟨  p',γ' v'⟩, θ_2) for j<i. By the induction hypothesis, ((p”',γ_1),θ”)→^* ((p',γ'),θ_2) holds. Moreover, we have ((p,γ),θ_1) →^* ((p”',γ_1),θ”), hence ((p,γ),θ_1) →^*((p',γ'),θ_2). So we can have a path ((p,γ),θ_1)→^*  ((p”',γ_1),θ”)→^*((p',γ'),θ_2), thus we have that ((p,γ),θ_1)→^r ((p',γ'),θ_2);
 	   				
  -If (⟨ p”',γ_1  ⟩,θ”) ⇒^r (⟨ p',γ' v'⟩,θ_2), then by the induction hypothesis we have ((p”',γ_1),θ”)→^r ((p',γ'),θ_2). Thus, we can have a path ((p,γ),θ_1)→^*  ((p”',γ_1),θ”)→^*((p',γ'),θ_2), then we have that ((p,γ),θ_1)→^r ((p',γ'),θ_2);
 	   			
 	   			
  2. Case θ'≠θ_1: then  (⟨ p_1,γ⟩,θ') ⇒^r (⟨ p',γ' v⟩,θ_2). By the induction hypothesis we have ((p
 	   			_1,γ),θ')→^r ((p',γ'),θ_2). Since (⟨ p,γ⟩,θ_1) 1⇒ (⟨ p_1,γ⟩,θ')i-1⇒ (⟨ p',γ' v⟩,θ_2). 
 	   			
 	   			By the induction hypothesis to (⟨ p_1,γ⟩,θ')i-1⇒ (⟨ p',γ' v⟩,θ_2), we can obtain that ((p_1,γ),θ')→^* ((p',γ'),θ_2). Since (⟨ p,γ⟩,θ_1) 1⇒ (⟨ p_1,γ⟩,θ'), then we can have a path (( p,γ),θ_1) → (( p_1,γ),θ')→^*((p',γ'),θ_2). Thus, we have that ((p,γ),θ_1)→^r ((p',γ'),θ_2);
 	   			
 	   		
  			 Thus,   the property holds.
 		
 		
 	
Proof of Theorem <ref>
 	
 	We can now prove Theorem <ref>. 
 	
 	
 	Let (( p,γ),θ) be a repeating head, then there exists some v∈Γ^*, θ⊆Δ_c ∪Δ such that (⟨ p,γ⟩, θ) ⇒^r (⟨ p,γ v⟩,θ).  By Lemma <ref>, 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),θ')  ((p_2,γ_2),θ”) →^* ((p,γ),θ). Then ((p,γ),θ), ((p_1,γ_1),θ') and ((p_2,γ_2),θ”) are all in  the same loop with a 1-labelled edge. Conversely, whenever ((p,γ),θ) is in a component with such an edge, ((p,γ),θ)→^r ((p,γ),θ) holds, then   Lemma <ref> implies that (⟨ p,γ⟩, θ) ⇒^r (⟨ p,γ v⟩,θ) which means that (( p,γ),θ) is a repeating head.
	
 






 §.§ Labelled configurations and labelled ℬ𝒫-automata



To compute  𝒢, we need to be able to compute  predecessors of configurations of the form (⟨ p',ϵ⟩ ,θ'), and to 
determine whether these predecessors were backward-reachable using some control points in G (item 3 in Definition <ref>). 
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 <cit.> 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   ℬ𝒫-automata as follows:






 
 
 	 Let ℬ𝒫=(P,Γ,Δ,Δ_c, G) be a SM-BPDS. A labelled  ℬ𝒫-automaton is a tuple  
𝒜=(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   q[γ_0,b_0]_T q_0[γ_1,b_1]_T q_1⋯ q_n[γ_n+1,b_n+1]_T q'. 
   If q_T q' holds, we say that q_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 labelled configuration [(⟨ p, w ⟩, θ),b] is  accepted by the automaton 𝒜 iff there exists  a path
(p,θ)[γ_0,b_0]_T q_1[γ_1,b_1]_T q_2⋯ q_n[γ_n,b_n]_T q_n+1 in 𝒜  such that 
w=γ_0γ_1⋯γ_n, b=b_0 ∨ b_1∨...∨ b_n, (p,θ)∈ I, and q_n+1∈ F. 
Let L(𝒜) be the set of labelled configurations accepted by 𝒜.






 §.§ Computing pre^*((⟨ p',ϵ⟩ ,θ'))



Given a  configuration  
of the form   (⟨ p',ϵ⟩ ,θ'),

 
our goal is to compute a labelled ℬ𝒫-automaton 
𝒜_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.
𝒜_pre^*((⟨ p',ϵ⟩ ,θ'))=(Q,Γ,T, I, F) is computed as follows: 
Initially, Q=I=F={(p',θ')} and  T=∅. 
We add to T transitions as follows:



  α_1: If r=⟨ p,γ⟩↪⟨ p_1,w ⟩∈Δ.
If  there exists    in T a path   (p_1,θ)[w,b]_Tq   (in case |w|=0,
we have w=ϵ) with r∈θ. Then, add  (p,θ) to I, and ((p,θ),[γ, B(p)∨ b],q ) to T.


  α_2:  if  r=p (σ,σ') p_1 ∈Δ_c and there exists   in T a transition   (p_1,θ)  [γ,b]_Tq 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 𝒜_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 𝒜_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 𝒜_pre^*((⟨ p',ϵ⟩,θ'))
contains a path of the form π =(p_1,θ)_T q_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]_Tq[w',b_2]_Tq_f added by rule (α_1). 







Rule (α_2) deals with modifying rules: Let  r=p(r_1,r_2) p_1 ∈Δ_c.  Let c=(⟨ p_1,γ w'⟩,θ) and c'=(⟨ p,γ w'⟩,θ”) s.t. θ=θ”\{ r_1}∪{r_2}. Then, if c⇒^* (⟨ p',ϵ⟩,θ'), then necessarily, c'⇒^* (⟨ p',ϵ⟩, θ'). Moreover, c'⇒^r (⟨ p',ϵ⟩,θ') iff either c⇒^r (⟨ p',ϵ⟩,θ') or p∈ G (i.e. B(p)=1). Thus, we need to impose that if the automaton 𝒜_pre^*((⟨ p',ϵ⟩,θ')) contains a path of the form (p_1,θ) _T q _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 𝒜_pre^*( (⟨ p',ϵ⟩, θ') ) should also accept the labelled configuration [c',b∨ B(p)]. This configuration is accepted by the run (p,θ”)_T q _T q_f added by rule (α_2).



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

	Let 𝒜_pre^*( (⟨ p',ϵ⟩,θ'))=(Q,Γ,T,P,F) be the labelled 𝒫-automaton computed by the saturation procedure above. In this section, we use _T to denote the transition relation of 𝒜_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,θ)_Tq for a state q that is already in the automaton at step i-1, then, states of 𝒜_pre^*( (⟨ p',ϵ⟩,θ')) are all of the form (p,θ) for p∈ P and θ⊆Δ∪Δ_c.


We can  show that:


Let p,p”∈ P and θ,θ”⊆Δ∪Δ_c. Let w∈Γ^* and b∈{0,1}.   If a path (p,θ)[w,b]_T(p”,θ”) is in 𝒜_pre^*((⟨ p',ϵ⟩ ,θ')),   then (⟨ p,w ⟩, θ) ⇒^* (⟨ p”, ϵ⟩,θ”). Moreover, if b=1, then  (⟨ p,w ⟩,θ) ⇒^r (⟨ p”,ϵ⟩,θ”).  
	
	

 
	 Initially, the automaton contains no transitions.  
Let i be an index such that (p,θ)[i][w,b]_T(p”,θ”) holds.  We proceed  by induction on i. 
	

 Basis. i=0,   then (p”,θ”)[0][ϵ,0]_T (p”,θ”). This means p”=p', θ”=θ'. Since initially Q={(p',θ')}, then (⟨ p”,ϵ⟩,θ”)⇒^* (⟨ p”,ϵ⟩,θ”) always holds.
	
	 Step. i>0. Let t=((p_1,θ_1), [γ,b_1], (p_0,θ_0)) be the i-th transition added to 𝒜_pre^* and j be the number of times that t is used in the path   (p,θ)[i][w,b]_T(p”,θ”). The proof is by induction on j. If j=0, then we have  (p,θ)[i-1][w,b]_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 

	
    1
    (p,θ) [i-1][u,b']_T (p_1,θ_1) [i][γ,b_1]_T(p_0,θ_0) [i][v,b”]_T(p”,θ”)


The application of the induction hypothesis (induction on i) to (p,θ) [i-1][u,b']_T (p_1,θ_1) gives that 

    2
    (⟨ p,u⟩,θ) ⇒^* (⟨ p_1, ϵ⟩,θ_1),  moreover, if b'=1,(⟨ p,u⟩,θ) ⇒^r (⟨ p_1, ϵ⟩,θ_1)

There are 2 cases depending on whether transition t was added by saturation rule α_1 or α_2.



	
  * Case t was added  by rule α_1: There exist p_2∈ P and w_2∈Γ^* such that
	
    3
    	r=⟨ p_1,γ⟩↪⟨ p_2, w_2 ⟩∈Δ∩θ_1
 
	and 𝒜_pre^* contains the following path:
	
    4π'=(p_2,θ_1)[i-1][w_2,b_2]_T(p_0,θ_0)[i][v,b”]_T(p”,θ”),   b_1=b_2 ∨ B(p_1)

	
		
	
	Applying the transition rule r, we get that
	
    5
    		(⟨ p_1, γ v⟩,θ_1) ⇒ (⟨ p_2, w_2 v⟩,θ_1)

	
	By induction on j (since transition t is used j-1 times in π'), we get from (4) that 
	
    6
    		(⟨ p_2,w_2 v⟩,θ_1) ⇒^* (⟨ p”,ϵ⟩,θ”) moreover, if  b_2∨ b”=1,(⟨ p_2,w_2 v⟩,θ_1) ⇒^r 	(⟨ p”,ϵ⟩,θ”)

	
	
	
	Putting (2), (5) and (6) together, we can obtain that 
	
	
    (⟨ p,w⟩,θ)=(⟨ p, u γ v⟩,θ) ⇒^* (⟨ p_1, γ v⟩,θ_1) ⇒ (⟨ p_2, w_2 v⟩,θ_1)⇒^* 	(⟨ p”,ϵ⟩,θ”)

  	Furthermore, 
			if b=b' ∨ b_1 ∨ b”=1, then b'=1 or b_1∨ b”=1.
		
		For the first case, b'=1, then we can have (⟨ p,u ⟩,θ) ⇒^r (⟨ p_1,ϵ⟩,θ_1) from (2). Thus, we can obtain that (⟨ p,u γ v ⟩,θ) ⇒^r (⟨ p_1,γ v ⟩,θ_1) ⇒^*(⟨ p”,ϵ⟩,θ”) i.e. (⟨ p,w⟩, θ)⇒^r (⟨ p”,ϵ⟩,θ”).
		
					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 (6)). Therefore, (⟨ p,w⟩,θ_1)⇒^r 
			 (⟨ p”,ϵ⟩,θ”).
			
			 	
  * Case t was added by rule α_2: there exist p_2 ∈ P and θ_2⊆Δ∪Δ_c such that

    7
    				r=p_1  (σ,σ') p_2 ∈Δ_c ∩θ_2,θ_2=(θ_1 \σ) ∪σ'

	and the following path in the current automaton ( self-modifying rule won't change the stack) with r∈θ_2:	
	
    8
    	(p_2,θ_2) _T (p_0,θ_0) [i][v,b”]_T(p”,θ”),    b_1=B(p_1) ∨ b_1'

	Applying the transition rule, we can get from (7) that
	
    9
    	(⟨ p_1,γ v⟩, θ_1) ⇒ (⟨ p_2,γ v ⟩, θ_2)

	We can apply the induction hypothesis (on j) to (8), and obtain
	
    10
    	(⟨ p_2,γ v⟩, θ_2) ⇒^* (⟨ p”,ϵ⟩,θ”), moreover, if b_1'∨ b”=1,(⟨ p_2,γ v⟩, θ_2) ⇒^r (⟨ p”,ϵ⟩,θ”)

	
	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.
		
		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”,ϵ⟩,θ”).




 
	
	
	



 
 
	 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 𝒜_pre^*((⟨ p',ϵ⟩ ,θ')).
	 Moreover, if  (⟨ p,w ⟩,θ) ⇒^r (⟨ p',ϵ⟩,θ'), then b=1.  
	


	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 𝒜_pre^*((⟨ p',ϵ⟩,θ') ) a  path  (p”,θ”)[u,b”]_T(p',θ'). If (⟨ p”,u⟩, θ”) ⇒^r (⟨ p', ϵ⟩,θ'), b”=1.

Let (p_0,θ_0)  be a state of 𝒜_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',θ')

There are two cases depending on which rule is applied to get  (⟨ p, w⟩,θ) ⇒ (⟨ p”,u⟩, θ”).
	

	
  * 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”

	  
	 Putting (1) and (2) together, we can obtain that 
	 
    π=(p,θ”) [γ,b_0]_T(p_0,θ_0)  [w_1,b_1”]_T(p',θ')

	 
	 Thus, (p,θ”)[γ w_1,b_0∨ b_1”]_T(p',θ') i.e. (p,θ)[w,b]_T (p',θ') where b=b_0 ∨ b_1”. 
	 

  * 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”.

	 	
	 	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”

	 	
	 	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:



Let  [c,b] be a labelled configuration.
Then  [c,b] is in L(𝒜_pre^*((⟨ p',ϵ⟩ ,θ')) iff  
c∈ pre^*((⟨ p',ϵ⟩ ,θ')). Moreover, 
  c⇒^r(⟨ p',ϵ⟩ ,θ') iff b=1. 



	Let [(⟨ p, w⟩, θ),b] be a configuration of pre^*((⟨ p',ϵ⟩ ,θ'))). Then (⟨ p,w⟩,θ) ⇒^*(⟨ p', ϵ⟩, θ'). By Lemma <ref>, we can obtain that there exists a path (p,θ) _T(p',θ') in 𝒜_pre^*( (⟨ p',ϵ⟩,θ')). So [(⟨ p, w⟩, θ),b] is  in L(𝒜_pre^*((⟨ p',ϵ⟩ ,θ'))). Moreover,  if (⟨ p,w⟩,θ) ⇒^r(⟨ p', ϵ⟩, θ'), then b=1.

Conversely, let [(⟨ p, w ⟩,θ),b] be a configuration accepted by 𝒜_pre^*((⟨ p',ϵ⟩ ,θ')) i.e. there exists a path (p,θ) _T(p',θ')  in 𝒜_pre^*((⟨ p',ϵ⟩ ,θ')). By Lemma <ref>, (⟨ p,w ⟩, θ)⇒^* (⟨ p',ϵ⟩, θ') i.e. (⟨ p,w ⟩, θ) ∈ pre^*(L(A)). Moreover, if b=1, (⟨ p,w⟩,θ) ⇒^r(⟨ p', ϵ⟩, θ').




 

 §.§ Computing the Head Reachability Graph 𝒢
	
  

Based on the definition of the  Head Reachability Graph 𝒢, and on Theorem <ref>, we can compute 𝒢 as follows. 
Initially, 𝒢 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,γ),θ)((p',γ),θ_0) to  the graph 𝒢, where 
θ_0=θ∖σ∪σ'.



  α_2': if r:⟨ p,γ⟩↪⟨ p_0,γ_0 ⟩∈Δ, then for every phase θ such that
r∈θ, we add the edge ((p,γ),θ)((p_0,γ_0),θ) to the graph 𝒢.

 	   	
 	   
  α_3': 
if r: ⟨ p, γ⟩↪⟨ p_0, γ_0γ' ⟩∈Δ, 
then for every phase θ  such that
r∈θ, we add  to  the graph 𝒢 the edge ((p,γ),θ)((p_0,γ_0),θ).
Moreover, for  every control point p'∈ P and phase  θ' such that   
𝒜_pre^*((⟨ p',ϵ⟩ ,θ')) contains  a transition 
of the form t=(p_0,θ)[γ_0,b]_T(p',θ'), 
we add  to  the graph 𝒢 the edge ((p,γ),θ)((p',γ'),θ').

 







Items α_1' and α_2' are obvious.   They respectively correspond to item 1 and item 2 of Definition <ref> (since B(p)=1 iff p∈ G). 
Item α_3' is based on    Lemma  <ref> and on item 3 of  Definition <ref>. Indeed, it follows from     Lemma  <ref> that 
𝒜_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,γ),θ)((p',γ'),θ') is added to 𝒢 (item 3 of Definition <ref>) since ⟨ p,γ⟩↪⟨ p_0,γ_0γ'⟩∈Δ.











§ 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 <cit.>. 
 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 <ref>. 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<cit.>).  	 Column SM-PDS gives  the cost of our direct algorithm presented in this paper. 
Column PDS shows the cost it takes to get the equivalent PDS from the SM-PDS.
	Column Result reports the cost it takes to run the LTL PDS model-checker  Moped <cit.> 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 Total_1 is the total cost it takes to translate the SM-PDS into a symbolic PDS and then apply the standard LTL model checking algorithm of Moped.  
You can see that our direct algorithm (Column SM-PDS) is much more efficient than translating the SM-PDS to an equivalent (symbolic) PDS, and then run
the standard LTL model-checker Moped.
Translating the SM-PDS to a standard PDS may take more than 20 days, whereas our direct algorithm takes only a few seconds.
Moreover, since the obtained standard (symbolic) PDS is huge, Moped failed to handle several  cases (the time limit that we set for Moped is 20 minutes), 
whereas our tool was able to deal with all the cases in only a few seconds.

	 	 
 

	


 §.§ Malicious Behavior Detection on Self-Modifying Code










  §.§.§ Specifying Malicious Behaviors using LTL.
  
As described in <cit.>, several  malicious behaviors can be described  by LTL formulas. We give in what follows three 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:


ϕ_rk=F(call GetModuleFileNameA  ∧F( call RegSetValueExA) )
 	
 	
This formula expresses that if a call to the API function GetModuleFileNameA is followed by a call to the  API function RegSetValueExA, then probably a malware is trying to 
add itself into the registry key listing.


 


Data-Stealing: Stealing data from the host is a popular malicious behavior that intend to steal any valuable information 
including passwords, software codes,  bank information, etc. To do this, the malware needs to scan the disk to find the interesting file that he wants to steal.
After finding the file, the malware needs to locate it. To this aim, the malware first calls the API function GetModuleHandleA to get a base address  
 to search for a location of the file.  Then the malware starts looking for the  interesting file  by calling the API function FindFirstFileA. 
Then the API functions CreateFileMappingA and 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 GetModuleHandleA ∧F (call FindFirstFileA 
∧F  (call CreateFileMappingA 
∧F  
(call MapViewofFile
 	 ∧F call CopyFileA))))
 	
 	 
 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 (=a) ∧G(ret ∧ (=a)))
 

where the ⋁ is taken over all possible return addresses a, and  top-of-stack=a is a predicate that indicates that the 
top of the stack is a.
The subformula  call ∧X (=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.


[!bp]
 		    
 				Example     Size     LTL      Multiple pre^*     Example     Size   LTL     Multiple pre^*    Example     Size     LTL     Multiple pre^* 

 				Tanatos.b   12315   16.261s     46.635s   Netsky.c   45   0.002s     0.092s    Win32.Happy   23   0.042s   0.075s
 			
 					
 				Netsky.a   45   0.047s      0.085s    Mydoom.c    155     0.014s     0.206s   MyDoom-N   16980   30.231s   98.418s 

 	 			Mydoom.y   26902   12.462s     102.559s    Mydoom.j    22355     11.262s     111.617s   klez-N   6281   3.252s   78.419s 

 			
 			  klez.c   30   0.039s     0.088s     Mydoom.v     5965     3.971s     83.988s    Netsky.b   45   0.057s     0.183s 

 			   	
 			   	Repah.b   221   2.428s     8.852s     Gibe.b   5358   4.229s   17.239s    Magistr.b   4670   3.699s     93.818s

 			   	
 			   	Netsky.d   45   0.083s     0.123s      Ardurk.d     1913     0.482s    3.212s    klez.f   27   0.054s     4.518s

 			   	
 			   	Kelino.l   495   0.326s     5.468s    Kipis.t     20378     23.345s    48.689s    klez.d   31   0.085s     0.291s

 			   			
 			   			Kelino.g     470     0.672s     3.446s    Plage.b     395     0.291s    3.138s   Urbe.a   123   0.376s     2.981s 

 			   				
 			   				klez.e   27   0.094s     0.482s    Magistr.b   4670   3.987s     53.235s    Magistr.a.poly   36989   49.863s   159.195s

 			   			 		
 				
 				Adon.1703   37   0.358s    0.884s   Adon.1559   37   0.255s     4.088s    Spam.Tedroo.AB     487     0.924s    4.894s

 				Akez   273    0.136s     1.863s   Alcaul.d   845   0.165s     0.392s    Alaul.c     355     0.109s    5.757s

 				Haharin.A    210   1.462s     4.318s   fsAutoB.F026   245   1.698s     4.503s    Haharin.dr    235     1.558s    4.312s

 				
 				
 				 LdPinch.BX.DLL   2010   6.965s   8.128s   LdPinch.fmye   1845   6.194s    9.232s    LdPinch.Win32.5558   2015   6.907s   8.981s

 				  			  LdPinch-15   580   1.008s   3.957s   LdPinch.e   578   1.185s   3.392s    Win32/Toga!rfn   590   2.023s   3.978s

 				  			  Tanatos.b   12315   16.261s     46.635s   Netsky.c   45   0.002s     0.092s    Win32.Happy   23   0.042s   0.075s
 	 		
 	 			 	
 	 			Netsky.a   45   0.047s      0.085s    Mydoom.c    155     0.014s     0.206s   MyDoom-N   16980   30.231s   98.418s 

 	 			Mydoom.y   26902   12.462s     102.559s    Mydoom.j    22355     11.262s     111.617s   klez-N   6281   3.252s   78.419s 

 	 		
 	 		   klez.c   30   0.039s     0.088s     Mydoom.v     5965     3.971s     83.988s    Netsky.b   45   0.057s     0.183s 

 	 		    	
 	 		    	Repah.b   221   2.428s     8.852s     Gibe.b   5358   4.229s   17.239s    Magistr.b   4670   3.699s     93.818s

 	 		    	
 	 		    	Netsky.d   45   0.083s     0.123s      Ardurk.d     1913     0.482s    3.212s    klez.f   27   0.054s     4.518s

 	 		    	
 	 		    	Kelino.l   495   0.326s     5.468s    Kipis.t     20378     23.345s    48.689s    klez.d   31   0.085s     0.291s

 	 		    			
 	 		    			Kelino.g     470     0.672s     3.446s    Plage.b     395     0.291s    3.138s   Urbe.a   123   0.376s     2.981s 

 	 		    				
 	 		    				klez.e   27   0.094s     0.482s    Magistr.b   4670   3.987s     53.235s    Magistr.a.poly   36989   49.863s   159.195s

 	 		    			   Mydoom-EG[Trj]   230   0.242s     6.172s    Email.W32!c   220   0.249s     5.946s    W32.Mydoom.L   235   0.288s   6.452s

 	 		        	Mydoom.5   228   0.307s     8.163s    Mydoom.cjdz5239   225   0.392s     9.968s    Mydoom.DN.worm   220   0.299s   8.928s

 	 		         	Mydoom.R   230   0.322s     9.086s    Win32.Mydoom   235   0.296s     7.985s    Mydoom.o@MM!zip   235   0.403s   10.323s
	
 	 		         	Mydoom.M@mm   5965   5.633s     108.129s    MyDoom.54464   5935   5.939s     94.026s    MyDoom.N   5970   6.152s   86.468s

 	 		   	Sramota.avf   240   0.383s     2.691s     Mydoom   238   0.278     2.749s    Win32.Mydoom.288   248   0.410s   2.983s

 	 		   	 	Win32.Runouce   51678   92.692s     248.146s    Win32.Chur.A   51895   98.161s     298.047s    Win32.CNHacker   51095   94.952s   245.452s


 	 	 	Win32.Skybag   4180   6.891s     13.739s    Skybag.A   4310   6.205s      15.452s    Netsky.ah@MM   4480   6.991s   16.018s

		
 	 			Adon.1703   37   0.358s    0.884s   Adon.1559   37   0.255s     4.088s    Spam.Tedroo.AB     487     0.924s    4.894s

 	 			Akez   273    0.136s     1.863s   Alcaul.d   845   0.165s     0.392s    Alaul.c     355     0.109s    5.757s

 	 			Haharin.A   210   1.462s     4.318s   fsAutoB.F026   245   1.698s     4.503s    Haharin.dr    235     1.558s    4.312s

 	 			
 	 			LdPinch.BX.DLL   2010   6.965s   8.128s   LdPinch.fmye   1845   6.194s    9.232s    LdPinch..5558   2015   6.907s   8.981s

 	 			   	 		    	LdPinch-15   580   1.008s   3.957s   LdPinch.e   578   1.185s   3.392s    Win32/Toga!rfn   590   2.023s   3.978s

 	 	LdPinch.by     970     4.092s    11.327s    Generic.2026199   433   2.402s   9.614s    LdPinch.arr     1250     1.848s      9.986s 

 	 	 LdPnch-Fam   195   1.440s   4.097s   Troj.LdPinch.er   205   2.529s   6.154s    LdPinch.Gen.3   210   1.482s   4.973s

 	 	 	Androm     95     0.028s    0.192s      Ardurk.d     1913     3.679s    5.588s    Generic.12861   30183   72.264s   224.809s

  Jorik   837   4.159s   11.733s    Bugbear-B   9278   17.737s    52.549s    Tanatos.O   9284   21.481s   79.773s 




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

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.



[!bp]
   
 	 			Example     Size     Result     cost      Example     Size   Result     cost    Example     Size     Result     cost 

 	 			Tanatos.b   12315   Yes     16.261s   Netsky.c   45   Yes     0.002s    Win32.Happy   23   Yes   0.042s
 	 		
 	 			 	
 	 			Netsky.a   45   Yes     0.047s    Mydoom.c    155     Yes     0.014s   MyDoom-N   16980   Yes   30.231s 

 	 			Mydoom.y   26902   Yes     12.462s    Mydoom.j    22355     Yes     11.262s   klez-N   6281   Yes   3.252s 

 	 		
 	 		   klez.c   30   Yes     0.039s     Mydoom.v     5965     Yes     3.971s    Netsky.b   45   Yes     0.057s 

 	 		    	
 	 		    Repah.b   221   Yes     2.428s     Gibe.b   5358   Yes   4.229s    Magistr.b   4670   Yes     3.699s

 	 		    	
 	 		    Netsky.d   45   Yes     0.083s      Ardurk.d     1913     Yes    0.482s    klez.f   27   Yes     0.054s

 	 		    	
 	 		    Kelino.l   495   Yes     0.326s    Kipis.t     20378     Yes    25.345s    klez.d   31   Yes     0.085s

 	 		    			
 	 		    		Kelino.g     470     Yes     0.672s    Plage.b     395     Yes    0.291s   Urbe.a   123   Yes     0.376s 

 	 		    				
 	 		    			klez.e   27   Yes     0.094s    Magistr.b   4670   Yes     3.987s    Magistr.a.poly   36989   Yes   49.863s

 	 		   	Mydoom.M@mm   5965   Yes     5.633s    MyDoom.54464   5935   Yes     5.939s    MyDoom.N!worm   5970   Yes   6.152s

 	 		   	Win32.Runouce   51678   Yes     92.692s    Win32.Chur.A   51895   Yes     98.161s    Win32.CNHacker.C   51095   Yes   94.952s

 	 		     	Win32.Mydoom!O   215   Yes     0.481s    Mydoom.o@MM!zip   257   Yes     0.298s    W.Mydoom.kZ2L   228   Yes   0.729s

 	 		      	Mydoom-EG [Trj]   230   Yes     0.242s    Email.Worm.W32!c   220   Yes     0.249s    W32.Mydoom.L   235   Yes   0.288s

 	 		       	Worm.Mydoom-5   228   Yes     0.307s    Mydoom.CJDZ-5239   225   Yes     0.392s    Mydoom.DN.worm   220   Yes   0.299s

 	 		        
 	 		        
 	 		        
 	 		        	Win32.Mydoom.R   230   Yes     0.322s    Win32.Mydoom.dlnpqi   235   Yes     0.296s    Mydoom.o@MM!zip   235   Yes   0.403s

 	 		       	Sramota.avf   240   Yes     0.383s    BehavesLike.Mydoom   238   Yes     0.278s    Win32.Mydoom.288   248   Yes   0.410s

 	 		        	Mydoom.ACQ   19210   Yes     39.662s    Mydoom.ba   19423   Yes     38.269s    Mydoom.ftde   19495   Yes   39.583s

 	 		          	Worm.Anarxy   210   Yes     1.913s    Malware!15bf   220   Yes     2.017s    Anar.A.2   140   Yes   1.993s

 	 		           	Win32.Anar.a   215   Yes     1.631s    nar.24576   240   Yes     2.738s    Worm-email.Anar.S   155   Yes   2.093s

           	HLLW.NewApt   4230   Yes     6.954s    Win32.Worm.km   4405   Yes     7.396s    Newapt.Efbh   4550   Yes   7.254s

            	NewApt!generic   4815   Yes     9.002s    NewApt.A@mm   4485   Yes     8.159s    Newapt.Win32.1   4155   Yes   7.885s

             	W32.W.Newapt.A!   5015   Yes     8.925s    Worm.Mail.NewApt.a   51550   Yes     9.083s    malicious.154966   5155   Yes   9.291s

              Win32.Yanz   2250   Yes     4.357s    Yanzi.QTQX-0894   2120   Yes     4.109s    Win32.Yanz.a   2410   Yes   4.465s

               	Win32.Skybag   4180   Yes     6.891s    Skybag.A   4310   Yes     6.205s    Netsky.ah@MM   4480   Yes   6.991s

                	Skybag.b   4955   Yes     6.892s    Worm.Skybag-1   4820   Yes     7.119s    Win32.Agent.R   4490   Yes   7.898s

                  	Skybag [Wrm]   4985   Yes     7.482s    Skybag.Dvgb   4830   Yes     7.564s    Netsky.CI.worm   4550   Yes   7.180s


 	 		    			 	 				Agent.xpro     533     Yes     0.352s   Vilsel.lhb   15036   Yes     4.972s   Generic.2026199   433   Yes   3.489s
 	 		
 	 			 	
 	 			Vilsel.lhb   15036   Yes     26.962s     Generic.DF   5358   Yes   7.821s   LdPinch.aoq     7695     Yes    6.290s 

 	 		
 	 		    Jorik   837   Yes   4.159s    Bugbear-B   9278   Yes   17.737s    Tanatos.O   9284   Yes   21.481s 

 	 		    	
 	 		    	Gen.2   1510   Yes   5.632s     Gibe.b   5358   Yes   9.615s    Generic26.AXCN   837   Yes   3.792s

 	 		    	
 	 		    	Androm     95     Yes    0.028s      Ardurk.d     1913     Yes    3.679s    Generic.12861   30183   Yes   72.264s

 	 		    	
 	 		    	LdPinch.by     970     Yes    4.092s    Generic.2026199   433   Yes   2.402s    LdPinch.arr     1250     Yes      1.848s 

 	 		    			
 	 		    			Generic.12861   30183   Yes   88.294s    Generic.18017273     267     Yes     0.192s   LdPinch.mg     5957     Yes     9.297s 

 	 		    				
 	 		    				Script.489524   522   Yes   1.458s   Generic.DF   5358   Yes   8.291s    Zafi   433   Yes   1.028s

 	 		    	GenericKD4047614   3495   Yes   4.646s   Win32.Agent.es   3500   Yes   6.083s    W32.HfsAutoB.   3398   Yes   5.092s

 	 		    	Trojan.Sivis-1   5351   Yes   7.029s   Win32.Siggen.28   5440   Yes   6.998s    Trojan/Cosmu.isk.   5345   Yes   6.273s

 	 		    	Trojan.17482-4   381   Yes   1.495s   Delphi.Gen   375   Yes   1.948s    Trojan.b5ac.   370   Yes   2.089s

 	 		    	Delfobfus   798   Yes   3.909s   Troj.Undef   790   Yes   4.068s    Trojan-Ransom.   805   Yes   5.119s

 	 		    	LDPinch.400   1783   Yes   4.893s   PSW.LdPinch.plt   1808   Yes   5.088s    PSW.Pinch.1   1905   Yes   5.757s

 	 		    	LdPinch.BX.DLL   2010   Yes   6.965s   LdPinch.fmye   1845   Yes   6.194s    LdPinch.Win32.5558   2015   Yes   6.907s

 	 		    	TrojanSpy.Lydra.a   3450   Yes   8.289s   Trojan.StartPage   2985   Yes   5.982s    PSWTroj.LdPinch.au   2985   Yes   6.198s

 	 		    	LdPinch-21   3180   Yes   6.917s   LdPinch-R   3025   Yes   7.005s    LdPinch.Gen.2   2990   Yes   6.992s

 	 		    	Graftor.46303   3230   Yes   5.898s   LdPinch-AIH [Trj]   3010   Yes   6.095s    Win32.Heur.k   2970   Yes   5.950s

 	 		    	LdPinch-15   580   Yes   1.008s   LdPinch.e   578   Yes   1.185s    Win32/Toga!rfn   590   Yes   2.023s

 	 		    	PSW.LdPinch.mj   595   Yes   1.078s   Gaobot.DIH.worm   590   Yes   1.482s    LDPinch.DF!tr.pws   588   Yes   1.736s

 	 		    	TrojanSpy.Zbot   610   Yes   1.610s   LDPinch.10639   605   Yes   1.185s    SillyProxy.AM   590   Yes   1.882s

                 LdPinch.mj!c   590   Yes   4.5345s   LdPinch.H.gen!Eldorado   605   Yes   3.955s    Generic!BT   615   Yes   2.085s

                  LdPnch-Fam   195   Yes   1.440s   Troj.LdPinch.er   205   Yes   2.529s    LdPinch.Gen.3   210   Yes   1.482s

                   Win32.Malware.wsc   150   Yes   2.843s   malicious.7aa9fd   185   Yes   2.189s    WS.LDPinch.400   195   Yes   1.898s


 	 		    			
 	 		
 	 	
 	[!bp]
 	

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

 	 			calculation.exe   9952   No     18.352s    cisvc.exe    4105   No   3.631s    simple.exe   52   No     0.001s
 	 		
 	 			 	
 	 			shutdown.exe    2529   No     0.397s   loop.exe    529   No     9.249s     cmd.exe    1324   No    13.466s

 	 			notepad.exe    10529   No     24.583s   java.exe    800   No     15.852s     java.exe    21324   No    42.373s

 	 			sort.exe    8529   No    29.789s   bibDesk.exe    32800   No     50.279s     interface.exe    1005   No    8.462s

 	 			ipv4.exe    968   No    4.186s   TextWrangler.exe    14675   No     45.221s     sogou.exe    45219   No    55.259s

 	 			game.exe    34325   No    82.424s   cycle.tex    9014   No     42.555s     calender.exe    892   No    35.039s

 	 			SdBot.zk   3430   Yes     23.242s     Virus.Gen     661     Yes     9.437s    AutoRun.PR   240    Yes     4.181s
 	 		
 	 			 	
 	 			Adon.1703   37   Yes    0.358s   Adon.1559   37   Yes     0.255s    Spam.Tedroo.AB     487     Yes    0.924s

 	 			Akez   273   Yes     0.136s   Alcaul.d   845   Yes     0.165s    Alaul.c     355     Yes    0.109s

 	 			Virus.Win32.klk   5235   Yes     15.863s   Virus.Win32.Agent   5340   Yes     15.968s    Hoax.Gen     5455     Yes    13.569s

 	 			eHeur.Virus02   420   Yes     4.985s   Akez.11255   440   Yes     3.985s    Akez.Win32.1     455     Yes    4.008s

 	 				Weird.10240.C   430   Yes     3.929s   PEAKEZ.A   450   Yes     2.998s    Virus.Weird.c     473     Yes    3.302s

 	 				W95/Kuang   435   Yes     2.985s   Radar01.Gen   465   Yes     4.005s    Akez.Win32.5     490     Yes    3.958s

 	 				Haharin.A   210   Yes     1.462s   fsAutoB.F026   245   Yes     1.698s    Haharin.dr    235     Yes    1.558s

 	 			NGVCK1   329   Yes     0.933s   NGVCK2   455   Yes     1.109s    NGVCK3   2300   Yes   1.388s
 	 		
 	 			 	
 	 			NGVCK4   550   Yes     1.149s    NGVCK5    1555     Yes     1.825s   NGVCK6   1698   Yes   1.689s 

 	 			NGVCK7   6902   Yes     14.524s    NGVCK8    2355     Yes     4.254s   NGVCK9   281   Yes   13.301s 

 	 		
 	 		    NGVCK10   2980   Yes    9.262s    NGVCK11     5965     Yes     11.456s    NGVCK12   4529   Yes     10.094s 

 	 		    	
 	 		    	NGVCK13   2210   Yes     8.902s     NGVCK14   5358   Yes   10.294s    NGVCK15   970   Yes     1.912s

 	 		    	
 	 		    	NGVCK16   658   Yes     0.935s     NGVCK17     913     Yes    1.392s    NGVCK18   90   Yes     0.094s

 	 			NGVCK19   1295   Yes     6.958s    NGVCK20     4378     Yes    15.449s    NGVCK21   31   Yes     0.097s

 	 		    			
 	 		    			NGVCK22     370     Yes     0.898s    NGVCK23     3955     Yes    9.498s   NGVCK24   6924   Yes     11.983s 

 	 		    				
 	 		    			NGVCK25   8127   Yes     15.018s    NGVCK26   4970   Yes     9.982s    NGVCK27   7989   Yes   13.197s


 	 				NGVCK28   227   Yes     0.098s    NGVCK29   960   Yes     0.692s    NGVCK30   89   Yes   0.088s

 	 				NGVCK31   550   Yes     0.875s    NGVCK32   60   Yes     0.059s    NGVCK33   65   Yes   0.069s

 	 		    			NGVCK34   5990   Yes     9.848s    NGVCK35   4590   Yes     10.178s    NGVCK36   825   Yes   2.934s


 	 				NGVCK37   80   Yes     0.998s    NGVCK38   150   Yes     1.093s    NGVCK39   395   Yes   1.048s

 	 		    			NGVCK40   40   Yes     0.921s    NGVCK41   950   Yes     0.704s    NGVCK42   8290   Yes   15.085s

 	 		    			NGVCK43   6220   Yes     2.930s    NGVCK44   5215   Yes     11.006s    NGVCK45   9290   Yes   14.595s

 	 		    			NGVCK46   320   Yes     0.928s    NGVCK47   834   Yes     2.958s    NGVCK48   9810   Yes   14.696s

 	 		    			NGVCK49   12320   Yes     25.395s    NGVCK50   8810   Yes     19.969s    NGVCK51   39810   Yes   68.283s

 	 		    			NGVCK52   520   Yes     0.289s    NGVCK53   15   Yes     0.089s    NGVCK54   8883   Yes   11.393s

 	 		    			NGVCK55   12520   Yes     38.768s    NGVCK56   6218   Yes     15.489s    NGVCK57   32562   Yes   83.482s

 	 		    			NGVCK58   9520   Yes     23.658s    NGVCK59   818   Yes     2.592s    NGVCK60   12962   Yes   38.025s

 	 		    			NGVCK61   10020   Yes     24.976s    NGVCK62   8818   Yes     19.299s    NGVCK63   2068   Yes   3.662s

 	 		    			NGVCK64   273   Yes     1.987s    NGVCK65   5855   Yes     8.995s    NGVCK66   68   Yes   1.002s

 	 		    			NGVCK69   4150   Yes     8.052s    NGVCK70   9860   Yes     24.199s    NGVCK71   3240   Yes   7.951s

 	 		    			NGVCK72   31   Yes     0.591s    NGVCK73   549   Yes     1.052s    NGVCK74   9078   Yes   29.078s

 	 		    			NGVCK75   90   Yes     1.002s    NGVCK76   5890   Yes     10.128s    NGVCK77   1958   Yes   9.559s

 	 				NGVCK78   33468   Yes     75.098s    NGVCK79   4735   Yes     10.980s    NGVCK80   45273   Yes   82.396s

 	 		    			NGVCK66   777   Yes     0.198s    NGVCK67   895   Yes     0.223s    NGVCK81   6939   Yes   2.726s

 	 		    			NGVCK82   2931   Yes     0.463s    NGVCK83   8759   Yes     10.316s    NGVCK84   34563   Yes   53.244s

 	 		    			NGVCK85   19024   Yes     29.220s    NGVCK86   1026   Yes     0.572s    NGVCK87   7929   Yes   5.671s

 	 		    			NGVCK88   6126   Yes     8.682s    NGVCK89   580   Yes     2.036s    NGVCK90   27843   Yes   17.353s

 	 		    			NGVCK91   20   Yes     0.001s    NGVCK92   59   Yes     0.903s    NGVCK93   98   Yes   0.021s

 	 		    			NGVCK94   150   Yes     0.146s    NGVCK95   1679   Yes     0.294s    NGVCK96   6299   Yes   5.196s

 	 		    			NGVCK97   4496   Yes     5.272s    NGVCK98   428   Yes     0.329s    NGVCK99   158   Yes   1.153s

 	 		    			NGVCK100   895   Yes     0.961s    NGVCK101   745   Yes     1.117s    NGVCK102   704   Yes   0.269s

 	 		    			NGVCK103   86   Yes     0.282s    NGVCK104   145   Yes     0.998s    NGVCK105   24124   Yes   68.816s

 	 		    	
 		 	 		    		
 	 		    		
 	 		    		 	 		    		
 	 	 Experimental Results
 	 	 




  §.§.§ Applying our tool for malware detection.


We applied our tool to detect several malwares. We use the unpack tool unpacker <cit.> to handle  packers like UPX, and 
we use Jakstab <cit.> as  disassembler. 
We consider  160 malwares from the malware library VirusShare <cit.>, 
184 malwares from the malware library MalShare <cit.>, 288 email-worms from VX heaven <cit.> 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 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. To check this, we model such programs in two ways:




  * First, we take into account the self-modifying instructions and model these programs using SM-PDSs as described in Section <ref>. Then, we check whether these 
SM-PDSs satisfy  at least one of the malicious LTL formulas presented above.  If yes, the program is declared as malicious, if not, it is declared as benign.
 Our tool was able to detect all the 892 self-modifying malwares as malicious, 
and to determine that benign programs are benign.  We report  in Table  <ref>  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.




  * 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 <cit.>. By using PDSs as models, none of the malwares that we consider was detected as malicious, whereas,
as reported in Table <ref>, using self-modifying 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 <cit.>. 
However, this would be less efficient than performing our direct LTL model-checking algorithm, as shown in Table <ref>,
 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.









 

  §.§.§ Comparison with well-known antiviruses.

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




plain



