Wojciech Mostowski
email: w.mostowski@utwente.nl

A Case Study in Formal Verification using Multiple Explicit Heaps

In the context of the KeY program verifier and the associated Dynamic Logic for Java we discuss the first instance of applying a generalised approach to the treatment of memory heaps in verification. Namely, we allow verified programs to simultaneously modify several different, but possibly location sharing, heaps. In this paper we detail this approach using the Java Card atomic transactions mechanism, the modelling of which requires two heaps to be considered simultaneously -the basic and the transaction backup heap. Other scenarios where multiple heaps emerge are verification of real-time Java programs, verification of distributed systems, modelling of multi-core systems, or modelling of permissions in concurrent reasoning that we currently investigate for KeY. On the implementation side, we modified the KeY verifier to provide a general framework for dealing with multiple heaps, and we used that framework to implement the formalisation of Java Card atomic transactions. Commonly, a formal specification language, such as JML, hides the notion of the heap from the user. In our approach the heap becomes a first class parameter (yet transparent in the default verification scenarios) also on the level of specifications.

Introduction

In the formal verification of object-oriented programs the verification tools and associated logics are constantly improved and developed to handle new verification challenges and to deal with larger and more complex programs. Some of these challenges are efficient reasoning about linked data structures [START_REF] Distefano | jStar: towards practical verification for Java[END_REF][START_REF] Leino | Dafny: An automatic program verifier for functional correctness[END_REF] or concurrent programs [START_REF] Jacobs | Verifast: A powerful, sound, predictable, fast verifier for C and Java[END_REF][START_REF] Leino | Verification of concurrent programs with Chalice[END_REF][START_REF] Amighi | The VerCors project: Setting up basecamp[END_REF]. Central in all these efforts is the notion of the object heap that is used in respective logics to represent the memory that programs operate on and to handle possible object aliasing. In particular, Separation Logic [START_REF] Parkinson | The relationship between separation logic and implicit dynamic frames[END_REF], that some of the verification systems utilise, is strictly built around the notion of the heap, rather than the program that operates on it.

In a similar spirit, the KeY system1 [START_REF]Verification of Object-Oriented Software: The KeY Approach[END_REF], an interactive verifier for Java programs, was recently redesigned and reimplemented to introduce explicit heap representation to the Java Dynamic Logic [START_REF] Schmitt | Dynamic frames in Java dynamic logic[END_REF]. Previously, the heap was represented in the KeY logic implicitly through special semantics of object field updates with complex built-in rewrite rules [START_REF]Verification of Object-Oriented Software: The KeY Approach[END_REF]Chap. 3]. In the new version the heap is explicit, directly accessible through a dedicated program variable heap. In particular, this change in heap treatment enables reasoning with dynamic frames [START_REF] Kassios | Dynamic frames: Support for framing, dependencies and sharing without restrictions[END_REF] in KeY. To accommodate dynamic frames style of specifications KeY uses an extended version of the Java Modelling Language (JML) [START_REF] Burdy | An overview of JML tools and applications[END_REF], named JML*. In the proof obligation generation process the framing conditions expressed in JML* are translated to Java Dynamic Logic by constructing appropriate formulae over the heap program variable.

In the default scenario a Java program operates on just one main heap and so does the reasoning system when such programs are verified. Any specification elements, like the JML assignable clauses that express framing conditions, implicitly refer to this one heap. For example, "assignable o.f, o.g;" states that fields f and g of object o might be modified on the heap. There are, however, scenarios with computation models that refer to more than one heap. The first and the simplest example is in distributed programs, where some method may modify a set of locations locally as well as remotely through a remote call. For example, such a method could have this framing specification: assignable_local o.f, o.g; assignable_remote o.g, o.h; stating that an object o that is stored both locally and remotely (by holding a copy) is modified partly here and partly there. Note that this notion of multiple heaps is different from Separation Logic, which also talks about several heaps. In Separation Logic a heap can be split into two or more separate heaps with disjoint locations. Here we consider heaps that may (but do not have to) share common locations, i.e., one heap may be a (partial) copy of another. In particular, one location can be changed simultaneously on two or more heaps. Generally, different heaps represent different memory sites, either real physical ones or ones introduced to the reasoning system for modelling certain properties.

Our particular use case for considering more than one heap emerged during the rework of the support for Java Card atomic transactions [START_REF].2 Runtime Environment Specification[END_REF]Chap. 7] in KeY to follow the new explicit heap model. The Java Card technology [START_REF] Chen | Java Card Technology for Smart Cards: Architecture and Programmer's Guide[END_REF] provides a platform to program smart cards with a considerably stripped off version of Java with no concurrency, floating point numbers, or dynamic class loading. The lack of these features along with the security sensitive application areas of smart cards in the financial sector (bank cards), telecommunications (SIM cards), or identity (e.g., electronic passports), used to make Java Card an ideal verification target for many verification tools [START_REF] Stenzel | A formally verified calculus for full Java Card[END_REF][START_REF] Marché | The Krakatoa tool for certification of Java/Java Card programs annotated in JML[END_REF][START_REF] Burdy | Java applet correctness: A developer-oriented approach[END_REF]. However, one complicating factor in Java Card that was initially overseen by researchers is the said atomic transaction mechanism. The KeY system was the first verification tool to fully formalise the details of Java Card transactions and provide a working implementation [START_REF] Beckert | A program logic for handling Java Card's transaction mechanism[END_REF][START_REF] Mostowski | Formal reasoning about non-atomic Java Card methods in Dynamic Logic[END_REF].

In short, the transaction mechanism provides a way to group assignments into atomic blocks to preserve the consistency of heap data, which by default in Java Card physically resides in the permanent EEPROM memory. Furthermore, it provides mechanisms to make exceptions to the transaction data roll-back rules as well as to change the default target memory for heap data to reside in the volatile RAM instead. The core of our formalisation of this in Java Dynamic Logic is the simultaneous use of two heap variables in the computation model. The first represents the regular heap. The second one is used to store the backup copy of the heap for the case when the transaction needs to be aborted and the contents of the heap restored. The assignment rules in the logic operate on both heaps at the same time, raising the need to specify framing conditions for these two heaps in JML*. In effect, the heap becomes a specification parameter, a simple example for heap-parametric frame specification would be:

assignable[heap] o.f, o.g; assignable[backupHeap] o.f;
In the remainder of the paper we explain these ideas using the formalisation of the Java Card transaction mechanism in KeY as a case study. This consists of the core formalisation discussed in Sect. 2 and the extensions necessary for modular reasoning discussed in Sect. 3. The use of two heaps is not the only possible way to formalise Java Card transactions. However, the solution with two heaps provides a very clean formalisation with little implementation overhead (discussed in Sect. 4), especially compared to our previous work [START_REF] Beckert | A program logic for handling Java Card's transaction mechanism[END_REF], and gives a uniform framework to apply our ideas in other verification domains. We discuss this in Sect. 5. Finally, we conclude the paper in Sect. 6. The rest of this section is the relevant background information about Java Card [START_REF] Chen | Java Card Technology for Smart Cards: Architecture and Programmer's Guide[END_REF][START_REF].2 Runtime Environment Specification[END_REF] and the Java Dynamic Logic [START_REF]Verification of Object-Oriented Software: The KeY Approach[END_REF][START_REF] Schmitt | Dynamic frames in Java dynamic logic[END_REF].

Java Card

The Java Card technology provides means to program smart cards with Java. The technology consists of a language specification, which defines the subset of permissible Java in the context of smart cards, a Virtual Machine specification, which defines the semantics of the Java byte-code when run on a smart card, and finally the API, which provides access to the specific routines usually found on smart cards. The complicating feature of Java Card is that programs directly operate on two memories built into the card chip. Any data allocated in the EEPROM memory is persistent and kept between card sessions, the data that resides in RAM is transient and always lost on card power-down. The memory allocation rules are: (i) all local variables are transient, (ii) all newly created objects and arrays are by default persistent, and (iii) when allocated with a dedicated API call any array (but not an object) can be made transient. Note the important difference between a reference to an object and the actual object contents. While the object fields are stored in the persistent memory, the reference to that object can be kept in a local variable and be transient itself. 2 Any Java variable, once allocated in its target memory, is transparent to the programmer from the syntax point of view, and it is only the underlying Java Card VM that takes appropriate actions according to the memory type associated with the object.

Objects allocated in EEPROM provide the only permanent storage to an application. To maintain consistency of data in EEPROM, Java Card offers the atomic transaction mechanism accessed through the API. The following is a brief, but complete summary of the transaction rules. Updating a single object field or array element is always atomic. Updates can be grouped into transaction blocks, a static API call to beginTransaction opens such a block, which is ended by a commitTransaction call, an explicit abortTransaction call, or an implicit abort caused by an unexpected program termination (e.g., card power loss). A commit guarantees that all the updates in the block are executed in one atomic step. An abort reverts the contents of the persistent memory to the state before the transaction was entered. Note that an explicit abort does not terminate the whole application, only cancels out persistent updates from within the transaction and the program continues its execution. Finally, the API provides so-called nonatomic methods to bypass the transaction mechanism. A non-atomic update of a persistent array element is never cancelled out by an abort, provided the same array was not manipulated with regular assignments earlier in the same transaction. We provide illustrative examples for these rules later in Sect. 2.

