Reachability Analysis of Self Modifying Code
Tayssir Touili Xin Ye








































































Reachability Analysis of Self Modifying Code
    Tayssir Touili
LIPN, CNRS and University Paris 13 


Xin Ye
Shanghai Key Lab. of Trustworthy Comput., ECNU and LIPN, CNRS and University Paris 13



    December 11th, 2019; revised on July 2nd, 2021
========================================================================================================================================================







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 they allow to accurately model procedure  calls and mimic the program's stack.
In this work, 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.





§ 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 <cit.> 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 <cit.>.


In this work, we consider another kind of self-modifying code,  caused by self-modifying 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 <ref>. 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 self-modifying.
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 paper, we consider the reachability 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 (PDS) are known to be a natural model for sequential programs <cit.>, as they allow 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 obfuscated calls.  This is why  PushDown Systems were used in <cit.> 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 work 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 reachability analysis on the equivalent PDS is not efficient. We propose then  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 (1) 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. 
We implemented our algorithms in a tool that takes as input either an SM-PDS or a self-modifying program.
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 
reachability algorithms  for PDSs <cit.>.
Moreover, we  successfully applied our tool to the analysis of several self-modifying malwares.

This paper is an expanded version of  the conference paper <cit.>. Compared to <cit.>, in this expanded  version, we propose new  algorithms  for
  computing the forward and backward  reachable configurations for SM-PDSs, and we provide the detailed proofs
  that show the correctness of our constructions.






Outline.
The rest of the paper is structured as follows: Section 2 introduces our new model and shows how to translate a SM-PDS to an equivalent pushdown system.
In Section 3, we give the  translation from  a binary code to a SM-PDS. In Section 4, we define finite automata to represent regular (potentially infinite) 
sets of configurations of  SM-PDSs.  Sections 5 and 6 give our algorithms  to compute the backward and forward reachability sets of SM-PDSs.
Section 7 describes our experiments.

Related Work.


Reachability analysis of  pushdown systems  was  considered  in <cit.>.
Our algorithms are extensions of the saturation approach of these works. 



Model checking and static analysis approaches have been widely used to analyze binary programs, for instance, 
in <cit.>. These works cannot handle self-modifying code.


Cai et al. <cit.> 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, <cit.>  requires programs to be manually annotated with invariants. 
In <cit.>, 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 <cit.>, 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 <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 self-modifying pushdown systems, these techniques <cit.> cannot handle the program's stack. 



Finally, unpacking binary code is considered in <cit.>. These works do not consider self-modifying 
mov instructions. 





§ SELF-MODIFYING PUSHDOWN SYSTEMS 





 §.§ Definition

