Marcio Diaz
email: diaz@lipn.univ-paris13.fr

Tayssir Touili
email: touili@lipn.univ-paris13.fr

Model Checking Dynamic Pushdown Networks with Locks and Priorities

Introduction

Writing multi-threaded programs is notoriously difficult, as concurrency related bugs are hard to find and reproduce. This difficulty is increased if we consider that several software systems consist of different components that react to the environment and use resources like CPU or memory according to a real time need. For instance, in systems that control automobiles we can have a component in charge of the music sub-system and another component in charge of the braking sub-system. Obviously, the braking sub-system should have a higher priority access to the resources needed, since a delay in the action of the brakes can cost lives.

The programming model used in the vast majority of these software systems, used from automobiles to spacecrafts, defines a set of threads that perform computation monitoring or respond to events. Each thread is typically assigned a priority and are scheduled by a priority round-robin preemptive scheduler: if a thread with a higher static priority becomes ready to run, the currently running thread will be preempted and returned to the wait list for its priority level. The round-robin scheduling policy allows each thread to run only for a fixed amount of time before it must yield its processing slot to another thread of the same priority. The use of threads with different priorities and other synchronization primitives, like locks, can easily lead to a large number of undesirable behaviors. Consider for example the control flow graph of Figure 1. It consists of three threads: a main thread M starting at control location m 0 that creates two threads A and B. The thread A takes and releases (uses) a lock l inside a loop, and the thread B loops while holding the lock l (between b 1 and b 2 ). Suppose that A and B should act like daemon threads, continuously running in the background reacting to events. This means that the LTL formula G F a 1 ∧ G F b 1 , saying that a 1 is executed frequently often and b 1 is executed frequently often, should be valid for all executions.

But this is not the case in the program of Figure 1: once thread B starts executing its loop and holding lock l, thread A is going to starve since it cannot take the lock until it is released. A similar problem occurs if threads A and B have different priority of execution, the thread with lower priority will starve. The program of Figure 1 shows that there is a real need for formal methods to find automatic verification techniques for checking liveness properties in multi-threaded programs with locks and priorities. Indeed, starvation or absence of livelocks are among the most crucial properties that need to be checked for multi-threaded programs.

Dynamic pushdown networks (DPNs) [START_REF] Bouajjani | Regular symbolic analysis of dynamic networks of pushdown systems[END_REF] are a natural model for multithreaded programs with (possibly recursive) procedure calls and thread creation. A DPN consists of a finite set of pushdown systems (PDSs), each of them models a sequential program that can dynamically create new instances of PDSs. The model-checking problems of DPNs against Linear Temporal Logic (LTL), Computation Tree Logic (CTL) and reachability properties are well studied in the literature [START_REF] Song | Model checking dynamic pushdown networks[END_REF][START_REF] Wenner | Weighted dynamic pushdown networks[END_REF][START_REF] Lammich | Precise fixpoint-based analysis of programs with thread creation and procedures[END_REF][START_REF] Martin Gawlitza | Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation[END_REF][START_REF] Lugiez | Forward analysis of dynamic network of pushdown systems is easier without order[END_REF][START_REF] Bouajjani | Regular symbolic analysis of dynamic networks of pushdown systems[END_REF].

However, DPNs cannot model communication between processes. Previous works [START_REF] Lammich | Contextual locking for dynamic pushdown networks[END_REF][START_REF] Lammich | Predecessor sets of dynamic pushdown networks with tree-regular constraints[END_REF][START_REF] Diaz | Reachability Analysis of Dynamic Pushdown Networks with Priorities[END_REF][START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF] extended DPNs with locks and priorities (called PL-DPN), where PDSs can communicate using locks and priorities. This allows to model multithreaded programs where threads communicate via locks and where each thread can have a different priority. Indeed, locks and priorities are frequently used in multithreaded programs as synchronisation primitives. However, only reachability properties are studied for PL-DPNs [START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF] with some restricted lock and priority usages.

In general, the model checking problem of DPNs against unrestricted LTL or CTL formulas (where atomic propositions can be interpreted over the control states of two or more threads) is undecidable. In [START_REF] Song | Model checking dynamic pushdown networks[END_REF] it is shown that this problem becomes decidable if we consider single-indexed LTL/CTL properties (formulas of the form f i s.t. f i is a LTL/CTL formula interpreted over the PDS i). On the other hand, pairwise reachability of PL-DPNs without thread creation is undecidable in the general case [START_REF] Kahlon | An automata-theoretic approach for model checking threads for LTL properties[END_REF][START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF]. It becomes decidable if locks are accessed in a well-nested style [START_REF] Kahlon | An automata-theoretic approach for model checking threads for LTL properties[END_REF], where each thread can only releases the latest acquired lock, and a thread does not change its priority while holding a lock [START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF].

In this work, we combine these ideas and show that model-checking single indexed LTL/CTL properties is decidable for PL-DPNs under these restrictions. It is non-trivial to do LTL/CTL model checking for PL-DPNs, since the number of instances of PDSs can be unbounded. Checking independently whether all the different PDSs satisfy the corresponding subformula f i is not correct. Indeed, we do not need to check whether an instance of a PDS j satisfies f j if this instance is not created during a run. The approach of [START_REF] Song | Model checking dynamic pushdown networks[END_REF] cannot be directly applied to perform single-indexed LTL/CTL model-checking for PL-DPNs due to locks and priorities. Indeed, we have to consider communication between each instance of PDSs running in parallel in the network. To overcome this problem, we will reduce single-indexed LTL/CTL model-checking for PL-DPNs to the membership problem of PL-DPNs with Büchi acceptance condition (PL-BDPNs). This latter problem is reduced to the membership problem of DPNs with Büchi acceptance condition (BDPNs).

In [START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF] we presented an approach for checking pairwise reachability of PL-DPNs using priority-lock structures, an extension of acquisition structures introduced in [START_REF] Lammich | Predecessor sets of dynamic pushdown networks with tree-regular constraints[END_REF]. This structure is used to get rid of locks and priorities in PL-DPNs such that pairwise reachability of PL-DPNs can be reduced to constrained pairwise reachability on DPNs. It works by keeping track of the locks and priorities used in a run. For pairwise reachability, we only need to consider finite runs, as a configuration of a PL-DPN reaches another configuration only using finite steps. However, we have to consider infinite runs of PL-DPNs when we study LTL/CTL model checking.

In this work, we adapted the priority-lock structures to keep track also of the infinitely used locks and priorities. Indeed, we need to assure that a finally acquired lock cannot be infinitely used and that an infinitely used priority does not block other threads. Also, in the case of CTL model checking, we modified the priority-lock structure to keep track of the locks and priorities of differents branched runs.

After getting rid of locks and priorities using the modified priority-lock structure, we construct Büchi dynamic PDSs (resp. alternating Büchi dynamic PDSs) which are a synchronization of a PDS i and the LTL (resp. CTL) formula f i . The language accepted by a Büchi dynamic PDS corresponds to the configurations that satisfy the formula f i . This language is computed by the automata-based approach for standard LTL/CTL model checking for PDSs [START_REF] Song | Model checking dynamic pushdown networks[END_REF].

Thus, the contributions of this paper are:

-An algorithm for single-indexed LTL Model Checking for PL-DPNs, developed in section 4. -An algorithm for single-indexed CTL Model Checking for PL-DPNs, developed in section 5.

For lack of space proofs can be found in the extended version of this paper at [1].

Model Definition

Let L be the set of all locks and I be the set of all priorities. A PL-DPN can be seen as a collection of threads running in parallel, each of them having a set of acquired locks and a priority. They are able to:

1. Perform pushdown operations. This can be used to model calls and returns from (possible recursive) functions. 2. Change its priority if its set of acquired locks is empty. Removing this constraint leads to undecidability [START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF]. 3. Acquire a lock that does not belong to any set of acquired locks (of the running threads). 4. Release a lock belonging to its set of acquired locks. 5. Create a new thread with any (initial) priority and an empty set of acquired locks.

Definition 1. Dynamic Pushdown System with Locks and Priorities (PL-DPDS) is a tuple P = (P, Γ, δ, η p , η l ), where P is a finite set of control states, Γ is a finite stack alphabet, η p is a function from control states to priorities from I, η l is a function from control states to set of locks from L, δ is a finite set of transition rules of the following forms:

1. pγ τ - → qw, with η p (q) = η p (p) and η l (q) = η l (p); 2. pγ ch(x) ---→ qw, with η p (q) = x and η l (q) = η l (p) = ∅; 3. pγ acq l ---→ qw, with η p (q) = η p (p), η l (q) = η l (p) ∪ {l} and l ∈ η l (p); 4. pγ rel l --→ qw, with η p (q) = η p (p), η l (q) = η l (p) \ {l} and l ∈ η l (p); 5. pγ τ - → q 1 w 1 q 2 w 2 , with η p (q 1 ) = η p (p), η l (q 1 ) = η l (p) and η l (q 2 ) = ∅.
where p, q 1 , q 2 ∈ P, γ ∈ Γ , w, w 1 , w 2 ∈ Γ * , l ∈ L, x ∈ I.

A local configuration pω ∈ P Γ * of a PL-DPDS P = (P, Γ, δ, η p , η l ), represents the state of a thread. The state of a thread consists of a priority, a set of acquired locks and a stack. The priority of a thread and the set of acquired locks are represented by its control state p and can be retrieved from it by using the functions η p and η l , respectively. The stack of a thread is represented by the sequence of stack letters ω ∈ Γ * .

The function η p assigns a priority to each control state. Intuitively, this means that a thread can be in configurations with different priorities. The function η l assigns a set of locks to each control state. This set of locks represents the locks held (acquired but not yet released) by the thread at such configuration. Definition 2. A Dynamic Pushdown Network with Priorities and Locks (PL-DPN) is a tuple (Act, L, I, P 1 , . . . , P n ) such that L is a set of locks, I is set of priorities (natural numbers), Act is a finite set of actions {acq(l), rel(l)|l ∈ L} ∪ {ch(x)|x ∈ I} ∪ {τ }, where the action acq(l) (resp. rel(l)) for every l ∈ L denotes the acquisition (resp. release) of the lock l, the action ch(x) denotes the change to priority x and the action τ denotes a pushdown action. For every i ∈ {1, . . . , n}, P i is a PL-DPDS.

A global configuration of a PL-DPN M is a sequence of local configurations, each of them corresponding to the configuration of one of the threads running in parallel on the system. Let Conf M be the set of all global configurations of a PL-DPN M .

Following previous works we assume that locks are used in a well-nested fashion, i.e. a process has to release locks in the opposite order of acquisition, an assumption that is often satisfied in practice. Note that for non-well-nested locks even simple reachability problems are undecidable [START_REF] Kahlon | Reasoning about threads communicating via locks[END_REF].

Example

The PL-DPN modeling the program of Figure 1 is defined as follows M = ({acq l, rel l, ch l, τ }, {l}, {1}, P 1 , P 2 , P 3 ) where:

-P 1 = ({p 1 }, {m 0 , m 1 , m f }, {p 1 m 0 τ - → p 1 m 1 p 1 a 0 , p 1 m 1 τ - → p 1 m f p 1 b 0 }, η p , η l ) such that η p (p 1 ) = 1 and η l (p 1 ) = ∅. -P 2 = ({p 1 , p 1,l }, {a 0 , a 1 , a 2 , a f }, {p 1 a 0 acq l ---→ p 1,l a 1 , p 1,l a 1 τ - → p 1,l a 2 , p 1,l a 2 τ - → p 1 a f , p 1 a f τ - → p 1 a 0 }, η p , η l ) such that η p (p 1 ) = η p (p 1,l ) = 1 and η l (p 1 ) = ∅, η l (p 1,l ) = {l}. -P 3 = ({p 1 , p 1,l }, {b 0 , b 1 , b 2 , b f }, {p 1 b 0 acq l ---→ p 1,l b 1 , p 1,l b 1 τ - → p 1,l b 2 , p 1,l b 2 rel l --→ p 1 b f , p 1,l b 2 τ - → p 1,l b 1 }, η p , η l ) such that η p (p 1 ) = η p (p 1,l ) = 1 and η l (p 1 ) = ∅, η l (p 1,l ) = {l}.
The initial configuration of this PL-DPN M is p 1 m 0 .

The semantics of PL-DPNs is defined such that:

-Transitions of threads with highest priority should be executed first.

-Transitions that manipulate locks should follow the locking rules:

• A transition attempting to acquire a lock can only be executed if the lock is free, i.e. does not belong to any set of acquired locks. • A transition attempting to release a lock can only be executed if the lock is in possession of the corresponding thread, i.e. in its set of acquired locks.

We overload the functions η p and η l to global configurations as follows: for all

c = p 1 ω 1 . . . p n ω n ∈ Conf M , η p (p 1 ω 1 . . . p n ω n ) := max(η p (p 1 ), . . . , η p (p n )) and η l (p 1 ω 1 . . . p n ω n ) := η l (p 1 ) ∪ • • • ∪ η l (p n ). Definition 3. The transition relation -→ M is defined as the smallest relation in Conf M × Conf M such that ∀c 1 , c 2 ∈ Conf M : 1. c 1 pγr c 2 -→ M c 1 qωr c 2 , if η p (p) = η p (c 1 pγr c 2 ) and pγ act --→ qω ∈ ∆, s.t. act ∈ {τ, rel l} ∪ {ch(x) | x ∈ I}; 2. c 1 pγr c 2 -→ M c 1 qωr c 2 , if η p (p) = η p (c 1 pγr c 2 ), l ∈ η l (c 1 pγr c 2 ) and pγ acq l ---→ qω ∈ ∆; 3. c 1 pγr c 2 -→ M c 1 q 2 ω 2 q 1 ω 1 r c 2 , if η p (p) = η p (c 1 pγr c 2 ) and pγ τ - → q 1 ω 1 q 2 ω 2 ∈ ∆;
where p, q, q 1 , q 2 ∈ P, γ ∈ Γ, ω, ω 1 , ω 2 , r ∈ Γ * , l ∈ L.

The semantics above says that:

1. A thread in a local configuration with control state p and top of stack γ can move to a local configuration with control state q, replacing the top of its stack γ by w, if there is a τ , ch(x) or release rule pγ lab --→ qw ∈ ∆ and its priority (η p (p)) is equal to the highest priority among all the threads (η p (c 1 pγr c 2 )); 2. A thread in a local configuration with control state p and top of stack γ can move to a local configuration with control state q, replacing the top of its stack γ by w, if there is an acquire rule pγ acq l ---→ qw ∈ ∆, the lock that the rule attempts to take is free (l ∈ η l (c 1 pγr c 2 )), and its priority (η p (p)) is equal to the highest priority among all the threads (η p (c 1 pγr c 2 )); 3. A thread in a local configuration with control state p and top of stack γ can move to a local configuration with control state q 1 , replacing the top of its stack γ by w 1 and create another thread in control state q 2 with stack w 2 , if there is a rule pγ τ -→ q 1 w 1 q 2 w 2 ∈ ∆ and its priority (η p (p)) is equal to the highest priority among all the threads (η p (c 1 pγr c 2 )).

Note that the semantics of locks corresponds to the one of spin-locks, found in most of the libraries for threads (like Pthreads). Spin-locks are similar to mutexes, but they might have lower overhead for very short-term blocking. When the calling thread requests a spin-lock that is already held by another thread, the calling thread spins in a loop to test if the lock has become available. This means that if a thread with lower priority, holding a lock l, is interrupted by a thread with higher priority, attempting to acquire the same lock, then the program becomes blocked (assuming there is only one CPU). In this paper we assume that programs are free of deadlocks since they can be detected using the technique of our previous work [START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF].

Given a configuration c, the set of immediate predecessors of c in a PL-DPN M is defined as pre M (c) = {c ∈ Conf M : c -→ M c}. This notation can be generalized straightforwardly to sets of configurations. Let pre * M denote the reflexive-transitive closure of pre M . For the rest of this paper, we assume that we have fixed a PL-DPN M = (Act, L, I, P 1 , . . . , P n ).

4 Single-Indexed LTL Model Checking for PL-DPNs

Linear Temporal Logic (LTL) and Büchi Automata

From now on, we fix a finite set of atomic propositions AP . Definition 4. The set of LTL formulas is given by (where q ∈ AP ):

ϕ ::= q | ϕ 1 ∧ ϕ 2 | ¬ϕ | Xϕ | F ϕ | G ϕ | ϕ 1 U ϕ 2
Given an ω-word α = α 0 α 1 . . . over 2 AP , let α k denote the suffix of α starting from α k . The notation α |= ϕ indicates that α satisfies ϕ, where |= is inductively defined as follows:

α |= q if q ∈ α 0 ; α |= ¬ϕ if α¬ |= ϕ; α |= ϕ 1 ∧ ϕ 2 if α |= ϕ 1 and α |= ϕ 2 ; α |= Xϕ if α 1 |= ϕ; α |= ϕ 1 U ϕ 2 if
there exists k ≥ 0 such that α k |= ϕ 2 and for every j : 1 ≤ j < k, α j |= ϕ 1 . The temporal operators F and G can be defined using the following equivalences: F ϕ ≡ true U ϕ, G ϕ ≡ ¬F ¬ϕ. Definition 5. A Büchi automaton (BA) B is a tuple (G, Σ, θ, g 0 , F ), where G is a finite set of states, Σ is the input alphabet, θ ⊆ G × Σ × G is a finite set of transitions, g 0 ∈ G is the initial state and F ⊆ G is a finite set of accepting states.

A run of B over an ω-word α 0 α 1 . . . is a sequence of states q 0 q 1 . . . s.t. q 0 = g 0 and (q i , α i , q i+1 ) ∈ θ for every i ≥ 0. A run is accepting iff it infinitely often visits some states in F .

Theorem 1. (From [START_REF] Vardi | Automata-theoretic techniques for modal logics of programs[END_REF]) Given a LTL formula f we can construct a BA B f (s.t. Σ = 2 AP ) recognizing all the ω-words that satisfy f .

The Model Checking Problem

The model checking problem of PL-DPNs against doble-indexed LTL formulas where the validity of atomic propositions depends on two or more PL-DPNs is undecidable [START_REF] Kahlon | An automata-theoretic approach for model checking threads for LTL properties[END_REF].

In this work, in order to obtain decidability results, we consider the modelchecking problem of PL-DPNs against single-indexed LTL properties of the form f = n i=1 f i , where f i is interpreted over the PL-DPDS P i . Let λ be a labeling function λ : i P i → 2 AP , that assigns to each control location of the PL-DPN M a set of atomic propositions. Definition 6. Given a labeling function λ, a local run r = p 0 w 0 p 1 w 1 . . . of the PL-DPDS P i satisfies f i , denoted by r |= f i , iff the ω-word λ(p 0 )λ(p 1 ) . . . satisfies f i . Definition 7. A global run R satisfies f = i f i , denoted by R |= f , iff all local runs of each instance of P i running in parallel in R satisfy f i . Definition 8. A PL-DPN M , with initial configuration p 0 γ 0 , satisfies f = i f i , denoted by M |= f , iff all global runs starting with p 0 γ 0 satisfy f . From now on, we fix a single-indexed LTL formula f = n i=1 f i .

Priority-Lock Structures

Definition 9. (From [START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF]) A priority-lock structure of a global run R of a PL-DPN under DPN semantics, is defined as either a tuple x, y, g r , g a , la or the symbol ⊥.

In [START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF] is given an algorithm to compute a priority-lock structure from a global run R such that we get ⊥ if the run is not a valid under PL-DPN semantics, or we get the tuple x, y, g r , g a , la if the run is valid under PL-DPN semantics, where:

x is the lowest transition priority, from the control states visited during the run, y is the highest final priority, from the control states of the final configuration, g r is a set of dependencies between lock usages (acquire and release of a lock) and final releases of a lock (release without acquisition), g a is a set of dependencies between lock usages and initial acquisitions of a lock (acquisition of a lock without the corresponding release), la set of lock actions and their corresponding priorities.

In this work we just need to know that given a PL-DPN M and a regular set of configurations S, we can construct a DPN M , with priority-lock structures embedded in the control states, such that the predecessor configurations of S over M are the predecessor configurations of S over M with a priority-lock structure not equal to ⊥. Formally, from [START_REF] Diaz | Dealing with Priorities and Locks for Concurrent Programs[END_REF]:

Theorem 2. pre * M (S) = {pω | (p, s)ω ∈ pre * M (S × ∞, 0, ∅, ∅, ∅ ) ∧ s = ⊥}.
Using the previous theorem we can reduce LTL/CTL model checking on the PL-DPN M to a series of pre * queries over the DPN M . In order to keep the queries consistent with each other, taking in account the priorities and locks, we will need to inspect the priority-lock structure stored in the configurations. For that, given a control state p in the DPN M , let X(p), U (p), R(p) and A(p) be the lowest transition priority, set of lock usages, set of initial releases and set of final acquisitions, respectively, embedded in the control state p.

Example The PL-DPN M of Example 2.1 can be reduced to the DPN M = ({τ }, P 1 , P 2 , P 3 ) where:

-P 1 = ({p 0 = (p 1 , 1, 1, ∅, ∅, ∅ ), p 1 = (p 1 , 1, 1, ∅, ∅, {(l, usg, 1, 1)} ), p 2 = (p 1 , 1, 1, ∅, ∅, {(l, acq, 1, 1)} ), p 3 = (p 1 , 1, 1, ∅, ∅, {(l, acq, 1, 1), (l, usg, 1, 1)} ), p 4 = (p 1 , ⊥), }, {m 0 , m 1 , m f }, {p 1 m 0 τ - → p 1 m 1 p 1 a 0 , p 3 m 0 τ - → p 1 m 1 p 2 a 0 , p 3 m 0 τ - → p 2 m 1 p 1 a 0 , p 4 m 0 τ - → p 2 m 1 p 2 a 0 , p 2 m 0 τ - → p 0 m f p 2 b 0 , p 1 m 0 τ - → p 0 m f p 1 b 0 , })
-P 2 and P 3 are defined similar. In particular, they have the same set of control states.