Java Dynamic Logic with Explicit Heap

The Java Dynamic Logic (JDL) [START_REF]Verification of Object-Oriented Software: The KeY Approach[END_REF][START_REF] Schmitt | Dynamic frames in Java dynamic logic[END_REF] of the KeY system is an instance of Dynamic Logic [START_REF] Harel | Dynamic Logic[END_REF] tailored to Java. Modalities p φ and [p]φ represent the notion of total and partial correctness, respectively, of program p w.r.t. property φ. Java programs are deterministic, hence total correctness requires p's termination, including the absence of top-level exceptions, for partial correctness termination is not required. Formula φ is built from logic terms using the usual connectives. Terms contain references to logic variables -rigid symbols whose valuation is independent of the program state, and program variables -non-rigid symbols that are program state dependent.

The verification of Java programs in the KeY system is based on symbolic execution realised through a sequent calculus. Program p in the modality is transformed by dedicated calculus rules to progressively reduce the program p into a description of the resulting program state. This description, denoted by U, is called an update, and is essentially a set of canonical assignments of terms to program variables. The following two rules are characteristic for JDL:

Γ, Ub |= U π p ω φ Γ, U!b |= U π q ω φ Γ |= U π if(b){p}else{q} ω φ if Γ |= U{v := se} π ω φ Γ |= U π v=se; ω φ assign
In these rules π denotes an inactive prefix of the program, e.g., a try{ block opening, a label, or a logic-only description of the current method call stack. The remaining statements of the verified program that the current rule does not operate on is denoted with ω. The if rule unfolds the if-statement, which is removed from the modality, and two proof branches are created, where the execution of the two if branches, resp. p and q, can continue. The branch condition b is evaluated in the current state by applying the state update U to it. The assign rule transforms an assignment of a simple expression se to a local variable v into the update U.

A complete symbolic execution of a program results in an empty modality and a set of updates that can be applied to the formula φ to check the validity of the initial claim p φ. If we consider U to be an operator on φ then it actually is another modality, one that only accepts sequences of canonical assignments as valid programs with the important property that the valuation of the formula φ can be quickly performed with a sequence of one-way update simplification and application rules, i.e., an equivalent of the weakest precondition calculus.

So far this covers only local Java variables, the need to reason about objects and arrays introduces the notion of a heap into the logic. The heap is represented as a dedicated program variable of a logic sort Heap and treated on equal grounds with other program variables. In particular, references and updates to the heap variable can directly appear in the set of updates U. The immutable terms of the sort Heap are built using rigid function symbols select and store, that allow, respectively, querying the heap for a value of a given location, and constructing a new heap with some location updated to a new value w.r.t. some old heap. In particular, the assignment rule for updating an object field f is the following (fields are also first class citizens in JDL):

Γ |= U{heap := store(heap, o, f, se)} π ω φ Γ |= U π o.f=se; ω φ assignField
For a specification language the KeY systems employs JML*, an extension of JML [START_REF] Burdy | An overview of JML tools and applications[END_REF] to accommodate dynamic frames [START_REF] Kassios | Dynamic frames: Support for framing, dependencies and sharing without restrictions[END_REF]. This extension introduces the primitive type of location sets into JML and allows the assignable clauses to refer to variables of such a type instead of static locations. Since dynamic frames are an orthogonal issue to our formalisation of transactions, JML* is synonymous with JML for the work we present here. Moreover, only very basic JML constructs, that we assume the reader is familiar with, are discussed in the paper. In the verification process the KeY systems translates a single Java method to be verified and the associated JML* specification into a JDL formula. In this process the heap variable is treated in a special way -it is the properties over this variable that need to be expressed to reflect any framing conditions specified in JML*. A very similar process is applied with similar implications on the heap variable when JML* specifications are used as axioms to replace method calls following the modular verification principles.

The JDL offers other strong facilities for reasoning about Java programs, e.g., the modelling of static initialisation, or comprehensive treatment of Java arithmetic including overflow. However, the work we present in this paper neither affects nor is affected by these other features of the logic. The KeY system itself is a GUI based user-friendly interactive verifier for JDL with a high degree of automation to minimise unnecessary interaction, often leading to fully automatic proofs even for considerably complex programs and properties.

Java Card Transactions on Explicit Heaps

In the following, driven by examples, we gradually present the complete formalisation of the Java Card transaction semantics in the KeY JDL and show how multiple heap variables are used. To start with, we introduce native transaction statements to the Java syntax handled by the logic. That is, the logic should allow for the symbolic execution of #beginTr, #commitTr, and #abortTr that define the transaction boundaries in the verified program. Bridging the actual transaction calls from the API to these statements is a straightforward extension int newBalance = 0; #beginTr; this.opCount++; newBalance = this.balance + change; if(newBalance < 0) { #abortTr; }else{ this.balance = newBalance; #commitTr; } of the verification system. Then, consider the snapshot (slightly artificial on purpose) of a Java Card program on the right, where the fields balance and opCount of object this are persistent, permanently storing the current balance and operation count of some payment application. The local variables change and newBalance are transient. Ignoring the transaction statements for the moment, the symbolic execution of this program results in the following state updates: newBalance := 0, heap := store(heap, this, opCount, select(heap, this, opCount) + 1), newBalance := select(heap, this, balance) + change, heap := store(heap, this, balance, newBalance) (when newBalance ≥ 0)

The symbolic execution of the if statement splits the proof, so the last update only appears on the else proof branch where newBalance ≥ 0 is assumed.

After further simplification, this set of state updates can be applied to evaluate a property querying e.g., the value of operation count, which in the logic would be the term select(heap, this, opCount). The result would indicate a one unit increase w.r.t. the value stored on the heap before this code is executed.

Basic Transaction Roll-back

Assuming a simplified Java Card definition, updates to local variables should be kept, while the updates to persistent locations should be rolled back to the state before the transaction was started. The persistent locations in the actual program are synonymous with the data stored on the heap in the logic. Hence, in the first attempt it should be sufficient to roll back the value of the whole heap. This can be done by introducing two simple rules for transaction statements #beginTr and #abortTr that, respectively, store and restore the value of the heap to and from a backup heap variable bHeap:

Γ |= U{bHeap := heap} π ω φ Γ |= U π #beginTr; ω φ begin Γ |= U{heap := bHeap} π ω φ Γ |= U π #abortTr; ω φ abort
This can be done and works as expected because the heap variable as modelled in KeY JDL has call by value characteristics. Now the set of state updates (on the negative newBalance branch) of our example program is the following:

newBalance := 0, bHeap := heap, heap := store(heap, this, opCount, select(heap, this, opCount) + 1), newBalance := select(heap, this, balance) + change, heap := bHeap (when newBalance < 0)

Whatever terms referring to heap contents should be evaluated with this set of updates, the result would be the values on the heap at the point where it was saved in the bHeap variable. The commit statement needs no special handling apart from silent stepping over this statement. In this case the saved value of the heap in the bHeap variable is simply forgotten until a possible subsequent new transaction where bHeap is freshly overwritten with a more recent heap.

For the very superficial treatment of transaction semantics this is enough to model transactions in JDL. Note that, so far, no new or assignment rules of any kind were introduced and the new heap variable bHeap is not modified in any way apart from being initialised to hold a complete copy of the regular heap.

Transaction Marking and Balancing

The two rules we just introduced do not enforce any order on the transaction statements, they allow to successfully verify malformed programs like "#abortTr; #beginTr;" or "#commitTr; #commitTr;". Furthermore, by Java Card specification, transactions cannot be nested, i.e., the maximum allowed transaction depth is 1, attempts to exceed this limit cause a run-time exception. On the other hand, the scope of a single transaction is very liberal according to the specification -a transaction can be in progress for as long as the card session is active, regardless of the stack of method calls. To simplify our formalisation, we opt for enforcing a stronger requirement -a transaction should be contained in one single Java method. That is, any method that opens a transaction has to close it before the method terminates. This does not exclude complete methods to be called during a transaction, but it does exclude a transaction opening in one method, and closing in another one that is eventually called later on. Our requirement is justified by Java Card security guidelines [START_REF] Pallec | NFC cardlet development guidelines v2.2[END_REF] that ban programs with transaction blocks spanning over several methods (to prevent transaction buffer overruns). 3 In practice, our formalisation not only relies on this requirement, but also enforces it, i.e., programs not adhering to this requirement do not verify.

Consequently, our formalisation restricts the transaction scope in the following way. A transaction marker TR attached to a modality indicates that the current execution context of the verified program is an open transaction. Rules for handling transaction opening and closing statements are now sensitive to this marker and automatically enforce correct transaction balancing. Similarly, rules for discharging empty modalities prevent closing proofs with a remaining transaction marker. In turn, any transaction block has to appear in a single verification context (modality), i.e., one method. Furthermore, the dedicated rule for array assignments can be singled out for transaction contexts only. This keeps verification of regular Java programs clear of any unnecessary transaction artefacts in the proofs. Finally, knowing that the current point in the symbolic execution is a transaction context is important in modular verification for the local interpretation of heap parametric specifications as explained later in Sect. 3.

The rules for transaction statements are the following. An explicit rule for the commit statement is added, in which nothing happens to the heap variable, but the transaction context is cancelled out by removing the TR marker:

Γ |= U{bHeap := heap} TR π ω φ Γ |= U π #beginTr; ω φ begin Γ |= U{heap := bHeap} π ω φ Γ |= U TR π #abortTr; ω φ abort Γ |= U π ω φ Γ |= U TR π #commitTr; ω φ commit
Persistent and Transient Arrays So far in our formalisation we roll back the whole contents of the backup heap, i.e., we operate the bHeap variable as a whole without changing single object locations on it. The separate transaction treatment for the persistent and transient arrays in Java Card now requires also selectively modifying the backup heap, as we describe in the following. 4The Java Card transaction rules require that the contents of transient arrays, allocated by dedicated API methods, are never rolled back. Since in JDL all arrays are stored on the heap, we somehow need to introduce a selective roll-back mechanism. We achieve this with the following. Whenever an array element is updated in a transaction we check for the persistency type of the array. The check itself is done by introducing an additional implicit boolean field to all objects, called <transient>, that maintains the information about the object's persistency type. Standard allocation rules set this field to false, while the dedicated API methods for creating transient arrays specify this field to be true.

Then, when handling assignments, for persistent arrays we take no additional action, for transient arrays we update the value on the heap and simultaneously update the value on the backup heap bHeap. During an abort, the regular heap is restored to the contents of the backup heap that now also includes updates to transient arrays that were not supposed to be rolled back. The core of the resulting assignment rule for arrays is the following: heap := store(heap, tr, 0, 0), heap := store(heap, ps, 0, 0), bHeap := heap, heap := store(heap, tr, 0, 1), bHeap := store(bHeap, tr, 0, 1), heap := store(heap, ps, 0, 1), heap := bHeap With these updates, the valuation of select(heap, ps, 0) and select(heap, tr, 0) results in resp. 0 and 1 as required by the Java Card transaction semantics.

Non-atomic Updates

The last complication in the transaction rules are the so-called non-atomic updates of persistent array elements. Such updates bypass transaction handling, i.e., no roll-back of data updated non-atomically is performed. Updates to transient arrays as defined by Java Card are in fact nonatomic, as they are never rolled back either. We have just introduced a mechanism that prevents the roll-back of transient arrays, by checking the <transient> field of the array and providing corresponding state updates. To extend this behaviour to persistent arrays, we allow for the implicit <transient> field of an array to be mutable in our logic. In turn, we can temporarily change the assignment semantics for an array by manipulating the <transient> field. Concretely, a non-atomic assignment to a persistent array element can be modelled by first setting the <transient> field to true, then performing the actual assignment, and then changing the value of <transient> back to false. Hence, a non-atomic assignment "a[i] = se;" to a persistent array a, is simply modelled as: a.<transient> = true; a[i] = se; a.<transient> = false; Then, the array assignment rule we provided above introduces the necessary updates to the regular and backup heaps to achieve transaction bypass.

In Java Card the non-atomic updates are delegated to dedicated API methods, i.e., they are not part of the language syntax. Hence, the manipulation of the <transient> field is delegated to the reference implementation of these API methods, and this emulation of non-atomic assignments is easily achieved in the actual Java Card programs to be verified by KeY.

a[0] = 0; #beginTr; a[0] #= 1; a[0] = 2; #abortTr; a[0] = 0; #beginTr; a[0] = 2; a[0] #= 1; #abortTr;
Unfortunately, there is one more condition for nonatomic updates that we need to check. A request for a non-atomic update becomes effective only if the persistent array in question has not been already updated atomically (i.e., with a regular assignment) within the same transaction. If such an update has been performed, any subsequent updates to the array are always atomic within the same transaction and rolled back upon transaction abort. We illustrate this with two simple programs operating on a persistent array a above on the right, for simplicity we mark non-atomic assignments with #= instead of quoting the actual API call that does that. The top program results in a[0] equal to 1 (a non-atomic update is in effect), the bottom program rolls a[0] back to 0, as the regular assignment "a[0] = 2;" disables any subsequent non-atomic assignments, and hence all transaction updates are reverted.

To introduce this additional check in the logic, we employ one more implicit field for array objects, <trUpdated>, that maintains information about atomic updates. Set to true, it indicates that the array was already updated with a regular assignment, false indicates no such updates and allows for non-atomic updates in the same transaction still to be effective. The new assignment rule for arrays needs to be altered to handle all these conditions and also to record the changes to the <trUpdated> field itself. The saturated state updates to be introduced under different conditions in the assignment rule for "a[i] = se;" are the following:

Condition

State update Always heap := store(heap, a, i, se) !a.<transient> bHeap := store(bHeap, a, <trUpdated>, TRUE) a.<transient> and !a.<trUpdated> bHeap := store(bHeap, a, i, se)

The updates to the <trUpdated> field are purposely stored on the backup heap to ease the resetting of this field with each new transaction, because the backup heap is freshly assigned with each new transaction while the regular heap is not. Now, on transaction abort, the heap reverting update filters out any updates to this field on the backup heap using the anonymisation function of the JDL:

heap := anon(bHeap, allObjects(<trUpdated>), heap)

Intuitively, this expresses the operation of copying the contents of heap bHeap to heap, but retaining the value of the <trUpdated> field in all objects in heap. This way all manipulations of <trUpdated> in proofs are local to a single transaction.

Heaps as Parameters in JML*

The previous section spelled out the details of formalising Java Card transactions in JDL. The key point in this formalisation is the modified assignment rule in the sequent calculus that now operates on two heap variables. In some sense, assignment rules are always the core of the program logic -they give semantics of state changes for the verified program. A specification language that describes the program behaviour also deals in a large part with the corresponding state changes (or lack thereof). Hence, one can say there is a special correspondence between the assignment rules and the specification language. This means that specifications for methods called in transactions should additionally express properties about data on the backup heap together with the framing conditions. To this end we introduced the following extensions. To redirect any object field access o.f to a different heap one can use the \at operator, e.g., accessing data on the backup heap is expressed with \at(backupHeap,o.f). In this context, the plain field access o.f in fact means \at(heap,o.f). Then, for framing specifications, the assignable clauses also take a heap parameter to bind locations with a corresponding heap: Now is possible to generate separate proof obligations for the framing conditions for the two heaps and correctly apply method contracts in the presence of two heaps.

We generalise this further. Any specification element in JML*, like a precondition specified with the requires clause, receives a heap parameter. This parameter specifies the applicability context of the given specification element. In particular, specification elements defined for the backup heap are only considered in verification contexts of an open transaction, i.e., within the marked TR • modality. Specification elements not annotated with any heap apply to the default heap that is always active. This way we achieve transparency -old style specifications refer to the regular heap by default and retain their previous semantics. An illustration for this is given in Fig. 1, where a complete specification for the Java Card API method for updating chunks of arrays in a non-atomic way is given for both the transaction and non-transaction contexts.

Implementation in KeY

Implementing the support for Java Card transactions in KeY was done in two steps. The first step was to generalise the JML* interface to accept multiple heaps and convey the information about them to the proof obligation generation component and the modular reasoning component. This was simply done by considering an arbitrary list of heaps in the corresponding modules rather than referring to the one predefined heap. Until this point the extensions were fully generic, i.e., not specific to the Java Card transaction mechanism in any way. In particular, the generation of concrete formulae for framing conditions remained the same, only now several ones for different heaps are created.

In the second step we added the core formalisation of Java Card transactions to the KeY system. In KeY the logic rules are defined externally, using the socalled taclet language [START_REF]Verification of Object-Oriented Software: The KeY Approach[END_REF]Chap. 4] for defining the corresponding rewrites. The TR marker was added by simply declaring a new modality. Then a handful of new rules we discussed in Sect. 2 were added to the rule base. As an example, a self-explanatory taclet for the #beginTr statement is the following in KeY: beginJavaCardTransaction { \find (==> \diamond{.. #beginTr; ...}\endmodality phi) \replacewith(==> {backupHeap := heap} \diamond_transaction{.. ...}\endmodality phi) };