We introduce in this section our new model: Self-modifying Pushdown Systems. 


	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 × (Δ∪Δ_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 𝒞 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 ⇒_𝒫.
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
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 omit the subscript 𝒫 when it is understood from the context.  


	Let 𝒫=(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_2,γ_2γ_1 γ_1 ⟩,θ_0). Then, applying rule r_2, we get (⟨ p_2,γ_2γ_1 γ_1 ⟩,θ_0)⇒_𝒫  (⟨ p_3,γ_1 γ_1 ⟩,θ_0). Then, applying rule r', we get (⟨ p_3,γ_1 γ_1 ⟩,θ_0) ⇒_𝒫  (⟨ 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_2,γ_2 γ_3 γ_1 ⟩,θ_1). Then, applying rule r_2 again, we get  (⟨ p_2,γ_2 γ_3 γ_1 ⟩,θ_1) ⇒_𝒫  (⟨ 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,Γ,Δ,Δ_c) be a SM-PDS, we compute the PDS 𝒫'=(P',Γ,Δ') as follows:
P'=P× 2^Δ∪Δ_c. 
Initially, Δ'=∅. For every θ∈ 2^Δ∪Δ_c,  r∈θ:

	
  * If r =⟨ p,γ⟩↪(p',w)∈Δ,  we add ⟨(p,θ),γ⟩↪⟨(p',θ),w⟩ to Δ'
	
  * 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:


	(⟨ p,w⟩,θ)⇒_𝒫 (⟨ p',w'⟩,θ') iff
	⟨ (p,θ),w⟩⇒_𝒫'⟨ (p',θ'),w'⟩.



	⇒: We will show that if (⟨ p,w⟩,θ)⇒_𝒫 (⟨ p',w'⟩,θ'), then we have ⟨ (p,θ),w⟩⇒_𝒫'⟨ (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 self-modifying 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 𝒫', we have ⟨ (p,θ),γ⟩↪⟨ (p',θ),u' ⟩∈Δ'. Therefore, ⟨ (p,θ),γ u⟩⇒_𝒫'⟨ (p',θ),u'u⟩ holds. This implies that ⟨ (p,θ),w⟩⇒_𝒫'⟨ (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 𝒫', we have ⟨ (p,θ),γ⟩↪⟨ (p',θ'),γ⟩∈Δ' where θ'=(θ\{r_1}) ∪{ r_2}. Therefore, ⟨ (p,θ),γ u⟩⇒_𝒫'⟨ (p',θ'),γ u⟩ holds.  This implies that ⟨ (p,θ),w⟩⇒_𝒫'⟨ (p',θ'),w'⟩.
		 		
	
		⇐: We will show that if ⟨ (p,θ),w⟩⇒_𝒫'⟨ (p',θ'),w'⟩, then (⟨ p,w⟩,θ)⇒_𝒫 (⟨ 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 𝒫', there must exist a rule r∈θ such that r=⟨ p,γ⟩↪⟨ p',u'⟩. Therefore, (⟨ p,γ u⟩,θ ) ⇒_𝒫(⟨ p,u' u⟩,θ ) holds. This implies that (⟨ p,w⟩,θ ) ⇒_𝒫(⟨ p,w'⟩,θ' ).
		
  * Case θ≠θ'.  Let r=⟨ (p,θ),γ⟩↪⟨ (p',θ'), γ⟩∈Δ' be the rule leading to the transition and u'=γ. By the construction of PDS 𝒫', there must exist a rule r∈θ such that r=p(r_1,r_2)p' where θ'=(θ\{r_1}) ∪{ r_2}. Therefore, (⟨ p,γ u⟩,θ ) ⇒_𝒫(⟨ p',γ u⟩,θ' ) holds. This implies that (⟨ p,w⟩,θ ) ⇒_𝒫(⟨ p,w'⟩,θ' ).
	


Thus, we get:


	Let 𝒫=(P,Γ,Δ,Δ_c) be a SM-PDS, we can compute an equivalent PDS  𝒫'=(P',Γ,Δ')
	such that   |Δ'|=(|Δ|+|Δ_c|·|Γ|)· 2^𝒪(|Δ| +|Δ_c|)
	and  |P'|=|P|· 2^𝒪(|Δ| +|Δ_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 <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:



	A symbolic pushdown system is a tuple 𝒫=(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 _𝒫 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',ww'⟩,θ') for (θ,θ')∈ R. Let _𝒫^*
be the transitive, reflexive closure of  _𝒫.
Then, given a SM-PDS 𝒫=(P,Γ,Δ,Δ_c), we can compute an equivalent symbolic PDS 𝒫'=(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:


	(⟨ p,w⟩,θ)⇒_𝒫 (⟨ p',w'⟩,θ') iff
	(⟨ p,w⟩,θ) _𝒫'(⟨ p',w'⟩,θ').



⇒: we will show that if (⟨ p,w⟩,θ)⇒_𝒫 (⟨ p',w'⟩,θ'), then (⟨ p,w⟩,θ) _𝒫'(⟨ 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 self-modifying 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,γ⟩R_id⟨ p',u'⟩∈Δ', therefore, (⟨ p,γ u⟩,θ) _𝒫'(⟨ p',u' u⟩,θ) holds. This implies that (⟨ p,w⟩,θ) _𝒫'(⟨ 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,γ⟩R⟨ p',γ⟩∈Δ' and R={(θ,θ')∈ 2^Δ∪Δ_c× 2^Δ∪Δ_c|  r∈θ and θ'=(θ∖{ r_1})∪{r_2}}, therefore, (⟨ p,γ u⟩,θ) _𝒫'(⟨ p',γ u⟩,θ') holds.  This implies that (⟨ p,w⟩,θ) _𝒫'(⟨ p',w'⟩,θ').	
		
		⇐: we will show that  if (⟨ p,w⟩,θ) _𝒫'(⟨ p',w'⟩,θ'), then (⟨ p,w⟩,θ)⇒_𝒫 (⟨ 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 𝒫', there must exist a rule r∈θ s.t. r=⟨ p,γ⟩↪⟨ p',u'⟩∈Δ. Therefore, (⟨ p,γ u⟩,θ)⇒_𝒫 (⟨ p', u'u⟩,θ) holds.  This implies that (⟨ p,w⟩,θ) ⇒_𝒫(⟨ 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 𝒫', 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',γ u⟩,θ') hold.  This implies that (⟨ p,w⟩,θ) _𝒫'(⟨ p',w'⟩,θ').	
	


Thus, we get:


	Let 𝒫=(P,Γ,Δ,Δ_c) be a SM-PDS, we can compute an equivalent symbolic  PDS  𝒫'=(P',Γ,Δ')
	such that |P'|=|P|, |Δ'|=|Δ|+|Δ_c|· |Γ|, and the size of the relations used in the symbolic transitions is
	2^𝒪(|Δ|+|Δ_c|).










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







 §.§ From self-modifying code to  SM-PDS



We show in what follows how to build a SM-PDS from a binary program.
We suppose we are given  an oracle  𝒪  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 <cit.> to get this oracle.
We translate the assembly program  into a  self-modifying pushdown system
where the control locations store the control points of the binary program and
the stack  memics the program's stack. The non self-modifying instructions  of the program define the rules Δ of the SM-PDS (which are standard PDS rules),
and can be obtained following the translation of <cit.> 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 <cit.> 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 θ:


 
 	 Let 𝒫=(P,Γ,Δ,Δ_c) be a SM-PDS. A  𝒫-automaton is a tuple  𝒜=(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, θ'∈ 2^Δ∪Δ_c,  ∀γ∈Γ∪{ϵ},  
	∀ w ∈Γ^*  for w=γ_0γ_1⋯γ_n,  qγ w_T q' iff ∃ q”∈ Q, q γ_T q”  q”w_T q'.  If q_Tq' holds, we say that q_Tq' is a path of 𝒜.  
	A configuration (⟨ p, w ⟩, θ) is  accepted by  𝒜 iff  𝒜 contains a path
	(p,θ)γ_0_T q_1γ_1_T q_2⋯ q_nγ_n_T q where q∈ F.	Let L(𝒜) be the set of configurations accepted by 𝒜.
	Let 𝒞 be a  set of configurations of the  SM-PDS 𝒫. 
	𝒞 is regular  if there exists a 𝒫-automaton 𝒜 such that  𝒞=L(𝒜)



§ EFFICIENT COMPUTATION OF PRE^* IMAGES

Let 𝒫=(P,Γ,Δ,Δ_c) be a SM-PDS, and let 𝒜=(Q,Γ,T,P,F) be a  𝒫-automaton that represents a regular
set of configurations 𝒞 ( 𝒞=L(𝒜)). To compute pre^*( 𝒞), one can use the translation of Section <ref> to compute an equivalent PDS, and then apply the algorithms of  <cit.>. This procedure is too complex since the size of the obtained PDS is huge. One can also use the translation of Section <ref> to compute an equivalent symbolic PDS, and then use the algorihms of  <cit.>.
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^*( 𝒞) without any need to translate the SM-PDS to an equivalent PDS or symbolic PDS.
We assume w.l.o.g. that 𝒜 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 𝒜_pre^* follows the same idea  as  
for standard  pushdown systems (see <cit.>).
It consists in adding iteratively new transitions to the automaton 𝒜 according
to  saturation rules (reflecting the backward application of the transition
rules in the system), while the set of states remains unchanged.  Therefore, let 𝒜_pre^*  be the 𝒫-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_Tq, 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,θ)γ_Tq,  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'qw'_T'q_F, where q_F∈ F. This means, by definition of  𝒫-automata,  that the configuration c=(⟨ p',ww'⟩,θ') is accepted by 𝒜_pre^*.
If r is in θ', then the configuration c'=(⟨ p,γ w'⟩,θ') is a predecessor of c. Therefore, it should be added to 
𝒜_pre^*. This configuration is accepted by the run (p,θ')γ_T'qw'_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'qw'_T'q_F, where q_F∈ F. 
This means, by definition of 𝒫-automata,  that the configuration c=(⟨ p',γ w'⟩,θ') is accepted by 𝒜_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 
𝒜_pre^*. This configuration is accepted by the run π'=(p,θ)γ_T'qw'_T'q_F added by rules  (α_2).



Thus, we can show that:


	𝒜_pre^* recognizes  pre^*(L(A)).


Before proving this theorem, let us illustrate the construction on 2 examples.



	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 of Fig. <ref>.  Let 𝒜 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. <ref>. The result is obtained through the following steps: 
	
		
  *  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) (p_0,θ_0) to T'.
		
  *  Now that we have (p_4,θ_0)_T' (p_0,θ_0), since r_5∈θ_0, Rule (α_1) adds  (p_1,θ_0) (p_0,θ_0) to T'.
		
  *  Since we have (p_4,θ_0)_T' (p_0,θ_0), the self-modifying transition r'∈θ_0 can be applied. Thus, Rule (α_2) adds (p_3,θ_1) (p_0,θ_0) to T' where θ_1 =(θ_0 ∖{r_5} )∪{r_1} ={r_1,r_2,r_3,r_4,r'}.
		
  *  Since (p_3,θ_1) (p_3,θ_1) and r_3 ∈θ_1, Rule (α_1) adds (p_2,θ_1) (p_3,θ_1) to T'.
		
  *  Then, there is a path  (p_2,θ_1)_T' (p_3,θ_1) _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) (p_0,θ_0) to T'.
		
  *  No further additions are possible. Thus, the procedure terminates.
 	




	Let us give another example. Consider the SM-PDS with control points P={ p_1,p_2,p_3,p_4,p_5} and Δ,Δ_c as shown in the left half of Fig. <ref>. Let 𝒜 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 𝒜_pre^* of the algorithm is on the right half of Fig. <ref>. The result is obtained through the following steps:
	
		
  * Since (p_0,θ_0) _T's_1 and  r_1∈θ_0, then Rule (α_1) adds (p_1,θ_0) s_1 to T'.
		
  * Since (p_1,θ_0)_T' s_1  and r_2∈θ_0, Rule (α_1) adds the transition (p_2,θ_0) s_1 to T'.
		
  * Since (p_2,θ_0)_T' (p_2,θ_0) and r_3∈θ_0, Rule (α_1) adds the transition (p_3,θ_0) (p_2,θ_0) to T'.
		
  * Then, there is a path (p_3,θ_0)_T' (p_2,θ_0) _T's_1  and  r_4∈θ_0, Rule α_1 adds the transition (p_4,θ_0)s_1 to T'.
		
  * Because (p_4,θ_0)_T' (p_4,θ_0) and r_5 ∈θ_0, Rule (α_1) adds the transition (p_0,θ_0) (p_4,θ_0) to T'.
		
  * Since (p_0,θ_0) _T'(p_4,θ_0) and r_1∈θ_0, Rule (α_1)  adds the transition (p_1,θ_0)(p_4,θ_0) to T'. Then, since r_2∈θ_0, Rule (α_1) adds the transition (p_2,θ_0)(p_4,θ_0) to T'.
		
  * Since there is  a path (p_3,θ_0)_T'(p_2,θ_0)_T'(p_4,θ_0) and r_4∈θ_0, Rule (α_1) adds (p_4,θ_0)(p_4,θ_0) to T'.
		
  * Since (p_4,θ_0)_T's_1,(p_4,θ_0)_T'(p_4,θ_0) and r_c^1,r_2∈θ_0, Rule (α_2) adds (p_5,θ_1)s_1 and (p_5,θ_1)(p_4,θ_0) to T' where θ_1=(θ_0 ∖{ r_2}) ∪ r_6={r_1,r_3,r_4,r_5,r_6,r_c^1,r_c^2,r_c^3,r_c^4}. For the same reason, since  (p_0,θ_0) _T'(p_4,θ_0), (p_0,θ_0) _T's_1 and r_1,∈θ_1, r_c^2∈θ_0, Rule (α_2)  adds the transitions (p_5,θ_2)(p_4,θ_0) and (p_5,θ_2) s_1 to T' where θ_2=(θ_0∖{r_1}) ∪{r_7}={r_2,r_3,r_4,r_5,r_7,r_c^1,r_c^2,r_c^3,r_c^4}.
		
  * Since (p_5,θ_1)_T's_1, (p_5,θ_1)_T'(p_4,θ_0) and r_6∈θ_1, Rule (α_1) adds the transitions (p_2,θ_1) s_1 and (p_2,θ_1) (p_4,θ_0) to T'.
		
  * Since (p_2,θ_1)_T'(p_2,θ_1)  and r_3 ∈θ_1, Rule (α_1) adds (p_3,θ_1)(p_2,θ_1).
		
  * Because there are paths (p_3,θ_1)_T'(p_2,θ_1)_T'(p_4,θ_0) and (p_3,θ_1)_T'(p_2,θ_1)_T's_1,  Rule (α_1)
   adds the transitions (p_4,θ_1)(p_4,θ_0) and (p_4,θ_1)s_1 to T'.
		
  * Since (p_4,θ_0)_T' (p_4,θ_0) and r_5 ∈θ_1, Rule (α_1) adds (p_0,θ_1)(p_4,θ_1).
		
  * Now we have (p_0,θ_1)_T'(p_4,θ_1) and r_c^2,r_1∈θ_1, Rule (α_2) adds the transition (p_5,θ_3)(p_4,θ_1)  to T' where θ_3={r_3,r_4,r_5,r_6,r_7,r_c^1,r_c^2,r_c^3,r_c^4}. For the same reason, since (p_3,θ_1)(p_2,θ_1) and r_c^3,r_6∈θ_1, Rule α_2 adds the transition (p_2,θ_0)(p_2,θ_1) to T' because θ_0=(θ_1 ∖{r_6})∪{r_2}.
		
  * Since (p_5,θ_3)_T'(p_5,θ_3) and r_7∈θ_3, Rule (α_1)  adds the transition (p_2,θ_3)(p_5,θ_3) to T'.
		
  * Because (p_2,θ_3)_T'(p_2,θ_3)  and r_3∈θ_3, Rule (α_1) adds the transition  (p_3,θ_3)(p_2,θ_3) to T'. Then, since there is  a  path (p_3,θ_3)_T'(p_2,θ_3)_T'(p_5,θ_3) and r_4 ∈θ_3, Rule (α_1) adds the transition (p_4,θ_3)(p_5,θ_3) to T'. Then, since r_5∈θ_3, Rule (α_1) adds the transition (p_0,θ_3)(p_4,θ_3) to T'.
		
  * Since (p_3,θ_3)_T'(p_2,θ_3) and r_c^3 ∈θ_3, Rule (α_2)  adds  the transition (p_2,θ_2)_T'(p_2,θ_3) to T' where (θ_3∖{r_6})∪{r_2}=θ_2. Meanwhile,  since  (p_2,θ_3)(p_5,θ_3)  and r_c^4, r_7 ∈θ_3, Rule (α_2) adds the transition (p_4,θ_1)(p_5,θ_3) to T' where (θ_3∖{ r_7})∪{r_1}=θ_1.
		
  * Because r_7∈θ_2 and (p_5,θ_2)_T'(p_5,θ_2), Rule (α_1) adds the transition  (p_2,θ_2)(p_5,θ_2) to T'.
		
  * Since (p_2,θ_2)_T'(p_2,θ_2) and r_3 ∈θ_2, Rule (α_1) adds (p_3,θ_2)_T'(p_2,θ_2) to T'. Then, there is a path  (p_3,θ_2)_T'^* (p_5,θ_2), since r_4∈θ_2,  Rule (α_1) adds the transition (p_4,θ_2)_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)(p_4,θ_2) to T'.
		
  * Now we have (p_2,θ_2)_T'(p_5,θ_2) and  (p_2,θ_2)_T'(p_2,θ_3), since r_c^4,r_7∈θ_2, Rule α_2 adds the transitions (p_4,θ_0)(p_5,θ_2) and (p_4,θ_0)(p_2,θ_3) to T' where (θ_2 ∖{ r_7}∪ ){ r_1} =θ_0.
		
  * Since (p_4,θ_2)_T'(p_5,θ_2) and r_2,r_c^1∈θ_2, Rule (α_2) adds the transition  (p_5,θ_3)(p_5,θ_2) to T' where (θ_2∖{ r_2}) ∪{r_6}=θ_3.
		
  * Since  (p_5,θ_3)_T'(p_5,θ_2) and r_6∈θ_3,  Rule (α_1)  adds the transition (p_2,θ_3)(p_5,θ_2) to T'.
		
  * No further additions are possible, so the procedure terminates.
	







 §.§ Proof of Theorem <ref>


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



	For every configuration (⟨ p, w ⟩,θ_0) ∈ L(A), if (⟨ p',w'⟩,θ) ⇒_𝒫^* (⟨ p, w ⟩,θ_0),  then (p',θ)_T'q for some final state q of 𝒜_pre^*. 




Assume  (⟨ p',w'⟩,θ) i⇒_𝒫 (⟨ 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)_T' q always holds for some final state q i.e.  (p',θ)_T' q holds.

