Towards Verification of the Pastry Protocol using TLA+

• Main Authors: Merz, Stephan, Lu, Tianxiang, Weidenbach, Christoph
• Other Authors: VERIfication pour les systèmes DIStribués (VERIDIS), Inria Nancy - Grand Est, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS)-Université de Lorraine (UL)-Centre National de la Recherche Scientifique (CNRS), Microsoft Research - Inria Joint Centre (MSR - INRIA), Institut National de Recherche en Informatique et en Automatique (Inria)-Microsoft Research Laboratory Cambridge-Microsoft Corporation Redmond, Wash., Max-Planck-Institut für Informatik (MPII), Max-Planck-Gesellschaft, R. Bruni and J. Dingel
• Format: Conference Object
• Language: English
• Published: HAL CCSD 2011
• Subjects: network protocols; verification methods; model checking; formal specification; ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.2: Correctness proofs; ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification/D.2.4.3: Formal methods; ACM: C.: Computer Systems Organization/C.2: COMPUTER-COMMUNICATION NETWORKS/C.2.4: Distributed Systems; [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; Iceland
• Online Access: https://inria.hal.science/inria-00593523

International audience Pastry is an algorithm that provides a scalable distributed hash table over an underlying P2P network. Several implementations of Pastry are available and have been applied in practice, but no attempt has so far been made to formally describe the algorithm or to verify its properties. Since Pastry combines rather complex data structures, asynchronous communication, concurrency, resilience to churn and fault tolerance, it makes an interesting target for verification. We have modeled Pastry's core routing algorithms and communication protocol in the specification language TLA+. In order to validate the model and to search for bugs we employed the TLA+ model checker TLC to analyze several qualitative properties. We obtained non-trivial insights in the behavior of Pastry through the model checking analysis. Furthermore, we started to verify Pastry using the very same model and the interactive theorem prover TLAPS for TLA+. A first result is the reduction of global Pastry correctness properties to invariants of the underlying data structures.