Apart from this rule and the transaction specific rule for array assignments the addition of the second heap variable backupHeap required only declaring it. This declaration automatically tells the other components of the KeY system to include it (considering the current verification context) in the corresponding verification tasks, like proof obligation generation or modular application of contracts.

To evaluate our work we revisited our earlier work on the fully verified reference implementation of the Java Card API [START_REF] Mostowski | Fully verified Java Card API reference implementation[END_REF]. We specified the Java Card API methods following the extended JML* syntax (see again Fig. 1) and verified both the reference implementation of the API as well as a handful of other Java Card examples that make calls to the Java Card API.

The overall result of our work shows considerable improvements compared to our old formalisation of transactions [START_REF] Beckert | A program logic for handling Java Card's transaction mechanism[END_REF][START_REF] Mostowski | Formal reasoning about non-atomic Java Card methods in Dynamic Logic[END_REF] back when the heap model in JDL was not based on explicit heap access through a special program variable. The complete set of changes to the logic and the calculus is now much smaller, the implementation overhead of the new rules practically negligible, and finally the resulting automatic proofs for Java Card programs much more readable. We attribute these improvements to the use of multiple heaps, which was not possible before. Previously, the semantics of state updates on the implicit heap had to be heavily modified to include a notion of a forgetting update to model data rollback in the logic with deep implications for the calculus and the implementation. Preliminary work in the area of concurrent verification provides another strong case for the explicit use of multiple heaps as we briefly describe next.