The Model-Checking Approach

The next step is to define a DPN with Büchi acceptance condition.

Definition 10. A Büchi DPDS (BDPDS) is a tuple BP = (P, Γ, ∆, F ), where (P, Γ, ∆) is a DPDS and F ⊆ P is a finite set of accepting control locations.

For i ∈ {1, . . . , n} , let B i = (G i , Σ i , θ i , g 0 i , F i ) be the Büchi automaton recognizing the ω-words that satisfy the LTL formula f i . Definition 11. We define BDPDSs BP i = ((

P i × G i ) × (2 L × I), Γ i , ∆ i , F i ) where F i = {((p, g), (A(p), X(p))) | (p, g) ∈ P i × F i )}. ∆ i is computed such that for every (g 1 , λ(p), g 2 ) ∈ θ i , a ∈ Act, x, x 1 , x 2 ∈ I, u, u 1 , u 2 ∈ 2 L and (p 2 , s 2 )ω 2 ∈ P j × Γ * j we have: 1. ((p, g 1 ), (u, x))γ a - → ((p 1 , g 2 ), (u, x))ω 1 ∈ ∆ i , if pγ a - → p 1 ω 1 ∈ ∆ i , 2. If pγ a - → p 1 ω 1 p 2 ω 2 ∈ ∆ i , 2.1. ((p, g 1 ), (u 1 ∪u 2 , x))γ a - → ((p 1 , g 2 ), (u 1 , x 1 ))ω 1 ((p 2 , g 0 j ), (u 2 , x 2 ))ω 2 ∈ ∆ i , if A(p 1 ) ∩ u 1 = A(p 2 ) ∩ u 2 = ∅ and x 1 = x 2 , 2.2. ((p, g 1 ), ⊥)γ a - → ((p 1 , g 2 ), (u 1 , x 1 ))ω 1 ((p 2 , g 0 j ), (u 2 , x 2 ))ω 2 ∈ ∆ i , other- wise.
Sometimes we write a configuration ((p , g), (u, x)) of a BP i as (p, s), where p = (p , g) is called control state and s = (u, x) is called "priority-lock structure".

Let L(BP i ) be the set of all the tuples ((p, g 0 i ), (u, x))γ, D) such that BP i has an accepting run starting from the configuration ((p, g 0 i ), (u, x))γ, using infinitely the lowest priority x, the set of locks u and spawning the set of configurations D. We can compute the language of BP i using the algorithm from [START_REF] Song | Model checking dynamic pushdown networks[END_REF]: Theorem 3. (From [START_REF] Song | Model checking dynamic pushdown networks[END_REF]) For every BDPDS BP i = (P i , Γ i , ∆ i , F i ) we can construct a finite automaton A i such that L(A i ) = L(BP i ).

Main Algorithm

Given a PL-DPN M = (Act, P 1 , . . . , P n ) and a single-indexed LTL formula f = i f i , in order to check if M |= f , we proceed as follows:

1. Create the DPN M = (P 1 , . . . , P n ), as in Section 5.1.

Create Buchi automatons B ¬

i satisfying the formulas ¬f i .

Construct BDPDSs B ¬

i P i from the DPN M and the Buchi automatons B ¬ of (2), as in Definition 11. 4. If an initial configuration ((p 0 , g 0 ), (u, x))γ 0 is in X, the set of configurations that satisfy the formula ¬f , with some set of locks u and priority x then M |= f . Otherwise we continue to the next step, to be sure there are no livelocks. 5. Create Buchi automatons B i satisfying the formulas f i . 6. Construct BDPDSs B i P i from them the DPN M and the Buchi automatons B i of ( 5), as in Definition 11. 7. If an initial configuration ((p 0 , g 0 ), ⊥)γ 0 is in Y , the set of of configurations that satisfy the formula f , then there is a livelock and M |= f , otherwise M |= f . We can construct the set X in the following iterative way:

1. X = i L(B ¬ i P i ). 2. X = {pγ | (pγ, D) ∈ Z ∧ D ∩ X = ∅}. 3. If X = X , set X = X and go to 2. Otherwise return X.
where Z is the language of initial configurations of all infinite paths in each DPDS P i . We can construct the set Y in the following iterative way:

1. Y = i L(B i P i ). 2. Y = {(pγ, D) ∈ Y | ∀p γ ∈ D ∃D ⊆ Conf M s.t. (p γ , D ) ∈ Y }. 3. If Y = Y , set Y = Y
and go to 2. Otherwise return Y . Theorem 4. A PL-DPN M satisfies a single-indexed LTL formula f (M |= f ) iff there is not initial configuration in X with non-bottom priority-lock structure and there is not initial configuration in Y with bottom priority-lock structure.

Example

We want to check if the single-indexed LTL formula f = f 1 ∧ f 2 ∧ f 3 , where f 1 = true, f 2 = GF a 1 and f 3 = GF b 1 , is satisfied by the PL-DPN M = (Act, P 1 , P 2 , P 2 ) of Example 2.1.

The first step was to create the DPN M = (P 1 , P 2 , P 3 ) as in Example 4.3. The second step is to create Buchi automatons B ¬ 1 , B ¬ 2 and B ¬ 3 recognizing the ω-words that satisfy the formulas ¬f 1 = false, ¬f 2 = F G ¬a 1 and ¬f 3 = F G ¬b 1 , respectively. Then we create the BDPDSs B ¬ 1 P 1 , B ¬ 2 P 2 and B ¬ 2 P 3 using Definition 11. The next step is to construct the set of configurations X, we get:

1. X = L(B ¬ P 1 ) ∪ L(B ¬ P 2 ) ∪ L(B ¬ P 3 ) = ∅ ∪ ∅ ∪ ∅ = ∅. 2. X = {pγ | (pγ, D) ∈ Z) ∧ D ∩ ∅ = ∅} = ∅.
We have that X = ∅, this means that the negation of f is not satisfied, but still can be the case that we have some livelock. Thus we continue calculating Y . The algorithm proceeds as follows:

1. L(BP 1 ) = {(((p 3 , g 0 ), ⊥)m 0 , {((p 1 , g 0 ), ({l}, 1))a 0 , ((p 2 , g 0 ), (∅, 1))b 0 }), . . . }.

L(BP

2 ) = {((p 1 , g 0 ), ({l}, 1))a 0 , ∅)} with A(p 1 ) = ∅. 3. L(BP 3 ) = {((p 2 , g 0 ), (∅, 1))b 0 , ∅)} with A(p 2 ) = {l}. 4. Y = L(BP 1 ) ∪ L(BP 2 ) ∪ L(BP 3 ). 5. Y = {(((p 3 , g 0 ), ⊥)m 0 , {((p 1 , g 0 ), ({l}, 1))a 0 , ((p 2 , g 0 ), (∅, 1))b 0 })}.
We can observe that Y has the initial configuration ((p 3 , g 0 ), ⊥)m 0 . This configuration has a ⊥ priority-lock structure, since the child corresponding to thread A infinitely uses lock l and the child corresponding to thread B acquire lock l without releasing it (see the rules of Definition 11). This means that there is a livelock and then the formula f is not always satisfied int the PL-DPN M .

Single-Indexed CTL model checking of PL-DPNs

In this section we consider single-indexed CTL model checking for PL-DPNs. For technical reasons we suppose that CTL formulas are given in positive normal form, i.e. only atomic propositions are negated. Definition 12. The set of CTL formulas is given by (where a ∈ AP ):

ϕ ::= q | ¬q | ϕ∧ϕ | ϕ∨ϕ | AXϕ | EXϕ | A(ϕU ϕ) | E(ϕU ϕ) | A(ϕRϕ) | E(ϕRϕ)
The other standard CTL operators can be expressed by the above operators. For instance EF ϕ = E(true U ϕ), AF ϕ = A(true U ϕ), EGϕ = E(false Rϕ) and AGϕ = A(false Rϕ). The closure cl(ϕ) is the set of all the sub-formulas of ϕ

(including ϕ). Let At(ϕ) = {a ∈ AP | a ∈ cl(ϕ)} and cl R (ϕ) = {θ ∈ cl(ϕ) | θ = E(ϕ 1 Rϕ 2 ) ∨ θ = A(ϕ 1 Rϕ 2 )}.
Let λ : AP → 2 Pi×Γ * i a valuation assigning to each atomic proposition a finite set of local configurations. A local configuration c satisfies a CTL formula f i (denoted by c |= f i ) iff there exists D ⊆ D i such that c |= D f i holds, where |= D is inductively defined as follows: Intuitively, c |= D f i means that c satisfies f i and the executions that made c satisfy f i spawn the configurations in D, i.e. when a transition rule qγ → p 1 w 1 p 2 w 2 is used to make f i satisfied, p 2 w 2 is in D.

-c |= ∅ a if c ∈ λ(a). -c |= ∅ ¬a if c ∈ λ(a). -c |= D ϕ 1 ∧ ϕ 2 if ∃D 1 , D 2 ⊆ D i such that D = D 1 ∪ D 2 , c |= D1 ϕ 1 and c |= D2 ϕ 2 ; -c |= D ϕ 1 ∨ ϕ 2 if c |= D ϕ 1 or c |= D ϕ 2 ; -c |= D AXϕ if for every c 1 , . . . , c m ∈ Conf M such that c ⇒ c j D j , c j |= Dj ϕ and D = j D j ; -c |= D EXϕ if there exist c ∈ Conf M such that c ⇒ i c D , c |= D ϕ and D = D ∪ D ; -c |= D A(ϕ 1 U ϕ 2 ) if for every path c 0 c 1 . . . with c 0 = c for every m ≥ 1, ∃D m ⊆ D, such that c m-1 ⇒ c m D m , and ∃k such that c k |= D k ϕ 2 , ∀j < k c j |= Dj ϕ 1 . -c |= D E(ϕ 1 U ϕ 2 ) if exists a path c 0 c 1 . . . with c 0 = c, for every m ≥ 1, ∃D m such that c m-1 ⇒ c m D m and ∃k such that c k |= D k ϕ 2 , ∀k, j < k c j |= Dj ϕ 1 . -c |= D A(ϕ 1 Rϕ 2 ) if

Priority-Lock Alternating BDPDSs

Definition 13. A priority-lock alternating BDPDS (PL-ABDPDS) is a tuple

BP i = (P i , Γ i , ∆ i , F i )
, where P i is a finite set of control locations, Γ i is the stack alphabet, F i ⊆ P i is a set of accepting control locations, ∆ i is a finite set of transition rules in the form of pγ → {p 1 ω 1 , . . . , p h ω h } {q 1 u 1 , . . . , q k u k }.

