Gwen Salaün

Lina Ye

Stability of Asynchronously Communicating Systems

Keywords: Communicating Systems, Labelled Transition Systems, Unbounded Buffers, Automated Verification Systèmes communicants, systèmes de transitions étiquetées, buffers non bornés, vérification automatique

Recent software is mostly constructed by reusing and composing existing components. Software components are usually stateful and therefore described using behavioral models such as finite state machines. Asynchronous communication is a classic interaction mechanism used for such software systems. However, analyzing communicating systems interacting asynchronously via reliable FIFO buffers is an undecidable problem. A typical approach is to check whether the system is bounded, and if not, the corresponding state space can be made finite by limiting the presence of communication cycles in behavioral models or by fixing buffer sizes. In this paper, our focus is on systems that are likely to be unbounded and therefore result in infinite systems. We do not want to restrict the system by imposing any arbitrary bounds. We introduce a notion of stability and prove that once the system is stable for a specific buffer bound, it remains stable whatever larger bounds are chosen for buffers. This enables us to check certain properties on the system for that bound and to ensure that the system will preserve them whatever larger bounds are used for buffers. We also prove that computing this bound is undecidable but we show how we succeed in computing these bounds for many typical examples using heuristics and equivalence checking.

Introduction

Most software systems are now constructed by reusing and composing existing components or peers. This is the case in many different areas such as component-based systems, cloud applications, Web services, or cyber-physical systems. Software entities are often stateful and therefore described using behavioral models. Moreover, asynchronous communication via FIFO buffers is a classic communication model used for such distributed, communicating systems. A crucial problem in this context is to check whether a new system consisting of a set of interacting peers respects certain properties. Analyzing asynchronously communicating software has been studied extensively in the last 30 years and is known to be undecidable in general [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. A common approach to circumvent this issue is to bound the state space by restricting the cyclic behaviors or imposing an arbitrary bound on buffers. Bounding buffers to an arbitrary size during the execution is not a satisfactory solution: if at some point buffers' sizes change (due to changes in memory requirements for example), it is not possible to know how the system would behave compared to its former version and new unexpected errors can show up.

In this paper, we do not want to impose any arbitrary bounds for buffer sizes. Hence, our focus is on systems that are likely to be unbounded and therefore result in infinite state spaces. It was shown recently that certain properties of distributed systems interacting asynchronously through unbounded buffers can be checked using the synchronizability property. [START_REF] Basu | Deciding Choreography Realizability[END_REF] relies on this property to check whether a choreography is realizable and [START_REF] Ouederni | Compatibility Checking for Asynchronously Communicating Software[END_REF] uses it for verifying the compatibility of communicating systems. A set of peers is synchronizable if and only if the system generates the same sequences of messages under synchronous and unbounded asynchronous communication, considering only the ordering of the send actions and ignoring the ordering of receive actions. Focusing only on send actions makes sense for verification purposes because: (i) send actions are the actions that transfer messages to the network and are therefore observable, (ii) receive actions correspond to local consumptions by peers from their buffers and can therefore be considered to be local and private information. Synchronizability can be verified by checking the equivalence of the synchronous and 1-bounded asynchronous compositions of the given system. In the 1bounded asynchronous composition, each peer is equipped with one input buffer bounded to size 1. Thus, this property can be verified using equivalence checking techniques on finite state spaces, although the system consisting of peers interacting asynchronously via unbounded buffers can result in infinite state spaces. Figure 1 gives an example where peers are modelled using Labelled Transition Systems (LTSs). Transitions are labeled with either emissions (exclamation marks) or receptions (question marks). Initial states are marked with incoming half-arrows. This simple system is synchronizable because the synchronous system consists of sequences of interactions request, result, and ack, and this order is the same in the 1-bounded asynchronous system considering only send actions. Let us now focus on a sligthly extended version of this example where in addition the server Salaün & Ye stores every request answered in a database (log) as depicted in Figure 2. This system is not synchronizable because the client can submit a second request in the 1-bounded asynchronous system before the server sends the log message to the database, and this behavior is not possible in the synchronous composition. Synchronizability is rather strong and many communicating systems do not satisfy this property. So what can we do for non-synchronizable systems? This second example is typically unbounded, because the database peer has no obligation to consume from its buffer which can infinitely receive log messages. So far, and to the best of our knowledge, existing approaches cannot analyze such infinite-state systems. In this paper, we propose a new approach for analyzing a set of peers described using LTSs, communicating asynchronously via reliable (no loss of messages) and possibly unbounded FIFO buffers. We do not want to restrict the system by imposing any arbitrary bounds on cyclic behaviors or buffers. We introduce a notion of stability for the asynchronous versions of the system. A system is stable if asynchronous compositions exhibit the same observable behavior from some buffer bound. We prove that once the system is stable for a specific buffer bound, it remains stable whatever larger bounds are chosen for buffers. This enables one to check temporal properties on the system for that bound (using model checking techniques for instance) and ensures that the system will preserve them whatever larger bounds are used for buffers. Practically speaking, this allows any developer to check that his/her system satisfies some property for the minimal k satisfying stability, and then (s)he can choose any bound from that k as actual parameter for his/her system. This choice may be guided by memory constraints or performance issues for instance. We also prove that computing this bound is undecidable, but we show how we succeed in computing such bounds in practice for many examples.

Going back to the former example (Fig. 2), we can use our approach to detect that when each peer is equipped with a buffer bound fixed to 2, the observable behavior of this system is stable. This means that we can check properties, such as the absence of deadlocks, on the 2-bounded asynchronous version of the system and the results hold for any asynchronous version of the system where buffer bounds are greater or equal to 2.

We implemented our approach in a tool that first encodes the peer LTSs and their compositions into process algebra, and then uses heuristics, search algorithms, and equivalence checking techniques for verifying whether the system satisfies the stability property. If this is the case, we return the smallest bound respecting this property. Otherwise, when we reach a certain maximal bound, our check returns an inconclusive result. Heuristics and search algorithms aim at guiding the approach towards the smallest bound satisfying stability whereas equivalence checking techniques is used for checking the stability property given a specific bound k. All the steps of our approach are fully automated (no human intervention). We applied our tool support to more than 300 examples of communicating systems, many of them taken from the literature on this topic. These experiments show that a large number of these examples are stable and can therefore be formally analyzed using our approach.

Inria

Our contributions with respect to existing results on formal verification of asynchronously communicating systems are the following:

• A general framework for verifying systems interacting asynchronously via reliable FIFO buffers;

• The introduction of the stability property for such systems and a proof showing that stability once acquired for a specific bound k is preserved for upper bounds;

• A proof demonstrating that computing this bound k is undecidable;

• A fully automated tool support that implements the presented approach and was applied to many examples for evaluation purposes.

The organization of the rest of this paper is as follows. Section 2 defines our models for peers and their synchronous/asynchronous compositions. Section 3 presents the stability property and our results on stable systems. Section 4 describes our tool support and experiments we carried out to evaluate our approach. Finally, Section 5 reviews related work and Section 6 concludes.

Communicating Systems

We use Labeled Transition Systems (LTSs) for modeling peers. This behavioral model defines the order in which a peer executes the send and receive actions.

Definition 1 A peer is an LTS P = (S, s 0 , Σ, T ) where S is a finite set of states, s 0 ∈ S is the initial state, Σ = Σ ! ∪ Σ ? ∪ {τ } is a finite alphabet partitioned into a set of send messages, a set of receive messages, and the internal action, and T ⊆ S × Σ × S is a transition relation.

We write m! for a send message m ∈ Σ ! and m? for a receive message m ∈ Σ ? . We use the symbol τ for representing internal activities. A transition is represented as s l -→ s ′ ∈ T where l ∈ Σ. This can be directly extended to s σ -→ s ′ , σ ∈ Σ * , where σ = l 1 , ..., l n , s l1 -→ s 1 , . . . , s i li+1 --→ s i+1 , . . . , s n-1 ln -→ s ′ ∈ T . In the following, for the sake of simplicity, we will denote this by s

σ -→ s ′ ∈ T * .
We assume that peers are deterministic on observable messages meaning that if there are several transitions going out from one peer state, and if all the transition labels are observable, then they are all different from one another. Observable determinism can be easily obtained in peers using standard determinization algorithms [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF]. Nondeterminism can also result from internal choices when several transitions (at least two) outgoing from a same state are labeled with τ . It is worth observing that these internal transitions are important when checking the synchronizability property [START_REF] Basu | Deciding Choreography Realizability[END_REF][START_REF] Ouederni | Compatibility Checking for Asynchronously Communicating Software[END_REF], which partly relies on synchronous communication. In such a case, internal transitions outgoing from a same state express an internal choice whereas transitions labeled with observable messages outgoing from a same state stand for an external choice semantics.

Given a set of peers {P 1 , . . . , P n }, we assume that each message has a unique sender and a unique receiver: ∀i

, j ∈ 1..n, i = j, Σ ! i ∩ Σ ! j = ∅ and Σ ? i ∩ Σ ? j = ∅.
Furthermore, each message is exchanged between two different peers: Σ ! i ∩ Σ ? i = ∅ for all i. We also assume that each emission has a reception counterpart in another peer (closed systems

): ∀i ∈ 1..n, ∀m ∈ Σ ! i =⇒ ∃j ∈ 1..n, i = j, m ∈ Σ ? j .
The synchronous composition of a set of peers corresponds to the system where a communication occurs when one peer can send a message and another peer is in a state in which that message can be received.

Salaün & Ye

Definition 2 (Synchronous Composition) Given a set of peers {P 1 , . . ., P n } with P i = (S i , s 0 i , Σ i , T i ), the synchronous composition is the labeled transition system LT S s = (S s , s 0 s , Σ s , T s ) where:

• S s = S 1 × . . . × S n • s 0 s ∈ S s such that s 0 s = (s 0 1 , . . . , s 0 n ) • Σ s = ∪ i Σ i • T s ⊆ S s × Σ s × S s , and for s = (s 1 , . . . , s n ) ∈ S s and s ′ = (s ′ 1 , . . . , s ′ n ) ∈ S s (interact) s m -→ s ′ ∈ T s if ∃i, j ∈ {1, . . . , n} where i = j : m ∈ Σ ! i ∩ Σ ? j where ∃ s i m! --→ s ′ i ∈ T i , and s j m? --→ s ′ j ∈ T j such that ∀k ∈ {1, . . . , n}, k = i ∧ k = j ⇒ s ′ k = s k (internal) s τ -→ s ′ ∈ T s if ∃i ∈ {1, . . . , n}, ∃ s i τ -→ s ′ i ∈ T i such that ∀k ∈ {1, . . . , n}, k = i ⇒ s ′ k = s k
In the asynchronous composition, the peers communicate with each other asynchronously via FIFO buffers. Each peer P i is equipped with an unbounded input message buffer Q i . A peer can either send a message m ∈ Σ ! to the tail of the receiver buffer Q j at any state where this send message is available, read a message m ∈ Σ ? from its buffer Q i if the message is available at the buffer head, or evolve independently through an internal transition. We recall that we focus on send actions in this paper. We consider that reading from the buffer is private non-observable information, which is encoded as an internal transition in the asynchronous system. Definition 3 (Asynchronous Composition) Given a set of peers {P 1 , . . ., P n } with P i = (S i , s 0 i , Σ i , T i ), and Q i being its associated buffer, the asynchronous composition is the labeled transition system LT S a = (S a , s 0 a , Σ a , T a ) where:

• S a ⊆ S 1 × Q 1 × . . . × S n × Q n where ∀i ∈ {1, . . . , n}, Q i ⊆ (Σ ? i ) * • s 0
a ∈ S a such that s 0 a = (s 0 1 , ǫ, . . . , s 0 n , ǫ) (where ǫ denotes an empty buffer)

• Σ a = ∪ i Σ i • T a ⊆ S a × Σ a × S a , and for s = (s 1 , Q 1 , . . . , s n , Q n ) ∈ S a and s ′ = (s ′ 1 , Q ′ 1 , . . . s ′ n , Q ′ n ) ∈ S a (send) s m! --→ s ′ ∈ T a if ∃i, j ∈ {1, . . . , n} where i = j : m ∈ Σ ! i ∩ Σ ? j , (i) s i m! --→ s ′ i ∈ T i , (ii) Q ′ j = Q j m, (iii) ∀k ∈ {1, . . . , n} : k = j ⇒ Q ′ k = Q k , and (iv) ∀k ∈ {1, . . . , n} : k = i ⇒ s ′ k = s k (consume) s τ -→ s ′ ∈ T a if ∃i ∈ {1, . . . , n} : m ∈ Σ ? i , (i) s i m? --→ s ′ i ∈ T i , (ii) mQ ′ i = Q i , (iii) ∀k ∈ {1, . . . , n} : k = i ⇒ Q ′ k = Q k , and (iv) ∀k ∈ {1, . . . , n} : k = i ⇒ s ′ k = s k (internal) s τ -→ s ′ ∈ T a if ∃i ∈ {1, . . . , n}, (i) s i τ -→ s ′ i ∈ T i , (ii) ∀k ∈ {1, . . . , n} : Q ′ k = Q k ,
(∀q ≥ k) (LT S k a ⊆ LT S q a (∀q ≥ k)).

Stability

In this section, we introduce successively the synchronizability property, the stability property, the proof of undecidability for the stability property, and several other results on stable systems.

Synchronizability

The composition of finite peer LTSs can result into an infinite state system if these peers communicate asynchronously over unbounded buffers. This makes the exhaustive analysis of all executed communication traces impossible and verification tasks in this setting are undecidable [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. This issue can be avoided for systems that are synchronizable [START_REF] Basu | Deciding Choreography Realizability[END_REF]. The synchronizability property checks whether the sequences of send actions generated by the peer composition remain the same under synchronous and asynchronous communication semantics. This enables one to analyze asynchronous systems, even those generating an infinite state space, using the synchronous version of the given system (which has a finite state space). This property was used recently for analyzing properties on communicating systems [START_REF] Ouederni | Compatibility Checking for Asynchronously Communicating Software[END_REF] and is checked using branching equivalence [START_REF] Van Glabbeek | Branching Time and Abstraction in Bisimulation Semantics[END_REF], which is the finest equivalence notion in presence of internal behaviors.

Definition 4 (Branching Bisimulation) Given two LTSs LT S 1 and LT S 2 , they are branching bisimilar, denoted by LT S 1 ≡ br LT S 2 , if there exists a symmetric relation R (called a branching bisimulation) between the states of LT S 1 and LT S 2 satisfying the following two conditions:

• The initial states are related by R;

• If R(r, s) and r δ -→ r′, then either δ = τ and R(r′, s), or there exists a path s τ * -→ s 1 δ -→ s′, such that R(r, s 1 ) and R(r′, s′).

For the sake of simplicity and consistency, the relation R is replaced by ≡ br in the rest of this paper, i.e.,, R(r, s) is noted r ≡ br s.

Definition 5 (Branching Synchronizability) A set of peers {P 1 , . . . , P n } is branching synchronizable if ∀k ≥ 1, LT S s ≡ br LT S k a , where ≡ br in that particular case compares synchronizations in the synchronous composition with emissions from peers to peer buffers in the asynchronous composition.

It was proved that LT S s ≡ br LT S 1 a is a sufficient and necessary condition for branching synchronizability [START_REF] Ouederni | Compatibility Checking for Asynchronously Communicating Software[END_REF].

The synchronizability property is quite strong and there are many non-synchronizable systems, see e.g., Fig. 2. If the set of peers is not synchronizable, there is no standard approach for formally analyzing those systems. The stability notion we introduce in the next section is a solution to this problem.

Salaün & Ye

Stability

In this section, we show that systems consisting of a finite set of peers involving cyclic behaviors and communicating over FIFO buffers may stabilize from a specific buffer bound k. We call this property stability and we say that the corresponding systems are stable. The class of systems which are stable corresponds to systems whose asynchronous compositions remain the same from some buffer bound when we observe send actions only (we ignore receive actions and buffer contents). Stability results do not hold if we consider that receptions are also observable. Focusing only on send actions makes sense for verification purposes because: (i) send actions are the actions that transfer messages to the network and are therefore observable, (ii) receive actions correspond to local consumptions by peers from their buffers and can therefore be considered to be local and private information.

Since stable systems produce the same behavior from a specific bound k, they can be analyzed for that bound to detect for instance the presence of deadlocks or to check whether they satisfy any kind of temporal properties. Stability ensures that these properties will be also satisfied for larger bounds. The stability definition relies on branching equivalence checking, and this equivalence preserves properties written with ACTL\X logic [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF].

Contrarily, some systems are not stable. Unstability is due to some particular cycle dependency in the peer behaviors that makes the asynchronous composition exhibit new behaviors every time the buffer bound is increased. In the rest of this section, we will first define the stability property. We will show how stability is established and what can be deduced for such systems. We will also present other results such as the undecidability of the stability problem.

Definition 6 (Stability) Given a set of peers {P 1 , . . . , P n }, we say that this system is stable if and only if ∃k such that LT S k a ≡ br LT S q a (∀q > k).

Before presenting our main results, we first introduce a few definitions that will be used in the following deduction. First, we define a special state of LT S k a as a border state that is considered as a boundary between LT S k a and LT S k+1 a if the latter has more behaviors than the former due to larger buffers. Precisely, a border state of LT S k a should satisfy a condition stating that it has a successor state in LT S k+1 a that is not reachable in LT S k a due to limited buffer size. Then the new behavior, which leads to a state whose buffers contain k + 1 messages that are not contained in LT S k a , must begin after this border state.

Definition 7 (Border State) Given a set of peers {P 1 , . . . , P n }, given a state

s k = (s k 1 , Q k 1 , ..., s k n , Q k n ) ∈ S k
a , if it satisfies the following condition, we call it a k-border state, simply a border state if there is no ambiguity:

• ∃s k m! --→ s ′′k ∈ T k+1 a
, where s ′′k has one peer whose buffer contains k + 1 messages.

A single k-message state is a state where only one buffer contains k messages. Note that such a state cannot be reachable in LT S k-1 a and we must have such a state as a successor state for a (k -1)-border state in LT S k a according to the condition of Definition 7. Characterizing such states is a key step for demonstrating some of our results, i.e., Lemma 1 and Theorem 1. In the left part of Figure 3, the small ellipsis represents LT S k-1 a and the bigger one is LT S k a . Here,

Definition 8 (Single k-message State (SG(s k ))) Given a set of peers {P 1 , . . . , P n } and a state s k = (s k 1 , Q k 1 , ..., s k n , Q k n ) ∈ S k a , if ∃i ∈ {1, ..., n}, |Q k i | = k, ∀j ∈ {1, ..., n}, j = i, |Q k j | < k, and there exists a border state s k-1 such that s k-1 m! --→ s k ∈ T k a , m? ∈ Σ k i , then s k is a single k-message state, denoted by SG(s k ).
s k ∈ S k a is a single k-message state and s k-1 ∈ S k-1 a
is the corresponding border state. Next we define a special state s k in LT S k a such that it contains only one buffer with k messages, whose precedent state is a border state, denoted by s b . Furthermore, from s b , there are two outgoing transitions. One can reach s k with one emission. The other can reach another state s k-1 through a reception followed by the same emission such that s k-1 contains at most k -1 messages in its buffers. Then we will show s k ≡ br s k-1 by demonstrating that these two traces diverging from s b will converge in the future, i.e., there will form a confluent diamond.

Definition 9 (Loose k-message State (LS(s k ))) Given a set of peers {P 1 , . . . , P n } and a state s k such that SG(s k ), i.e., ∃s k-1 m m! --→ s k ∈ T k a , m? ∈ Σ ? i , i ∈ {1, ..., n}, where s k-1 m is a border state, then s k is called a loose k-message state, denoted by LS(s k ), if the following conditions are satisfied • ∃m′? ∈ Σ ? i , such that s k-1 m m′? --→ s k-1 n m! --→ s ′k-1 , where s k-1 m m′? --→ s k-1 n , s k-1 n m! --→ s ′k-1 ∈ T k a ; • for s k and s ′k-1 , we have s k ≡ br s ′k-1
In the right part of Figure 3,s

k ∈ S k
a is a loose k-message state which is a single k-message state satisfying the above condition. Next we will show that for a given single k-message state, it has a corresponding branching equivalent state in LT S k-1 a iff it is a loose k-message state. The proof is based on the fact that branching equivalence between two states s k ∈ S k a and

s k+1 ∈ S k+1 a ∧ s k+1 / ∈ S k a implies a confluent diamond for them in LT S k+1 a .
Lemma 1 Given a set of peers {P 1 , . . . , P n }, the following holds for each single k-message state

s k ∈ S k a . LS(s k ) ⇔ ∃s k-1 ∈ S k-1 a such that s k-1 ≡ br s k Proof . ⇒ Suppose that for a single k-message state s k = (s k 1 , Q k 1 ,...,s k n , Q k n ) ∈ S k a , |Q k i | = k, i ∈ {1, ..., n}, LS(s k ) holds. Then in LT S k a , ∃m? ∈ Σ ? i , such that s k 0 σ -→ s k m m! --→ s k , where s k 0 σ -→ s k m ∈ T k * a , s k m m! --→ s k ∈ T k a .
From Definition 9, we know that s k m is a border state and that ∃m′? ∈

Σ ? i , s k 0 σ -→ s k m m′? --→ s k n m! --→ s ′k , where s k m m′? --→ s k n , s k n m! --→ s ′k ∈ T k a .
This implies that there must be a corresponding part in LT S k-1 a

: s k-1 0 σ -→ s k-1 m m′? --→ s k-1 n m! --→ s ′k-1 , where s k-1 0 σ -→ s k-1 m ∈ T k-1 * a , s k-1 m m′? --→ s k-1 n , s k-1 n m! --→ s ′k-1 ∈ T k-1 a , s ′k-1 = (s ′k-1 1 , Q ′k-1 1 , ..., s ′k-1 n , Q ′k-1 n ), |Q ′k-1 j | < RR n°8561
Salaün & Ye k, ∀j ∈ {1, ..., n}. The reason is that the maximum number of messages in all states between s k-1 0 and s ′k-1 is smaller than k. Now from the second condition of Definition 9, we know that beginning from the state s k in LT S k a and from s ′k-1 in LT S k-1 a , we have exactly the same branching structure. This implies s k ≡ br s ′k-1 . ⇐ Now suppose that in LT S k a , we have a single k-message state

s k = (s k 1 , Q k 1 , ..., s k n , Q k n ) ∈ S k a , |Q k i | = k, i ∈ {1, .
.., n}, such that LS(s k ) does not hold. From Definition 9, we show that the violation of each one of the two conditions implies ∄s k-1 ∈ S k-1 a , such that s k ≡ br s k-1 .

1. If the first condition is not satisfied, i.e., ∄m′? ∈ Σ ? i , such that s k m m′?

--→ s k n m! --→ s ′k , where s k m m′? --→ s k n , s k n m! --→ s ′k ∈ T k a .
This implies that the reception of m′ that is contained in the buffer Q k i cannot be executed between the border state s k m and the state juste before m!. If m′? is executed after m! preceding the border state, then there is no equivalent state in LT S k-1 a with respect to s k since the part after the border state cannot be reached in

LT S k-1 a
. Otherwise, if m′? is before the border state, e.g., suppose

s k h l!/? --→ s k m m! --→ s k , where s k h l!/? --→ s k m , s k m m! --→ s k ∈ T k a , we have s k h m′? --→ s k p l!/? --→ s k q m! --→ s k r , where s k h m′? --→ s k p , s k p l!/? --→ s k q , s k q m! --→ s k r ∈ T k a .
In this case, we can deduce that m′? should execute before l!/?. In other words, ∄s k m′? --→ s ∈ T k a . This means that we cannot reach s k r from s k , i.e., there is no confluent diamond. Thus, there is no branching equivalent state in LT S k-1 a for s k .

∃m′? ∈ Σ

? g , s k m m′? --→ s k n m! --→ s ′k , where s k m m′? --→ s k n , s k n m! --→ s ′k ∈ T k a , s k ≡ br s ′k . It is clear that we have also s k ≡ br s k n since m! is before s k but after s k n .
Thus, there is no branching equivalent state in LT S k-1 a for the state s k .

From above, if a single k-message state is not a loose one, then

∄s k-1 ∈ S k-1 a such that s k-1 ≡ br s k .
Thus, we have proved this lemma for both directions.

Here is one of the main results of this paper. If we are able to find a bound k such that the k-bounded and the (k + 1)-bounded asynchronous systems are branching equivalent, then we prove that the system remains stable, meaning that the observable behavior is always the same for any bound greater than k. The main interest of the stability property is that the k-bounded version of the system can be analyzed using existing model checking tools and this result ensures that these properties are preserved when buffer bounds are increased or if buffers are unbounded.

Theorem 1 Given a set of peers {P 1 , . . . , P n }, if ∃k ∈ N, such that LT S k a ≡ br LT S k+1 a , then we have LT S k a ≡ br LT S q a , ∀q > k.

Proof . We prove this theorem by induction. The idea is to show LT S k a ≡ br LT S q a , ∀q > k from LT S k a ≡ br LT S k+1 a . We rewrite q > k by q = k + m, m ≥ 1. Now the base case m = 1 is true from the hypothesis, i.e., LT S k a ≡ br LT S k+1 a . To prove that this is also true for ∀m > 1, we suppose LT S k a ≡ br LT S k+1 a ≡ br ... ≡ br LT S k+m a , m ≥ 1 and we show LT S k a ≡ br LT S k+m+1 a . To do this, we consider two cases according to whether the maximum number of messages in all buffers is smaller than k + m + 1 or not in the asynchronous composition, which are formally represented as follows:

1. In LT S k+m+1 a , ∀s k+m+1 = (s k+m+1 1 , Q k+m+1 1 , ..., s k+m+1 n , Q k+m+1 n ) ∈ S k+m+1 a , we have ∀i ∈ {1, ..., n}, |Q k+m+1 i | ≤ k + m; Inria 2. In LT S k+m+1 a , ∃s k+m+1 = (s k+m+1 1 , Q k+m+1 1 , ..., s k+m+1 n , Q k+m+1 n ) ∈ S k+m+1 a , such that ∃i ∈ {1, ..., n}, |Q k+m+1 i | = k + m + 1.
Now we show that in each of the two cases, we can deduce LT S k a ≡ br LT S k+m+1 a .

• The first case implies that in the asynchronous composition of this set of peers LT S a , the buffer of any peer contains at most k+m messages in all states of LT S a . Hence, LT S , we have LS(s k+m ), i.e., ∃s k+m-1 ∈ S k+m-1 a , such that s k+m-1 ≡ br s k+m . From Definition 9, we know that the only difference between the path from s 0 a to s k+m-1 and that from s 0 a to s k+m is that the former has one more reception that has however no impact on the execution after s k+m-1 since s k+m-1 ≡ br s k+m . This implies that we have exactly the same structure with respect to emissions from the states s k+m-1 and s k+m . Now suppose that LT S k+m a ≡ br LT S k+m+1 a , i.e., ∃s k+m+1 ∈ S k+m+1 a , for which ∄s k+m ∈ S k+m a , such that s k+m+1 ≡ br s k+m . In other words, we have SG(s k+m+1 ) and ¬LS(s k+m+1 ). Now let s k+m be the border state for s k+m+1 , we can deduce that if ¬LS(s k+m+1 ), for its border state s k+m , ∄s k+m-1 ∈ S k+m-1 a , such that s k+m ≡ br s k+m-1 . In other words, ¬LS(s k+m+1 ) implies ¬LS(s k+m ). Given this result, one can check on the minimal k-bounded system satisfying stability, any temporal property written with ACTL\X logic involving emissions, and this property will hold for any system with larger bounds. Proposition 1 Given a set of peers {P 1 , . . . , P n }, if ∃k s.t. LT S k a ≡ br LT S q a (∀q > k), and for some property P , LT S k a |= P , then LT S q a |= P (∀q > k).

Proof . This trivially follows from Theorem 1.

Undecidability

Before showing the undecidability of checking the stability of a system, we first present a sufficient and necessary condition for a system that is stable.

Lemma 2 Given a set of peers {P 1 , . . . , P n }, this system is stable iff the following condition is satisfied, denoted by C:

∃k ∈ N, ∀s k ∈ S k a .[¬SG(s k ) ∨ LS(s k )].

RR n°8561

Salaün & Ye

Proof . ⇒ Suppose that the given set of peers is stable. Next we show that the stability of the set of peers implies that the condition C is satisfied. Since this set of peers is stable, from Theorem 1, we deduce ∃k ∈ N, such that LT S k a ≡ br LT S k-1 a . There are two cases for this:

1. LT S k a = (S k a , s 0 a , Σ k a , T k a ) and LT S k-1 a = (S k-1 a , s 0 a , Σ k-1 a , T k-1 a
) have exactly the same structure, i.e.,

S k a = S k-1 a , Σ k a = Σ k-1 a , T k a = T k-1 a ;
2. LT S k a and LT S k-1 a do not have the same structure but are branching equivalent, i.e.,

S k a = S k-1 a and T k a = T k-1 a .
We demonstrate that any one of the two cases must satisfy the condition C.

• In the first case, we can deduce that in LT S k a , for each peer, its buffer contains at most k -1 messages in all states, i.e.,

∀s k = (s k 1 , Q k 1 , ..., s k n , Q k n ) ∈ S k a , ∀i ∈ {1, ..., n}, |Q k i | < k.
This implies that there is no single k-message state in LT S k a , i.e., ∀s k ∈ S k a , ¬SG(s k ). Hence, the condition C is satisfied.

• Now consider the second case, where LT S k a and LT S k-1 a are not exactly the same one. Hence, we can deduce

∃s k = (s k 1 , Q k 1 , ..., s k n , Q k n ) ∈ S k a , ∃i ∈ {1, ..., n}, |Q k i | = k in LT S k a .
In other words, there exists at least one single k-message state. Furthermore, since LT S k a ≡ br LT S k-1 a , for all states in LT S k a , there must be a corresponding branching equivalent state in LT S k-1 a , including all single k-message states. Thus, from Lemma 1, we can deduce that ∀s k ∈ S k a , we have either ¬SG(s k ) or LS(s k ). This means that the condition C is satisfied. So if the set of peers is stable, then the condition C must be satisfied. ⇒ Now suppose that the condition C is satisfied. Thus, we consider three cases: all states are not single k-message states, formally described by the first case in the following; all states are loose k-message states, which is not possible since the initial state has no message in all buffers; some of the states are single k-messages states that should be loose ones, formally presented by the second case below:

1. ∃k ∈ N, ∀s k ∈ S k a , we have ¬SG(s k ); 2. ∃k ∈ N, ∀s k ∈ S k a such that SG(s k ), we have LS(s k ). Now we show that any one of these two conditions implies that the system is stable.

• The first condition means that in LT S k a , there is no single k-message state, i.e., the maximum number of messages in buffers is smaller than k for any state. It can thus be deduced that LT S k a and LT S k-1 a have exactly the same structure, which implies LT S k a ≡ br LT S k-1 a . From Theorem 1, this is a stable set of peers.

• The second condition means that all single k-message state in LT S k a are loose ones. From Lemma 1, it can be deduced that ∀s k ∈ S k a , there is a corresponding state

s k-1 ∈ S k-1 a , such that s k ≡ br s k-1 . It is clear that ∀s k ∈ S k-1 a
, we have at least one corresponding branching equivalent state in LT S k a . This implies that LT S k a ≡ br LT S k-1 a . Hence, this set of peers is stable from Theorem 1.

Hence, if the condition C is satisfied, then the system is stable.

Next we show that checking the stability of the system is undecidable by showing that verifying the condition C is an undecidable problem. Yet there are many cases in which stability is satisfied and the corresponding bound can be computed in those cases using heuristics, search algorithms, and equivalence checking (see Section 4).

Inria

Theorem 2 Given a set of peers {P 1 , . . . , P n }, it is undecidable whether the corresponding asynchronous system is stable.

Proof . From Lemma 2, we know that C is a sufficient and necessary condition to check that a system is stable. We show that the problem of checking this condition is undecidable. The idea is to demonstrate that the boundedness problem [START_REF] Brand | On Communicating Finite-State Machines[END_REF] is its subproblem. The communication of a set of peers with FIFO buffers is said to be bounded iff ∃k ∈ N such that for any reachable state s = (s 1 , Q 1 , ..., s n , Q n ) ∈ S a , we have ∀i ∈ {1, ..., n}, |Q i | < k. Now recall that to check whether the condition C is violated, the following two conditions should be both checked one after another:

• ∀k ∈ N, ∃s k ∈ S k a , such that SG(s k ); • ¬LS(s k ).
Now we show that the first condition is equivalent to the boundedness problem. If this condition is satisfied, it can be deduced that ∄k ∈ N, such that ∀s = (s 1 , Q 1 , ..., s n , Q n ) ∈ S a , we have ∀i ∈ {1, ..., n}, |Q i | < k. So this system is not bounded. On the other hand, if the condition is not satisfied, i.e., ∃k ∈ N, there does not exist a reachable state such that it is a single k-message state. This means that

∀s k = (s k 1 , Q k 1 , ..., s k n , Q k n ) ∈ S k a ,
we have ¬SG(s k ). From Definition 8, to have ¬SG(s k ), consider three cases for s k : 1) at least two buffers contain k messages, i.e., ∃i 1 , ..., i m ∈ {1, ..., n}, |Q k ij | = k, j ∈ {1, ..., m}, m ≥ 2; 2) no buffer contains k messages, i.e., ∀i ∈ {1, ..., n}, |Q k i | < k; 3) there does not exist a border state s k-1 such that s k-1 m! --→ s k ∈ T k a , where SG(s k ). For the first case, if this is true, there must be at least one s k such that SG(s k ) since to reach a state where more than one buffer has k messages, we have to first reach such a state s k , SG(s k ). This implies that the first case is not possible with the assumption without single k-message states. Then the second case means that the maximum number of messages in buffers is smaller than k. And for the third case, even in s k , there exists a buffer containing k messages, this state cannot be reached in LT S k a since there is no border state before it. From above, we analyze all three cases for a state s k such that ¬SG(s k ). We can see that ¬SG(s k ) implies that s k is bounded by k. This implies that if ∀s k ∈ S k a , we have ¬SG(s k ), then the system is bounded. So we have shown that this first condition is equivalent to the boundedness problem, which is thus a subproblem of checking C: consequently, if the former is undecidable, which was proved in [START_REF] Brand | On Communicating Finite-State Machines[END_REF], then so is the latter.