New Applications for Multiple Heaps in Verification

In the introduction we mentioned distributed computing as an example where multiple heaps should be considered in the computation model, with at least the local and one remote heap. Another scenario is low level reasoning about systems with (possibly multi-level) cache memory, where one heap would represent the cache and one the main memory. Here the verification could concentrate on the data dependencies and synchronisation between the cache and the main memory. Going further, multi-core systems (like GPUs) could be also modelled using multiple explicit heaps, each heap representing the local memory of a single core. Finally, the real-time Java can be also considered in this context, where programs access memories with different physical characteristics on one embedded device [START_REF] Kwon | Memory management based on method invocation in RTSJ[END_REF].

In the context of the ongoing VerCors project5 [START_REF] Amighi | The VerCors project: Setting up basecamp[END_REF] we currently concentrate on extending the KeY logic to deal with permission based verification of concurrent programs. Permission accounting is a specification oriented methodology for ensuring race freedom in concurrent programs that allows for efficient threadlocal reasoning. Similarly to the implementation of permissions in the Chalice tool [START_REF] Leino | Verification of concurrent programs with Chalice[END_REF][START_REF] Parkinson | The relationship between separation logic and implicit dynamic frames[END_REF] we introduce a permission mask to the JDL to keep track of permissions in the verified programs. From our point of view, this permission mask is nothing more than a parallel heap-like structure that stores permission values for each location instead of the actual values. In the first experimental attempt, using the multiple heap framework that we discussed, we simply added a new heap structure to the logic, represented with the program variable permissions, to keep track of the permissions that the local Java thread owns. The location assignment and access rules were amended to ensure, respectively, a write or read permission to a given location. Now, using our heap-aware JML*, we can give permission based specifications: This states that we require a write permission to the location o.f, that this location is changed on the actual heap (the regular assignable), and also that the permission to the location may be modified, e.g., through permission transfer to another thread. Disregarding any specification clauses associated with permissions, in the example the first and the third line, transforms the specification into a permission unaware specification. This can be useful for verifying permission and functional properties separately. Very basic examples with permissions have been already verified with an experimental version of KeY.

Conclusions

In this paper we discussed the use of multiple heaps in formal verification of Java programs using the formalisation of Java Card atomic transactions fully implemented in KeY as an example. We also took the opportunity to give full details of this formalisation that were not yet published elsewhere. In the ongoing work we apply the same methodology to introduce permission based reasoning for concurrent Java programs in KeY. Few other applications in verification have been named as possible directions for more future work.

It seems that none of the other verification systems that we are aware of try to make heap or heap-like structures explicit on the level of the specification language, although certainly some of them indeed use multiple heap or heaplike structures internally. Most notably, the Chalice tool [START_REF] Leino | Verification of concurrent programs with Chalice[END_REF][START_REF] Parkinson | The relationship between separation logic and implicit dynamic frames[END_REF] works with two global variables H and P , that, respectively, represent the heap and the permission mask in the Boogie proof obligations. Not exposing the heap in the Separation Logic specifications and associated tools [START_REF] Jacobs | Verifast: A powerful, sound, predictable, fast verifier for C and Java[END_REF][START_REF] Distefano | jStar: towards practical verification for Java[END_REF] seems natural, however, applying them to new verification scenarios named in Sect. 5 becomes significantly more difficult in our opinion.

When it comes to the formalisation of Java Card atomic transactions, only the Krakatoa tool [START_REF] Marché | Verification of Java Card applets behavior with respect to transactions and card tears[END_REF] also provides a sound formalisation and implementation of the transaction roll-back that accounts for the specifics of non-atomic methods. The Krakatoa formalisation relies on keeping extra copies of data to be rolled back on the same heap as all the other data in dedicated backup fields associated with regular fields, i.e., all data fields are backed-up separately instead of the whole heap. This is very similar to our first formalisation of transactions [START_REF] Beckert | A program logic for handling Java Card's transaction mechanism[END_REF], which turns out to be very heavy-weight compared to our current work. We believe that our current formalisation can be applied easily in other verification systems, as long as such a system is capable of manipulating the heap variable as we do in the KeY logic. A partial support for Java Card transactions has been also recently reported for the VeriFast platform [START_REF] Jacobs | The VeriFast program verifier -a tutorial for Java Card developers[END_REF], however, the semantics of the transaction roll-back has not been formalised there. Finally, Java Card transactions have been considered to be formalised in the LOOP tool using program transformation to explicitly model transaction recovery directly in the Java code, but the ideas where never implemented in the tool [START_REF] Hubbers | Reasoning about card tears and transactions in Java Card[END_REF].

  Γ, U!a.<transient> |= U{heap := store(heap, a, i, se)} TR π ω φ Γ, Ua.<transient> |= U{heap := store(heap, a, i, se), bHeap := store(bHeap, a, i, se)} TR π ω φ Γ |= U TR π a[i] = se; ω φ arrayAssign Assuming that arrays tr and ps are, respectively, transient and persistent, the symbolic execution of this program: tr[0] = ps[0] = 0; #beginTr; tr[0] = 1; ps[0] = 1; #abortTr; results in the following sequence of state updates:

Fig. 1 .

 1 Fig. 1. Complete JML* specification for one of the Java Card API methods.

  requires[permissions] \at(permissions, o.f) == 1; assignable o.f; assignable[permissions] o.f;

http://www.key-project.org.

A garbage collector is not obligatory in Java Card either. Careless handling of references actually leads to memory leaks, something that is often addressed in Java Card programming guidelines[START_REF] Pallec | NFC cardlet development guidelines v2.2[END_REF].

Following a similar security rationale we disallow object allocation inside transactions. Real Java Card programs cause serious security risks when objects are allocated in transactions[START_REF] Mostowski | Malicious code on Java Card smartcards: Attacks and countermeasures[END_REF], while the formalisation to deal with the "shady" semantics of object deallocation mandated by the Java Card specification[START_REF].2 Runtime Environment Specification[END_REF] would require modelling of explicit garbage collection, something that Java verification systems in principle are not designed for.

Only arrays can be made persistent or transient in Java Card, regular objects are always persistent. Thus, we only discuss arrays in this context, but our formalisation works for regular objects, too.

http://fmt.cs.utwente.nl/research/projects/VerCors/.

Acknowledgements The work of W. Mostowski is supported by ERC grant 258405 for the VerCors project. We would like to thank Richard Bubel for his insights and invaluable help with the implementation.


Sergio Feo-Arenis

Bernd Westphal

Parameterized Verification of Track Topology Aggregation Protocols

Keywords:

We present an approach for the verification aggregation protocols, which may be used to perform critical tasks and thus should be verified. We formalize the class of track topology aggregation protocols and provide a parameterized proof of correctness where the problem is reduced to checking a property of the node's aggregation algorithm. We provide a verification rule based on our property and illustrate the approach by verifying a non-trivial aggregation protocol.

Introduction

We study the verification of aggregation protocols, which are often used in sensor networks [START_REF] Feng | Aggregation protocols for high rate, low delay data collection in sensor networks[END_REF][START_REF] Liu | A distributed energy-efficient data gathering and aggregation protocol for wireless sensor networks[END_REF][START_REF] Montresor | Robust aggregation protocols for largescale overlay networks[END_REF]. Such protocols compute an aggregation function in a distributed fashion. An aggregation function is a function of the data at sensor nodes where the messages sent by a node are determined by messages received from other nodes and the own data. Data is propagated from sensor nodes towards specially designated sink nodes, where the result of the computation is made available.