An PL-ABDPDS BP induces a relation → defined as follows: for every ω ∈ Γ * if pγ → {p 1 ω 1 , . . . , p h ω h } {q 1 u 1 , . . . , q k u k } ∈ ∆ , then pγω → {p 1 ω 1 ω, . . . , p h ω h ω} {q 1 u 1 , . . . , q k u k }. Intuitively, if BP is at the configuration pγω, it can fork into h copies in the configurations p 1 ω 1 ω, . . . , p h ω h ω and creates k new instances. We write pγ → {p 1 ω 1 , . . . , p h ω h } if pγ → {p 1 ω 1 , . . . , p h ω h } ∅.

A run is accepting if each branch of this run infinitely often visits some control locations in F . Let L(BP) be the set of all the pairs (c, D) such that BP has an accepting run from c and that creates the set of configurations D.

Computing an Alternating BDPDS

To perform single-indexed CTL model checking for PL-DPNs we follow the approach for LTL model checking, but in this case we need alternating BDPDSs, since CTL formulas can be translated to alternating Büchi automata.

On [START_REF] Song | Model checking dynamic pushdown networks[END_REF] it is shown how to model check DPNs against CTL formulas using alternating BDPDS. Here we reduce CTL model checking in a PL-DPN to CTL model checking in a DPN by using priority-lock structures and applying the result of [START_REF] Song | Model checking dynamic pushdown networks[END_REF].

Let BP i = (P i , Γ i , ∆ i , F i ) be the PL-ABDPDS such that P i = P i × cl(f i ), F i = {(p, a) | a ∈ cl(f i ) ∩ AP, p ∈ f (a)} ∪ {(p, ¬a) | ¬a ∈ cl(f i ), a ∈ AP, p ∈ f (a)} ∪ P i × cl R (f i ), where cl R (f i ) is the set of formulas of cl(f i ) of the form E(ϕ 1 Rϕ 2 ) or A(ϕ 1 Rϕ 2 ); and ∆ i is the smallest set of transitions rules such that for every control location p ∈ P i , every subformula ϕ ∈ cl(f i ) and every γ ∈ Γ i we have:

Fig. 1 .

 1 Fig. 1. Control-flow graph of a main thread starting at m0 that creates two child threads starting at a0 and b0. The child threads execute a loop and use a lock l.

  for every path c 0 c 1 . . . with c 0 = c, for every m ≥ 1 ∃D m such that c m-1 ⇒ c m D m and either for all j, c j |= Dj ϕ 2 or ∃k such that c k |= D k ϕ 1 and ∀j ≤ k, c j |= Dj ϕ 2 . c |= D E(ϕ 1 Rϕ 2 ) if exists a path c 0 c 1 . . . with c 0 = c, for every m ≥ 1 ∃D m such that c m-1 ⇒ c m D m and either for all j, c j |= Dj ϕ 2 or ∃k such that c k |= D k ϕ 1 and ∀j ≤ k, c j |= Dj ϕ 2 .

1.

  If ϕ = a, a ∈ AP and p ∈ f (a) then (p, ϕ)γ → (p, ϕ)γ ∈ ∆ ; 2. If ϕ = ¬a, a ∈ AP and p ∈ f (a) then (p, ϕ)γ →(p, ϕ)γ ∈ ∆ ; 3. If ϕ = ϕ 1 ∧ ϕ 2 then (p, ϕ)γ → {(p, ϕ 1 )γ, (p, ϕ 2 )γ} ∈ ∆ i ; 4. If ϕ = ϕ 1 ∨ ϕ 2 then (p, ϕ)γ → {(p, ϕ 1 )γ} ∈ ∆ i and (p, ϕ 2 )γ → {(p, ϕ 2 )γ} ∈ ∆ i ; 5. If ϕ = EF ϕ 1 then: if pγ → p ω p ω ∈ ∆ i then (p, ϕ)γ → {(p , ϕ 1 )ω} {p ω } ∈ ∆ i , similar for non-spawning rules; 6. If ϕ = AXϕ 1 then (p, ϕ)γ → {(p , ϕ 1 )ω | pγ → p ω p ω ∈ ∆ i } {p ω | pγ → p ω p ω ∈ ∆ i }; 7. If ϕ = E(ϕ 1 U ϕ 2 ) then: (p, ϕ)γ → {(p, ϕ 1 )γ, (p, ϕ 2 )γ} ∈ ∆ i , and if pγ → p ω p ω ∈ ∆ i then (p, ϕ)γ → {(p, ϕ 1 )γ, (p , ϕ)ω} {p ω } ∈ ∆ i , similar for non-spawning rules; 8. If ϕ = A(ϕ 1 U ϕ 2 ) then: (p, ϕ)γ → {(p, ϕ 2 )γ} ∈ ∆ i , if pγ → p ω p ω ∈ ∆ i then (p, ϕ)γ → {(p, ϕ 1 )γ, (p , ϕ)ω | pγ → p ω p ω ∈ ∆ i } {p ω } ∈ ∆ i , similar for non-spawning rules; 9. If ϕ = E(ϕ 1 Rϕ 2 ) then: if pγ → p ω p ω ∈ ∆ i then (p, ϕ)γ → {(p, ϕ 2 )γ, (p, ϕ 1 )γ} ∈ ∆ i and (p, ϕ)γ → {(p, ϕ 2 )γ, (p , ϕ)ω} {p ω } ∈ ∆ i ; 10. If ϕ = A(ϕ 1 Rϕ 2 ) then (p, ϕ)γ → {(p,ϕ 2 )γ, (p, ϕ 1 )γ} ∈ ∆ i and (p, ϕ)γ → {(p, ϕ 2 )γ, (p , ϕ)ω | pγ → p ω p ω ∈ ∆ i } {p ω | pγ → p ω p ω ∈ ∆ i } ∈ ∆ i .


Huu-Vu Nguyen

Tayssir Touili

Branching Temporal Logic of Calls and Returns for Pushdown Systems

Pushdown Systems (PDSs) are a natural model for sequential programs with (recursive) procedure calls. In this work, we define the Branching temporal logic of CAlls and RETurns (BCARET) that allows to write branching temporal formulas while taking into account the matching between calls and returns. We consider the model-checking problem of PDSs against BCARET formulas with "standard" valuations (where an atomic proposition holds at a configuration c or not depends only on the control state of c, not on its stack) as well as regular valuations (where the set of configurations in which an atomic proposition holds is regular). We show that these problems can be effectively solved by a reduction to the emptiness problem of Alternating Büchi Pushdown Systems. We show that our results can be applied for malware detection.

Introduction

Pushdown Systems (PDSs) are a natural model for sequential programs with (recursive) procedure calls. Thus, it is very important to have model-checking algorithms for PDSs. A lot of work focuses on proposing verification algorithms for PDSs, e.g, for both linear temporal logic (LTL and its extensions) [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF][START_REF] Esparza | Model checking LTL with regular valuations for pushdown systems[END_REF][START_REF] Esparza | Efficient algorithms for model checking pushdown systems[END_REF][START_REF] Finkel | A direct symbolic approach to model checking pushdown systems[END_REF][START_REF] Kupferman | An automata-theoretic approach to infinite-state systems[END_REF][START_REF] Song | LTL model-checking for malware detection[END_REF] and branching temporal logic (CTL and its extensions) [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF][START_REF] Bozzelli | Complexity results on branching-time pushdown model checking[END_REF][START_REF] Burkart | Model checking the full modal mu-calculus for infinite sequential processes[END_REF][START_REF] Walukiewicz | Pushdown processes: Games and model checking[END_REF][START_REF] Song | Efficient CTL model-checking for pushdown systems[END_REF]. However, LTL and CTL are not always adequate to specify properties. Indeed, some properties need to talk about matching between calls and returns. Thus, CARET (a temporal logic of calls and returns) was introduced by Alur et al [START_REF] Alur | A temporal logic of nested calls and returns[END_REF]. This logic allows to write linear temporal logic formulas while taking into account matching of calls and returns. Later, VP-µ (also named NT-µ in other works of the same authors) [START_REF] Alur | A fixpoint calculus for local and global program flows[END_REF][START_REF] Alur | Languages of nested trees[END_REF][START_REF] Alur | Software model checking using languages of nested trees[END_REF], a branching-time temporal logic that allows to talk about matching between calls and returns, was introduced. VP-µ can be seen as an extension of the modal µ-calculus which allows to talk about matching of calls and returns.

In [START_REF] Alur | A fixpoint calculus for local and global program flows[END_REF], the authors proposed an algorithm to model-check VP-µ formulas for Recursive State Machines (RSMs) [START_REF] Alur | Analysis of recursive state machines[END_REF]. RSMs can be seen as a natural model to represent sequential programs with (recursive) procedure calls. Each procedure is modelled as a module. The invocation to a procedure is modelled as a call node; the return from a module corresponds to a ret node; and the remaining statements are considered as internal nodes in the RSMs. Thus, RSMs are a good formalism to model sequential programs written in structured programming languages like C or Java. However, they become non suitable for modelling binary or assembly programs; since, in these programs, explicit push and pop instructions can occur. This makes impossible the use of RSMs to model assembly programs and binary codes directly (whereas Pushdown Systems can model binary codes in a natural way [START_REF] Song | Efficient malware detection using model-checking[END_REF]). Model checking binary and assembly programs is very important. Indeed, sometimes, only the binary code is available. Moreover, malicious programs are often executables, i.e., binary codes. Thus, it is very important to be able to model check binary and assembly programs against branching-time formulas with matchings between calls and returns. One can argue that from a binary/assembly program, one can compute a PDS as described in [START_REF] Song | Efficient malware detection using model-checking[END_REF] and then apply the translation in [START_REF] Alur | Analysis of recursive state machines[END_REF] to obtain a RSM and then apply the VP-µ model-checking algorithm of [START_REF] Alur | A fixpoint calculus for local and global program flows[END_REF] on this RSM. However, by doing so, we loose the explicit manipulation of the program's stack. Explicit push and pop instructions are not represented in a natural way anymore, and the stack of the RSM does not correspond to the stack of the assembly program anymore. Thus, it is not possible to state intuitive formulas that correspond to properties of the program's behaviors on the obtained RSM. Especially, when these formulas talk about the content of the program's stack. Thus, it is very important to have a direct algorithm for model-checking a branching-time temporal logic with matching of calls and returns for PDSs.