Other Results

In the rest of this section, we present several additional results on the stability of communicating systems.

Proposition 2 A set of peers {P 1 , . . . , P n } is stable if it is synchronizable.

Proof . From Definition 5, a system is synchronizable meaning that all its asynchronous compositions are branching equivalent whatever is the bound for buffers. This means that ∀k, q ∈ N, we have LT S k a ≡ br LT S q a . Now from Definition 6, it follows that this system is stable.

The opposite is false because stability ensures branching equivalence of the asynchronous systems from a specific bound k, which means that systems for lower bounds and for its synchronous version behave differently.

The next result concerns computability of the smallest buffer bound for stable systems.

Salaün & Ye

Proposition 3 Given a stable set of peers {P 1 , . . . , P n }, the minimal bound k satisfying the stability property is computable.

Proof . Since this set of peers is stable, from Theorem 1, we know that ∃k ∈ N, LT S k a ≡ br LT S k+1 a . Since k is finite, the construction of LT S k a , LT S k+1 a and their equivalence checking is computable. Hence, the minimal bound k for the stability property is also computable.

The computability of the stability property will be illustrated on real-world examples in Section 4 by using heuristics, search algorithms, and equivalence checking.

Beyond these results on stability, a common approach is to identify classes of systems where stability is guaranteed. Synchronizable systems (Prop. 3) and finite systems lie in this category. By finite systems, we mean systems where peers interact over unbounded FIFO buffers and whose asynchronous compositions are finite. This is the case for instance for acyclic peers, for systems with a single cyclic peer where cycles do not involve only emissions, or for systems with peers exhibiting independent cycles, i.e., cycles that are not included one from another [START_REF] Leue | Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes[END_REF]. Apart from these simple cases, two candidates are (i) systems where peers exhibit cycles of emissions, and (ii) well-formed systems (Definition 10).