A simple example of an aggregation protocol is one where the maximum value among the sensors' data is calculated at a sink node. Here, if intermediate nodes transmit only the maximum value among the received data as it is forwarded to the sink, the utilization of resources can be improved. The reduced amount of data packets can, e.g., reduce energy usage, reduce the use of available bandwidth and increase the maximum data collection rate.

Sensor networks may use unreliable communication channels. In order to mitigate the problem of unreliable communications, sensor networks may take advantage of the fact that broadcast transmissions may be received by multiple nodes. In this way, they effectively provide multiple aggregation paths over which a node's data can be collected. Some aggregation functions are, however, duplicate-sensitive. That is, obtaining a correct result requires that sensor values are aggregated only once. This is the case when, e.g., calculating the sum or the average of the sensor values.

Data aggregation protocols are correct in the presence of unreliable communications if, whenever an aggregation path is available from a node to the sink, the sensor's data is correctly aggregated at the sink. I.e., it is aggregated, but exactly once if the function being calculated is duplicate-sensitive. This concept of correctness is the strongest possible when unreliable communications are employed. The failure of all aggregation paths cannot be completely ruled out. Our goal is to provide a method to (semi-)automatically verify correctness of aggregation protocols given the implementation of the algorithm executed by network nodes. As a first approach, we concentrate on track topologies, where nodes are arranged in tracks according to their distance (in hops) to the sink, and aggregation paths traverse consecutive track boundaries as shown in Figure 1.

We study aggregation protocols for topologies that have a reliable correction infrastructure. I.e., nodes within tracks have reliable communication links that can be used to correct communication errors. This is the case for, e.g., the use of short-range directional antennas or aggregation systems where communication units have multiple transceivers.

We additionally assume a schedule, i.e., the sequence in which nodes perform their computations and transmit their data, such that the data from input nodes is always available at the time of executing a node's algorithm.

Even under those assumptions, verifying correctness of an aggregation protocol requires considering all possible topologies, with a possibly unbounded number of nodes. Aggregation protocols are parameterized systems and can thus not be verified by explicitly verifying all instances. The problem of parameterized verification is undecidable in general [START_REF] Apt | Limits for automatic verification of finite-state concurrent systems[END_REF].

We approach the problem of verifying a specific class of aggregation protocols in this work. We make the following contributions.

1. We identify the class of aggregation protocols for track topologies with reliable correction infrastructure and provide a formalization as a parameterized verification problem, including the presence of link failures. 2. We provide a proof rule that reduces the parameterized verification problem to checking a verification condition on the nodes' algorithm and show its soundness. We thus provide an inductive invariant for the verification of track topology aggregation protocols. 3. We illustrate the utility of our results by applying the verification rule to a non-trivial aggregation protocol.

This work illustrates the possibility of performing parameterized verification for distributed systems with topologies that are not regular and with dynamic aspects such as node or link failures. We are able to concentrate the effort of verification on single nodes, without the need to consider topology or scheduling issues. Our formalization could be used together with approaches such as [START_REF] Namjoshi | Uncovering symmetries in irregular process networks[END_REF] to obtain parametric proofs for such systems. Formalizing link and node reliability can provide the basis for deriving inductive invariants.

Track Topologies and Aggregation Protocols

We define the class of systems that are the subject of our verification effort. Inspired by instances seen in wireless sensor networks [START_REF] Feng | Aggregation protocols for high rate, low delay data collection in sensor networks[END_REF], we develop the concept of track topologies by establishing the properties that characterize them.

∀ (n, n ) ∈-→ • track (n) = track (n ) + 1 (1)
For (n, n ) ∈-→,
∀ (n, n ) ∈ PA ∃ n 0 , n 1 , . . . , n m • n 0 = n ∧ ∀ 0 ≤ i < m • n i n i+1 ∧ SA(n) ⊆ {n 0 , . . . , n m }. (2)
Note that due to the restriction that the aggregation relation connects only adjacent tracks, always connects nodes in the same track.

k is called the size of T , denoted by |T |.

An example of a track topology with primary, secondary and correction relations can be seen in Figure 2.

For our inductive proof, we require track topologies to be closed under removal of single nodes in the sink track. By allowing to remove only nodes in the sink track without outgoing correction edges, it is ensured that no correction path between a primary aggregator and the backup aggregators of some node is broken, thus preserving the property (2). Lemma 1. Let n 0 ∈ N 0 be a node from the sink track of a track topology T = (N 0 , -→ 0 , 0 , V 0 ) with domain D which does not have any outgoing edges in the correction relation to any other node.

Then T \ {n 0 } := (N, -→, , V) with

-N = N 0 \ {n 0 }, V = V 0 | N , --→= {(n, n ) ∈-→ 0 | n = n 0 }, = {(n, n ) ∈ 0 | n = n 0 }, -track (n) = track 0 (n) -1 if N 00 = {n 0 }, and track (n) = track 0 (n) otherwise,
is a track topology with domain D.

Whenever aggregation is performed, nodes initiate a transmission round, each transmitting their computed messages over the communication medium. In the following, we formalize unreliable communication links. We introduce an edge labeling function for the aggregation relation of a topology that indicates whether communication is successful or not during a transmission round.

f (n, n ) = 1.
The value of node n is available at the sink track if and only if there exists a -→-path from n to a node in the sink track such that the communication along the path was successful according to f . We use V f (n) to denote the value of n if the value is available at the sink track according to f and "•" otherwise, i.e. V f is pointwise defined as

V f (n) = V (n) , if ∃ n 0 ∈ N 0 • n -→ * f n 0 , • , otherwise. (3)
In the following, we present the formalization of aggregation protocols and their correctness, which provides the framework necessary to develop a formal verification approach.

We observe that an aggregation protocol can be formalized as a function that maps a set of sensor values to a final aggregation value. For simplicity, and without loss of generality, we assume that the domain of the sensor values and that of the aggregation result are the same. In practice, complex functions may utilize different domains.

We continue by defining correctness of an aggregation protocol in the presence of unreliable communication links. For that, we formalize correctness relative to the communication function f : whenever there is a working path from a node to a sink, the data of the node should arrive (in aggregated form) at the sink.

The assumption that the correction infrastructure is reliable plays an important role. If the correction links were not reliable, then one would have to define correctness not only for working aggregation paths but also for working correction paths. We restrict our analysis to a reliable correction infrastructure. Extending it to unreliable correction links should work in a similar fashion and is the subject of future work. Definition 3. Let T be a set of track topologies with domain D and

P : T × F T → D,
a track topology aggregation protocol on T , where F T denotes the set of communication functions of the track topologies in T .

Let A be a family of aggregation functions

A k : D k • → D, over domain D where k ∈ N 0 and D • = D {•}.
The aggregation protocol P is called correct wrt. A if and only if, whenever the value of a node n is available to the sink track, then the data transmitted by n is aggregated exactly once by P, i.e. if

∀ T = (N, -→, , V) ∈ T , k = |N | ∀ f ∈ F T • P(T, f ) = A k (V f (n 1 ), . . . , V f (n k )) . (4)
Now we formally characterize the aggregation protocols that are the subject of this work. We formalize the distributed calculation of the aggregation function as an equation system over local aggregation functions that map incoming messages and additional parameters to outgoing messages. The most prominent requirement in our formalization is that correction requests are directly observable in the network transmissions, thus allowing reasoning about the consistency of the messages computed by the nodes. Definition 4. Let T be a set of track topologies with a domain D such that (D • , ⊕, •) is a monoid. A track topology aggregation protocol P on T is called distributed homogeneous if and only if there exists a family of sets Msg k of messages together with two families

A k : Msg k k → D E k : Msg k k → 2 ID k of decoder functions, k ∈ N 0 , ID k = {1, . . . , k}.
Decoder function A k obtains the aggregation value encoded in a message and

E k : Msg k k → 2 ID k
extracts from a message the correction requests contained in that message, i.e., the set of nodes encoded in the message for which a corrective action should be taken if possible, there exists a family of local aggregation functions

aggr k : ID k × D × (ID k → Msg k ) → Msg k , k ∈ N 0 ,
such that, for track topology T = (N, -→, , V) ∈ T and communication function f ∈ F T , the aggregation result of the protocol P is the ⊕-sum of the messages emitted by the sink track, i.e.

P(T, f ) = ni∈N0 A (τ i ) ( 5
)
where message τ i of node n i ∈ N in the track topology is defined by applying the local aggregation function to the identity i of the node, its value, and the set of messages relevant for n i which have successfully been communicated according to f . That is, the messages τ 1 , . . . , τ k are the solution of the equation system

τ 1 = aggr k (1, V n 1 , M 1 ) M 1 = {i → τ i | (n i , n 1 ) ∈ (-→ f ∪ )} τ 2 = aggr k (2, V n 2 , M 2 ) M 2 = {i → τ i | (n i , n 2 ) ∈ (-→ f ∪ )} . . . . . . τ k = aggr k (k, V n k , M k ) M k = {i → τ i | (n i , n k ) ∈ (-→ f ∪ )}.
Note 1. A distributed homogeneous track topology aggregation protocol P with domain D is correct for track topologies with a single node in the sink track if and only if