However, VP-µ is a heavy formalism that can't be used by novice users. Indeed, VP-µ can be seen as an extension of the modal µ calculus with several modalities loc , [loc], call , [call], ret , [ret] that allow to distinguish between calls, returns, and other statements (neither calls nor returns). Writing a simple specification in VP-µ is complicated. For example, the following simple property stating that "the configuration e can be reached in the same procedural context as the current configuration" can be described (as shown in [START_REF] Alur | A fixpoint calculus for local and global program flows[END_REF]) by the complex VP-µ formula ϕ 2 = µX(e ∨ loc X ∨ call ϕ 3 {X}) where ϕ 3 = µY ( ret R 1 ∨ loc Y ∨ call Y {Y }). Thus, we need to define a more intuitive branching-time temporal logic (in the style of CTL) that allow to talk naturally and intuitively about matching calls and returns.

Therefore, we define in this work the Branching temporal logic of CAlls and RETurns BCARET. BCARET can be seen as an extension of CTL with operators that allow to talk about matchings between calls and returns. Using BCARET, the above reachability property can be described in a simple way by the formula EF a e where EF a is a BCARET operator that means "there exists a run on which eventually in the future in the same procedural context". We consider the model-checking problem of PDSs against BCARET formulas with "standard" valuations (where an atomic proposition holds at a configuration c or not depends only on the control state of c, not on its stack) as well as regular valuations (where the set of configurations in which an atomic proposition holds is a regular set of configurations). We show that these problems can be effectively solved by a reduction to the emptiness problem of Alternating Büchi Pushdown Systems (ABPDSs). The latter problem can be solved effectively in [START_REF] Song | Efficient CTL model-checking for pushdown systems[END_REF]. Note that the regular valuation case cannot be solved by translating the PDSs to RSMs since as said previously, by doing the translation of PDSs to obtain RSMs, we loose the structure of the program's stack.

The rest of the paper is organized as follows. In Section 2, we define Labelled Pushdown Systems. In Section 3, we define the logic BCARET. Section 4 presents applications of BCARET in specifying malicious behaviours. Our algorithm to reduce BCARET model-checking to the membership problem of ABPDSs is presented in Section 5. Section 6 discusses the model-checking problem for PDSs against BCARET formulas with regular valuations. Finally, we conclude in Section 7. The proofs can be found in the full version of the paper [START_REF] Nguyen | BCARET model checking for pushdown systems[END_REF].

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 | CARET model checking 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: -The global-successors of p 1 , ω 1 and p 2 , ω 2 are p 2 , ω 2 and p 3 , ω 3 respectively. -The abstract-successors of p 2 , ω 2 and p 5 , ω 5 are p k , ω k and p 9 , ω 9 respectively.

• If p i , ω i = ⇒ P p i+1 ,
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.

Multi Automata

Definition 2. [START_REF] Bouajjani | Reachability analysis of pushdown automata: Application to model-checking[END_REF] Let P = (P, Γ, ∆, ) be a PDS. A P-Multi-Automaton (MA for short) is a tuple

A = (Q, Γ, δ, I, Q f ), where Q is a finite set of states, δ ⊆ Q × Γ × Q is a finite set of transition rules, I = P ⊆ Q is a set of initial states, Q f ⊆ Q is a set of final states. The transition relation - → δ ⊆ Q × Γ * × Q is defined as follows:
q -→ δ q for every q ∈ Q q γ -→ δ q if (q, γ, q ) ∈ δ if q ω -→ δ q and q γ -→ δ q , then, q ωγ --→ δ q A recognizes a configuration p, ω where p ∈ P , ω ∈ Γ * iff p ω -→ δ q for some q ∈ Q f . The language of A, L(A), is the set of all configurations which are recognized by A. A set of configurations is regular if it is recognized by some Multi-Automaton.

Branching Temporal Logic of Calls and Returns -BCARET

In this section, we define the Branching temporal logic of CAlls and RETurns BCARET. For technical reasons, we assume w.l.o.g. that BCARET formulas are given in positive normal form, i.e. negations are applied only to atomic propositions. To do that, we use the release operator R as a dual of the until operator U .

Definition 3. Syntax of BCARET

Let AP be a finite set of atomic propositions, a BCARET formula ϕ is defined as follows, where b ∈ {g, a}, e ∈ AP :

ϕ ::= true | f alse | e | ¬e | ϕ∨ϕ | ϕ∧ϕ | EX b ϕ | AX b ϕ | E[ϕU b ϕ] | A[ϕU b ϕ] | E[ϕR b ϕ] | A[ϕR b ϕ]
Let P = (P, Γ, ∆, ) be a PDS, λ : AP → 2 P ×Γ * be a labelling function that assigns to each atomic proposition e ∈ AP a set of configurations of P. The satisfiability relation of a BCARET formula ϕ at a configuration p 0 , ω 0 w.r.t. the labelling function λ, denoted by p 0 , ω 0 λ ϕ, is defined inductively as follows:

p 0 , ω 0 λ true for every p 0 , ω 0 p 0 , ω 0 λ f alse for every p 0 , ω 0 p 0 , ω 0 λ e (e ∈ AP ) iff p 0 , ω 0 ∈ λ(e)

-p 0 , ω 0 λ ¬e (e ∈ AP ) iff p 0 , ω 0 / ∈ λ(e) -p 0 , ω 0 λ ϕ 1 ∨ ϕ 2 iff ( p 0 , ω 0 λ ϕ 1 or p 0 , ω 0 λ ϕ 2 ) -p 0 , ω 0 λ ϕ 1 ∧ ϕ 2 iff ( p 0 , ω 0 λ ϕ 1 and p 0 , ω 0 λ ϕ 2 ) -p 0 , ω 0 λ EX g ϕ iff there exists a global-successor p , ω of p 0 , ω 0 such that p , ω λ ϕ -p 0 , ω 0 λ AX g ϕ iff p , ω λ ϕ for every global-successor p , ω of p 0 , ω 0 -p 0 , ω 0 λ E[ϕ 1 U g ϕ 2 ] iff there exists a global-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω ... of P starting from p 0 , ω 0 s.t. ∃i ≥ 0, p i , ω i λ ϕ 2 and for every 0 ≤ j < i, p j , ω j λ ϕ 1 -p 0 , ω 0 λ 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 λ ϕ 2 and for every 0 ≤ j < i, p j , ω j λ ϕ 1 -p 0 , ω 0 λ E[ϕ 1 R g ϕ 2 ] iff there exists a global-path π = p 0 , ω 0 p 1 , ω 1 p 2 , ω ... of P starting from p 0 , ω 0 s.t. for every i ≥ 0, if p i , ω i λ ϕ 2 then there exists 0 ≤ j < i s.t. p j , ω j λ ϕ 1 -p 0 , ω 0 λ 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 λ ϕ 2 then there exists 0 ≤ j < i s.t. p j , ω j λ ϕ 1 -p 0 , ω 0 λ EX a ϕ iff there exists an abstract-successor p , ω of p 0 , ω 0 such that p , ω λ ϕ -p 0 , ω 0 λ AX a ϕ iff p , ω λ ϕ for every abstract-successor p , ω of p 0 , ω 0 -p 0 , ω 0 λ E[ϕ 1 U a ϕ 2 ]
iff there exists an abstract-path π = p 0 , ω 0 p 1 , ω 1 p , ω 2 ... of P starting from p 0 , ω 0 s.t. ∃i ≥ 0, p i , ω i λ ϕ 2 and for every 0 ≤ j < i, p j , ω j λ ϕ 1 p 0 , ω 0 λ 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 λ ϕ 2 and for every 0 ≤ j < i, p j , ω j λ ϕ 1 p 0 , ω 0 λ E[ϕ 1 R a ϕ 2 ] iff there exists an abstract-path π = p 0 , ω 0 p 1 , ω 1 p , ω 2 ... of P starting from p 0 , ω 0 s.t. for every i ≥ 0, if p i , ω i λ ϕ 2 then there exists 0 ≤ j < i s.t. p j , ω j λ ϕ 1 p 0 , ω 0 λ 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 λ ϕ 2 then there exists 0 ≤ j < i s.t. p j , ω j λ ϕ 1

Other BCARET 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 BCARET formula ϕ, the closure Cl(ϕ) is the set of all subformulae of ϕ, including ϕ.

Regular Valuations. We talk about regular valuations when for every e ∈ AP , λ(e) is a regular language.

Remark 1. CTL can be seen as the subclass of BCARET where the operators

EX a ϕ, AX a ϕ, E[ϕU a ϕ], A[ϕU a ϕ], E[ϕR a ϕ], A[ϕR a ϕ] are not considered.

Application

In this section, we show how BCARET can be used to describe branching-time malicious behaviors. More malicious behaviors can be found in the full version of the paper [START_REF] Nguyen | BCARET model checking for pushdown systems[END_REF].

Spyware Behavior. The typical behaviour of a spyware is hunting for personal information (emails, bank account information,...) on local drives by searching files matching certain conditions. To do that, it has to search directories of the host to look for interesting files whose names match a specific condition. When a file is found, the spyware will invoke a payload to steal the information, then continue looking for the remaining matching files. When a folder is found, it will enter the folder path and continue scanning that folder recursively. To achieve this behavior, the spyware first calls the API function 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 succeeds or not. If the function call fails, the spyware will call the function GetLastError. Otherwise, if the function call is successful, F indF irstF ileA will return a search handle h. 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 API function F indN extF ileA using h as first parameter to look for the remaining matching files. This behavior cannot be expressed by LTL or CTL because it requires to express that the return value of the function F indF irstF ileA should be used as input to the API function F indN extF ileA. It cannot be described by CARET neither (because this is a branching-time property). 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 which contain the values of search handles h in the program, EX a is a BCARET operator that means "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 that means "eventually in all runs, in the same procedural context".

In binary codes and assembly programs, the return value of an API function is put in the register eax. Thus, the return value of F indF irstF ileA is the value of eax at its corresponding return-point. Then, the subformula (call(FindFirstFileA)∧ EX a (eax = d)) states that there is a call to the API F indF irstF ileA and the return value of this function is d (the abstract successor of a call is its corresponding return-point). When FindNextFileA is invoked, it requires a search handle as parameter and this search handle must be put on top of the program stack (since parameters are passed through the stack in assembly). The requirement that d is on top of the program stack is expressed by the regular expression dΓ * . Thus, the subformula [call(FindNextFileA) ∧ dΓ * ] expresses that FindNextFileA is called with d as parameter (d stores the information of the search handle). Therefore, ϕ sb expresses then that there is a call to the API F indF irstF ileA with the return value d (the search handle), then, in all runs starting from that call, there will be either a call to the API function GetLastError or a call to the function F indF irstF ileA or a call to the function F indN extF ileA in which d is used as a parameter.

To detect spyware, [START_REF] Nguyen | CARET model checking for pushdown systems[END_REF] used the following CARET formula:

ϕ sb = d∈D F g (call(FindFirstFileA) ∧ X a (eax = d) ∧ F a (call(FindNextFileA) ∧ dΓ * ))
It can be seen that this CARET formula ϕ sb is not as precise as the BCARET formula ϕ sb , as it does not deal with the case when the returned result of F indF irstF ileA is a folder or an error. Thus, this CARET formula ϕ sb may lead to false alarms that can be avoided using our BCARET formula ϕ sb . BCARET can deal with it because BCARET is a branching-time temporal logic. For example, AF a allows us to take into account all possible abstract-paths from a certain state in the computation tree. By using AF a , ϕ sb can deal with different returned values of F indF irstF ileA as presented above.

