Huu-Vu Nguyen

Tayssir Touili

BCARET Model Checking for Malware Detection

The number of malware is growing fast recently. Traditional malware detectors based on signature matching and code emulation are easy to bypass. To overcome this problem, model-checking appears as an efficient approach that has been extensively applied for malware detection in recent years. Pushdown systems were proposed as a natural model for programs, as they allow to take into account the program's stack into the model. CARET and BCARET were proposed as formalisms for malicious behavior specification since they can specify properties that require matchings of calls and returns which is crucial for malware detection. In this paper, we propose to use BCARET for malicious behavior specification. Since BCARET formulas for malicious behaviors are huge, we propose to extend BCARET with variables, quantifiers and predicates over the stack. Our new logic is called SBPCARET. We reduce the malware detection problem to the model checking problem of PDSs against SBPCARET formulas, and we propose an efficient algorithm to model check SBPCARET formulas for PDSs.

Introduction

The number of malware is growing fast in recent years. Traditional approaches including signature matching and code emulation are not efficient enough to detect malwares. While attackers can use obfuscation techniques to hide their malware from the signature based malware detectors easily, the code emulation approaches can only track programs in certain execution paths due to the limited execution time. To overcome these limitations, model-checking appears as an efficient approach for malware detection, since model-checking allows to check the behaviors of a program in all its execution traces without executing it.

A lof of works have been investigated to apply model-checking for malware detection [START_REF] Bergeron | Static detection of malicious code in executable programs[END_REF][START_REF] Kinder | Detecting malicious code by model checking[END_REF][START_REF] Christodorescu | Static analysis of executables to detect malicious patterns[END_REF][START_REF] Song | LTL model-checking for malware detection[END_REF][START_REF] Song | Efficient malware detection using model-checking[END_REF][START_REF] Song | Pushdown model checking for malware detection[END_REF][START_REF] Nguyen | CARET model checking for pushdown systems[END_REF]. [START_REF] Kinder | Detecting malicious code by model checking[END_REF] proposed to use finite state graphs to model the program and use the temporal logic CTPL to specify malicious behaviours. However, finite graphs are not exact enough to model programs, as they don't allow to take into account the program's stack into the model. Indeed, the program's stack is usually used by malware writers for code obfuscation as explained in [START_REF] Lakhotia | A method for detecting obfuscated calls in malicious binaries[END_REF]. In addition, in binary codes and assembly programs, parameters are passed to functions by pushing them on the stack before the call is made. The values of these parameters are used to determine whether the program is malicious or not [START_REF] Nguyen | CARET model checking for malware detection[END_REF]. Therefore, being able to record the program's stack is critical for malware detection. To this aim, [START_REF] Song | LTL model-checking for malware detection[END_REF][START_REF] Song | Efficient malware detection using model-checking[END_REF][START_REF] Song | Pushdown model checking for malware detection[END_REF][START_REF] Song | Pommade: pushdown model-checking for malware detection[END_REF] proposed to use pushdown systems to model programs, and defined extensions of LTL and CTL (called SLTPL and SCTPL) to precisely and compactly describe malicious behaviors. However, these logics cannot specify properties that require matchings of calls and returns, which is crucial to describe malicious behaviours [START_REF] Nguyen | Branching temporal logic of calls and returns for pushdown systems[END_REF]. Let us consider the typical behaviour of a spyware to illustrate this. The typical behaviour of a spyware is seeking personal information (emails, bank account information,...) on local drives by searching files that match specific conditions. To do that, it has to search directories of the host to look for interesting files whose names match a certain condition. If a file is found, the spyware will invoke a payload to steal the information, then continue looking for the remaining matching files. If a folder is found, it will pass into the folder path and continue investigating the folder recursively. To obtain this behavior, the spyware first calls the API F indF irstF ileA to search for the first matching file in a given folder path. After that, it has to check whether the call to the API function F indF irstF ileA is successful or not. When the function call fails, the spyware will call the API GetLastError. Otherwise, when the function call succeeds, a search handle h will be returned by F indF irstF ileA. There are two possibilities in this case. If the returned result is a folder, it will call the API function F indF irstF ileA again to search for matching results in the found folder. If the returned result is a file, it will call the function F indN extF ileA using h as first parameter to look for the remaining matching files. This behavior cannot be described by LTL or CTL since it requires to express that the return value of the API function F indF irstF ileA should be used as input to the function F indN extF ileA.

CARET was introduced to express linear-temporal properties that involve matchings of calls and returns [START_REF] Alur | A temporal logic of nested calls and returns[END_REF] and CARET model-checking for PDSs was considered [START_REF] Nguyen | CARET model checking for pushdown systems[END_REF][START_REF] Nguyen | CARET model checking for malware detection[END_REF]. However, the above behaviour cannot be described by CARET since it is a branching-time property. To specify that behaviour naturally and intuitively, BCARET was introduced to express these branching-time properties that involve matchings of calls and returns [START_REF] Nguyen | Branching temporal logic of calls and returns for pushdown systems[END_REF]. Using BCARET, the above behavior can be expressed by the following formula:

ϕ sb = d∈D EF g call(F indF irstF ileA) ∧ EX a (eax = d) ∧ AF a call(GetLastError) ∨ call(F indF irstF ileA) ∨ call(F indN extF ileA) ∧ dΓ *
where the is taken over all possible memory addresses d that contain the values of search handles h in the program, EX a is a BCARET operator saying that "next in some run, in the same procedural context"; EF g is the standard CTL EF operator (eventually in some run), while AF a is a BCARET operator stating that "eventually in all runs, in the same procedural context".

In binary codes and assembly programs, the return value of an API function is placed in the register eax. Therefore, the return value of F indF irstF ileA is the value of the register eax at the corresponding return-point of the call.

Then, the subformula (call(FindFirstFileA) ∧ EX a (eax = d)) expresses that there is a call to the API function F indF irstF ileA whose return value is d (the abstract successor of a call is its corresponding return-point). A call to FindNextFileA requires a search handle h as parameter and h must be put on top of the program's stack (as parameters are passed through the stack in assembly programs). To express that d is on top of the program stack, we use the regular expression dΓ * . Thus, the subformula [call(FindNextFileA) ∧ dΓ * ] states that the API FindNextFileA is invoked with d as parameter (d stores the information of the search handle h). Therefore, ϕ sb states that there is a call to the function F indF irstF ileA whose return value is d (the search handle), then, in all runs starting from that call, there will be either a call to the API GetLastError or a call to the API function F indF irstF ileA or a call to the function F indN extF ileA in which d is used as a parameter.

However, it can be seen that this formula is huge, since it considers the disjunction (of different BCARET formulas) over all possible memory addresses d which contain the information of search handles h in the program. To represent it in a more compact fashion, we follow the idea of [START_REF] Kinder | Detecting malicious code by model checking[END_REF][START_REF] Song | LTL model-checking for malware detection[END_REF][START_REF] Song | Pushdown model checking for malware detection[END_REF][START_REF] Nguyen | CARET model checking for malware detection[END_REF] and extend BCARET with variables, quantifiers, and predicates over the stack. We call our new logic SBPCARET. The above formula can be concisely described by a SBPCARET formula as follows:

ϕ sb = ∃xEF g call(F indF irstF ileA) ∧ EX a (eax = x) ∧ AF a call(GetLastError) ∨ call(F indF irstF ileA) ∨ call(F indN extF ileA) ∧ xΓ *
Thus, we propose in this work to use pushdown systems (PDSs) to model programs, and SBPCARET formulas to specify malicious behaviors. We reduce the malware detection problem to the model checking problem of PDSs against SBPCARET formulas, and we propose an efficient algorithm to check whether a PDS satisfies a SBPCARET formula. Our algorithm is based on a reduction to the emptiness problem of Symbolic Alternating Büchi Pushdown Systems. This latter problem is already solved in [START_REF] Song | Pushdown model checking for malware detection[END_REF].

The rest of paper is organized as follows. In Section 2, we recall the definitions of Pushdown Systems. Section 3 introduces our logic SBPCARET. Model checking SBPCARET for PDSs is presented in Section 4. Finally, we conclude in Section 5.

Pushdown Systems: A model for sequential programs

Pushdown systems is a natural model that was extensively used to model sequential programs. Translations from sequential programs to PDSs can be found e.g. in [START_REF] Schwoon | Model-Checking Pushdown Systems[END_REF]. As will be discussed in the next section, to precisely describe malicious behaviors as well as context-related properties, we need to keep track of the call and return actions in each path. Thus, as done in [START_REF] Nguyen | Branching temporal logic of calls and returns for pushdown systems[END_REF], we adapt the PDS model in order to record whether a rule of a PDS corresponds to a call, a return, or another instruction. We call this model a Labelled Pushdown System. We also extend the notion of run in order to take into account matching returns of calls. Definition 1. A Labelled Pushdown System (PDS) P is a tuple (P, Γ, ∆, ), where P is a finite set of control locations, Γ is a finite set of stack alphabet, / ∈ Γ is a bottom stack symbol and ∆ is a finite subset of ((P × Γ ) × (P × Γ * ) × {call, ret, int}). If ((p, γ), (q, ω), t) ∈ ∆ (t ∈ {call, ret, int}), we also write p, γ t -→ q, ω ∈ ∆. Rules of ∆ are of the following form, where p ∈ P, q ∈ P, γ, γ 1 , γ 2 ∈ Γ , and ω ∈ Γ * :

-(r 1 ): p, γ call --→ q, γ 1 γ 2 -(r 2 ): p, γ ret --→ q, -(r 3 ): p, γ int --→ q, ω
Intuitively, a rule of the form p, γ call --→ q, γ 1 γ 2 corresponds to a call statement. Such a rule usually models a statement of the form γ call proc ------→ γ 2 . In this rule, γ is the control point of the program where the function call is made, γ 1 is the entry point of the called procedure, and γ 2 is the return point of the call. A rule r 2 models a return, whereas a rule r 3 corresponds to a simple statement (neither a call nor a return). A configuration of P is a pair p, ω , where p is a control location and ω ∈ Γ * is the stack content. For technical reasons, we suppose w.l.o.g. that the bottom stack symbol is never popped from the stack, i.e., there is no rule in the form p, t -→ q, ω ∈ ∆ (t ∈ {call, ret, int}). P defines a transition relation = ⇒ P (t ∈ {call, ret, int}) as follows: If p, γ t -→ q, ω , then for every ω ∈ Γ * , p, γω = ⇒ P q, ωω . In other words, q, ωω is an immediate successor of p, γω . Let * = ⇒ P be the reflexive and transitive closure of = ⇒ P . A run of P from p 0 , ω 0 is a sequence p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... where p i , ω i ∈ P ×Γ * s.t. for every i ≥ 0, p i , ω i = ⇒ P p i+1 , ω i+1 . Given a configuration p, ω , let T races( p, ω ) be the set of all possible runs starting from p, ω .

Global and abstract successors

Let π = p 0 , ω 0 p 1 , ω 1 ... be a run starting from p 0 , ω 0 . Over π, two kinds of successors are defined for every position p i , ω i :

global-successor : The global-successor of p i , ω i is p i+1 , ω i+1 where p i+1 , ω i+1 is an immediate successor of p i , ω i . abstract-successor : The abstract-successor of p i , ω i is determined as follows: For example, in Figure 1: -The global-successors of p 1 , ω 1 and p 2 , ω 2 are p 2 , ω 2 and p 3 , ω 3 respectively.

• If p i , ω i = ⇒ P p i+1 ,
-The abstract-successors of p 2 , ω 2 and p 5 , ω 5 are p k , ω k and p 9 , ω 9 respectively.

Let p, ω be a configuration of a PDS P. A configuration p , ω is defined as a global-successor of p, ω iff p , ω is a global-successor of p, ω over a run π ∈ T races( p, ω ). Similarly, a configuration p , ω is defined as an abstractsuccessor of p, ω iff p , ω is an abstract-successor of p, ω over a run π ∈ T races( p, ω )

A global-path of P from p 0 , ω 0 is a sequence p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... where p i , ω i ∈ P × Γ * s.t. for every i ≥ 0, p i+1 , ω i+1 is a global-successor of p i , ω i .

Similarly, an abstract-path of P from p 0 , ω 0 is a sequence p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... where p i , ω i ∈ P ×Γ * s.t. for every i ≥ 0, p i+1 , ω i+1 is an abstract-successor of p i , ω i . For instance, in Figure 1, p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 p 3 , ω 3 p 4 , ω 4 p 5 , ω 5 ... is a global-path, while p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 p k , ω k ... is an abstract-path.

Malicious Behaviour Specification

In this section, we define the Stack Branching temporal Predicate logic of CAlls and RETurns (SBPCARET) as an extension of BCARET [START_REF] Nguyen | Branching temporal logic of calls and returns for pushdown systems[END_REF] with variables and regular predicates over the stack contents. The predicates contain variables that can be quantified existentially or universally. Regular predicates are expressed by regular variable expressions and are used to describe the stack content of PDSs.

Environments, Predicates and Regular Variable Expressions

Let X = {x 1 , ..., x n } be a finite set of variables over a finite domain D. Let B : X ∪ D → D be an environment that associates each variable x ∈ X with a value d ∈ D s.t B(d) = d for every d ∈ D. Let B[x ← d] be an environment obtained from B such that B[x ← d](x) = d and B[x ← d](y) = B(y) for every y = x. Let Abs x (B) = {B ∈ B | ∀y ∈ X , y = x, B(y) = B (
y)} be the function that abstracts away the value of x. Let B be the set of all environments.

Let AP = {a, b, c, ...} be a finite set of atomic propositions. Let AP D be a finite set of atomic predicates of the form b(α 1 , ..., α m ) such that b ∈ AP and α i ∈ D for every 1 ≤ i ≤ m. Let AP X be a finite set of atomic predicates b(α 1 , ..., α n ) such that b ∈ AP and α i ∈ X ∪ D for every 1 ≤ i ≤ n.

Let P = (P, Γ, ∆) be a Labelled PDS. A Regular Variable Expression (RVE) e over X ∪ Γ is defined by e ::= | a ∈ X ∪ Γ | e + e | e.e | e * . The language L(e) of a RVE e is a subset of P × Γ * × B and is defined as follows:

-L( ) = {( p, , B) | p ∈ P, B ∈ B} -for x ∈ X , L(x) = {( p, γ , B) | p ∈ P, γ ∈ Γ, B ∈ B s.t B(x) = γ} -for γ ∈ Γ , L(γ) = {( p, γ , B) | p ∈ P, B ∈ B} -L(e 1 .e 2 ) = {( p, ω ω , B) | ( p, ω , B) ∈ L(e 1 ); ( p, ω , B) ∈ L(e 2 )} -L(e * ) = {( p, ω , B) | ω ∈ {v ∈ Γ * | ( p, v , B) ∈ L(e)} * }

The Stack Branching temporal Predicate logic of CAlls and RETurns -SBPCARET

A SBPCARET formula is a BCARET formula where predicates and RVEs are used as atomic propositions and where quantifiers are applied to variables. For technical reasons, we assume w.l.o.g. that formulas are written in positive normal form, where negations are applied only to atomic predicates, and we use the release operator R as the dual of the until operator U . From now on, we fix a finite set of variables X , a finite set of atomic propositions AP , a finite domain D, and a finite set of RVEs V. A SBPCARET formula is defined as follows,

where v ∈ {g, a}, x ∈ X , e ∈ V, b(α 1 , ..., α n ) ∈ AP X : ϕ :=true | f alse | b(α1, ..., αn) | ¬b(α1, ..., αn) | e | ¬e | ϕ ∨ ϕ | ϕ ∧ ϕ | ∀xϕ | ∃xϕ | EX v ϕ | AX v ϕ | E[ϕU v ϕ] | A[ϕU v ϕ] | E[ϕR v ϕ] | A[ϕR v ϕ]
Let λ : P -→ 2 AP D be a labelling function which associates each control location to a set of atomic predicates. Let ϕ be a SBPCARET formula over AP . Let p, ω be a configuration of P. Then we say that P satisfies ϕ at p, ω (denoted by p, ω |= λ ϕ) iff there exists an environment B ∈ B such that p, ω satisfies ϕ under B (denoted by p, ω |= B λ ϕ). The satisfiability relation of a SBPCARET formula ϕ at a configuration p 0 , ω 0 under the environment B w.r.t. the labelling function λ, denoted by p 0 , ω 0 B λ ϕ, is defined inductively as follows:

-p 0 , ω 0 B λ true for every p 0 , ω 0 -p 0 , ω 0 B λ f alse for every p 0 , ω 0 -p 0 , ω 0 B λ b(α 1 , ..., α n ), iff b(B(α 1 ), ..., B(α n )) ∈ λ(p 0 ) -p 0 , ω 0 B λ ¬b(α 1 , ..., α n ), iff b(B(α 1 ), ..., B(α n )) / ∈ λ(p 0 ) -p 0 , ω 0 B λ e iff ( p 0 , ω 0 , B) ∈ L(e) -p 0 , ω 0 B λ ¬e iff ( p 0 , ω 0 , B) / ∈ L(e) -p 0 , ω 0 B λ ϕ 1 ∨ ϕ 2 iff ( p 0 , ω 0 B λ ϕ 1 or p 0 , ω 0 B λ ϕ 2 ) -p 0 , ω 0 B λ ϕ 1 ∧ ϕ 2 iff ( p 0 , ω 0 B λ ϕ 1 and p 0 , ω 0 B λ ϕ 2 ) -p 0 , ω 0 B λ ∀xϕ iff for every d ∈ D, p 0 , ω 0 B[x←d] λ ϕ -p 0 , ω 0 B λ ∃xϕ iff there exists d ∈ D, p 0 , ω 0 B[x←d] λ ϕ -p 0 , ω 0 B λ EX g ϕ iff there exists a global-successor p , ω of p 0 , ω 0 such that p , ω B λ ϕ -p 0 , ω 0 B λ AX g ϕ iff p , ω B λ ϕ for every global-successor p , ω of p 0 , ω 0 -p 0 , ω 0 B λ E[ϕ 1 U g ϕ 2 ]
iff there exists a global-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... of P starting from p 0 , ω 0 s.t. ∃i ≥ 0, p i , ω i B λ ϕ 2 and for every 0

≤ j < i, p j , ω j B λ ϕ 1 -p 0 , ω 0 B λ A[ϕ 1 U g ϕ 2 ]
iff for every global-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ...of P starting from p 0 , ω 0 , ∃i ≥ 0, p i , ω i B λ ϕ 2 and for every 0

≤ j < i, p j , ω j B λ ϕ 1 -p 0 , ω 0 B λ E[ϕ 1 R g ϕ 2 ]
iff there exists a global-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... of P starting from p 0 , ω 0 s.t. for every i ≥ 0, if p i , ω i B λ ϕ 2 then there exists 0

≤ j < i s.t. p j , ω j B λ ϕ 1 -p 0 , ω 0 B λ A[ϕ 1 R g ϕ 2 ] iff for every global-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... of P starting from p 0 , ω 0 , for every i ≥ 0, if p i , ω i B λ ϕ 2 then there exists 0 ≤ j < i s.t. p j , ω j B λ ϕ 1 -p 0 , ω 0 B λ EX a ϕ iff there exists an abstract-successor p , ω of p 0 , ω 0 such that p , ω B λ ϕ -p 0 , ω 0 B λ AX a ϕ iff p , ω B λ ϕ for every abstract-successor p , ω of p 0 , ω 0 -p 0 , ω 0 B λ E[ϕ 1 U a ϕ 2 ] iff there exists an abstract-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... of P starting from p 0 , ω 0 s.t. ∃i ≥ 0, p i , ω i B λ ϕ 2 and for every 0 ≤ j < i, p j , ω j B λ ϕ 1 -p 0 , ω 0 B λ A[ϕ 1 U a ϕ 2 ] iff for every abstract-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... of P, ∃i ≥ 0, p i , ω i B λ ϕ 2 and for every 0 ≤ j < i, p j , ω j B λ ϕ 1 -p 0 , ω 0 B λ E[ϕ 1 R a ϕ 2 ] iff there exists an abstract-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... of P starting from p 0 , ω 0 s.t. for every i ≥ 0, if p i , ω i B λ ϕ 2 then there exists 0 ≤ j < i s.t. p j , ω j B λ ϕ 1 -p 0 , ω 0 B λ A[ϕ 1 R a ϕ 2 ] iff for every abstract-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω 2 ... of P starting from p 0 , ω 0 , for every i ≥ 0, if p i , ω i B λ ϕ 2 then there exists 0 ≤ j < i s.t. p j , ω j B λ ϕ 1
Other SBPCARET operators can be expressed by the above operators:

EF g ϕ = E[true U g ϕ], EF a ϕ = E[true U a ϕ], AF g ϕ = A[true U g ϕ], AF a ϕ = A[trueU a ϕ],...
Closure. Given a SBPCARET formula ϕ, the closure Cl(ϕ) is the set of all subformulae of ϕ, including ϕ.

Let AP + (ϕ) = {b(α 1 , ..., α n ) ∈ AP X | b(α 1 , ..., α n ) ∈ Cl(ϕ)}; AP -(ϕ) = {b(α 1 , ..., α n ) ∈ AP X | ¬b(α 1 , ..., α n ) ∈ Cl(ϕ)}, Reg + (ϕ) = {e ∈ V | e ∈ Cl(ϕ)}, Reg -(ϕ) = {e ∈ V | ¬e ∈ Cl(ϕ)}

SBPCARET Model-Checking for Pushdown Systems

In this section, we show how to do SBPCARET model-checking for PDSs. Let then P be a PDS, ϕ be a SBPCARET formula, and V be the set of RVEs occuring in ϕ. We follow the idea of [START_REF] Song | Pushdown model checking for malware detection[END_REF] and use Variable Automata to represent RVEs.

