Specifying and Verifying the Kademlia Protocol in Maude

Kademlia is a peer-to-peer distributed hash table (DHT) currently used in the P2P eDonkey file sharing network. Kademlia offers a number of desirable features that result from the use of a notion of distance between objects based on the bitwise exclusive (XOR) of the n-bit quantities that represent both nodes and files. Nodes keep information about files close or near to them in the key space in their routing tables. The search algorithm is based on looking for the closest node (or almost closest node, if the information is replicated) to the file key. The structure of the routing tables defined in each peer guarantees that the lookup algorithm takes no longer than log n steps.

Members

Papers

• I. Pita. A formal specification of the Kademlia distributed hash table. In V. M. Gulías, J. Silva, and A. Villanueva, editors, Proceedings of the 10 Spanish Workshop on Programming Languages, PROLE 2010, pages 223-234. Ibergarceta Publicaciones, 2010. Informal publication.

  Abstract:

  This paper explains the specification of the behaviour of a P2P network that uses the Kademlia DHT in the formal specification language Maude. We use the initial description of the Kademlia DHT and fill some open issues with the eMule real implementation. We allow peers to connect to the network and leave it by simulating time using the Real Time Maude facilities.

• I. Pita, and A. Riesco, Specifying and Analyzing the Kademlia Protocol in Maude.. 9th International Workshop on Rewriting Logic and its Applications, WRLA 2012.

  Abstract:

  We present the distributed specification of the behavior of a P2P network that uses the Kademlia DHT in the formal specification language Maude. We use sockets to connect different Maude instances and create a P2P network where the Kademlia protocol may be used. This protocol is executed on top of a previously developed routing protocol that provides real-time by connecting Maude to an external Java server and allows peers to enter and leave the network dynamically. Then, we show how to represent this distributed system in one single term in order to simulate and analyze the system using the Real-Time Maude facilities.

• I. Pita and M.I. Fernández Camacho. Formal Specification of the Kademlia and the Kad Routing Tables in Maude. WADT 2012.Submitted for acceptance.

  Abstract:

  This paper presents the specification of both the Kademlia and the Kad routing tables, using the specification language Maude. As far as we know, this is the first such a formal development. Using our two formal specifications, we can isolate some of those differences and detect some open issues on the original description, mainly related with message passing. In this context, our main contribution is the integration of the dynamic aspects of the routing table with the full protocol specification.

Download

• The source files of the Java server in charge of the time are available here. The main class of this package is MultiClientTimer. It must be started before launching the Maude processes.
• The Maude files specifying the distributed protocol are available here. All the files are introduced in Maude by loading kademlia.prj.
• The centralized specification of the system is available here. All the files are introduced in Maude by loading centralized-kademlia.prj.
• The Maude file for the Kademlia routing table is available here. The file is introduced in Maude by loading the file kademliaRT.maude.
• The Maude file for the Kad routing table are available here. The file is introduced in Maude by loading the file kadRT.maude.

Examples

• Distributed configuration. To use the distributed protocol the erew command must be used. It must receive a configuration containing a location, an EIGRP router, and a peer. We provide here 6 erew commands, that must be executed in different Maude instances in any order. These commands assume that they are located in the same folder as the distributed configuration and thus they can load the appropriate modules and start the external rewrites. Note that tracing options are activated to show when the Kademlia rules are applied. Files: erew1, erew2, erew3, erew4, erew5, and erew6.
• Centralized configuration. Sample files for executing the centralized specification are available in KademliaTest.maude. This files provides different centralized specifications, where the architecture has been abstracted and sockets connecting all the peers are included. We can use these initial terms to check the properties given in the module MODEL-CHECK-KAD.
• Kad routing table configuration of 26 contacts: KadRT26