BCARET Model-Checking for Pushdown Systems

In this section, we consider "standard" BCARET model-checking for pushdown systems where an atomic proposition holds at a configuration c or not depends only on the control state of c, not on its stack.

Alternating Büchi Pushdown Systems (ABPDSs).

Definition 4. An Alternating Büchi Pushdown System (ABPDS) is a tuple BP = (P, Γ, ∆, F ), where P is a set of control locations, Γ is the stack alphabet, F ⊆ P is a set of accepting control locations and ∆ is a transition function that maps each element of P × Γ with a positive boolean formula over P × Γ * .

A configuration of BP is a pair p, ω , where p ∈ P is the current control location and ω ∈ Γ * is the current stack content. Without loss of generality, we suppose that the boolean formulas of ABPDSs are in disjunctive normal form n j=1 mj i=1 p j i , ω j i . Then, we can see ∆ as a subset of (P × Γ ) × 2 P ×Γ * by rewriting the rules of ∆ in the form p, γ → n j=1 mj i=1 p j i , ω j i as n rules of the form p, γ → { p j 1 , ω j 1 , ..., p j mj , ω j mj }, where 1 ≤ j ≤ n. Let p, γ → { p 1 , ω 1 , ..., p n , ω n } be a rule of ∆, then, for every ω ∈ Γ * , the configuration p, γω (resp. { p 1 , ω 1 ω , ..., p n , ω n ω }) is an immediate predecessor (resp. successor) of { p 1 , ω 1 ω , ..., p n , ω n ω } (resp. p, γω ).