Let us start with systems where peers can infinitely send messages. We establish that the existence of a cycle of emissions in one peer does not determine whether whether the system is stable or not, which is however a sufficient condition for unboundedness [START_REF] Brand | On Communicating Finite-State Machines[END_REF].

Proposition 4 Given a set of peers {P 1 , . . . , P n }, if a peer

P i ∈ {P 1 , . . . , P n } exhibits a cycle of emissions φ = s k i m1! --→ s k+1 i ... mn! --→ s k
i , this does not imply that the system is unstable.

Proof . We prove this result by demonstrating that a system with a cycle of emissions in one peer that is able to infinitely send messages may be stable or not. Suppose first that for this system, in LT S a , ∀σ ∈ Σ * a , s 0

a σ -→ s n-1 mi! --→ s n , s 0 a σ -→ s n-1 ∈ T * a , s n-1 mi! --→ s n ∈ T a , where m i ! is one send message in φ, then ∃σ′ ∈ Σ * a , s 0 a σ′ -→ s m-1 mi! --→ s m mi? --→ s m+1 , s 0 a σ′ -→ s m-1 ∈ T * a , s m-1 mi! --→ s m , s m mi? --→ s m+1 ∈ T a
, where P ! (σ) = P ! (σ′). Here we denote the projection of σ on send messages by P ! (σ). This means that whenever a message in this cycle is emitted, there exists at least one execution with the same sequence of emissions, where the corresponding peer is ready to receive it. In this case, the system may be stable. Now suppose that in this system, ∃σ ∈ Σ * a , s 0