Variable Automata

Given a PDS P = (P, Γ, ∆) s.t. Γ ⊆ D, a Variable Automaton (VA) [START_REF] Song | Pushdown model checking for malware detection[END_REF] is a tuple (Q, Γ, δ, s, F ), where Q is a finite set of states, Γ is the input alphabet, s ∈ Q is an initial state; F ⊆ Q is a finite set of accepting states; and δ is a finite set of transition rules of the form p α -→ {q 1 , ..., q n } where α can be x, ¬x, or γ, for any x ∈ X and γ ∈ Γ .

Let B ∈ B. A run of VA on a word γ 1 , ..., γ m under B is a tree of height m whose root is labelled by the initial state s, and each node at depth k labelled by a state q has h children labelled by p 1 , ..., p h respectively, such that:

-either q γ k -→ {p 1 , ..., p h } ∈ δ and γ k ∈ Γ ; -or q x -→ {p 1 , ..., p h } ∈ δ, x ∈ X and B(x) = γ k ; -or q ¬x --→ {p 1 , ..., p h } ∈ δ, x ∈ X and B(x) = γ k .
A branch of the tree is accepting iff the leaf of the branch is an accepting state. A run is accepting iff all its branches are accepting. A word ω ∈ Γ * is accepted by a VA under an environment B ∈ B iff the VA has an accepting run on the word ω under the environment B.

The language of a VA M , denoted by L(M ), is a subset of (P A configuration of a SABPDS BP is a tuple p, B , ω , where p ∈ P is the current control location, B ∈ B is an environment and ω ∈ Γ * is the cur-

× Γ * ) × B. ( p, ω , B) ∈ L(M ) iff M
rent stack content. Let p, γ R -→ { p 1 , ω 1 , ..., p n , ω n } be a rule of ∆, then, for every ω ∈ Γ * , B, B 1 , ..., B n ∈ B, if B ∈ R(B 1 , ..., B n ), then the config- uration p, B , γω (resp. { p 1 , B 1 , ω 1 ω , ..., p n , B n , ω n ω }) is an immedi- ate predecessor (resp. successor) of { p 1 , B 1 , ω 1 ω , ..., p n , B n , ω n ω } (resp.
p, B , γω ).

A run ρ of a SABPDS BP starting form an initial configuration p 0 , B 0 , ω 0 is a tree whose root is labelled by p 0 , B 0 , ω 0 , and whose other nodes are labelled by elements in P × B × Γ * . If a node of ρ is labelled by a configuration p, B , ω and has n children labelled by p 1 , B 1 , ω 1 , ..., p n , B n , ω n respectively, then, p, B , ω must be a predecessor of { p 1 , B 1 , ω 1 , ..., p n , B n , ω n } in BP. A path of a run ρ is an infinite sequence of configurations c 0 c 1 c 2 ... s.t. c 0 is the root of ρ and c i+1 is one of the children of c i for every i ≥ 0. A path is accepting iff it visits infinitely often configurations with control locations in F . A run ρ is accepting iff every path of ρ is accepting. The language of BP, L(BP), is the set of configurations c s.t. BP has an accepting run starting from c.

BP defines the reachability relation = ⇒ BP : 2 (P ×B)×Γ * → 2 (P ×B)×Γ * as follows: [START_REF] Alur | A temporal logic of nested calls and returns[END_REF]

c = ⇒ BP {c} for every c ∈ P × B × Γ * , (2) c = ⇒ BP C if C is an immediate successor of c; (3) if c = ⇒ BP {c 1 , c 2 , ..., c n } and c i = ⇒ BP C i for every 1 ≤ i ≤ n, then c = ⇒ BP n i=1 C i . Given c 0 = ⇒ BP C ,
then, BP has an accepting run from c 0 iff BP has an accepting run from c for every c ∈ C . Theorem 3. [START_REF] Song | Pushdown model checking for malware detection[END_REF] The membership problem of SABPDS can be solved effectively.

Functions of R.

In what follows, we define several functions of R which will be used in the next sections. These functions were first defined in [START_REF] Song | Pushdown model checking for malware detection[END_REF].

1. id(B) = {B}. This is the identity function. 2.

equal(B 1 , ..., B n ) = {B 1 } if B i = B j for every 1 ≤ i, j ≤ n; ∅ otherwise
This function checks whether all the environments are equal and returns {B 1 } (which is also equal to B i for every i). Otherwise, it returns the emptyset. 3.

meet x {c1,...,cn} (B 1 , ..., B n ) =      Abs x (B 1 ) if B i (x) = c i for 1 ≤ i ≤ n,
and

B i (y) = B j (y) for y = x, 1 ≤ i, j ≤ n; ∅ otherwise
This function checks whether (1) B i (x) = c i for every 1 ≤ i ≤ n (2) for every y = x; every 1 ≤ i, j ≤ n B i (y) = B j (y). If the conditions are satisfied, it returns Abs x (B 1 )1 , otherwise it returns the emptyset. 4.

join x c (B 1 , ..., B n ) =      B 1 if B i (x) = c for 1 ≤ i ≤ n and B i = B j for 1 ≤ i, j ≤ n; ∅ otherwise
This function checks whether B i (x) = c for every i. If this condition is satisfied, equal(B 1 , ..., B n ) is returned, otherwise, the emptyset is returned. 5.

join ¬x c (B 1 , ..., B n ) =          B 1 if B i (x) = c for 1 ≤ i ≤ n and B i = B j for 1 ≤ i, j ≤ n; ∅ otherwise
This function checks whether B i (x) = c for every i. If this condition is satisfied, equal(B 1 , ..., B n ) is returned, otherwise, the emptyset is returned.

From SBPCARET model checking of PDSs to the membership problem in SABPDSs

Let P = (P, Γ, ∆) be a PDS. We suppose w.l.o.g. that P has a bottom stack symbol that is never popped from the stack. Let AP be a set of atomic propositions. Let ϕ be a SBPCARET formula over AP , λ : P -→ 2 AP D be a labelling function. Given a configuration p 0 , ω 0 , we propose in this section an algorithm to check whether p 0 , ω 0 λ ϕ, i.e., whether there exists an environment B s.t. p 0 , ω 0 B λ ϕ. Intuitively, we compute an SABPDS BP ϕ s.t. p, ω B λ ϕ iff p, ϕ , B , ω ∈ L(BP ϕ ) for every p ∈ P , ω ∈ Γ * , B ∈ B. Then, to check if p 0 , ω 0 λ ϕ, we will check whether there exists a B ∈ B s.t. p 0 , ϕ , B , ω 0 ∈ L(BP ϕ ). Let Reg + (ϕ) = {e 1 , ..., e k } and Reg -(ϕ) = {e k+1 , ..., e m }. Using Theorems 1 and 2; for every 1 ≤ i ≤ k, we can compute a VA M ei = (Q ei , Γ, δ ei , s ei , F ei ) s.t. L(M ei ) = L(e i ). In addition, for every k + 1 ≤ j ≤ m, we can compute a VA M ¬ej = (Q ¬ej , Γ, δ ¬ej , s ¬ej , F ¬ej ) s.t. L(M ¬ej ) = (P × Γ * ) × B \ L(e j ). Let M be the union of all these automata, S and F be respectively the union of all states and final states of these automata.

