Section: New Results

Modeling and verifying the Pastry routing protocol

Participants : Tianxiang Lu, Stephan Merz.

As a significant case study for the techniques that we are developing within VeriDis, we are modeling and verifying the routing protocol of the Pastry algorithm [25] for maintaining a distributed hash table in a peer-to-peer network. As part of his PhD work (under the joint supervision of Stephan Merz and Christoph Weidenbach from MPI-INF Saarbrücken), Tianxiang Lu has developed a TLA⁺ model of the Pastry routing protocol, which has uncovered several issues in the existing presentations of the protocol in the literature, and in particular a loophole in the join protocol that had been fixed by the algorithm designers in a technical report that appeared after the publication of the original protocol.

In 2011, we have worked towards a correctness proof of the routing protocol. We have in particular identified a number of candidate invariants that have been validated by extensive model checking over finite instances and for which we have formally proved that their validity would imply the correctness of the protocol. Our proofs are carried out in TLAPS (section 5.2 ) and represent a sizable case study for the different proof tools of the proof system. Our results have been presented at FORTE 2011 [12] .