A (τ) = A k (V f (n 1 ), . . . , V f (n k )) ( 6
)
where τ is the message emitted by the sink node.

Also note that we implicitly assume a computation sequence (or schedule) that ensures data availability for all nodes. That is, whenever a node starts its computations, all the input data is available. Thus, we assume that all nodes connected to a node n are scheduled to transmit their data before n.

Verification of Track Topology Aggregation Protocols

To be able to provide a parameterized proof of correctness as defined in the previous section, we require the aggregation function to be an associative operator over the aggregation domain, so that there is a correspondence between the final aggregated values and the partial values transmitted by intermediate nodes. We also require the operator to provide a neutral element to be able to aggregate sensors whose communication fails or do not have data available in a uniform fashion.

Definition 5. A family of aggregation functions A

k : D k • → D, k ∈ N 0 , over domain D is called monoidal with respect to (D • , ⊕, •), if and only if (D • , ⊕, •) is a monoid and ∀ v 1 , . . . , v k ∈ D • • A k (v 1 , . . . , v k ) = v 1 ⊕ • • • ⊕ v k . (7)
Bringing together the use of correction links and the transmission of correction requests, we introduce the concept of responsibility among nodes, defined as the confluence of both the availability of another node's data and of a correction request for that node. Definition 6. Let T = (N, -→, , V) be a track topology and f ∈ F T a communication function.

A node n ∈ N is called responsible for node n ∈ N , denoted by n -→ g n , if and only if n is an aggregator of n, communication from n to n was successful according to f , and communication from n to the predecessors of n in the correction relation was not successful according to f , i.e. if

n -→ g n :⇐⇒ n -→ f n ∧ ∀ (n , n) ∈ + •f (n, n ) = 0 (8)
We say a node n has a working aggregation path to node n ∈ N if and only if there is a sequence of responsible nodes between them, i.e., if n -→ * g n .

Note that working aggregation paths are unique (if existent). Protocol correctness can then be reformulated as the property that every node correctly aggregates the data of those nodes with a working aggregation path to it. Lemma 2. Let A be a monoidal aggregation function family with respect to (D • , ⊕, •) and P a distributed homogeneous track topology aggregation protocol on track topologies T with domain D.

If the message of a node n ∈ N encodes the ⊕-aggregation of the values of all nodes n for which n is responsible, i.e. if

∀ T ∈ T , f ∈ F T ∀ i ∈ ID k • A (τ i ) = n-→ * g ni V (n), ( 9
)
then P is correct wrt. A.

Proof. Let T ∈ T be a topology of size k and f ∈ F T a communication function.

Let n ∈ N be a node with a working aggregation path to a node n ∈ N 0 in the sink layer, i.e. if n -→ * g n , By Definition 6, there is a path from n to n with successful communications, i.e. n -→ * f n . Thus, by Definition 2, V f (n) = V (n). Let n ∈ N be a node with no working aggregation path to any node n ∈ N 0 in the sink layer. Because such a path consists of primary and backup parents which are, by Definition 1, connected by the correction relation . Thus there would exist a unique first parent for each track, and therefore n would have a working aggregation path, thus the value of n is not available at the sink track. Hence, by Definition 2, V f (n) = •.

By Definition 4, the premise (9), and the premise that A is monoidal we obtain

P(T, f ) = ni∈N0 n-→ * g ni V (n) = n∈N V f (n) = A k (V f (n 1 ), . . . , V f (n k )) ( 10
)
thus P is correct.

Now that we stated a property local to every node in a network, we introduce an abbreviation in the style of Hoare logic to denote the satisfaction of a postcondition given some precondition. We can in this form state the verification condition that must be satisfied in order to show protocol correctness. We choose this notation given that we intend to allow the verification of the implementation of the local aggregation functions against this property using software model checking.

Definition 7. Let P be a distributed homogeneous track topology aggregation protocol and let P k , Q k be families of formulae over id , v, M id , and τ id .

We write {P } aggr {Q} if and only if for for each k ∈ N 0 and each valuation of id , v, M id which satisfies P k , that valuation extended by

τ id = aggr k (id , v, M id ) satisfies Q k .
Having provided all the prerequisites, we can now state the main theorem of this work, where we reduce protocol correctness to the verification of a local node property. Assuming that all nodes in the network execute the same implementation of the local aggregation function aggr , we claim that if the local computation at a node ensures consistent aggregation up to that node, including the transmission of consistent correction requests, then the protocol is correct. We prove the soundness of this claim inductively.

Theorem 1. Let P be a distributed homogeneous track topology aggregation protocol for the set T of track topologies with domain D.

If {P } aggr {Q} with

P k ≡ id ∈ ID k ∧ v = V (n id )
and

Q k ≡ A (τ id ) = V (n id ) ⊕ τi∈M id ∧((ni,n id )∈PA∨(i∈E (M id )∧(ni,n id )∈SA)) A (τ i ) ∧ E (τ id ) = {i | τ i ∈ M id ∧ (n i , n id ) ∈ PA} ∪ {i | i ∈ E (M id ) ∧ (τ i ∈ M id ∨ (n i , n id ) ∈-→)} then P is correct.
Proof (sketch). We show by double induction on the depth d of topologies and the size of their sink track that the set of messages emitted by the nodes according to the protocol satisfy the following properties:

-( ): For each node n, the emitted message comprises the aggregation of all nodes which n is (transitively) responsible for. -( ): Correction for node n j is initially requested by a node n i if and only if n i is the primary parent and there was no successful communication between the two. -( ): A correction request for node n j emitted by n i implies that no predecessor of n i in the correction relation was able to provide a correction.

Formally, we show

∀ d ∈ N 0 , ∈ N 0 ∀ T = (N, -→, , V) ∈ T • depth(T ) = d ∧ |N 0 | = =⇒ ∀ n i ∈ N • A (τ i ) = n-→ * g ni V (n) ( ) ∧ ∀ j • j ∈ E (τ i ) \ E (M i ) ⇐⇒ (n j , n i ) ∈ PA ∧ f (n j , n i ) = 0 ( ) ∧ ∀ j ∈ E (τ i ) =⇒ ∀ (n , n i ) ∈ * • n j -→ n =⇒ f (n j , n ) = 0. ( )
Then ( ) in particular implies (9), thus P is correct by Lemma 2.

Discussion

The theorem presented allows us to eliminate most sources of infiniteness from the parameterized correctness proof for the studied protocols. Taking advantage of the fact that nodes have only local knowledge of the state of the system and the topology, we are able to implicitly profit from the resulting local symmetry of irregular networks.

The resulting verification problem is one where the system parameter k remains as a variable, and can thus be treated symbolically by verification tools. Alternatively, even a bounded correctness proof (up to some maximum size) can be provided by explicit model checking, provided that the data types used in the implementation are finite.

Developers of aggregation protocols can profit from the inductive proof provided. They can concentrate on verifying their particular implementations against our verification condition; a process that is less involved than providing a complete proof. Some implicit assumptions were taken into account. We considered a single aggregation round, where nodes transmit only once. We thus assume that nodes are memoryless between aggregation rounds. This has, nonetheless, an advantage: systems are allowed to dynamically change their topology between aggregation rounds.

Case Study

We analyze the ridesharing protocol [START_REF] Gobriel | Ridesharing: Fault tolerant aggregation in sensor networks using corrective actions[END_REF][START_REF] Iskander | Privacy and robustness for data aggregation in wireless sensor networks[END_REF], proposed for use in DARPA's satellite cluster system F6 [START_REF] Brown | The value proposition for Fractionated space architectures[END_REF]. Nodes are arranged in tracks and reliability in the presence of failing communication links is improved by coordinating corrective actions between nodes. We concentrate on a variant of the ridesharing protocol with reliable correction links. An initial attempt of the verification of the ridesharing protocol without considering the aggregation function, but the participation vector is presented in [START_REF] Feo-Arenis | Formal verification of a parameterized data aggregation protocol[END_REF], for self-containment, we recall the protocol description here.

The goal of the protocol is to aggregate the readings of sensor arranged in a track graph towards a single, specially designated node called sink. Except from the sink, every node has one assigned parent (the main parent), which is responsible for aggregating its data. Additionally, other nodes in communication range are designated as fail-over aggregators (the backup parents) in case the communication between a node and its main parent fails.

The possible data paths from sensors to the sink form a directed, acyclic graph (DAG) with multiple paths through the track graph (See Fig. 2). Primary and backup edges are between adjacent tracks. There are also side edges within the same track. A side edge points to a node from its side parent. The main edges form a spanning tree with the sink as root.

Main parents transmit correction requests if the communication to their children fails. Those requests are relayed by the track nodes towards the backup parents connected to them using the reliable side links. If a backup parent receives a correction request for a backup child, and the data is available, it aggregates the data and stops propagating the error correction request.