a σ -→ s n-1 mi! --→ s n , s 0 a σ -→ s n-1 ∈ T * a , s n-1 mi! --→ s n ∈ T a , where m i ! is one send message in φ, for which ∄σ′ ∈ Σ * a , s 0 a σ′ -→ s m-1 mi! --→ s m mi? --→ s m+1 , such that s 0 a σ′ -→ s m-1 ∈ T * a , s m-1 mi! --→ s m , s m mi? --→ s m+1 ∈ T a , where P ! (σ) = P ! (σ′). This means that ∃σ′′ ∈ Σ * a , s 0 a σ′ -→ s m-1 mi! --→ s m σ′′ --→ s t mi? --→ s t+1 , where s 0 a σ′ -→ s m-1 , s m σ′′ --→ s t ∈ T * a and s m-1 mi! --→ s m , s t mi? --→ s t+1 ∈ T a .
Next we show that there is at least one send message in the sequence σ′′. This can be proved by assuming that all messages in σ′′ are receive messages, which in turn implies ∃s 0 a σ′ -→ s m mi! --→ s n mi? --→ s n+1 and thus a contradiction. So it is clear that in σ′′, we must have at least one send message. This implies that ∀k ∈ N, in LT S k+1 a ,

∃s 0 σ -→ s m mi! --→ s n m (i+1) mod n ! ---------→ s n+1 ... m (i+j) mod n ! ---------→ s n+j , whose corresponding part in LT S k a is s 0 σ -→ s m mi! --→ s n m (i+1) mod n ! ---------→ s n+1 ... m (i+j-1) mod n !
-----------→ s n+j-1 . This implies LT S k a ≡ br LT S k+1 a and the system is thus not stable.

Inria

The example shown in Figure 4 has a cycle of emissions. In its synchronous composition, before entering this cycle, d! should be synchronized with d? only after c! while c! can only be synchronized with c? after d!, which leads to a deadlock. It follows that this system is not synchronizable due to this deadlock, which is however not the case for its asynchronous composition. This means that there is no branching equivalence between the synchronous and asynchronous compositions. However, it is stable from bound 1, i.e., LT S 1 a ≡ br LT S k a , k > 1.

Figure 4: A Stable System Exhibiting a Cycle of Emissions Figure 5 depicts another example with a cycle of emissions that is not stable. For this example, if we first execute a! and b! before c!, then to read the receive message from the buffer of peer 2, we have to wait for c!. Hence, consider the execution where c is still not sent. We have that ∀k, LT S k+1 a always exhibits a new observable behavior compared to LT S k a . The reason is that the cycle of emissions in peer 1 can infinitely send a and b, which is only constrained by the size of buffer in peer 2. This implies that this system is not stable.

Another result concerns well-formed systems [START_REF] Basu | Deciding Choreography Realizability[END_REF]. A system consisting of a set of peers is well-formed iff whenever the size of the buffer, Q i , of the i-th peer is non-empty, the system can move to a state where Q i is empty. In other words, well-formedness concerns the ability of a system to eventually consume all messages in any of its buffers. In order to check this property, we have to keep receive messages and thus analyze it on LT S a instead of LT S a .

Definition 10 (Well-formed System) Given a set of peers {P 1 , . . . , P n }, it is well-formed, denoted by W F (LT S a ),

if ∀s = (s 1 , Q 1 , ..., s n , Q n ) ∈ S a , ∀Q i , such that |Q i | > 0, then ∃s σ -→ s′ ∈ T a * , where s′ = (s 1 ′, Q 1 ′, ..., s n ′, Q n ′) ∈ S a , |Q i ′| = 0.
Proposition 5 The well-formedness of a set of peers {P 1 , . . . , P n } can be checked with the following CTL temporal formula on its asynchronous composition LT S a :

AG(|Q i | > 0) ⇒ EF (|Q i | = 0)
This formula means that whenever the size of any buffer is non-empty, i.e., AG(|Q i | > 0), then there is at least one execution in the system to move to a state where Q i is empty, i.e., EF (|Q i | = 0). We show that a well-formed system is not mandatorily stable, i.e., well-formedness is not a sufficient condition for stability. Proposition 6 Given a set of peers {P 1 , . . . , P n }, its well-formedness does not imply that this set of peers is stable.

Proof . This can be proved by demonstrating that a well-formed system can be unstable. We illustrate this through the example depicted in Figure 5. Suppose that one peer in the system contains a cycle φ = s k i σ -→ s k i , where σ ∈ Σ + a and σ contains at least one send message. In this example, one