Step. i>0. Then there exists a configuration (⟨ p”, u ⟩,θ”) such that 

    (⟨ p', w'⟩,θ) ⇒_𝒫 (⟨ p”,u⟩, θ”) i-1⇒_𝒫 (⟨ p, w ⟩,θ_0)

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 𝒜_pre^* s.t.

    (p”,θ”)u_1_T'q' w_1_T'q

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',θ”) γ'_T'q'

	  
	 Putting (1) and (2) together, we can obtain that 
	 
    π=(p',θ”) γ'_T'q'  w_1_T'q

	 
	 Thus, (p',θ”)γ'w_1_T'q i.e. (p',θ)w'q for some final state q∈ F.	  
	  
	 	
  * 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}.

	 	
	 	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

	 	



	 If a path π=(p,θ)_T'q for θ⊆Δ∪Δ_c is in 𝒜_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 𝒫-automaton 𝒜;
	 	
  (II) Moreover, if q is an initial state i.e. in the form (p,θ), then w'=ϵ.
 	 




 Let 𝒜_pre^*=(Q,Γ,T,P,F) be the  𝒫-automaton computed by the saturation procedure. In this proof, we use [i]_T' to denote the transition relation of 𝒜_pre^* obtained after adding i-transitions using the saturation procedure. In particular, since initially  𝒜_pre^*=𝒜,  𝒜_pre^* contains the path (p',θ_0)w'_Tq where (⟨ p',w' ⟩,θ_0)∈ L(A), then we write (p',θ_0)[0]w'_Tq.