We show the aggregation algorithm as proposed in [START_REF] Iskander | Privacy and robustness for data aggregation in wireless sensor networks[END_REF] (see Algorithm 1). Each node in a given ridesharing topology has a unique identity. Input id gives the identity of the node and PC , BC , SP are the sets of primary children, backup children, and side parents of the node respectively. Input v gives the current sensor reading and rcv the messages received by id . The algorithm computes the message to be sent by id , given v and rcv .

Nodes transmit triples A, P, E with the accumulated sensor value A and two control boolean vectors of length |N |. The participation vector P indicates for each node whether its value is included in A and the error vector E indicates at each position, whether correction is required for the node at that position.

Aggregation starts by initializing A with zero and P and E with all zeroes. If node id has sensor data, it is aggregated to A and P is updated accordingly.

Algorithm 1: The ridesharing aggregation algorithm. [START_REF] Iskander | Privacy and robustness for data aggregation in wireless sensor networks[END_REF] input: id, PC , BC , SP, v, rcv A := 0; P := 0; E := 0; We use rcv [SP ] to denote the bit-wise disjunction of the error vectors received from id 's side parents. Then, E comprises all requests for corrections. In the loop, the received messages from id 's children are processed: if id received the message from c and if c is a primary child or a backup child with a pending request for correction in E then c's data is aggregated, i.e. A is updated and the P vector becomes the disjunction of the incoming P vectors. If id did not receive the message from primary child c, it flags a request for the correction of c and leaves A and P unchanged.

if v = NULL then { A := A + v; P [id] := 1 } ; // Aggregate local sensor reading E := rcv [SP]; foreach c ∈ PC ∪ BC do if rcv [c] = undefined then if c ∈ PA ∨ (c ∈ SA ∧ E[c] = 1)

Verification of the Ridesharing Protocol

We show how the ridesharing protocol fits into the framework presented in Section 2. First, we show that the topologies used are track topologies.

-The set of nodes N = {n 1 , . . . , n k } is the set of nodes present in a ridesharing topology, there is a single sink node in the sink track N 0 = {n k }, -The main parent relation is the primary aggregation relation PA. -The track function can be defined with respect to PA since it forms a spanning tree:

track (n) = 0 iff (n, n ) ∈ PA track (n ) + 1 iff ∃ (n, n ) ∈ PA
each node n i has access to its sensor value v i from the domain D of bounded integers, if the sensor does not have a value, v i = 0 is used. Thus the labeling function is defined as:

V = {n i → v i | 1 ≤ i ≤ k}.
Second, we show that the protocol is distributed homogeneous.

-The domain is the type of the sensor readings, we assume it to be bounded integer numbers: D = {-2 n , . . . , 2 n -1} for some positive integer n.

-The aggregation operator is the sum operator. I.e., ⊕ = +.

-The domain, aggregation operator and neutral element (D, +, 0) form a monoid. Thus the aggregation function

A k (v 1 , . . . , v k ) = v 1 + • • • + v k is monoidal.
-The set of messages is the set of transmissions of the nodes τ i = A i , P i , E i where A i , P i , E i are the values calculated by ridesharing at node i. Thus,

Msg k = D × B k × B k .
-The value decoder function reads the aggregation value directly from a message, i.e., A (τ i ) = A i . The correction requests can also be read directly from the transmitted messages:

E (τ i ) = {j ∈ ID k | E i [j] = 1}.
-The local aggregation function is Algorithm 1. I.e.,

aggr k (i, v, M ) = ridesharing(i, PA(i), SA(i), SP (i), v, M )
where PA(i) = {j ∈ ID k | (j, i) ∈ PA}. SA(i) and SP (i) are defined analogously w.r.t. SA and . M is defined with respect to a communication function as in Def. 4.

We can thus apply the verification theorem to the ridesharing protocol. It is left to verify whether the formula {P } ridesharing(i, PA(i), SA(i), (i), v, M ) {Q} is valid for P and Q as defined in Theorem 1.

To that end, we developed a model including our formalization from Sec. 2 using Boogie [START_REF] Barnett | Boogie: A modular reusable verifier for object-oriented programs[END_REF]. The topology and communication functions are represented by axioms. Additional axioms represent the properties of the system analyzed. The aggregation algorithm is input directly in imperative form by representing boolean arrays as functions of type array : N → B. Instead of bounded integers, we used unbounded integers to simplify the model, thus introducing the assumption that the actual data types used in an implementation are enough to accommodate the aggregation values without overflowing. Simple invariants for the loop in the algorithm were necessary: framing conditions for the loop variables and the fact that consistency is preserved across iterations of the loop was sufficient. P and Q were expressed in terms of the protocol variables and used as pre-and postconditions of the algorithm respectively 1 .

The verification took 1.05 seconds to verify 35 partial verification conditions (including sanity checks), while using approximately 13 MB of memory. Boogie was able to show that the verifications conditions are all valid. We thus have shown correctness of the ridesharing protocol with reliable side links.

Discussion. Due to the symbolic representation of the parametric set of nodes, the theorem prover used by Boogie requires only a finite number of cases to show the validity of the generated verification conditions fully automatically. recall all assumptions

1 Model available at http://www.informatik.uni-freiburg.de/ ~arenis/forte13/ Thanks to the result that the ridesharing protocol is correct, in the sense of Definition 3, a reliability measure can be simply computed from the failure probability of the inter-track radio links as follows:

Let p(n i , n j ) be the probability of node n j successfully receiving the transmission of a connected node n i . The probability of the data of some node n being successfully aggregated is then equal to the probability of all links in each possible aggregation path failing:

1 - π∈paths(n)   1 - 1≤j<|π| p (π[j], π[j + 1])  
where paths(n) are the sequences π = n 1 , . . . , n m of nodes starting at node n, connected by the aggregation relation and ending in the sink node. The length |π| = m. The expression π[i] refers to the i-th node on the path π.

If all links have the same success probability p, then the probability of a node n in track t successfully being aggregated at the sink simplifies to

1 -1 -p track (n) |paths(n)|
assuming that link failures are independent.

These results thus reduce the need to use simulation tools to determine the overall reliability of the ridesharing protocol.

Related Work

The parameterized analysis of safety properties is undecidable in the general case [START_REF] Apt | Limits for automatic verification of finite-state concurrent systems[END_REF]. The problem of verifying properties for parameterized systems has been approached by several authors. We discuss a few that we feel are the closest to our line of work.

We can best situate our work in the line of work of Namjoshi et al. [START_REF] Namjoshi | Uncovering symmetries in irregular process networks[END_REF] for the verification of irregular networks. Although we concentrate on asynchronous systems, the verification condition presented in this work can be viewed as a particular case of an inductive, compositional invariant, though used in the context of irregular networks with dynamic links. We ensure the local symmetry of aggregation networks with redundancy by explicitly considering three types of edges and restricting the analysis to systems where inter-node communication occurs after computation, without interleaving. We enrich the computation model by explicitly including the network dynamic as part of the system state.

The particular problem of network dynamic in the form of link and node failures has been the subject of recent efforts [START_REF] Delzanno | Verification of ad hoc networks with node and communication failures[END_REF]. We present an instance of verification of broadcast networks with link unreliability, which can simulate node failures, for the special case of aggregation protocols.

The method of "network grammars" [START_REF] Clarke | Verifying parameterized networks[END_REF], where regular families of networks are described using context-free grammars is used to verify parameterized systems by using abstraction. Several model checking problems are derived, which, if solved, deliver a proof of correctness. We do not explicitly perform any kind of abstraction on the states of the local aggregation programs, leaving that possibility open for the method used to establish the satisfaction of our verification condition.

Similar methods rely on finding so called network invariants [START_REF] Kesten | Network invariants in action[END_REF][START_REF] Pnueli | Automatic deductive verification with invisible invariants[END_REF], overapproximations of the sets of reachable states of the systems, and proving that they imply the property being verified. The focus lies on automatically finding those invariants through model checking. We distance ourselves from the automatic finding of invariants and perform explicit induction using a fixed invariant, delivering a proof rule for the class of aggregation protocols with irregular topology. Explicit induction has been also used for the verification of regular networks [START_REF] Emerson | On reasoning about rings[END_REF].

The systems we consider in this work are asynchronous systems where computation steps of network components are considered atomic. The systems could be, however, considered as an instance of bounded-data parameterized systems in the sense of [START_REF] Pnueli | Automatic deductive verification with invisible invariants[END_REF].

This work is a follow-up of the initial analysis of the protocol from our case study [START_REF] Feo-Arenis | Formal verification of a parameterized data aggregation protocol[END_REF]. We improve the analysis by extending it to the use of arbitrary duplicate-sensitive aggregation functions, eliminating the need for the explicit transmission of a vector of aggregated nodes. Here, we provide a complete, formal inductive proof and, as a result, simplify the resulting verification conditions. The software model checking step of the verification is thus simplified, improving the chances of obtaining a verification problem within the capabilities of current software verification tools.