Salaün & Ye such cycle is σ = a!.b! in peer 1. Furthermore, there is at least one receive message corresponding to one send message in φ, denoted by m k ?, in another peer with a preceding send message m t !, such as a? or b? in peer 2, that is the reception of the emission a! or b! in peer 1, with a preceding emission c!. Suppose further that the execution of the cycle φ is totally independent of the send message m t !, i.e., φ can continue to execute regardless of the emission of m t , and that there is no constraint on m t !, i.e., m t can be emitted at any moment. This is the case for our example, where the cycle a!.b! is independent of c! whose execution is however possible at any moment. For such a system, we can deduce that it is not stable due to the cycle of emissions in peer 1 that can infinitely send messages, which generates new observable behaviors in LT S k+1 a compared to LT S k a , ∀k ∈ N, when c! is still not executed. Furthermore, this system is well-formed because the execution of c! is possible at any moment in peer 2, then all messages in its buffer can be eventually read (cycle of receptions) until the buffer is empty.

Although well-formedness does not imply stability, one can check whether a stable system is well-formed for the smallest k satisfying stability for instance. Then, we show below that if a system is both stable and well-formed for some k, it remains well-formed for larger bound q greater than k. Proof . Suppose that for the given system, we have LT S k a ≡ br LT S k+1 a ∧W F (LT S k a ). Its stability ensures that ∀s k ∈ S k a , ∃s k+1 ∈ S k+1 a such that s k ≡ br s k+1 , and the inverse is also true. Furthermore, the well-formedness of LT S k a means that

∀s k ∈ S k a , ∀Q k i ∈ s k , |Q k i | > 0, there must exist another state s′ k reachable from s k in LT S k
a such that all messages in this buffer are consumed, i.e., Q k i ′ ∈ s′ k , |Q k i ′| = 0. Now there are two possible cases for ∀s k+1 ∈ S k+1 a : 1)

∄Q k+1 i ∈ s k+1 , |Q k+1 i | = k + 1; 2) ∃Q k+1 i ∈ s k+1 , |Q k+1 i | = k + 1.
For the first case, s k+1 must also exist in LT S k a . Hence, from W F (LT S k a ), for each non-empty buffer in s k+1 , there must be another reachable state where this buffer becomes empty. Consider the second case, where we have at least one buffer containing k + 1 messages. Since LT S k a ≡ br LT S k+1 a , then ∃s k ∈ S k a , such that s k ≡ br s k+1 . From Lemma 1, we have LS(s k+1 ), i.e., it satisfies the two conditions described in Definition 9. From the first condition meaning the existence of a confluent diamond, it can be deduced that from such a s k+1 , we can reach a state that is also contained in LT S k a . Hence, with W F (LT S k a ), it follows that for s k+1 in the second case, for each non-empty buffer, we can find another reachable state where this buffer is empty. Thus, we have W F (LT S k+1 a ). Now from LT S k a ≡ br LT S q a (∀q > k), we have LT S k+1 a ≡ br LT S k+2 a . Furthermore, we have proved W F (LT S k+1 a ). Thus, similarly, we can prove W F (LT S k+2 a ) and also W F (LT S q a ), (∀q > k).

Inria

Finally, we show that the stability results cannot be used for checking properties involving not only emissions but also receptions. Proposition 7 Given a set of peers {P 1 , . . . , P n }, if this system is stable, i.e., ∃k s.t. LT S k a ≡ br LT S q a (∀q > k), and for some property P , LT S k a |= P , then we do not have necessarily LT S q a |= P (∀q > k).

Proof .

Consider the example in Figure 2. As explained in Section 1, this system is stable from k = 2. Suppose now that the property under consideration is that it is forbidden to have three successive receptions of log. This property is verified on LT S 2 a but not on LT S 3 a , because to have three successive receptions of log, this peer requires a buffer with size at least three. Therefore, the property is satisfied for LT S 2 a , but is violated for LT S 3 a .

Tool Support

In this section, we first present our method for checking whether a set of LTSs is stable. Our approach relies on an encoding into process algebra on the one hand, which is used for computing peer synchronous and asynchronous compositions, and on heuristics and search algorithms for computing the smallest bound satisfying the stability property on the other hand. These different aspects will be introduced in this section as well. Finally, we will comment on experiments we made either on real-world examples taken from the literature or on hand-crafted examples to see how our approach scales.

Method

First of all, we introduce some methodological aspects that put in practice the results on systems stability we have presented in the former section. Figure 6 overviews the main steps of the overall approach. Given a set of peer LTSs, we first check whether this system is branching synchronizable [START_REF] Ouederni | Compatibility Checking for Asynchronously Communicating Software[END_REF]. If this is the case, it means that the observable behavior for the synchronous and asynchronous composition always remains the same whatever buffer size is chosen. Therefore, in such a case, the synchronous product can be used for analysis purposes.

If the set of peers is not synchronizable, we compute an initial bound k using one of the heuristics we will introduce below (Section 4.3). For that bound, we verify whether the kbounded asynchronous system is branching equivalent to the (k + 1)-bounded system. If it is the case, the system is stable for bound k. Then, we decrement k for searching the smallest k satisfying the stability property. Thus, we can analyze properties of interest for that system (buffers bounded to the smallest k) and, if they are satisfied, we proved that these properties are preserved for any upper bound.

If for a specific k, the equivalence check between the k-bounded asynchronous system and the (k + 1)-bounded system returns false, we modify k (using, e.g., binary search or incremental update of the former bound) and apply the check again. We repeat the process up to a certain arbitrary bound kmax that makes the approach abort if attained. If we reach that bound, the test is inconclusive. The only solution in that situation is to bound arbitrarily the system and analyze the system for that specific bound.

Salaün & Ye

Process Algebra Encoding

In order to automate these different checks, we use an encoding into process algebra and equivalence checking. In particular, we encode the set of peer LTSs into the LNT process algebra [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF], one of the input languages of the CADP toolbox [START_REF] Garavel | CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF]. Each peer LTS is represented in LNT using several processes. Each state in the peer LTS is encoded by one process, whose body corresponds to a choice between all the possible transitions outgoing from that state. Each branch of this choice first executes the action labelling the corresponding transition (message emission or reception, or internal action) followed by a call to the process encoding the target state of that transition. We also define in LNT FIFO buffers and classic operations to manipulate them. Finally, synchronous and bounded asynchronous compositions are generated using parallel composition and hiding operators. More precisely, in the asynchronous composition case, all peers and buffers are composed in parallel. Each peer reads from its buffer and sends messages to other peer buffers. Receptions corresponding to message consumptions for peers from their buffers are hidden.

In a second step, from this encoding, we use CADP compilers and exploration tools to generate synchronous and asynchronous composition LTSs. These LTSs are finally compared with CADP equivalence checking tools [START_REF] Bergamini | BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking[END_REF] for checking the stability property. The whole process is fully automated thanks to some Python scripts we wrote and SVL verification scripts [START_REF] Garavel | Svl: A Scripting Language for Compositional Verification[END_REF] that are automatically generated. Python scripts are particularly used for generating the LNT code and for searching the smallest bound k satisfying stability. SVL scripts automate the compilation from LNT to LTSs and call the equivalence checking tools.

Heuristics and Search Algorithms

In our experimental results, we use five strategies for searching the smallest bound k from which the set of peers interacting asynchronously become stable. Since the calculation of this bound is undecidable, all computations are bound by an arbitrary upper bound kmax. Each strategy consists of the computation of an initial bound k and an algorithm calculating the next bound to attempt.