Let i be an index such that  π=(p,θ)[i]w_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 𝒜.  
	

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 𝒜_pre^* and j be the number of times that t is used in the path (p,θ)[i]w_T'q. The proof is by induction on j. If j=0, then we have (p,θ)[i-1]w_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 𝒫-automaton 𝒜.   So assume that j>0. Then, there exist u and v such that w=uγ v and 

    1
    (p,θ) [i-1]u_T' (p_1,θ_1) [i]γ_T'q'[i]v_T'q



The application of the induction hypothesis (induction on i) to (p,θ) [i-1]u_T' (p_1,θ_1)  (notice that (p_1,θ_1) is an initial state) gives that 

    2
    (⟨ p,u⟩,θ) ⇒^* (⟨ 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_T'q'[i]v_T'q

	
		
	
	Applying the transition rule r gets 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',w'⟩,θ_0)  s.t. (p',θ_0)w'_T' q 
     in the initial 𝒫-automaton 𝒜

	
	
	
	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 𝒫-automaton 𝒜
 	
 	
  * Case t was added by rule α_2: there exist p_2 ∈ P and θ”⊆Δ∪Δ_c such that
	
    7
    		p_1 (r_1,r_2) p_2 ∈Δ_c ∩θ”,θ”=(θ_1 \{r_1}) ∪{r_2}

	and the following path in the current automaton ( self-modifying rule won't change the stack) with r∈θ”:	
	
    8
    	(p_2,θ”) _T' q' [i]v_T'q

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

	We can apply the induction hypothesis (on j) to (8), and obtain
	
    10
    		(⟨ p_2,γ v⟩, θ”) ⇒^* (⟨ p',w' ⟩,θ_0)  s.t. (p',θ_0)w'_T q 
     in the initial 𝒫-automaton 𝒜

	
	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 𝒫-automaton 𝒜.




Then, we can prove  Theorem <ref>: 



	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 𝒜 for q∈ F. By lemma 1, we can obtain that there exists a path (p,θ) _T'q for some final state q of 𝒜_pre^*. So (⟨ p, w ⟩,θ) is recognized by 𝒜_pre^*.

Conversely, let (⟨ p, w ⟩,θ) be a configuration accepted by 𝒜_pre^* i.e. there exists a path (p,θ) _T'q  in 𝒜_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) _Tq in the initial automaton 𝒜 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)).








§ EFFICIENT COMPUTATION OF POST^* IMAGES


Let 𝒫=(P,Γ,Δ,Δ_c) be a SM-PDS, and let 𝒜=(Q,Γ,T,P,F) be a  𝒫-automaton that represents a regular
set of configurations 𝒞 ( 𝒞=L(𝒜)). Similarly, it is not optimal  to compute post^*( 𝒞) using the translations of 
Sections <ref> and <ref> to compute  equivalent PDSs or symbolic PDSs, and then apply the algorithms of  <cit.>. 
We present in this section a  direct and    efficient  algorithm that computes post^*( 𝒞).
We assume w.l.o.g. that 𝒜 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 𝒜_post^* consists in adding iteratively new transitions to the automaton 𝒜 according
to  saturation rules (reflecting the forward application of the transition
rules in the system).
We define 𝒜_post^* to be the 𝒫-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'qw'_T'q_F, where q_F∈ F. 
This means, by definition of 𝒫-automata,  that the configuration c=(⟨ p,γ w'⟩,θ) is accepted by 𝒜_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 
𝒜_post^*. This configuration is accepted by the run (p',θ)ϵ_T'qw'_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 
𝒜_post^*. This configuration is accepted by the run (p',θ)γ'_T'qw'_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 
𝒜_post^*. 
This configuration is accepted by the run (p',θ)γ_1_T'q_p'γ_1^θγ_2_T'qw'_T'q_F added by rules  (β_3).




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 
𝒜_post^*. This configuration is accepted by the run (p',θ')γ_T'qw'_T'q_F added by rules  (β_4).





Thus, we can show that:


	𝒜_post^*  recognizes the set
	post^*(L(A)).


Before proving this theorem, let us illustrate the construction on 2 examples.




 	Let us illustrate this procedure by an example. Consider  the SM-PDS shown in the left half of Fig. <ref> and the automaton 𝒜 from Fig. <ref> 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. Then the result 𝒜_post^* of the algorithm is shown in the right half of  Fig. <ref>. The result is derived through the following steps:
	
		
  * First, since (p_0,θ_0)_T' s_1 and  r_1∈θ_0, Rule (β_3) generates a new state q_p_1γ_1^θ_0 and adds the two transitions: (p_1,θ_0)  q_p_1γ_1^θ_0 and q_p_1γ_1^θ_0 s_1 to T'.
		
  * Since (p_1,θ_0) _T' q_p_1γ_1^θ_0 and r_2 ∈θ_0,   Rule (β_3) generates a new state   q_p_2γ_2^θ_0 and adds two transitions : (p_2,θ_0)  q_p_2γ_2^θ_0 and q_p_2γ_2^θ_0  q_p_1γ_1^θ_0 to T'.
		
  * Because  (p_2,θ_0) _T' q_p_2γ_2^θ_0 and r_3 ∈θ_0, Rule (β_1) adds the transition (p_3,θ_0) q_p_2γ_2^θ_0 to T'.
		
  * Since (p_3,θ_0) _T'q_p_2γ_2^θ_0 and  r' ∈θ_0, Rule (β_4) adds the transition (p_4,θ_1)  q_p_2γ_2^θ_0 to T' where θ_1 =(θ_0 ∖{r_3} ) ∪{r_5} ={ r_1,r_2,r_4,r_5,r'}.
		
  * Since (p_4,θ_1) _T' q_p_2γ_2^θ_0 and r_4 ∈θ_1, Rule (β_1) adds the transition (p_1,θ_1)q_p_2γ_2^θ_0 to T'.
		
  * Then, since there is a path  (p_1,θ_1)_T'^*q_p_1γ_1^θ_0 and  r_2∈θ_1, Rule (β_3) generates         new state q_p_2,γ_2^θ_1 and adds two transitions (p_2,θ_1) q_p_2,γ_2^θ_1 and q_p_2,γ_2^θ_1 q_p_1γ_1^θ_0 to T'.
		
  * Since (p_2,θ_1) _T'q_p_2,γ_2^θ_1  and r_5 ∈θ_1, Rule (β_2) adds the transition (p_4,θ_1)q_p_2,γ_2^θ_1 to T'.
		
  * No unprocessed matches remain. The procedure terminates.
	



 
	Let us illustrate this procedure by another example. Consider the SM-PDS shown in the left half of Fig. <ref> where (p_0,θ_0) is the initial state and s_2 is the  final state. The result 𝒜_post^* of the algorithm is shown in the right half of Fig. <ref> obtained as follows:
	
		
  * First, since (p_0,θ_0)_T's_1 and r_1∈θ_0, Rule (β_3) generates a new state q_p_1γ_1^θ_0 and adds two transitions: (p_1,θ_0)  q_p_1γ_1^θ_0 and q_p_1γ_1^θ_0 s_1 to T'.
		
  * Since (p_1,θ_0) _T' q_p_1γ_1^θ_0 and  r_2 ∈θ_0,   Rule (β_3) generates a new state q_p_2γ_2^θ_0 and adds two transitions: (p_2,θ_0)  q_p_2γ_2^θ_0 and q_p_2γ_2^θ_0  q_p_1γ_1^θ_0 to T'.
		
  * Because (p_2,θ_0) _T' q_p_2γ_2^θ_0 and r_3∈θ_0, Rule (β_2) adds (p_3,θ_0)  q_p_2γ_2^θ_0 to T'. 
		
  * Since (p_3,θ_0) _T' q_p_2γ_2^θ_0  and r_c^1,r_1∈θ_0, Rule (β_4) adds the transition (p_4,θ_1)q_p_2γ_2^θ_0 to T' where θ_1=(θ_0 ∖{r_1}) ∪{r_5 }.
		
  * Since (p_4,θ_1)_T'q_p_2γ_2^θ_0 and r_4 ∈θ_1, Rule (β_1) adds the transition (p_0,θ_1)q_p_2γ_2^θ_0 to T'. Then there is a   path (p_0,θ_1)_T'^* q_p_1γ_1^θ_0, since r_5∈θ_1, Rule (β_2) adds the transition  (p_5,θ_1)q_p_1γ_1^θ_0 to T'.
		
  * Since  (p_5,θ_1)_T'q_p_1γ_1^θ_0 and r_c^4,r_5∈θ_1, Rule (β_4) adds the transition (p_0,θ_0)q_p_1γ_1^θ_0 to T' where (θ_1 ∖{r_5} )∪{ r_1} =θ_0.
		
  * Since (p_0,θ_0)_T'q_p_1γ_1^θ_0 and  r_1∈θ_0, Rule (β_3) adds the transitions  (p_1,θ_0)  q_p_1γ_1^θ_0 and q_p_1γ_1^θ_0 q_p_1γ_1^θ_0 to T'.
		
  * Because (p_4,θ_1)_T'q_p_2γ_2^θ_0 and r_c^2∈θ_1, Rule (β_4) adds the transition (p_2,θ_2)q_p_2γ_2^θ_0 to T'.
		
  * Since (p_2,θ_2)_T'q_p_2γ_2^θ_0 and r_6∈θ_2, Rule (β_2) adds the transition (p_4,θ_2)q_p_2γ_2^θ_0 to T'.
		
  * Since p_4,θ_2_T'q_p_2γ_2^θ_0 holds and r_6,r_c^3∈θ_2,  Rule (β_4)  adds the transition (p_5,θ_1) q_p_2γ_2^θ_0 to T'.
		
  * Then, since (p_5,θ_1) _T'q_p_2γ_2^θ_0 and  r_c^4∈θ_1, Rule (β_4)  adds the transition  (p_0,θ_0)q_p_2γ_2^θ_0 to T'.
		
  * Since r_1∈θ_0 and (p_0,θ_0)_T'q_p_2γ_2^θ_0, Rule (β_3) adds two transitions: (p_1,θ_0)  q_p_1γ_1^θ_0 and q_p_1γ_1^θ_0q_p_2γ_2^θ_0 to T'.
		
  * No more rules can be applied. Thus, the procedure terminates.
	




 §.§ Proof of Theorem <ref>

Let us now prove Theorem <ref>. To prove this theorem, we first show the following lemma:





	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 𝒜_post^*. 

 
 
 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 𝒜_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


    1
    (p”,θ”)u_T' q  for some  q∈ F
 

Then, let γ∈Γ, u_1,w_1∈Γ^* be such that  u=γ u_1, w'=w_1 u_1. Let  q_1 be a state of 𝒜_post^* s.t. we have the following path in 𝒜_post^*:


    2
    (p”,θ”)_T' q_1 u_1_T' q
 
There are two cases depending on whether (⟨ p”,u ⟩,θ”)⇒(⟨ p',w'⟩,θ) is corresponding to a self-modifying transition (i.e. (θ”=θ)) or not.


	
  * 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  

    3
    	(p',θ)_T'q_1

	  
Putting (2) and (3) together, we can have (p',θ)_T'q_1 u_1_T' q i.e. (p',θ)_T' q for some final state q of 𝒜_post^*.
 
		
  - Case |w_1|=1, then let γ'∈Γ s.t. w_1=γ'.  By applying the saturation rule  α_2,    we can get  

    4
    	(p',θ)_T'q_1

	  
Putting (2) and (4) together, we can have (p',θ)_T'q_1 u_1_T' q i.e. (p',θ)_T' q  for some final state q of 𝒜_post^*.

		

	
  - Case |w_1|=2, let γ_0', γ_1'∈Γ be such that w_1=γ_0'γ_1'. By applying the saturation rule α_3,    we can get 
	
    5
    	(p',θ)γ_0'_T'q^θ_p'γ_0'γ_1'_T'q_1
 
	Putting (2) and (5) together, then we have a path (p',θ)_T'q^θ_p'γ_0'_T'q_1_T'q i.e. (p',θ)_T' q  for some final state q of 𝒜_post^*.
		
	
		
	
  * 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:
	
	
    5
    	(p',θ)_T'q_1_T'q

	i.e.  (p',θ)_T'q for some final state q of 𝒜_post^*.





	If a path  π=(p,θ)_T'q is in 𝒜_post^*, then the following holds:

	
	
  (I) if q is a  state of 𝒜, then
	(⟨ p',w'⟩ ,θ_0)⇒^* (⟨ p,w ⟩,θ) for a configuration
	(⟨ p',w'⟩,θ_0) such that (p',θ_0)_Tq is a path in the initial 𝒫-automaton 𝒜 ;
	
	
  (II) if q is a new state of the form q=q_p_1γ_1^θ_1, then
	(⟨ p_1,γ_1 ⟩, θ_1) ⇒^* (⟨ p,w ⟩,θ).
	


  Let 𝒜_post^*=( Q',Γ, T',P,F) be the 𝒫-automaton computed by the saturation procedure. In this proof, we use [i]_T' to denote the transition relation →_T' of 𝒜_post^* obtained after adding i transitions using the saturation procedure. 
 
 

Let i be an index such that
(p,θ)[i]w_T'q holds. We prove both parts of the lemma  by induction on i.

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,θ)[i]w_T'q.   
𝒜 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,θ)_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)_T q is a path of initial 𝒫-automaton 𝒜. So
assume that j>0. We distinguish three possible cases:

	
  * 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:
	
    1
    	(p,θ)=(p_1,θ_1)[i]v_T' q_1 [i-1]w_1_T'q

		
	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:
		
		
		
	
		
    2
    		(p_2,θ_2)[i-1]v_T' q_1 [i-1]w_1_T'q, θ_1=θ_2\{r_1}∪{r_2}

		
		

		By induction on (i), we get from (2)  that there exists a configuration (⟨ p',w' ⟩,θ_0) s.t. (p',θ_0) _T q is a path in the initial 𝒫-automaton 𝒜:
		
    3
       (⟨ p',w' ⟩,θ_0) ⇒^* (⟨ p_2, vw_1⟩,θ_2)

		  By applying the rule  p_2 (r_1,r_2)p_1, we get that 
		
    4
    		(⟨ p_2, vw_1 ⟩,θ_2)⇒(⟨ p_1, vw_1 ⟩,θ_1)

		Thus, putting (3) and (4) together, we get that  there exists a configuration (⟨ p',w' ⟩,θ_0) s.t. (p',θ_0) _T q is a path in the initial 𝒫-automaton 𝒜  and:
		
    5
    			 (⟨ p',w' ⟩,θ_0)⇒^* (⟨ p_2,vw_1⟩,θ_2)⇒
    
    		(⟨ p_1, w ⟩ ,θ_1)=(⟨ p,w⟩,θ)

		
			
		
  - Case t is added by β_1 or β_2:  then there exists p_2∈ P, γ_2∈Γ such that 
		
    6	
    	r=⟨ p_2,γ_2⟩↪⟨ p_1,v ⟩∈Δ

		and 𝒜_post^* contains the following path:

		
    7
    		(p_2,θ_1)[i-1]γ_2_T'q_1[i-1]w_1_T'q

		By induction on (i),  We can get from (7)  that  there exists a configuration (⟨ p',w' ⟩,θ_0) s.t. (p',θ_0) _T q is a path in the initial 𝒫-automaton 𝒜  and:
		
    8 
    			 (⟨ p',w' ⟩,θ_0)⇒^* (⟨ p_2, γ_2 w_1 ⟩,θ_1)
		
		
		
		Thus, putting (6) and (8) together, we have that  there exists a configuration (⟨ p',w' ⟩,θ_0) s.t. (p',θ_0) _T q is a path in the initial 𝒫-automaton 𝒜  and:
		
    9
    			(⟨ p',w' ⟩,θ_0)⇒^* (⟨ p_2,γ_2 w_1 ⟩,θ_1)⇒
    
    			(⟨ p_1,w ⟩ ,θ_1)=(⟨ p,w⟩,θ)
	
	
	
		
  * If t is the first transition added by rule β_3 i.e. t is in the form of ((p_1,θ”),γ_1,q_p_1γ_1^θ_1). If this transition is new, then there are no transitions outgoing from  q_p_1γ_1^θ_1. So the only path using t is (p_1,θ”) [i]γ_1_T'q_p_1γ_1^θ_1. For this path, we only need to prove part (II), and (⟨ p_1,γ_1 ⟩, θ_1) ⇒^*(⟨ p_1,γ_1 ⟩, θ_1) holds trivially.

		

  * Let t=(q_p_1γ_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: 

    10
    	(p,θ) [i-1]u_T' q_p_1γ_1^θ_1[i]γ”_T' q' [i]v_T' q


Because t was added via the saturation rule, then there exist p_2 ∈ P, γ_2∈Γ and a rule of the form
	
    11⟨ p_2,γ_2 ⟩↪⟨ p_1,γ_1 γ”⟩∈Δ∩θ_1

and  𝒜_post^* contains the following path:

	
    12
    		(p_2,θ_1)[i-1]γ_2_T'q'[i]v_T'q




We apply the induction hypothesis on i and obtain that


    13
    		(⟨ p_1,γ_1⟩,θ_1)⇒^* (⟨ p,u⟩,θ)


	
We apply the induction hypothesis on i to obtain that there exists a configuration (⟨ p',w'⟩,θ_0) s.t.  (p',θ_0) _T q is a path in the initial 𝒫-automaton 𝒜  and:

    14
    		(⟨ p',w' ⟩,θ_0)⇒^* (⟨ p_2,γ_2 v ⟩,θ_1)

	
	Thus, putting (11) (13) and (14) together, we have that there exists a configuration (⟨ p',w'⟩,θ_0) s.t.  (p',θ_0) _T q is a path in the initial 𝒫-automaton 𝒜  and:
	
	
    15
    		(⟨ p',w' ⟩,θ_0) ⇒^* (⟨ p_2,γ_2v ⟩,θ_1) ⇒
    
    		(⟨ p_1,γ_1γ” v⟩,θ_1)
     ⇒^* (⟨ p, u γ” v ⟩,θ)=(⟨ p, w ⟩,θ)




Then we continue to prove Theorem <ref>:



	Let (⟨ p',w' ⟩, θ) be a configuration of post^*(L(𝒜)). Then there exists a configuration (⟨ p,w ⟩,θ_0) such that there exists a path (p,θ_0)_Tq in the initial automaton 𝒜 and (⟨ p,w ⟩,θ_0) ⇒^* (⟨ p', w'⟩, θ). By Lemma 3, we can have (p',θ) _T' q for q is a final state of 𝒜_post^*. So (⟨ p' ,w'⟩,θ) is recognized by  𝒜_post^*.

Conversely, let (⟨ p',w' ⟩,θ) be a configuration recognized by
𝒜_post^*. Then there exists a path (p',θ) _T'q  in 𝒜_post^* for some final
state q. By Lemma 4, since q is a final state, we have
(⟨ p,w ⟩,θ_0) ⇒_𝒫^* (⟨ p',w' ⟩,θ) s.t. there exists a configuration (⟨ p,w ⟩,θ_0) s.t. (p,θ_0)_T'q is a path in the initial automaton 𝒜 i.e.  (⟨ p,w ⟩,θ_0)∈ L(A). Therefore, (⟨ p',w'  ⟩,θ)∈
post^*(L(A))







§ EXPERIMENTS





 §.§ Our algorithms vs. standard pre^* and post^* algorithms of PDSs


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 <cit.>, 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 1 (resp. Table 2). 


	


In Table <ref>,  
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 <cit.> 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   mark  - for the total execution time. 
You can see that our direct algorithm (Column SM-PDS) is much more efficient. 

Table <ref> 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.





 §.§ Malware Detection

Self-modifying code is widely used as an obfuscation technique for malware writers. 
Thus, we applied our tool for malware detection.


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.


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 <ref>, (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 
<cit.>.

The results are reported in Table 3, 
Column Example reports the name of the  worm. Column SM-PDS shows the result obtained by  applying our method 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. 
alpha



