Let BP ϕ = (P , Γ , ∆ , F ) be the SABPDS defined as follows:

-

P = P ∪ (P × Cl(ϕ)) ∪ S ∪ {p ⊥ } -Γ = Γ ∪ (Γ × Cl(ϕ)) ∪ {γ ⊥ } -F = F 1 ∪ F 2 ∪ F 3 ∪ F 4 where • F 1 = { p, b(α 1 , ..., α n ) , β | b(α 1 , ..., α n ) ∈ AP + (ϕ), and β = {B ∈ B | b(B(α 1 ), ..., B(α n )) ∈ λ(p)} • F 2 = { p, ¬b(α 1 , ..., α n ) , β | b(α 1 , ..., α n ) ∈ AP -(ϕ), and β = {B ∈ B | b(B(α 1 ), ..., B(α n )) / ∈ λ(p)} • F 3 = P × Cl R (ϕ) × B where Cl R (ϕ) is the set of formulas of Cl(ϕ) in the form E[ϕ 1 R v ϕ 2 ] or A[ϕ 1 R v ϕ 2 ] (v ∈ {g, a}) • F 4 = F × B
The transition relation ∆ is the smallest set of transition rules defined as follows: For every p ∈ P , φ ∈ Cl(ϕ), γ ∈ Γ and t ∈ {call, ret, int}:

( 1) If φ = b(α 1 , ..., α n ), then, p, φ , γ id -→ p, φ , γ ∈ ∆ ( 2) If φ = ¬b(α 1 , ..., α n ), then, p, φ , γ id -→ p, φ , γ ∈ ∆ ( 3) If φ = φ 1 ∧ φ 2 , then, p, φ , γ equal ---→ [ p, φ 1 , γ , p, φ 2 , γ ] ∈ ∆ ( 4) If φ = φ 1 ∨ φ 2 , then, p, φ , γ id -→ p, φ 1 , γ ∈ ∆ and p, φ , γ id -→ p, φ 2 , γ ∈ ∆ ( 5) If φ = ∃xφ 1 , then, p, φ , γ meet x {c} -----→ p, φ 1 , γ ∈ ∆ for every c ∈ D ( 6) If φ = ∀xφ 1 , then, p, φ , γ meet x D ----→ [ p, φ 1 , γ , ..., p, φ 1 , γ ] ∈ ∆ where p, φ 1 , γ is repeated m times in the right-hand side, where m is the number of elements in D ( 7) If φ = EX g φ 1 , then p, φ , γ id -→ q, φ 1 , ω ∈ ∆ for every p, γ t - → q, ω ∈ ∆ ( 8) If φ = AX g φ 1 , then, p, φ , γ equal ---→ [ q 1 ,
φ 1 , ω 1 , ..., q n , φ 1 , ω n ] ∈ ∆ , where for every 1 ≤ i ≤ n, p, γ t -→ q i , ω i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ t -→ q, ω that have p, γ on the left hand side.

( 9) If φ = EX a φ 1 , then, (a) p, φ , γ id -→ q, γ γ , φ 1 ∈ ∆ for every p, γ call --→ q, γ γ ∈ ∆ (b) p, φ , γ id -→ q, φ 1 , ω ∈ ∆ for every p, γ int --→ q, ω ∈ ∆ (c) p, φ , γ id -→ p ⊥ , γ ⊥ ∈ ∆ for every p, γ ret --→ q , ∈ ∆ ( 10) If φ = AX a φ 1 , then, p, φ , γ equal ---→ [ p 1 , γ 1 γ 1 , φ 1 , ..., p m , γ m γ m , φ 1 , q 1 , φ 1 , ω 1 , ..., q n , φ 1 , ω n , p ⊥ , γ ⊥ , ..., p ⊥ , γ ⊥ ] ∈ ∆ ,
where p ⊥ , γ ⊥ is repeated k times in the righthand side s.t.: (a) for every 1 ≤ i ≤ m, p, γ call --→ p i , γ i γ i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ call --→ q, γ γ that have p, γ on the left hand side. (b) for every 1 ≤ i ≤ n, p, γ int --→ q i , ω i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ int --→ q, ω that have p, γ on the left hand side. (c) for every 1 ≤ i ≤ k, p, γ ret --→ q i , ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ ret --→ q , that have p, γ on the left hand side. [START_REF] Song | Efficient malware detection using model-checking[END_REF]

If φ = E[φ 1 U g φ 2 ], then, (a) p, φ , γ id -→ p, φ 2 , γ ∈ ∆ (b) p, φ , γ equal ---→ [ p, φ 1 , γ , q, φ , ω ] ∈ ∆ for every p, γ t - → q, ω ∈ ∆ ( 12) If φ = E[φ 1 U a φ 2 ], then, (a) p, φ , γ id -→ p, φ 2 , γ ∈ ∆ (b) p, φ , γ equal ---→ [ p, φ 1 , γ , q, γ γ , φ ] ∈ ∆ for every p, γ call --→ q, γ γ ∈ ∆ (c) p, φ , γ equal ---→ [ p, φ 1 , γ , q, φ , ω ] ∈ ∆ for every p, γ int --→ q, ω ∈ ∆ (d) p, φ , γ id -→ p ⊥ , γ ⊥ ∈ ∆ for every p, γ ret --→ q , ∈ ∆ ( 13) If φ = A[φ 1 U g φ 2 ], then, (a) p, φ , γ id -→ p, φ 2 , γ ∈ ∆ (b) p, φ , γ equal ---→ [ p, φ 1 , γ ; q 1 ,
φ , ω 1 , ..., q n , φ , ω n ] ∈ ∆ where for every 1 ≤ i ≤ n, p, γ t -→ q i , ω i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ t -→ q, ω that have p, γ on the left hand side.

( 14) If φ = A[φ 1 U a φ 2 ], then, (a) p, φ , γ id -→ p, φ 2 , γ ∈ ∆ (b) p, φ , γ equal ---→ [ p, φ 1 , γ ; p 1 , γ 1 γ 1 , φ , ..., p m , γ m γ m , φ ; q 1 ,
φ , ω 1 , ..., q n , φ , ω n , p ⊥ , γ ⊥ , ..., p ⊥ , γ ⊥ ] ∈ ∆ , where p ⊥ , γ ⊥ is repeated k times in the right-hand side s.t.:

for every 1 ≤ i ≤ m, p, γ call --→ p i , γ i γ i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ call --→ q, γ γ that have p, γ on the left hand side.

for every 1 ≤ i ≤ n, p, γ int --→ q i , ω i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ int --→ q, ω that have p, γ on the left hand side.

for every 1 ≤ i ≤ k, p, γ ret --→ q i , ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ ret --→ q , that have p, γ on the left hand side.

( 15) If φ = E[φ 1 R g φ 2 ]
, then, we add to ∆ the rule:

(a) p, φ , γ equal ---→ [ p, φ 2 , γ , p, φ 1 , γ ] ∈ ∆ (b) p, φ , γ equal ---→ [ p, φ 2 , γ , q, φ , ω ] ∈ ∆ for every p, γ t - → q, ω ∈ ∆ ( 16) If φ = A[φ 1 R g φ 2 ]
, then, we add to ∆ the rule:

(a) p, φ , γ equal ---→ [ p, φ 2 , γ , p, φ 1 , γ ] ∈ ∆ (b) p, φ , γ equal ---→ [ p, φ 2 , γ ; q 1 ,
φ , ω 1 , ..., q n , φ , ω n ] ∈ ∆ where for every 1 ≤ i ≤ n, p, γ t -→ q i , ω i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ t -→ q, ω that have p, γ on the left hand side.

( 17) If φ = E[φ 1 R a φ 2 ], then, (a) p, φ , γ equal ---→ [ p, φ 2 , γ , p, φ 1 , γ ] ∈ ∆ (b) p, φ , γ equal ---→ [ p, φ 2 , γ , q, γ γ , φ ] ∈ ∆ for every p, γ call --→ q, γ γ ∈ ∆ (c) p, φ , γ equal ---→ [ p, φ 2 , γ , q, φ , ω ] ∈ ∆ for every p, γ int --→ q, ω ∈ ∆ (d) p, φ , γ id -→ p ⊥ , γ ⊥ ∈ ∆ for every p, γ ret --→ q , ∈ ∆ ( 18) If φ = A[φ 1 R a φ 2 ], then, (a) p, φ , γ equal ---→ [ p, φ 2 , γ , p, φ 1 , γ ] ∈ ∆ (b) p, φ , γ equal ---→ [ p, φ 2 , γ ; p 1 , γ 1 γ 1 , φ , ..., p m , γ m γ m , φ ; q 1 , φ , ω 1 , ..., q n , φ , ω n , p ⊥ , γ ⊥ , ..., p ⊥ , γ ⊥ ] ∈ ∆ , where p ⊥ , γ ⊥ is repeated k times in the right-hand side s.t.:
for every 1 ≤ i ≤ m, p, γ call --→ p i , γ i γ i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ call --→ q, γ γ that have p, γ on the left hand side.

for every 1 ≤ i ≤ n, p, γ int --→ q i , ω i ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ int --→ q, ω that have p, γ on the left hand side.

for every 1 ≤ i ≤ k, p, γ ret --→ q i , ∈ ∆ and these transitions are all the transitions of ∆ that are in the form p, γ ret --→ q , that have p, γ on the left hand side.

( 19) for every p, γ ret --→ q, ∈ ∆:

-q, γ , φ 1 id -→ q, φ 1 , γ ∈ ∆ for every γ ∈ Γ , φ 1 ∈ Cl(ϕ) ( 20) p ⊥ , γ ⊥ id -→ p ⊥ , γ ⊥ ∈ ∆ ( 21) for every p, γ t - → q, ω ∈ ∆: p, γ id -→ q, ω ∈ ∆ ( 22) If φ = e, e is a regular expression, then, p, φ , γ id -→ s e , γ ∈ ∆ ( 23) If φ = ¬e, e is a regular expression, then, p, φ , γ id -→ s ¬e , γ ∈ ∆ ( 24) for every transition q α -→ {q 1 , .., q n } in M: q, γ R -→ [ q 1 , , ..., q n , ] ∈ ∆ , where: (a) R = equal iff α = γ (b) R = join x γ iff α = x ∈ X (c) R = join ¬x γ iff α = ¬x and x ∈ X ( 25) for every q ∈ F, q, id -→ q, ∈ ∆
Roughly speaking, the SABPDS BP ϕ is a kind of product between P and the SBPCARET formula ϕ which ensures that BP ϕ has an accepting run from p, ϕ , B , ω iff the configuration p, ω satisfies ϕ under the environment B. The form of the control locations of BP ϕ is p, φ , B where φ ∈ Cl(ϕ), B ∈ B.

Let us explain the intuition behind our construction:

-If φ = b(α 1 , ..., α n ), then, for every ω ∈ Γ * , p, ω B λ φ iff b(B(α 1 ), ..., B(α n )) ∈ λ(p). Thus, for such a B, BP ϕ should have an accepting run from p, b(α 1 , ..., α n ) , B , ω iff b(B(α 1 ), ..., B(α n )) ∈ λ(p). This is ensured by the transition rules in ( 1) which add a loop at p, b(α 1 , ..., α n ) , B , ω and the fact that p, b(α 1 , ..., α n ) , B ∈ F (because it is in F 1 ). The function id in ( 1) ensures that the environments before and after are the same.

-If φ = ¬b(α 1 , ..., α n ), then, for every ω ∈ Γ * , p, ω B λ φ iff b(B(α 1 ), ..., B(α n )) / ∈ λ(p). Thus, for such a B, BP ϕ should have an accepting run from p, ¬b(α 1 , ..., α n ) , B , ω iff b(B(α 1 ), ..., B(α n )) / ∈ λ(p). This is ensured by the transition rules in ( 2) which add a loop at p, ¬b(α 1 , ..., α n ) , B , ω and the fact that p, ¬b(α 1 , ..., α n ) , B ∈ F (because it is in F 2 ). The function id in ( 2) ensures that the environments before and after are the same.

-If φ = φ 1 ∧ φ 2 , then, for every ω ∈ Γ * , p, ω B λ φ iff ( p, ω B λ φ 1 and p, ω B λ φ 2 )
. This is ensured by the transition rules in ( 3) stating that BP ϕ has an accepting run from p, φ 1 ∧φ 2 , B , ω iff BP ϕ has an accepting run from both p, φ 1 , B , ω and p, φ 2 , B , ω .

p, φ 1 , B[x ← c] , ω since B ∈ meet x {c} (B[x ← c]) -If φ = ∀xφ 1 , then, for every ω ∈ Γ * , p, ω B λ φ iff for every c ∈ D, p, ω B[x←c] λ
φ 1 . This is ensured by the transition rules in ( 6) stating that BP ϕ has an accepting run from p, ∀xφ 1 , B , ω iff for every c ∈ D, BP ϕ has an accepting run from

p, φ 1 , B[x ← c] , ω since if D = {c 1 , ..., c m }, then, B ∈ meet x D (B[x ← c 1 ], ..., B[x ← c m ]) -If φ = EX g φ 1 ,
then, for every ω ∈ Γ * , p, ω B λ φ iff there exists an immediate successor p , ω of p, ω s.t. p , ω B λ φ 1 . This is ensured by the transition rules in [START_REF] Nguyen | CARET model checking for pushdown systems[END_REF] stating that BP ϕ has an accepting run from p, EX g φ 1 , B , ω iff there exists an immediate successor p , ω of p, ω s.t. BP ϕ has an accepting run from p , φ 1 , B , ω . ( 8) is similar to [START_REF] Nguyen | CARET model checking for pushdown systems[END_REF].

-

If φ = E[φ 1 U g φ 2 ], then, for every ω ∈ Γ * , p, ω B λ φ iff p, ω B λ φ 2 or ( p, ω B
λ φ 1 and there exists an immediate successor p , ω of p, ω s.t. p , ω B λ φ). This is ensured by the transition rules in [START_REF] Song | Efficient malware detection using model-checking[END_REF] stating that BP ϕ has an accepting run from p, E[φ 1 U g φ 2 ] , B , ω iff BP ϕ has an accepting run from p, φ 2 , B , ω (by the rules in ( 11)(a)) or (BP ϕ has an accepting run from both p, φ 1 , B , ω and p , φ , B , ω where p , ω is an immediate successor of p, ω ) (by the rules in ( 11)(b)). ( 13) is similar to [START_REF] Song | Efficient malware detection using model-checking[END_REF].

-

If φ = E[φ 1 R g φ 2 ]
, then, for every ω ∈ Γ * , p, ω B λ φ iff ( p, ω B λ φ 2 and p, ω B λ φ 1 ) or ( p, ω B λ φ 2 and there exists an immediate successor p , ω of p, ω s.t. p , ω B λ φ). This is ensured by the transition rules in ( 15) stating that BP ϕ has an accepting run from p, E[φ 1 R g φ 2 ] , B , ω iff BP ϕ has an accepting run from both p, φ 2 , B , ω and p, φ 1 , B , ω (by the rules in ( 15)(a)); or BP ϕ has an accepting run from both p, φ 2 , B , ω and p , φ , B , ω where p , ω is an immediate successor of p, ω (by the rules in ( 15)(b)). In addition, for R g formulas, the stop condition is not required, i.e, for a formula φ 1 R g φ 2 that is applied to a specific run, we don't require that φ 1 must eventually hold. To ensure that the runs on which φ 2 always holds are accepted, we add p, φ , B to the Büchi accepting condition F (via the subset F 3 of F ). ( 16) is similar to ( 15). γ by the rule in ( 9)(a) stating that p, EX a φ 1 , γ id -→ p , γ γ , φ 1 ∈ ∆ . This allows to record φ 1 in the corresponding return point of the stack. After that, the rules in ( 21) allow BP ϕ to mimic the run π of P from p , ω till the corresponding return-point of this call, where γ , φ 1 is the topmost stack symbol. More specifically, the following sequence of P: p , γ γ ω * = ⇒ P p k-1 , βγ ω * = ⇒ P p k , γ ω will be mimicked by the following sequence of BP ϕ : p , B , γ γ , φ 1 ω = ⇒ BPϕ p k-1 , B , β γ , φ 1 ω = ⇒ BPϕ p k , B , γ , φ 1 ω using the rules of ( 21). At the return-point, we extract φ 1 from the stack and encode it into p k by adding the transition rules in ( 19) p k , γ , φ 1 id -→ p k , φ 1 , γ . Therefore, we obtain that p, φ , B , ω = ⇒ BPϕ p k , φ 1 , B , ω k . The property holds for this case.

• If p, ω = ⇒ P p , ω corresponds to a simple statement. Then, the abstract successor of p, ω is its immediate successor p , ω . Thus, we get that p k , ω k = p , ω . From the transition rules ( 9)(b), we get that p, EX a φ 1 , B , ω = ⇒ BPϕ p , φ 1 , B , ω . Therefore, p, EX a φ 1 , B , ω = ⇒ BPϕ p k , φ 1 , B , ω k . The property holds for this case.

2. Now, let us consider the case where p k , ω k , the abstract successor of p, ω , is ⊥. This case occurs when p, ω = ⇒ P p , ω corresponds to a return statement. Then, one abstract successor of p, ω is ⊥. Note that ⊥ does not satisfy any formula, i.e., ⊥ does not satisfy φ 1 . Therefore, from p, EX a φ 1 , B , ω , we need to ensure that the path of BP ϕ reflecting the possibility in (A1) that p k , ω k B λ φ 1 is not accepted. To do this, we exploit additional trap configurations. We use p ⊥ and γ ⊥ as trap control location and trap stack symbol to obtain these trap configurations. To be more specific, let p, γ ret --→ p , be the rule associated with the transition p, ω = ⇒ P p , ω , then we have ω = γω and ω = ω . We add the transition rule in ( 9)(c) to allow p, EX a φ 1 , B , ω = ⇒ BPϕ p ⊥ , B , γ ⊥ ω . Since a run of BP ϕ includes only infinite paths, we equip these trap configurations with self-loops by the transition rules in ( 20), i.e., p ⊥ , B , γ ⊥ ω = ⇒ BPϕ p ⊥ , B , γ ⊥ ω . As a result, we obtain a corresponding path in BP ϕ : p, EX a φ 1 , B , ω = ⇒ BPϕ p ⊥ , B , γ ⊥ ω = ⇒ BPϕ p ⊥ , B , γ ⊥ ω . Note that this path is not accepted by BP ϕ because p ⊥ , B / ∈ F .

In summary, for every abstract-successor

p k , ω k of p, ω , if p k , ω k = ⊥, then, p, EX a φ 1 , B , ω = ⇒ BPϕ p k , φ 1 , B , ω k ; otherwise p, EX a φ 1 , B , ω = ⇒ BPϕ p ⊥ , B , γ ⊥ ω = ⇒ BPϕ p ⊥ , B , γ ⊥ ω
p, E[φ 1 U a φ 2 ] , B , ω = ⇒ BPϕ { p, φ 1 , B , ω , p , φ , B , ω }. Therefore, p, E[φ 1 U a φ 2 ] , B , ω = ⇒ BPϕ { p, φ 1 , B , ω , p k , φ , B , ω k }.
In other words, BP ϕ has an accepting run from both p, φ 1 , B , ω and p k , φ , B , ω k where p k , ω k is an abstract successor of p, ω . The property holds for this case.

2. Now, let us consider the case where p k , ω k = ⊥. As explained previously, this case occurs when p, ω = ⇒ P p , ω corresponds to a return statement. Then, the abstract successor of p, ω is ⊥. Note that ⊥ does not satisfy any formula, i.e., ⊥ does not satisfy φ. Therefore, from p, E[φ 1 U a φ 2 ] , B , ω , we need to ensure that the path reflecting the possibility in (A2) that ( p, ω B λ φ 1 and p k , ω k B λ φ) is not accepted by BP ϕ . This is ensured as for the case φ = EX a φ 1 by the transition rules in ( 12)(d).

In summary, for every abstract-successor p k , ω k of p, ω , if p k , ω k = ⊥, then, p, E[φ 1 U a φ 2 ] , B , ω = ⇒ BPϕ { p, φ 1 , B , ω , p k , E[φ 1 U a φ 2 ] , B , ω k }; otherwise p, E[φ 1 U a φ 2 ] , B , ω = ⇒ BPϕ p ⊥ , B , γ ⊥ ω = ⇒ BPϕ p ⊥ , B , γ ⊥ ω which is not accepted by BP ϕ . Therefore, (A2) is ensured by the transition rules in [START_REF] Song | LTL model-checking for malware detection[END_REF] stating that BP ϕ has an accepting run from p, E[φ 1 U a φ 2 ] , B , ω iff BP ϕ has an accepting run from p, φ 2 , B , ω ; or BP ϕ has an accepting run from both p, φ 1 , B , ω and p k , E[φ 1 U a φ 2 ] , B , ω k where p k , ω k is an abstract successor of p, ω .

-The intuition behind the rules corresponding to the cases φ = A[φ 1 U a φ 2 ], φ = A[φ 1 R a φ 2 ] are similar to the previous case.

-If φ = e(e ∈ V). Given p ∈ P , e ∈ V, ω ∈ Γ * , we get that the SABPDS BP ϕ should accept p, e , B , ω iff ( p, ω , B) ∈ L(M e ). To check whether ( p, ω , B) ∈ L(M e ), we let BP ϕ go to state s e , the initial state corresponding to p in M e by adding rules in ( 22); and then, from this state, we will check whether ω is accepted by M e under B. This is ensured by the transition rules in ( 24) and ( 25). ( 24) lets BP ϕ mimic a run of M e on ω under B, which includes three possibilities:

• if BP ϕ is in a state q, B with γ on the top of the stack where γ ∈ Γ , and if q γ -→ {q 1 , ..., q n } is a transition rule in M e , then, BP ϕ will move to states q 1 , B , ..., q n , B and pop γ from its stack. Note that popping γ allows us to check the rest of the word. This is ensured by the rules corresponding to ( 24)(a). Then function equal ensures that all these environments are the same.

• if BP ϕ is in a state q, B with γ on the top of the stack, and if q x -→ {q 1 , ..., q n } is a transition rule in M e where x ∈ X , then, BP ϕ can mimic a run of M e under B iff B(x) = γ. If this condition is guaranteed, BP ϕ will move to states q 1 , B , ..., q n , B and pop γ from its stack. Again, popping γ allows us to check the rest of the word. This is ensured by the rules corresponding to ( 24)(b). Then function join x γ ensures that all these environments are the same B and B(x) = γ.

• Similar to ( 24)(b), ( 24)(c) deals with the cases where q ¬x --→ {q 1 , ..., q n } is a transition rule in M e where x ∈ X .

In each VA M e , a configuration is accepted if the run with the word ω reaches a final state in F e ; i.e., if BP ϕ reaches a state q ∈ F e with an empty stack, i.e., with a stack containing the bottom stack symbol . Thus, we should add F e × B as a set of accepting control locations in BP ϕ . This is why F 4 is a set of accepting control locations. In addition, since BP ϕ only recognizes infinite paths, ( 25) adds a loop on every configuration q, B , where q ∈ F e .

-If φ = ¬e(e ∈ V). This case is ensured by the transition rules in ( 23), ( 24) and ( 25). The intuition behind this case is similar to the case φ = e.

We can show that:

Theorem 4. Given a PDS P = (P, Γ, ∆), a set of atomic propositions AP , a labelling function λ : AP D → 2 P and a SBPCARET formula ϕ, we can compute an SABPDS BP ϕ such that for every configuration p, ω , for every B ∈ B, p, ω B λ ϕ iff BP ϕ has an accepting run from the configuration p, ϕ , B , ω .

Conclusion

In this paper, we present a new logic SBPCARET and show how it can precisely and succinctly specify malicious behaviors. We then propose an efficient algorithm for SBPCARET model-checking for PDSs. Our algorithm is based on reducing the model checking problem to the emptiness problem of Symbolic Alternating Büchi Pushdown Systems.

Fig. 1 :

 1 Fig. 1: Two kinds of successors on a run

  accepts the word ω under the environment B. Theorem 1. [10] For every regular expression e ∈ V, we can compute in polynomial time a Variable Automaton M s.t. L(M ) = L(e).

Theorem 2 .

 2 [START_REF] Song | Pushdown model checking for malware detection[END_REF] VAs are closed under boolean operations.4.2 Symbolic Alternating Büchi Pushdown Systems (SABPDSs).Definition 2. A Symbolic Alternating Büchi Pushdown System (SABPDS) is a tuple BP = (P, Γ, ∆, F ), where P is a set of control locations, Γ ⊆ D is stack alphabet, F ⊆ P × 2 B is a set of accepting control locations and ∆ is a finite set of transitions of the form p, γ R -→ { p 1 , ω 1 , ..., p n , ω n } where p ∈ P , γ ∈ Γ , for every 1 ≤ i ≤ n: p i ∈ P , ω i ∈ Γ * ; and R : (B) n → 2 B is a function that maps a tuple of environments (B 1 , ..., B n ) to a set of environments.

( 4 )

 4 is similar to ( 3). -If φ = ∃xφ 1 , then, for every ω ∈ Γ * , p, ω B λ φ iff there exists c ∈ D s.t. p, ω B[x←c] λ φ 1 . This is ensured by the transition rules in ( 5) stating that BP ϕ has an accepting run from p, ∃xφ 1 , B , ω iff there exists c ∈ D s.t. BP ϕ has an accepting run from

Fig. 2 :•

 2 Fig. 2: p, ω = ⇒ P p , ω corresponds to a call statement

  ω i+1 corresponds to a call statement, there are two cases: (1) if p i , ω i has p k , ω k as a corresponding return-point in π, then, the abstract successor of p i , ω i is p k , ω k ; (2) if p i , ω i does not have any corresponding return-point in π, then, the abstract successor of p i , ω i is ⊥.• If p i , ω i = ⇒ P p i+1 , ω i+1 corresponds to a simple statement, the abstract successor of p i , ω i is p i+1 , ω i+1 . • If p i , ω i = ⇒ P p i+1 , ω i+1 corresponds to a return statement, the abstract successor of p i , ω i is defined as ⊥.

	int	p2, ω2		p k , ω k
	p0, ω0 p1, ω1
		call
			p5, ω5	p9, ω9
		p3, ω3 p4, ω4		p10, ω10
	global-successor	call	ret
			p7, ω7
	abstract-successor	p6, ω6	p8, ω8

  which is not accepted by BP ϕ . Therefore, (A1) is ensured by the transition rules in[START_REF] Schwoon | Model-Checking Pushdown Systems[END_REF] stating that BP ϕ has an accepting run from p, EX a φ 1 , B , ω iff there exists an abstract successor p k , ω k of p, ω s.t. BP ϕ has an accepting run from p k , φ 1 , B , ω k . -If φ = AX a φ 1 : this case is ensured by the transition rules in[START_REF] Song | Pushdown model checking for malware detection[END_REF] together with ( 19) and ( 21). The intuition of (10) is similar to that of[START_REF] Schwoon | Model-Checking Pushdown Systems[END_REF].-If φ = E[φ 1 U a φ 2 ], then, for every ω ∈ Γ * , p, ω B λ φ iff p, ω B λ φ 2 or ( p, ω Bλ φ 1 and there exists an abstract successor p k , ω k of p, ω s.t. p k , ω k B λ φ) (A2) . Let π ∈ T races( p, ω ) be a run starting from p, ω on which p k , ω k is the abstract-successor of p, ω . Over π, let p , ω be the immediate successor of p, ω .1. Firstly, we show that for every abstract-successor p k , ω } where p , ω is the immediate successor of p, ω . Thus, to ensure that p, φ , B , ω = ⇒ BPϕ { p, φ 1 , B , ω , p k , φ , B , ω k }, we only need to ensure that p , ω = ⇒ BPϕ p k , φ , B , ω k . As for the case φ = EX a φ 1 , p , ω = ⇒ BPϕ p k , φ , B , ω k is ensured by the rules in ( 21) and the rules in ( 19): rules in ( 21) allow to mimic the run of the PDS P before the return and rules in ( 19) allow to extract and put back φ 1 when the return-point is reached.• If p, ω = ⇒ P p , ω corresponds to a simple statement. Then, the abstract successor of p, ω is its immediate successor p , ω . Thus, we get that p k , ω

k = ⊥ of p, ω , p, φ , B , ω = ⇒ BPϕ { p, φ 1 , B , ω , p k , φ , B , ω k } where B ∈ B. There are two possibilities: • If p, ω = ⇒ P p , ω corresponds to a call statement. From the rules in ( 12)(b), we get that p, φ , B , ω = ⇒ BPϕ { p, φ 1 , B , ω , p , ω k = p , ω . From the transition rules ( 12)(c), we get that

Absx(B1) is as defined in Section 3.1