• Our first strategy (#1) is brute force, i.e., we start from bound k equal to one and we increment it by one until obtaining a positive result for the equivalence check or reaching Inria kmax.

• A second strategy (#2) computes the longest sequence of emissions in all peer LTSs, then starts from this number and uses a binary search algorithm. For example, if the stability check for the first k is true (false, resp.), the next k to explore is midway between 1 and k (between k and kmax, resp.).

The intuition behind the longest sequence of emissions is that in that case all peers can at least send all their messages even if no peer consumes any message from its buffer. Experiments show that in most cases, the searched bound k is greater than or equal to this computed size.

• A third strategy (#3) uses again the longest sequence of emissions for the initial k, but then progresses by incrementing or decrementing the bound till reaching kmax or the smallest k satisfying stability. Precisely, if the stability check for the first k is true (false, resp.), the next bound to explore is k -1 (k + 1, resp.).

The problem of the longest sequence of emissions is when several peers have the same partner as recipient of their messages. In such a case, the partner buffer can get full even if the sending peers still want to emit other messages to it.

• A fourth strategy (#4) computes the maximum between the longest sequence of emissions in all peers and the highest number of emissions destinated to a same peer, and then uses the binary search algorithm (as for #2) for computing the next bounds. The second part of the maximum function corresponds to the case in which the buffer size prevents some peers to send messages because that buffer is already full. This case is somehow the counterpart of the longest sequence of emissions but from the receiver point of view.

• A fifth strategy (#5) uses the same initial k computation as presented for strategy #4, and then increments or decrements the bound till completion of the process as in strategy #3.

In the rest of this section, for the sake of evaluation of our approach, we will present experimental results and use them for comparing the strategies introduced above.

Experimental Results

We used a Mac OS laptop running on a 2.3 GHz Intel Core i7 processor with 16 GB of Memory and carried out experiments on more than 300 examples of communicating systems. Table 1 presents experimental results for some real-world examples. We also present at the end of the table a few hand-crafted examples for showing how our approach scales (the examples from the literature are quite small). The table gives for each example the number of peers (P), the total number of states (S) and transitions (T) involved in these peers, the bound k if the system is stable (0 if the system is synchronizable and kmax if this upper bound is reached during the analysis process), the size of the k-bounded asynchronous system (minimized modulo branching reduction), and the time for applying the whole process for each strategy introduced beforehand. In the LT S k a column, we give the size of the 1-bounded asynchronous composition for synchronizable systems and the size of the kmax-bounded asynchronous composition for non-stable systems. During our experiments, we used a bound kmax arbitrarily fixed to 10, which enabled us to keep computation times within a few hours during our experiments.

All the examples included in the table involve cyclic behaviors. The examples from the literature correspond to quite simple systems (up to 5 peers). 10 examples are synchronizable, 13 examples are stable, and 4 examples are not stable. To sum up, out of the 27 real-world time (slightly more than 10 minutes for the last example with 20 peers using #1, #3, or #5). This time remains quite low for peers exhibiting many states and transitions (about 3 minutes for the first hand-crafted example (28) using #1, #3, or #5). Now let us compare the five strategies we used in our experiments. It turns out that strategy #2 and #4 are not very efficient in terms of performance for two main reasons. First, if the equivalence check for the initial k returns false, the binary search algorithm computes a second value for k, which can be quite high. This results in calculating asynchronous systems with large buffer bounds, which requires more computation time than for lower k values as computed with the other strategies. Second, in some cases, binary search takes time before converging to the result, and this causes additional equivalence computations. The advantage of binary search is that for non-stable systems, k increases quite fast and quickly reaches kmax, see CFSM system (4) for instance.

Strategies #3 and #5 are much better than strategies #2 and #4 but also better in most cases than strategy #1. This gain is not clear for small examples and examples requiring a small buffer bound, but it becomes obvious for examples involving more peers and for those requiring larger buffer bounds. These two strategies (#3 and #5) are particularly satisfactory when the initial k finely approximates the expected result. In such cases, we can have up to a factor 2 gain in terms of computation time, see the fourth hand crafted example (31) for illustration purposes.

Related Work

One of the first results on analyzing communicating state machines was proposed by Brand and Zafiropulo [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. They defined the unspecified receptions compatibility notion for interaction protocols described using Communicating Finite State Machines (CFSMs). This work focuses on the verification of n interacting processes executed in parallel and exchanging messages via FIFO buffers. When considering unbounded buffers, the authors showed that the resulting state spaces may be infinite, and the problem becomes undecidable. Gouda et al. [START_REF] Gouda | On the Progress of Communications between Two Finite State Machines[END_REF] presents sufficient conditions to compute a bound k from which two finite state machines communicating through 1-directional channels are guaranteed to progress indefinitely. Jeron and Jard [START_REF] Jéron | Testing for Unboundedness of FIFO Channels[END_REF] propose a sufficient condition for testing unboundedness, which can be used as a decision procedure in order to check reachability for CFSMs.

Abdulla et al. [START_REF] Abdulla | On-the-Fly Analysis of Systems with Unbounded, Lossy FIFO Channels[END_REF] propose some verification techniques for CFSMs. They present a method for performing symbolic forward analysis of unbounded lossy channel systems. In [START_REF] Leue | A Scalable Incomplete Test for Message Buffer Overflow in Promela Models[END_REF], the authors present an incomplete boundedness test for communication channels in Promela and UML RT models. They also provide a method to derive upper bound estimates for the maximal occupancy of each individual message buffer. Cécé and Finkel [START_REF] Cécé | Verification of Programs with Half-duplex Communication[END_REF] focus on the analysis of infinite half-duplex systems and present several (un)decidability results. For instance, they prove that a symbolic representation of the reachability set is computable in polynomial time and show how to use this result to solve several verification problems. Recently, Beohar and Cuijpers [START_REF] Beohar | Avoiding Diamonds in Desynchronisation[END_REF] studied sufficient and necessary conditions for desynchronizability modulo branching bisimulation. This property ensures that the asynchronous version of the system where processes interact via half-duplex buffers do not introduce spurious interleavings compared to its synchronous version. Poizat et al. [START_REF] Poizat | Bounded Analysis and Decomposition for Behavioural Descriptions of Components[END_REF] propose the notions of bounded analysis and bounded decomposition for Symbolic Transition Systems, which can be used to test boundedness of systems and to generate finite simulations for them so that standard model-checking techniques may be applied for verification purposes.

Darondeau et al. [START_REF] Darondeau | Quasi-Static Scheduling of Communicating Tasks[END_REF] identify a decidable class of systems consisting of non-deterministic communicating processes that can be scheduled while ensuring boundedness of buffers. [START_REF] Deniélou | Buffered Communication Analysis in Distributed Multiparty Sessions[END_REF] proposed a causal chain analysis to determine upper bounds on buffer sizes for multi-party sessions with asynchronous communication. Bouajjani and Emmi [START_REF] Bouajjani | Bounded Phase Analysis of Message-Passing Programs[END_REF] consider a bounded analysis for message-passing programs, which does not limit the number of communicating processes nor the buffers' size. However, they limit the number of communication cycles. They propose a decision procedure for reachability analysis when programs can be sequentialized. By doing so, program analysis can easily scale while previous related techniques quickly explode. Recently, Ouederni et al. [START_REF] Ouederni | Compatibility Checking for Asynchronously Communicating Software[END_REF] presented a sufficient condition for checking compatibility of a set of asynchronously communicating components with unbounded message buffers. They exploit the synchronizability property introduced in [START_REF] Basu | Deciding Choreography Realizability[END_REF], but if systems are non-synchronizable, they cannot be analyzed with this approach.

Communicating systems have been intensively studied in the context of choreographies and realizability/conformance checking in the last 10 years. In [START_REF] Bravetti | Contract Compliance and Choreography Conformance in the Presence of Message Queues[END_REF], the authors tackle the choreography conformance issue from a theoretical point of view, and propose notions of contract refinement and choreography conformance for services that communicate through message queues. [START_REF] Gössler | Realizability of Choreographies for Services Interacting Asynchronously[END_REF] proposes techniques to check whether a set of peers interacting asynchronously can realize a choreography with finite buffers, and if so, for what buffer sizes. [START_REF] Lohmann | Decidability Results for Choreography Realization[END_REF] studies several notions of realizability and investigates decidability results for choreographies involving services interacting via buffers, which do not assume that messages arrive in the same order in which they have been sent. As mentioned earlier in this paper, Basu et al. proposed to check choreography conformance and realizability verifying the synchronizability property [START_REF] Basu | Deciding Choreography Realizability[END_REF]. The realizability problem for Message Sequence Charts (MSCs) has also been studied, see, e.g., [START_REF] Uchitel | Incremental Elaboration of Scenario-based Specifications and Behavior Models using Implied Scenarios[END_REF][START_REF] Alur | Realizability and Verification of MSC Graphs[END_REF]. [START_REF] Alur | Realizability and Verification of MSC Graphs[END_REF] for instance presents some decidability results on bounded MSC graphs, which are graphs obtained from MSCs using bounded buffers.

Compared to all these results, we do not impose any bound on the number of peers, cycles, or buffer bounds. Another main difference is that we do not want to ensure or check boundedness of the systems under analysis. Contrarily, we are particularly interested in unbounded (yet possibly stable) systems. We also go one step farther than synchronizable systems, since we propose verification techniques for systems that do not satisfy this property.

In [START_REF] Basu | Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers[END_REF], the authors work on a similar problem and propose an algorithm for identifying if the interactions of a given system with unbounded queues can be mimicked by the same system where queues are bounded. This paper assumes that determining the existence of a k verifying this property is computable, whereas we proved in this paper that this problem is undecidable. Moreover, [START_REF] Basu | Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers[END_REF] relies on trace equivalence and LTL logic. Trace equivalence is not adequate for analyzing communicating systems since this equivalence does not preserve important properties such as deadlock-freeness. We consider a finest notion of equivalence in this paper (branching), which allows one to check properties written with ACTL\X logic [START_REF] De Nicola | Action versus State Based Logics for Transition Systems[END_REF]. Last, the tool support provided in [START_REF] Basu | Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers[END_REF] does not provide any result (infinite loop, inconclusive result, or error) for more than half of the examples presented in Table 1.

Conclusion

We have presented in this paper a framework for formally analyzing systems communicating via (possibly unbounded) FIFO buffers. This work focuses on cyclic systems modelled using finite state machines. We have introduced the stability property, which shows that several systems become stable from a specific buffer bound k when focusing on send messages. The stability problem is undecidable in the general case, but for many systems we can determine whether those systems are stable using heuristics, search algorithms, and branching equivalence checking.

Inria

Experiments showed that many real-world examples satisfy this stability property and this can be identified in a reasonable time. Model checking techniques can then be used on the asynchronous version of the system with buffers bound to the smallest k satisfying stability. If a stable system satisfies a specific property for that k, the property will be satisfied too if buffer bounds are increased or if buffers are unbounded.

Figure 1 :

 1 Figure 1: Motivating Example (1)

Figure 2 :

 2 Figure 2: Motivating Example (2)

Inria

Figure 3 :

 3 Figure 3: A single k-message state (left part) and a loose k-message state (right part).

  It follows that LT S k+m-1 a ≡ br LT S k+m a , which contradicts our inductive hypothesis. Thus we must have LT S k+m a ≡ br LT S k+m+1 a . From above, based on LT S k a ≡ br ... ≡ br LT S k+m , we prove LT S k+m a ≡ br LT S k+m+1 a . This proves the theorem.

Figure 5 :

 5 Figure 5: A Well-formed yet Unstable System

Figure 6 :

 6 Figure 6: Methodological Aspects

  . Then from Lemma 1, we can deduce that for each single (k + m)-message state s k+m in LT S k+m a

	is exactly the same LTS as LT S k+m a inductive hypothesis LT S k a ≡ br LT S k+m . This implies LT S k+m+1 a a , we have LT S k a ≡ br LT S k+m+1 ≡ br LT S k+m a a .	k+m+1 a . From the
	• In the second case, since there exists a buffer containing k + m + 1 messages, there are
	new states in LT S k+m+1 a have LT S k+m-1 a ≡ br LT S k+m that are not in LT S k+m a a	. Now from the inductive hypothesis, we

RR n°8561

Acknowledgements. This work has been supported by the OpenCloudware project (2012-2015), which is funded by the French Fonds national pour la Société Numérique (FSN), and is supported by Pôles Minalogic, Systematic, and SCS. We would like to thank Radu Mateescu for his valuable suggestions to improve the paper.

As far as hand-crafted examples are concerned, we observe that the LTS sizes and computation times increase mainly with the size of the peer LTSs, the number of peers, and the size of buffer bounds. Yet we are able to check stable systems involving a large number of peers in a reasonable Inria


G Gogniat

V Fischer

A Baganne

C Mancillas López
email: cuauhtemoc.mancillas.lopez@univ-st-etienne.fr

M Méndez Real

L Bossuet

Trusted Computing using Enhanced Manycore Architectures with Cryptoprocessors

Keywords: manycore architectures, symmetric cryptography, key exchange, cryptoprocessor I Config. data, key Data bus Key memory bus Cipher key bus Master key Input

published or not. The documents may come

L'archive ouverte

INTRODUCTION

Secure handling of personal data and privacy in manycore architectures is a major issue. The economic and social challenges are numerous as this type of architecture will be massively deployed in the future both in infrastructure such as "cloud computing" and in most embedded systems constrained in resources and performance. It is thus essential to address the question of the definition of these architectures in terms of not only performance but also security to ensure a large adoption of these technologies by end users. Lack of trust will be a hindrance to economic development, the challenges are immense.

To propose an efficient and secure solution it is necessary to enhance hardware manycore architectures with closely coupling of heterogeneous processing resources (some dedicated to the processing of data in clear and some dedicated for treatment of protected data). It is also necessary to rethink the relationship between software and hardware to ensure a protection in depth. Today these issues are too often neglected resulting in solutions developed at the end of the design cycle as an afterthought. It is essential to provide a breakthrough in these design approaches to provide trusted manycore architectures by building hardware and software. This paper proposes an analysis of trust building to execute independent applications in parallel, securely and ensuring respect for the privacy of users. For this, several points are discussed: 1) proposition of a processing cluster to run both algorithms for processing information and cryptographic algorithms (with a strong level of coupling for performance reasons while ensuring no leakage of information), and 2) proposition of a manycore architecture integrating heterogeneous clusters for secure cryptographic. One key point discussed in this paper is related to the use of several cryptoprocessors for a single application. This point needs a deep analysis, especially for key exchange in order to guarantee no leakage of information.

The paper is organized as following. Section II discusses some challenges to enhance manycore architectures with cryptoprocessors. Section III illustrates how these challenges can be handled using an existing manycore solution named TSAR. Section IV provides an analysis of points that still need to be addressed and Section V concludes the paper.

II. CHALLENGES TO ENHANCE MANYCORE ARCHITECTURES WITH CRYPTOPROCESSORS

Manycore based systems will become the mainstream in a near future, it is thus mandatory to think these architectures with security properties by construction. Cloud computing is one of the numerous application domains that will rely on this technology. Several applications can be envisioned, for example secure access to private information. End users will perform many requests in parallel in order to retrieve, to search for, and to classify some personal data (e.g. text, images, and video). It is thus necessary to combine both processing power and cryptographic functions. In order to build a solution to execute many independent applications in parallel in a secure way, several points need to be targeted: 1) building of a processing cluster enhanced with cryptographic resources, 2) building of a manycore architecture integrating heterogeneous clusters for secure cryptographic, 3) building of mechanisms for logical isolation (in software) and physical (hardware level) to ensure execution of partitioned applications, 4) joint building of software layers (driver, API ...) and hardware to provide a chain of trust and 5) proposition of strategies for dynamically distributing applications on a manycore architecture taking into account the security needs. All these contributions need to be addressed to build an efficient and trusted execution platform. In this paper points 1) and 2) are discussed.