Conclusions

We have presented an inductive, parameterized proof of correctness for track topology aggregation protocols. We reduce the problem to the verification of a single verification consistency condition on the nodes' aggregation algorithm, which can be automatically checked using state of the art software verification tools.

We identify a class of aggregation protocols that allows us to illustrate the feasibility of reducing the verification of parameterized, asynchronous systems with irregular topologies and dynamic link (and thus node) reliability to establishing local consistency properties.

Possible directions for future work are the relaxation of the constraints for the systems verified -to enlarge the class of systems covered-, such as the reliability of the correction infrastructure and the acyclicity of some of the node connection relations.

Additionally, the use of our verification conditions as a template for the automatic generation of inductive node invariants can be explored, such that given decoding functions for a protocol messages, the verification task is further automated.

Finally, criteria for the decidability of the resulting verification problem can be studied. This would lead to the identification of a decidable class of parameterized systems.

Fig. 1 .

 1 Fig. 1. Track Topology

Definition 1 .

 1 A track topology T = (N, -→, , V) with domain D is a finite, node-labeled, acyclic graph with nodes N = {n 1 , . . . , n k }, edges -→ ∪ ⊆ N × N , and labeling function V : N → D which satisfies the following conditions: -The set of nodes is partitioned into d ∈ N 0 non-empty sets N 0 , . . . , N d called tracks. We call N 0 the sink track and use track (n) to denote the number of the track to which node n ∈ N belongs. The number d is called the depth of the topology, denoted by depth(T ). -The relation -→ is called aggregation relation and connects nodes in a track with nodes in the track immediately before, i.e.,

Definition 2 .

 2 A communication function of a track topology T = (N, -→, , V) is an edge labeling f : (-→) → B of the aggregation relation -→ of T where f (n, n ) = 1 if and only if the communication was successful between the connected nodes n and n . We use F T to denote the set of communication functions of T , and n -→ f n if and only if

Fig. 2 .

 2 Fig. 2. Ridesharing topology

  then // Aggregate received values (Ac, Pc) := rcv [c]; A := A + Ac; P := P | Pc; E[c] := 0; end else if c ∈ PC then // Request error correction E[c] := 1; end end return (A, P, E);

  It connects nodes between adjacent tracks and forms a tree with n k as root. -The backup parent relation is the secondary aggregation relation SA. It forms an acyclic directed graph (N, SA). -The side parent relation is the correction relation . It connects nodes sequentially.


Tevfik Bultan
email: bultan@cs.ucsb.edu

Analyzing Interactions of Asynchronously Communicating Software Components (Invited Paper)

Since software systems are becoming increasingly more concurrent and distributed, modeling and analysis of interactions among their components is a crucial problem. In several application domains, message-based communication is used as the interaction mechanism, and the communication contract among the components of the system is specified semantically as a state machine. In the service-oriented computing domain this type of message-based communication contracts are called "choreography" specifications. A choreography specification identifies allowable ordering of message exchanges in a distributed system. A fundamental question about a choreography specification is determining its realizability, i.e., given a choreography specification, is it possible to build a distributed system that communicates exactly as the choreography specifies? In this short paper we give an overview of this problem, summarize some of the recent results and discuss its application to web service choreographies, Singularity OS channel contracts, and UML collaboration (communication) diagrams.

Introduction

Nowadays, many software systems consist of multiple components that execute concurrently on different machines that are physically distributed, and interact with each other through computer networks. Moreover, new trends in computing, such as service-oriented architecture, cloud computing, multi-core hardware, wearable computing, all point to even more concurrency and distribution among the components of software systems in the future. Concurrent and distributed software systems are increasingly used in every aspect of society and in some cases provide safety critical services. Hence, it is very important to develop techniques that guarantee that these software systems behave according to their specifications.

A crucial problem in dependability of concurrent and distributed software systems is the coordination of different components that form the whole system. In order to complete a task, components of a software system have to coordinate their executions by interacting with each other. One fundamental question is, what should be the interaction mechanism given the trend for increased level of concurrency and distribution in computing? One emerging paradigm is messagebased communication [START_REF] Banavar | A Case for Message Oriented Middleware[END_REF][START_REF] Carbone | A Theoretical Basis of Communication-Centred Concurrent Programming[END_REF][START_REF] Menascé | Mom vs. rpc: Communication models for distributed applications[END_REF][START_REF] Fähndrich | Language support for fast and reliable message-based communication in singularity os[END_REF], where components interact with each other by sending and receiving messages. Given these trends, we conclude that analyzing message-based interactions among software components is a timely and significant research problem.

Specification of Message-Based Interactions

Specification and analysis of message-based interactions has been an active research area studied in several application domains including coordination in service-oriented computing [START_REF] Carbone | A Theoretical Basis of Communication-Centred Concurrent Programming[END_REF][START_REF]Web Service Choreography Description Language (WS-CDL[END_REF], interactions in distributed programs [START_REF] Armstrong | Getting Erlang to Talk to the Outside World[END_REF] and process isolation at the OS level [START_REF] Fähndrich | Language support for fast and reliable message-based communication in singularity os[END_REF].

Service oriented computing provides technologies that enable multiple organizations to integrate their businesses over the Internet. Typical execution behavior in this type of distributed systems involves a set of autonomous peers interacting with each other through messages. Modeling and analysis of interactions among the peers is a crucial problem in this domain due to following reasons: 1) Organizations may not want to share the internal details of the services they provide to other organizations. In order to achieve decoupling among different peers, it is necessary to specify the interactions among different services without referring to the details of their local implementations. 2) Modeling and analyzing the global behavior of this type of distributed systems is particularly challenging since no single party has access to the internal states of all the participating peers. Desired behaviors have to be specified as constraints on the interactions among different peers since the interactions are the only observable global behavior. Moreover, for this type of distributed systems, it might be worthwhile to specify the interactions among different peers before the services are implemented. Such a top-down design strategy may help different organizations to better coordinate their development efforts.

Choreography languages enable specification of such interactions. A choreography specification corresponds to a global ordering of the message exchange events among the peers participating to a composite service, i.e., a choreography specification identifies the set of allowable message sequences for a composite web service.

Choreography Analysis

Specification of interactions in a software system as a choreography leads to several interesting research problems [START_REF] Bultan | Analyzing conversations: Realizability, synchronizability, and verification[END_REF]:

-Realizability: Given a choreography specification, determining if there exists a set of components that generate precisely the set of message sequences specified by the choreography specification.

-Synthesis: Given a choreography specification, synthesizing a set of components that generate precisely the set of message sequences specified by the choreography specification. -Conformance: Determining if a set of given components adhere to a given choreography specification. -Synchronizability: Determining if the set of interactions generated by a given set of components remain the same under asynchronous and synchronous communication.

Some formalizations of these questions lead to unsolvable problems. For example, choreography conformance problem is undecidable when asynchronous communication is used. This is because, systems where peers communicate asynchronously with unbounded FIFO message queues can simulate Turing Machines [START_REF] Brand | On communicating finite-state machines[END_REF].

It is important to note that the choreography analysis problem is not isolated to the area of service-oriented computing. It is a fundamental problem that appears in any area where message-based communication is used to coordinate interactions of multiple concurrent or distributed components. For example, recently, earlier results on choreography analysis have been applied to analysis of Singularity channel contracts [START_REF] Stengel | Analyzing Singularity Channel Contracts[END_REF]. Singularity is an experimental operating system developed by Microsoft Research in order to improve the dependability of software systems [START_REF] Hunt | Singularity: rethinking the software stack[END_REF]. In the Singularity operating system all inter-process communication is done via messages sent through asynchronous communication channels. Each channel is governed by a channel contract [START_REF] Fähndrich | Language support for fast and reliable message-based communication in singularity os[END_REF]. A channel contract is basically a state machine that specifies the allowable ordering of messages between the client and the server. Hence, channel contracts serve the same purpose that choreography specifications serve in service oriented computing.

Recent Results

There has been some recent progress in addressing these research problems. It has been shown that synchronizability checking is decidable [START_REF] Basu | Choreography Conformance via Synchronizability[END_REF]. It can be solved by comparing the behavior of a system with synchronous communication to the behavior of the same system with bounded asynchronous communication where the queue sizes are limited to one. This result also leads to effective approaches to choreography conformance checking. Although choreography conformance problem is undecidable in general, synchronizability analysis identifies a class of systems for which choreography conformance can be checked using synchronous communication instead of asynchronous communication. This means that message queues can be removed during the conformance analysis, significantly reducing the state space of the analyzed system.

More recently, it has been shown that choreography realizability problem is decidable for systems communicating with asynchronous messages using unbounded FIFO message queues [START_REF] Basu | Deciding Choreography Realizability[END_REF]. This also means that for realizable choreography specifications, synthesis problem can be solved by projecting the given choreography specification to each component that participates to the choreography.