A run ρ of BP starting form an initial configuration p 0 , ω 0 is a tree whose root is labelled by p 0 , ω 0 , and whose other nodes are labelled by elements in P × Γ * . If a node of ρ is labelled by a configuration p, ω and has n children labelled by p 1 , ω 1 , ..., p n , ω n respectively, then, p, ω must be a predecessor of { p 1 , ω 1 , ..., p 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ϕ as follows:

(1) c = ⇒ BP {c} for every c ∈ P × Γ * , (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 1. [START_REF] Song | Efficient CTL model-checking for pushdown systems[END_REF] Given an ABPDS BP = (P, Γ, ∆, F ), for every configuration p, ω ∈ P × Γ * , whether or not p, ω ∈ L(BP) can be decided in time

O(|P | 2 .|Γ |.(|∆|2 5|P | + 2 |P | |ω|)).

From BCARET model checking of PDSs to the membership problem in ABPDSs

Let P = (P, Γ, ∆, ) be a pushdown system with an initial configuration c 0 . Given a set of atomic propositions AP , let ϕ be a BCARET formula. Let f : AP → 2 P be a function that associates each atomic proposition with a set of control states, and λ f : AP → 2 P ×Γ * be a labelling function s.t. for every e ∈ AP , λ f (e) = { p, ω | p ∈ f (e), ω ∈ Γ * }. In this section, we propose an algorithm to check whether c 0 λ f ϕ. Intuitively, we construct an Alternating Büchi Pushdown System BP ϕ which recognizes a configuration c iff c λ f ϕ.

Then to check whether c 0 λ f ϕ, we will check if c 0 ∈ L(BP ϕ ). The membership problem of an ABPDS can be solved effectively by Theorem 1.

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

-

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

(α1) If φ = e, e ∈ AP and p ∈ f (e), then, p, φ , γ → p, φ , γ ∈ ∆ (α2) If φ = ¬e, e ∈ AP and p / ∈ f (e), then, p, φ , γ → p, φ , γ ∈ ∆ (α3) If φ = φ 1 ∧ φ 2 , then, p, φ , γ → p, φ 1 , γ ∧ p, φ 2 , γ ∈ ∆ (α4) If φ = φ 1 ∨ φ 2 , then, p, φ , γ → p, φ 1 , γ ∨ p, φ 2 , γ ∈ ∆ (α5) If φ = EX g φ 1 , then p, φ , γ → p,γ t - → q,ω ∈∆ q, φ 1 , ω ∈ ∆ where t ∈ {call, int, ret} (α6) If φ = AX g φ 1 , then, p, φ , γ → p,γ t - → q,ω ∈∆ q, φ 1 , ω ∈ ∆ (α7) If φ = EX a φ 1 , then, p, φ , γ → h 1 ∨ h 2 ∨ h 3 ∈ ∆ , where -h 1 = p,γ call --→ q,γ1γ2 ∈∆ q, γ 1 γ 2 , φ 1 -h 2 = p,γ int --→ q,ω ∈∆ q, φ 1 , ω -h 3 = p,γ ret --→ q, ∈∆ p ⊥ , γ ⊥ (α8) If φ = AX a φ 1 , then, p, φ , γ → h 1 ∧ h 2 ∧ h 3 ∈ ∆ , where -h 1 = p,γ call --→ q,γ1γ2 ∈∆ q, γ 1 γ 2 , φ 1 -h 2 = p,γ int --→ q,ω ∈∆ q, φ 1 , ω -h 3 = p,γ ret --→ q, ∈∆ p ⊥ , γ ⊥ (α9) If φ = E[φ 1 U g φ 2 ], then, p, φ , γ → p, φ 2 , γ ∨ p,γ t - → q,ω ∈∆ ( p, φ 1 , γ ∧ q, φ , ω ) ∈ ∆ (α10) If φ = E[φ 1 U a φ 2 ], then, p, φ , γ → p, φ 2 , γ ∨ h 1 ∨ h 2 ∨ h 3 ∈ ∆ , where -h 1 = p,γ call --→ q,γ1γ2 ∈∆ p, φ 1 , γ ∧ q, γ 1 γ 2 , φ -h 2 = p,γ int --→ q,ω ∈∆ p, φ 1 , γ ∧ q, φ , ω -h 3 = p,γ ret --→ q, ∈∆ p ⊥ , γ ⊥ (α11) If φ = A[φ 1 U g φ 2 ], then, p, φ , γ → p, φ 2 , γ ∨ p,γ t - → q,ω ∈∆ ( p, φ 1 , γ ∧ q, φ , ω ) ∈ ∆ (α12) If φ = A[φ 1 U a φ 2 ], then, p, φ , γ → p, φ 2 , γ ∨ (h 1 ∧ h 2 ∧ h 3 ) ∈ ∆ , where -h 1 = p,γ call --→ q,γ1γ2 ∈∆ p, φ 1 , γ ∧ q, γ 1 γ 2 , φ -h 2 = p,γ int --→ q,ω ∈∆ p, φ 1 , γ ∧ q, φ , ω -h 3 = p,γ ret --→ q, ∈∆ p ⊥ , γ ⊥ (α13) If φ = E[φ 1 R g φ 2 ]
, then, we add to ∆ the rule:

p, φ , γ → ( p, φ 2 , γ ∧ p, φ 1 , γ )∨( p,γ t - → q,ω ∈∆ ( p, φ 2 , γ ∧ q, φ , ω ) (α14) If φ = A[φ 1 R g φ 2 ]
, then, we add to ∆ the rule:

p, φ , γ → ( p, φ 2 , γ ∧ p, φ 1 , γ )∨( p,γ t - → q,ω ∈∆ ( p, φ 2 , γ ∧ q, φ , ω ) (α15) If φ = E[φ 1 R a φ 2 ]: p, φ , γ → ( p, φ 2 , γ ∧ p, φ 1 , γ ) ∨ h 1 ∨ h 2 ∨ h 3 ∈ ∆ , where -h 1 = p,γ call --→ q,γ1γ2 ∈∆ p, φ 2 , γ ∧ q, γ 1 γ 2 , φ -h 2 = p,γ int --→ q,ω ∈∆ p, φ 2 , γ ∧ q, φ , ω -h 3 = p,γ ret --→ q, ∈∆ p ⊥ , γ ⊥ (α16) If φ = A[φ 1 R a φ 2 ], p, φ , γ → ( p, φ 2 , γ ∧ p, φ 1 , γ )∨(h 1 ∧h 2 ∧h 3 ) ∈ ∆ , where -h 1 = p,γ call --→ q,γ1γ2 ∈∆ p, φ 2 , γ ∧ q, γ 1 γ 2 , φ -h 2 = p,γ int --→ q,ω ∈∆ p, φ 2 , γ ∧ q, φ , ω -h 3 = p,γ ret --→ q, ∈∆ p ⊥ , γ ⊥ (α17) for every p, γ ret --→ q, ∈ ∆: -q, γ , φ 1 → q, φ 1 , γ ∈ ∆ for every γ ∈ Γ , φ 1 ∈ Cl(ϕ) (α18) p ⊥ , γ ⊥ → p ⊥ , γ ⊥ ∈ ∆
Roughly speaking, the ABPDS BP ϕ is a kind of product between P and the BCARET formula ϕ which ensures that BP ϕ has an accepting run from p, ϕ , ω iff the configuration p, ω satisfies ϕ. The form of the control locations of BP ϕ is p, φ where φ ∈ Cl(ϕ). Let us explain the intuition behind our construction:

-If φ = e ∈ AP , then, for every ω ∈ Γ * , p, ω λ f φ iff p ∈ f (e). In other words, BP ϕ should have an accepting run from p, e , ω iff p ∈ f (e). This is ensured by the transition rules in (α1) which add a loop at p, e , ω where p ∈ f (e) and the fact that p, e ∈ F . -If φ = ¬e (e ∈ AP ), then, for every ω ∈ Γ * , p, ω λ f φ iff p / ∈ f (e). In other words, BP ϕ should have an accepting run from p, ¬e , ω iff p / ∈ f (e). This is ensured by the transition rules in (α2) which add a loop at p, ¬e , ω where p / ∈ f (e) and the fact that p, ¬e ∈ F .

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

-If φ = E[φ 1 U g φ 2 ], then, for every ω ∈ Γ * , p, ω λ f φ iff p, ω λ f φ 2 or
( p, ω λ f φ 1 and there exists an immediate successor p , ω of p, ω s.t. p , ω λ f φ). This is ensured by the transition rules in (α9) stating that BP ϕ has an accepting run from p, E[φ 1 U g φ 2 ] , ω iff BP ϕ has an accepting run from p, φ 2 , ω or (BP ϕ has an accepting run from both p, φ 1 , ω and p , φ , ω where p , ω is an immediate successor of p, ω ). (α11) is similar to (α9).

-

If φ = E[φ 1 R g φ 2 ]
, then, for every ω ∈ Γ * , p, ω λ f φ iff ( p, ω λ f φ 2 and p, ω λ f φ 1 ) or ( p, ω λ f φ 2 and there exists an immediate successor p , ω of p, ω s.t. p , ω λ f φ). This is ensured by the transition rules in (α13) stating that BP ϕ has an accepting run from p, E[φ 1 R g φ 2 ] , ω iff BP ϕ has an accepting run from both p, φ 2 , ω and p, φ 1 , ω ; or BP ϕ has an accepting run from both p, φ 2 , ω and p , φ , ω where p , ω is an immediate successor of p, ω . 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, φ to the Büchi accepting condition F (via the subset F 3 of F ). ( α14) is similar to (α13).

-If φ = EX g φ 1 , then, for every ω ∈ Γ * , p, ω λ f φ iff there exists an immediate successor p , ω of p, ω s.t. p , ω λ f φ 1 . This is ensured by the transition rules in (α5) stating that BP ϕ has an accepting run from p, EX g φ 1 , ω iff there exists an immediate successor p , ω of p, ω s.t. BP ϕ has an accepting run from p , φ 1 , ω . (α6) is similar to (α5).

-If φ = EX a φ 1 , then, for every ω ∈ Γ * , p, ω λ f φ iff there exists an abstract-successor p k , ω k of p, ω s.t. p k , ω k λ f φ 1 (A1) .
Let π ∈ T races( p, ω ) be a run starting from p, ω on which p k , ω k is the abstractsuccessor of p, ω . Over π, let p , ω be the immediate successor of p, ω . In what follows, we explain how we can ensure (A1).

1. Firstly, we show that for every abstract-successor p k , ω k = ⊥ of p, ω , p, EX a φ 1 , ω = ⇒ BPϕ p k , φ 1 , ω k . There are two possibilities:

• If p, ω = ⇒ P p , ω corresponds to a call statement. Let us consider Figure 2 to explain this case. p, φ , ω = ⇒ BPϕ p k , φ 1 , ω k is ensured by rules corresponding to h 1 in (α7), the rules in ∆ ⊆ ∆ and the rules in (α17) as follows: rules corresponding to h 1 in (α7) allow to record φ 1 in the return point of the call, rules in ∆ ⊆ ∆ allow to mimic the run of the PDS P and rules in (α17) allow to extract and put back φ 1 when the return-point is reached. In what follows, we show in more details how this works: Let p, γ call --→ p , γ γ be the rule associated with the transition p, ω = ⇒ P p , ω , then we have ω = γω and ω = γ γ ω . Let p k-1 , ω k-1 = ⇒ P p k , ω k be the transition that corresponds to the ret statement of this call on π. Let then p k-1 , β ret --→ p k , ∈ ∆ be the corresponding return rule. Then, we have necessarily ω k-1 = βγ ω , since as explained in Section 2, γ is the return address of the call. After applying this rule, ω k = γ ω . In other words, γ will be the topmost stack symbol at the corresponding return point of the call. So, in order to ensure that p, φ , ω = ⇒ BPϕ p k , φ 1 , ω k , we proceed as follows:

At the call p, γ call --→ p , γ γ , we encode the formula φ 1 into γ by the rule corresponding to h 1 in (α7) stating that p, EX a φ 1 , γ -→ p , γ γ , φ 1 ∈ ∆ . This allows to record φ 1 in the corresponding return point of the stack. After that, the rules in ∆ ⊆ ∆ 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 , γ γ , φ 1 ω = ⇒ BPϕ p k-1 , β γ , φ 1 ω = ⇒ BPϕ p k , γ , φ 1 ω using the rules of ∆. At the return-point, we extract φ 1 from the stack and encode it into p k by adding the transition rules in (α17) p k , γ , φ 1 → p k , φ 1 , γ . Therefore, we obtain that p, φ , ω = ⇒ BPϕ p k , φ 1 , ω 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 corresponding to h 2 in (α7), we get that p, EX a φ 1 , ω = ⇒ BPϕ p , φ 1 , ω . Therefore, p, EX a φ 1 , ω = ⇒ BPϕ p k , φ 1 , ω 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 , ω , we need to ensure that the path of BP ϕ reflecting the possibility in (A1) that p k , ω k λ f φ 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 corresponding to h 3 in (α7) to allow p, EX a φ 1 , ω = ⇒ BPϕ p ⊥ , γ ⊥ ω . Since a run of BP ϕ includes only infinite paths, we equip these trap configurations with self-loops by the transition rules in (α18), i.e., p ⊥ , γ ⊥ ω = ⇒ BPϕ p ⊥ , γ ⊥ ω . As a result, we obtain a corresponding path in

BP ϕ : p, EX a φ 1 , ω = ⇒ BPϕ p ⊥ , γ ⊥ ω = ⇒ BPϕ p ⊥ , γ ⊥ ω . Note that this path is not accepted by BP ϕ because p ⊥ / ∈ F .
In summary, for every abstract-successor

p k , ω k of p, ω , if p k , ω k = ⊥, then, p, EX a φ 1 , ω = ⇒ BPϕ p k , φ 1 , ω k ; otherwise p, EX a φ 1 , ω = ⇒ BPϕ p ⊥ , γ ⊥ ω = ⇒ BPϕ p ⊥ , γ ⊥ ω
which is not accepted by BP ϕ . Therefore, (A1) is ensured by the transition rules in (α7) stating that BP ϕ has an accepting run from p, EX a φ 1 , ω iff there exists an abstract successor p k , ω k of p, ω s.t. BP ϕ has an accepting run from p k , φ 1 , ω k .

-If φ = AX a φ 1 : this case is ensured by the transition rules in (α8) together with (α17) and ∆ ⊆ ∆ . The intuition of (α8) is similar to that of (α7).

-If φ = E[φ 1 U a φ 2 ], then, for every ω ∈ Γ * , p, ω λ f φ iff p, ω λ f φ 2 or
( p, ω λ f φ 1 and there exists an abstract successor p k , ω k of p, ω s.t. p k , ω k λ f φ) (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 , ω k = ⊥ of p, ω , p, φ , ω = ⇒ BPϕ { p, φ 1 , ω , p k , φ , ω k }.
There are two possibilities:

• If p, ω = ⇒ P p , ω corresponds to a call statement. From the rules corresponding to h 1 in (α10), we get that p, φ , ω = ⇒ BPϕ { p, φ 1 , ω , p , ω } where p , ω is the immediate successor of p, ω . Thus, to ensure that p, φ , ω = ⇒ BPϕ { p, φ 1 , ω , p k , φ , ω k }, we only need to ensure that p , ω = ⇒ BPϕ p k , φ , ω k . As for the case φ = EX a φ 1 , p , ω = ⇒ BPϕ p k , φ , ω k is ensured by the rules in ∆ ⊆ ∆ and the rules in (α17):

rules in ∆ ⊆ ∆ allow to mimic the run of the PDS P before the return and rules in (α17) 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 = p , ω . From the transition rules corresponding to h 2 in (α10), we get that p, E[φ

1 U a φ 2 ] , ω = ⇒ BPϕ { p, φ 1 , ω , p , φ , ω }. Therefore, p, E[φ 1 U a φ 2 ] , ω = ⇒ BPϕ { p, φ 1 , ω , p k , φ , ω k }.
In other words, BP ϕ has an accepting run from both p, φ 1 , ω and p k , φ , ω 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 ] , ω , we need to ensure that the path reflecting the possibility in (A2) that ( p, ω λ f φ 1 and p k , ω k λ f φ) is not accepted by BP ϕ . This is ensured as for the case φ = EX a φ 1 by the transition rules corresponding to h 3 in (α10).

In summary, for every abstract-successor

p k , ω k of p, ω , if p k , ω k = ⊥, then, p, E[φ 1 U a φ 2 ] , ω = ⇒ BPϕ { p, φ 1 , ω , p k , E[φ 1 U a φ 2 ] , ω k }; other- wise p, E[φ 1 U a φ 2 ] , ω = ⇒ BPϕ p ⊥ , γ ⊥ ω = ⇒ BPϕ p ⊥ , γ ⊥ ω
= A[φ 1 U a φ 2 ], φ = E[φ 1 R a φ 2 ], φ = A[φ 1 R a φ 2 ]
are similar to the previous cases.

The Büchi accepting condition. The elements of the Büchi accepting condition set F of BP ϕ ensure the liveness requirements of until-formulas on infinite global paths, infinite abstract paths as well as on finite abstract paths.

-With regards to infinite global paths, the fact that the liveness requirement φ 2 in E[φ 1 U g φ 2 ] is eventually satisfied in P is ensured by the fact that p, E[φ 1 U g φ 2 ] doesn't belong to F . Note that p, ω

λ f E[φ 1 U g φ 2 ]
iff p, ω λ f φ 2 or there exists a global-successor p , ω s.t. ( p, ω λ f φ 1 and p , ω

λ f E[φ 1 U g φ 2 ]
). Because φ 2 should hold eventually, to avoid the case where a run of BP ϕ always carries E[φ 1 U g φ 2 ] and never reaches φ 2 , we don't set p, E[φ 1 U g φ 2 ] as an element of the Büchi accepting condition set. This guarantees that the accepting run of BP ϕ must visit some control locations in p, φ 2 which ensures that φ 2 will eventually hold. The liveness requirements of A[φ 1 U g φ 2 ] are ensured as for the case of

E[φ 1 U g φ 2 ].
-With regards to infinite abstract paths, the fact that the liveness requirement -With regards to finite abstract paths p 0 , ω 0 p 1 , ω 1 ... p m , ω m where p m , ω m = ⇒ P p m+1 , ω m+1 corresponds to a return statement, the fact that the liveness requirement φ 2 in E[φ 1 U g φ 2 ] is eventually satisfied in P is ensured by the fact that p ⊥ doesn't belong to F . Look at Figure 3 for an illustration. In this figure, for every i + 1 ≤ u ≤ k -1, the abstract path starting from p u , ω u is finite because the abstract successor of p k-1 , ω k-1 is ⊥ since p k-1 , ω k-1 = ⇒ P p k , ω k corresponds to a return statement. Suppose that we want to check whether

φ 2 in E[φ 1 U a φ 2 ] is
p k-1 , ω k-1 λ f E[φ 1 U a φ 2 ], then, we get that p k-1 , ω k-1 λ f E[φ 1 U a φ 2 ] iff p k-1 , ω k-1 λ f φ 2 or there ex- ists an abstract-successor p , ω s.t. ( p k-1 , ω k-1 λ f φ 1 and p , ω λ f E[φ 1 U a φ 2 ]
). Since φ 2 should eventually hold, φ 2 should hold at p k-1 , ω k-1 because the abstract-successor of p k-1 , ω k-1 on this abstract-path is ⊥.

To ensure this, we move p k-1 , ω k-1 to the trap configuration p ⊥ , γ ⊥ and add a loop here by the transition rule (α18). In addition, we don't set p ⊥ as an element of the Büchi accepting condition set, which means that

p k-1 , ω k-1 λ f E[φ 1 U a φ 2 ] iff p k-1 , ω k-1 λ f φ 2
by the transition rules in (α10). This ensures the liveness requirement φ 2 in E[φ 1 U a φ 2 ] is eventually satisfied.

-With regards to finite abstract paths p 0 , ω 0 p 1 , ω 1 ... p m , ω m where p m , ω m = ⇒ P p m+1 , ω m+1 corresponds to a call statement but this call never reaches its corresponding return-point, the fact that the liveness requirement φ 2 in E[φ 1 U g φ 2 ] is eventually satisfied in P is ensured by the fact that p / ∈ F . Look at Figure 4 where the procedure proc never terminates. In this figure, for every 0 ≤ u ≤ i, the abstract path starting from p u , ω u is finite. Suppose that we want to check whether p i , ω i λ f E[φ 1 U a φ 2 ], then, we get that p i , ω i λ f E[φ 1 U a φ 2 ] iff p i , ω i λ f φ 2 or there exists an abstractsuccessor p , ω s.t. ( p i , ω i λ f φ 1 and p , ω

λ f E[φ 1 U a φ 2 ]
). Since φ 2 should eventually hold, φ 2 should hold at p i , ω i because the abstractsuccessor of p i , ω i on this abstract-path is ⊥. As explained above, at p i , ω i , we will encode the formula E[φ 1 U a φ 2 ] into the stack and mimic the run of P on BP ϕ until it reaches the corresponding return-point of the call. In other words, if the call is never reached, the run of BP ϕ will infinitely visit the control locations of P. To ensure this path unaccepted, we don't set p ∈ P as an element of the Büchi accepting condition set, which means that p i , ω i λ f E[φ 1 U a φ 2 ] iff p i , ω i λ f φ 2 by the transition rules in (α10). This ensures the liveness requirement φ 2 in E[φ 1 U a φ 2 ] is eventually satisfied. Thus, we can show that (the proof can be found in the full version of the paper [START_REF] Nguyen | BCARET model checking for pushdown systems[END_REF]):

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

The number of control locations of BP ϕ is at most O(|P ||ϕ|), the number of stack symbols is at most O(|Γ ||ϕ|) and the number of transitions is at most O(|P ||Γ ||∆||ϕ|). Therefore, we get from Theorems 1 and 2: Theorem 3. Given a PDS P = (P, Γ, ∆, ), a set of atomic propositions AP , a labelling function f : AP → 2 P and a BCARET formula ϕ, for every configuration p, ω ∈ P × Γ * , whether or not p, ω satisfies ϕ can be solved in time

O(|P | 2 |ϕ| 3 .|Γ |(|P ||Γ ||∆|.|ϕ|.2 5|P ||ϕ| + 2 |P ||ϕ| .|ω|))

BCARET model-checking for PDSs with regular valuations

Up to now, we have considered the standard model-checking problem for BCARET, where the validity of an atomic proposition depends only on the control state, not on the stack. In this section, we go further and consider model-checking with regular valuations where the set of configurations in which an atomic proposition holds is a regular set of configurations (see Section 3 for a formal definition of regular valuations).

From BCARET model checking of PDSs with regular valuations to the membership problem in ABPDSs

Given a pushdown system P = (P, Γ, ∆, ), and a set of atomic propositions AP , let ϕ be a BCARET formula over AP , λ : AP → 2 P ×Γ * be a labelling function s.t. for every e ∈ AP , λ(e) is a regular set of configurations. Given a configuration c 0 , we propose in this section an algorithm to check whether c 0 λ ϕ. Intuitively, we compute an ABPDS BP ϕ s.t. BP ϕ recognizes a configuration c of P iff c λ ϕ.

Then, to check if c 0 satisfies ϕ, we will check whether BP ϕ recognizes c 0 .

For every e ∈ AP , since λ(e) is a regular set of configurations, let M e = (Q e , Γ, δ e , I e , F e ) be a multi-automaton s.t. L(M e ) = λ(e), M ¬e = (Q ¬e , Γ, δ ¬e , I ¬e , F ¬e ) be a multi-automaton s.t. L(M ¬e ) = P × Γ * \ λ(e), which means M ¬e will recognize the complement of λ(e) that is the set of configurations in which e doesn't hold. Note that for every e ∈ AP , the initial states of M e and M ¬e are the control locations p ∈ P. Thus, to distinguish between the initial states of these two automata, we will denote the initial state corresponding to the control location p in M e (resp. M ¬e ) by p e (resp. p ¬e ). Let AP

+ (ϕ) = {e ∈ AP | e ∈ Cl(ϕ)} and AP -(ϕ) = {e ∈ AP | ¬e ∈ Cl(ϕ)}.
Let BP ϕ = (P , Γ , ∆ , F ) be the ABPDS defined as follows:

- The transition relation ∆ is the smallest set of transition rules defined as follows: ∆ ⊆ ∆ , ∆ 0 ⊆ ∆ where ∆ 0 is the transitions of ∆ that are created by the rules from (α3) to (α18) and such that: (β1) for every p ∈ P , e ∈ AP + (ϕ), γ ∈ Γ : p, e , γ → p e , γ ∈ ∆ (β2) for every p ∈ P , e ∈ AP -(ϕ), γ ∈ Γ : p, ¬e , γ → p ¬e , γ ∈ ∆ (β3) for very (q 1 , γ, q 2 ) ∈ ( e∈AP + (ϕ) δ e )∪( e∈AP -(ϕ) δ ¬e ): q 1 , γ → q 2 , ∈ ∆ (β4) for very q ∈ ( e∈AP + (ϕ) F e ) ∪ ( e∈AP -(ϕ) F ¬e ): q, → q, ∈ ∆ Intuitively, we compute the ABPDS BP ϕ such that BP ϕ has an accepting run from p, φ , ω iff the configuration p, ω satisfies φ according to the regular labellings M e for every e ∈ AP . The only difference with the previous case of standard valuations, where an atomic proposition holds at a configuration depends only on the control location of that configuration, not on its stack, comes from the interpretation of the atomic proposition e. This is why ∆ contains ∆ and ∆ 0 (which are the transitions of BP ϕ that don't consider the atomic propositions). Here the rules (β 1 ) -(β 4 ) deal with the cases e, ¬e (e ∈ AP ). Given p ∈ P , φ = e ∈ AP , ω ∈ Γ * , we get that the ABPDS BP ϕ should accept p, e , ω iff p, ω ∈ L(M e ). To check whether p, ω ∈ L(M e ), we let BP ϕ go to state p e , the initial state corresponding to p in M e by adding rules in (β1); and then, from this state, we will check whether ω is accepted by M e . This is ensured by the transition rules in (β3) and (β4). (β3) lets BP ϕ mimic a run of M e on ω, i.e., if BP ϕ is in a state q 1 with γ on the top of the stack, and if (q 1 , γ, q 2 ) is a transition rule in M e , then, BP ϕ will move to state q 2 and pop γ from its stack. Note that popping γ allows us to check the rest of the word. In M e , a configuration is accepted if the run with the word ω reaches the 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 add F e as a set of accepting control locations in BP ϕ . Since BP ϕ only recognizes infinite paths, (β4) adds a loop on every configuration q, where q ∈ F e . The intuition behind the transition rules in (β2) is similar to that of (β1). They correspond to the case where φ = ¬e.

P = P ∪ P × Cl(ϕ) ∪ {p ⊥ } ∪ e∈AP + (ϕ) Q e ∪ e∈AP -(ϕ) Q ¬e -Γ = Γ ∪ (Γ × Cl(ϕ)) ∪ {γ ⊥ } -F = F 1 ∪ F 2 ∪ F 3 where • F 1 = e∈AP + (ϕ) F e • F 2 = e∈AP -(ϕ) F ¬e • F 3 = {P × Cl R (

Conclusion

In this paper, we introduce the Branching temporal logic of CAlls and RETurns BCARET and show how it can be used to describe malicious behaviors that CARET and other specification formalisms cannot. We present an algorithm for "standard" BCARET model checking for PDSs where whether a configuration of a PDS satisfies an atomic proposition or not depends only on the control location of that configuration. Moreover, we consider BCARET model-checking for PDSs with regular valuations where the set of configurations on which an atomic proposition holds is a regular language. Our approach is based on reducing these problems to the emptiness problem of Alternating Büchi Pushdown Systems.

Fig. 1 :

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

Fig. 2 :

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

Fig. 3 : 1 Fig. 4 :

 314 Fig. 3: p i , ω i finally reach its corresponding return-point

  ϕ)} where Cl R (ϕ) is the set of formulas of Cl(ϕ) in the form E[ϕ 1 R b ϕ 2 ] or A[ϕ 1 R b ϕ 2 ] (b ∈ {g, a})

Theorem 4 . 4 : 5 .

 445 Given a PDS P = (P, Γ, ∆, ), a set of atomic propositions AP , a regular labelling function λ : AP → 2 P ×Γ * and a BCARET formula ϕ, we can compute an ABPDS BP ϕ such that for every configuration p, ω , p, ω λ ϕ iff BP ϕ has an accepting run from the configuration p, ϕ , ωThe number of control locations of BP ϕ is at mostO(|P ||ϕ| + k) where k = e∈AP + (ϕ) |Q e | + e∈AP -(ϕ) |Q ¬e |,the number of stack symbols is at most O(|Γ ||ϕ|) and the number of transitions is at most O(|P ||Γ ||∆||ϕ| + d) where d = e∈AP + (ϕ) |δ e | + e∈AP -(ϕ) |δ ¬e |. Therefore, we get from Theorems 1 and Theorem Given a PDS P = (P, Γ, ∆, ), a set of atomic propositions AP , a regular labelling function λ : AP → 2 P ×Γ * and a BCARET formula ϕ, for every configuration p, ω ∈ P × Γ * , whether or not p, ω satisfies ϕ can be solved in time O((|P ||ϕ| + k) 2 .|Γ ||ϕ|((|P ||Γ ||∆||ϕ| + d).2 5(|P ||ϕ|+k) + 2 |P ||ϕ|+k .|ω|))

  ω 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, (A2) is ensured by the transition rules in (α10) stating that BP ϕ has an accepting run from p, E[φ 1 U a φ 2 ] , ω iff BP ϕ has an accepting run from p, φ 2 , ω ; or BP ϕ has an accepting run from both p, φ 1 , ω and p k , E[φ 1 U a φ 2 ] , ω k where p k , ω k is an abstract successor of p, ω .-The intuition behind the rules corresponding to the cases φ

  eventually satisfied in P is ensured by the fact that p, E[φ 1 U a φ 2 ] doesn't belong to F . The intuition behind this case is similar to the intuition of E[φ 1 U g φ 2 ]. The liveness requirements of A[φ 1 U a φ 2 ] are ensured as for the case of E[φ 1 U a φ 2 ].

			EX a φ1	encoded & passed down	γ , φ1	p k , ω k
	p0, ω0	call	pi, ωi		return-point
		proc pi+1, ωi+1	p k-2 , ω k-2	ret p k-1 , ω k-1