Using cryptoprocessors inside manycore architectures raises many challenges related to software and hardware layers. Links with the operating system and architecture of cryptoprocessors correspond to key issues. In this section some of these challenges such as heterogeneous clusters building, Trusted Computing Base analysis, and parallelism exploitation to improve the computation of cryptographic algorithms and the key exchange between cryptoprocessors are discussed.

A. Heterogeneous clusters building

The idea of enhancing GPPs using some coprocessor exclusively dedicated to perform some tasks that require intensive computation, such as numeric calculus or cryptography is not new. The use of heterogeneous clusters has been widely studied using for example Graphics Processing Units (GPUs) to perform intensive computations and thus reducing the GPP workload [START_REF] Song | A scalable framework for heterogeneous GPU-based clusters[END_REF].

Security is a very important service that a cluster in manycore architecture should hold. However cryptographic algorithms are based on operations that are generally not efficiently computed in GPPs such as bitwise operations, modular arithmetic, Galois field arithmetic, etc. [START_REF] Rodríguez-Henríquez | Cryptographic Algorithms on Reconfigurable Hardware (Signals and Communication Technology[END_REF]. So adding cryptoprocessor within a cluster will improve the performance of the cluster. Indeed, cryptographic algorithms implemented in software take thousands of clock cycles [START_REF] Krovetz | The software performance of authenticated-encryption modes[END_REF], while using a dedicated hardware coprocessor reduces the execution time to just few tens of clock cycles [START_REF] Chakraborty | Efficient hardware implementations of brw polynomials and tweakable enciphering schemes[END_REF]. So if the GPP delegates the cryptographic computations to the cryptoprocessor, its workload is significantly decreased. The saved time can be used to perform other tasks as image or signal computation.

The goal of the cryptoprocessor is to perform all cryptographic computations and to provide a secure generation, management and storage for session keys. When the amount of data to be processed by the cryptoprocessor is significantly large, several cryptoprocessors can be used in parallel to accelerate the process. Indeed several execution contexts can be considered. 1) An application requires a single cryptoprocessor. In that case the application will delegate the cryptographic computation to the cryptoprocessor. The key generation will be performed by the cryptoprocessor itself and no leakage of the key can occur. 2) An application requires several cryptoprocessors to handle a large amount of data while respecting a required bandwidth. In that case, data will be split into several sets and each set will be delegated to one cryptoprocessor. In that case the key management step is more complex as all cryptoprocessors need to share the same session key. A dedicated key exchange protocol within the architecture needs to be built. Key leakage needs to be considered with lot of care. 3) Several applications require a single cryptoprocessor. That case is similar to case 1) when preemption is not authorized. Such an assumption is relevant in order to guarantee a high level of security. In this work we discuss a solution in order to address these possible execution contexts. Symmetric key primitives are considered as they generally correspond to the main bottleneck when dealing with high amount of data, they are also cheaper in terms of hardware resources. It leads to a better tradeoff in terms of additional cost and achieved performances.

B. Cryptoprocessor as a Trusted Computing Base

The cryptoprocessor should provide algorithms for data privacy, data authentication, and hashing, furthermore a secure way to generate and store session keys is mandatory. Data privacy (i.e. confidentiality) guarantees the information can be understood only by authorized users, IV based encryption schemes are used to achieve this goal. NIST recommends Electronic Codebook (ECB), Cipher Block Chaining (CBC), Cipher Feedback (CFB), Output Feedback (OFB), and Counter (CTR) [START_REF] Dworkin | A 2001 Edition[END_REF]. In the context of symmetric key, data authentication means data integrity, i.e. it guarantees that the information has not been modified. Message Authentication Codes (MACs) correspond to the suitable cryptographic primitives to achieve this goal. In the literature there are several MAC schemes; interested readers can find a survey about them in [START_REF] Simplicio | Survey Survey and comparison of message authentication solutions on wireless sensor networks[END_REF]. In the context of manycore clusters, algorithms that provide a wide range of parallelism and high efficiency are expected. A selection of possible algorithms will be discussed latter in the paper.

Session keys should be generated using some of the existing True Random Number Generator [START_REF] Fischer | True Random Number Generators in FPGAs[END_REF]. The storage of session keys is performed inside the cryptoprocessor in a trust memory zone. As a security requirement when a key has to be transmitted outside the cryptoprocessor, the key is first encrypted and then sent to the GPP. The GPP has only access to encrypted keys in order to avoid software attacks like cache attacks [START_REF] Tromer | Efficient Cache Attacks on AES, and Countermeasures[END_REF]. To prevent some side-channel attacks, decryption primitive of block cipher should be used only to ensure the security of session keys. Other cryptographic services must only rely on the encryption primitive. Inside the cryptoprocessor an Arithmetic Logic Unit (ALU) is required. It performs the basic operations needed to compute mode of operations like bitwise XOR, increment, accumulators, etc.

From the system point of view the cryptoprocessor must be separated both at the architectural level and at the physical level from the GPP following the guidelines given in [START_REF] Gaspar | Secure Extension of FPGA General Purpose Processors for Symmetric Key Cryptography with Partial Reconfiguration Capabilities[END_REF] which allow building a secure system by design.

C. Notations

The next sections present the cryptographic parallel and the key exchange protocol. To describe these solutions, the following notation is considered: A block cipher is denoted as

) ( ⋅ K E
and n is its block length, the n-bit strings will be considered as members of

L xL 2 = , L L x 2 2 = ,…, L L x m m 2 =
this operation can be computed very efficiently using only one shift register and some XORs.

D. Performing cryptographic operations in parallel

When the amount of data is large, for example when encrypting an image or authenticating a video, more than one cryptoprocessor can be used in parallel to reduce the computation time. Some existing cryptographic algorithms allow their implementation in parallel. For encryption, Counter mode is easy to parallelize, it is defined as follows:

m K K K m P m IV E P IV E P IV E C C C ⊕ - + ⊕ + ⊕ = ) 1 ( || ... || ) 1 ( || ( || ... || || 2 1 2 1
where IV is an initialization vector,

) ( ⋅ K E
is totally independent from the previous, so that a message can be split into parts and each part can be sent to different cryptoprocessors along with the correct increment of the IV. For MAC the parallelization process is more complicated. As a first study Parallelizable Message Authentication Code (PMAC1) [START_REF] Rogaway | Efficient instantiations of tweakable blockciphers and refinements to modes OCB and PMAC[END_REF] is considered in this work, it is shown in Fig. 1:

Fig. 1. PMAC1 for complete blocks, ) 0 ( n K xE L = , 3 = β if m P is a complete block otherwise 5 = β .
Same as counter mode, in PMAC1 each invocation to

) ( ⋅ K E is independent, but in the masking sequence L x L x xL m ,..., , 2
each value is dependent from the previous, so the way to parallelized it is interleaving the blocks between the different cryptoprocessors. For example using two cryptoprocessors, one of them processes the odd blocks with the masking ,... , , .Each cryptoprocessor computes the intermediate addition and finally any of them computes the final tag τ . The same principle can be considered when more than two cryptoprocessors are available. In the Table 1 we show the computational cost of PMAC and counter mode.

When cryptoprocessors are used in parallel to perform some operation, all of them must use the same key, so a protocol for key exchange is necessary; this point is addressed in the following subsection.

E. Key exchange between cryptoprocessors

To perform parallel computation using several cryptoprocessors, all of them must handle the data using the same key. The output of the cryptoprocessors (i.e. cleartext or ciphertext) should be the same independently of the number of cryptoprocessors used to perform the computation. Indeed depending of the load of the system, encryption (or decryption) may be performed using n cryptoprocessors while decryption (or encryption) may use m cryptoprocessors. This point is defined at runtime based on the number of applications running in parallel on the manycore architecture. Keys can be shared using asymmetric cryptography but the cost in hardware of implementing such cryptography is huge in comparison with symmetric key primitive. The disadvantage of symmetric key based protocols is that they need to preload some master keys in each cryptoprocessor, but they can be implemented using just a MAC and a TRNG.

In order to allow an efficient key exchange between cryptoprocessors we propose a three levels hierarchical organization of the keys. The first level is the master key provided from the initialization of the system, the second level is the session keys generated by the cryptoprocessor at runtime and finally the third level is a pair of keys used to share and generate session keys for collaborative work between a set of cryptoprocessors. The mentioned organization allows the isolation of cryptoprocessors into sets and the authentication of the elements of the sets. A protocol to share a session key based on Location-Based Pairwise Key Establishments for Static Sensor networks [START_REF] Rodríguez-Henríquez | Cryptographic Algorithms on Reconfigurable Hardware (Signals and Communication Technology[END_REF] can be used. First, all the elements of the set of the cryptoprocessors are preloaded with a group master key G K and set key generation key K K , and a unique identifier ID. If there is a secure channel between cryptoprocessors in a set, any of them can generate a session key using the TRNG and sends it to the other elements of the set using such a channel. The main drawback with this approach is the architectural implication of dedicating an exclusive channel for cryptoprocessors and its isolation from the other communication resources.

Just some operations are necessary to perform the agreement of a key between to cryptoprocessors. Only one call to TRNG to generate a nonce and three executions of underlying MAC are required: one to prepare the request, another one for authentication and the last one to generate the pairwise key. The computational cost of a MAC is measured according to the number of blocks. A possible scenario is to consider that ACK and Hello are 16-bit fixed values, the identifiers of each cryptoprocessor A and B are 32-bit values (enough 2 32 different identifiers) and finally nonces N A and N B are 128-bit strings. If PMAC is used as the underlying MAC implemented with a 128-bit-block cipher like AES, the |HELLO||A||N A |=176 bits means a twoblock input to PMAC plus two additional block ciphers calls (see Table 1). The total cost of the MAC computation for request is four block ciphers calls. Following the same analysis, Table 2 shows the computational cost for all MACs involved in pairwise key agreement. If the amount of data to be processed is large, the cost of key agreement between a group of cryptoprocessors is negligible.

The key agreement is done only the first time that two cryptoprocessors collaborate for some task, after that the corresponding pairwise key is stored in a trust zone in each cryptoprocessor correctly indexed for its future use. The amount of storage is exactly one key for each cryptoprocessor in the group, and initially it is necessary to preload three keys in each cryptoprocessor: master key K M , group key K G and generation key K K . Some of the existing MAC algorithms based on block ciphers are parallelizable but not at the level required to be easily computed in a cluster, so some work still needs to be done to explore new constructions of MACs and Authenticated Encryption modes with a wide level of parallelization and efficiency.

III. CONTRIBUTIONS OF THE TSUNAMY PROJECT

The TSUNAMY project [START_REF]The TSUNAMY project[END_REF] explores some solutions to address main issues presented in Section II. The following section illustrates some of these solutions.

A. TSAR manycore originale architecture and enhancement

The TSUNAMY project relies on the TSAR manycore architecture [START_REF]The TSAR manycore architecture[END_REF]. The TSAR architecture is based on clusters connected through a NoC. Each cluster contains some GPPs, some memories and peripherals. Fig. 2 illustrates the TSAR architecture extended with a cryptoprocessor in each cluster. The cryptoprocessor is connected to the local interconnect and is reachable as any peripheral. DMA is used to send and retrieve data to/from the cryptoprocessor. This scheme allows reducing the load of CPUs. The cryptoprocessor used in this extended architecture is based on the HCrypt solution [START_REF] Gaspar | Secure Extension of FPGA General Purpose Processors for Symmetric Key Cryptography with Partial Reconfiguration Capabilities[END_REF].

Cryptoprocessor has configuration registers and its own DMA controller. When the GPP wants to use the cryptoprocessor first it has to send commands to configuration registers to indicate the task to be performed by the cryptoprocessor, the initial memory address and the size of the data buffer for the DMA, the initial memory address where the cryptoprocessors will write the result of

Total for the petitioner 13 17

Total for the responder [START_REF] Pearce | Virtualization: Issues, security threats, and solutions[END_REF] its computation, also establish initial values if necessary. After all the configurations are ready, GPP sends and starts command to the cryptoprocessor. When the cryptoprocessor ends the task it sends a ready message to the GPP.

The following section presents the HCrypt cryptoprocessor used to the enhancement of TSAR.

B. HCrypt Architecture and implementation

The HCrypt architecture is shown in Fig. 3. It is divided into three security zones: data, cipher and key zones [START_REF] Gaspar | Secure Extension of FPGA General Purpose Processors for Symmetric Key Cryptography with Partial Reconfiguration Capabilities[END_REF]. The HCrypt data zone contains 128-bit data registers, 128-bit ALU, I/O FIFOs (conversion between 32 bits and 128 bits) and the control logic. Configuration data buses (in black) are located in the configuration data zone and partly in the cipher zone. The HCrypt cipher zone contains two ciphers that work independently. Cipher 1 is dedicated to key protection and Cipher 2 to data protection. Cipher 1 uses a master key to decrypt session keys. Random numbers generated by the TRNG are transferred directly as an encrypted session key which is decrypted on both sides using the cipher (Cipher 1 in cryptoprocessor). For security reasons, Cipher 1 cannot be used in CBC-MAC mode for authentication of the session key because its output would need to be connected to the external data bus (in the data zone) and the processor could access the session key in clear. Instead, we propose to use a hashing function for session key authentication. In this way, the session key cannot be read in clear from the session key register. The session key is transferred in clear only from Cipher 1 to the key register and from the Cipher 1 to the HASH function using the dedicated key memory bus (in gray). The master key and session key registers each stores only one key. Before encryption, encryption keys (master or session keys) are transferred to key inputs of both ciphers via dedicated cipher key buses (in white).

Data are deciphered only by Cipher 2 using session keys. The cryptoprocessor supports all basic block encryption modes except ECB and CBC modes, because deciphering in both modes requires a decipher, which is not available in the HCrypt. However, data can be authenticated using the CBC-MAC mode, which requires only the cipher.

A prototype of HCrypt cryptoprocessor was described in VHDL and mapped to Virtex-6 XC6VLX240TFF1156 device using ISE ver. 12.4. It was implemented and tested in the Xilinx ML605 board. The proposed architecture uses only fine grain FPGA resources and embedded RAMs/FIFOs. HCrypt uses 1618 slices (including two AES ciphers, MD5 hash function, TRNG, data path including ALU, internal registers and control logic) and 1188 kbits of embedded RAM.

With a clock frequency of 100 MHz, the HCrypt cryptoprocessor reached the payload throughput of about 860 Mbits/s. To estimate this latency, Table 3 provides the latency in number of clock cycles for several cryptographic operations.

In Table 3 we can see the number of clock cycles taken by HCrypt to perform the counter mode and PMAC. Counter mode is very efficient because of the independence between the block cipher inputs, and the increment of the counter is performed in a dedicated register in the ALU of HCrypt. The Xtimes operations for PMAC is also computed inside a special register, the initial latency for PMAC is larger than in CBC-MAC because of the two extra block cipher calls. The extra latency of PMAC is not important when the amount of data to be processed is significantly large. In the case of key agreement process CBC-MAC could be used also in order to save some clock cycles.

The initial version of HCrypt is not designed to work in a collaborative way, so an important task of this work is to explore the way to use many cryptoprocessors together. We will explore the architectural and logical aspects to communicate cryptoprocessors in a secure way; this means the design of protocols that allow communicating of cryptoprocessors without the intervention of GPP. Another important task is the definition of the size of the groups of cryptoprocessors and the level of cooperation between the members, how many cryptoprocessors can be used for the same task and the limit of parallelization of the cryptographic algorithms. IV. DISCUSSION Building a trusted solution based on manycore architecture still requires some work in order to build a trust chain between the applications and the architectures. The software layer is a critical point where most of attacks are launched. It is thus essential to define the software Trusted Computing Base. Different solutions can be considered based on an operating system or combining an operating system and a virtualization layer. One key point is application isolation in order to guarantee a secure execution of application and no leakage of information (code, data). Some solutions to this issue propose to use virtualization mechanism [START_REF] Pearce | Virtualization: Issues, security threats, and solutions[END_REF], to use OS-level separation for multiprocessor system on chip [START_REF] Inoue | FIDES: An advanced chip multiprocessor platform for secure next generation mobile terminals[END_REF], or recently to run a trusted agent (TCB element) on every core of a many-core platform [START_REF] Masti | Isolated execution in many-core architectures[END_REF].

Combining software and hardware isolation needs to be considered in order to build a strong security layer being able to protect the system against confidentiality, integrity and denial of services attacks. It is also essential to extensively analyze the threat model in order to anticipate the risks when the application or/and the kernel are compromised. There have been many researches in that domain, it is required to adapt them to the manycore context where many applications can run concurrently and compete for some resources. Another important concern is how to distribute applications on the platform, how to schedule the applications and how to build some efficient heuristics taking into account processor workloads, execution parameters (temperature, frequency, and voltage) and security. Introducing security as a new dimension is a major concern and still many works needs to be done in that direction.

In the TSUNAMY project we address some of these challenges and our goal is to validate these propositions through simulation modeling using SystemC CABA. For that purpose the TSAR architecture and the ALMOS operating system [17] are used. The TSUNAMY project aims to provide the scientific community of academic and industrial with models of architectures and software libraries to efficiently and securely deploy applications on manycore architectures.

V. CONCLUSION

Manycore architectures correspond to an important computation paradigm shift for modern embedded systems. The secure execution of applications using these architectures still needs to be investigated. In this paper we propose to stress some of the challenges that are in front of us and we discuss some possible solutions in order to enhance these architectures with cryptoprocessors. Key agreement in a main step when several cryptoprocessors are used in parallel to increase the computation efficiency. We propose a first approach to address this point and evaluate the performance impact. Some research directions are also discussed and conclude the paper.

  polynomials of degree at most n-1. The addition in this field is a bit-wise ⊕ . + denotes an integer addition modulo n 2 . A||B denotes the concatenation of A and B and |A| is the length in bits of A. Xtimes means the multiplication of polynomial ) ( x q by monomial x modulo an irreducible polynomial ) ( x p and denoted as xL . In terms of values

  .., 1 the ciphertext. We can see from the definition that each invocation of

  and the other one the even blocks with the masking

Fig. 2 .

 2 Fig. 2. Enhanced TSAR architecture

Fig. 3 .

 3 Fig. 3. Architecture of the HCrypt cryptoprocessor.

TABLE 1

 1

	COMPUTATIONAL COST OF PMAC
	AND COUNTER MODE
	Cryptographic mode	BC* per block	XOR per block	Extra BC	Extra XOR
	PMAC	1	1	0	0
	Counter Mode	1	2	2	1
	*BC is for block cipher calls

TABLE 2 COMPUTATIONAL

 2 COSTS OF MACS USED TO AGREE A PAIRWISE KEY

	Operations involved in pairwise key agreement	Input-length	Block calls cipher	XOR
	MACKG(Hello, A, NA)	176-bit	4	5
	MACKG(ACK, B, A, NA, NB)	304-bit	5	7
	MACKG(NA, NB)	256-bit	4	5

TABLE 3

 3

	LATENCY O F HCRYPT OPERATION IN
	NUMBER OF CLOCK CYCLES
	Cryptographic operations and modes	HCrypt hardware resource	Number of clock cycles
	Session key generation	TRNG	1
	128-bit AES ECB	Cipher1	11
	256-bit AES ECB	Cipher2	22
	MD5 (128-bit input data)	Hash	66
	K.128-bit AES CFB	Cipher2	14.K+5*
	K.128-bit CBC-MAC	Cipher2	13.K+5*
	PMAC	Cipher2	26 # +13.K
	Counter mode	Cipher2	12.K
	*5 clock cycles for initialization vector, 26 clock cycles for the two extra block
		ciphers calls and extra XOR.

ACKNOWLEDGMENT

The work presented in this paper was realized in the frame of the TSUNAMY project number ANR-13-INSE-0002-02 supported by the French "Agence Nationale de la Recherche". BIBLOGRAPHY