Formal Verification of the Pastry Protocol

Le protocole Pastry realise une table de hachage distribue sur un reseau pair a pair organise en un anneau virtuel de noeuds. Alors qu'il existe plusieurs implementations de Pastry, il n'y a pas encore eu de travaux pour decrire formellement l'algorithme ou verifier son bon fonctionnement. Integrant des structures de donnees complexes et de la communication asynchrone entre des noeuds qui peuvent rejoindre ou quitter le reseau, ce protocole represente un interet certain pour la verification formelle. La these se focalise sur le protocole Join de Pastry qui permet a un noeud de rejoindre le reseau. Les noeuds ayant integre le reseau doivent avoir une vue du voisinage coherente entre eux. La propriete principale de correction, appelee CorrectDelivery, assure qu'a tout moment il y a au plus un noeud capable de repondre a une requete pour une cle, et que ce noeud est le noeud le plus proche numeriquement a ladite cle. Il n'est pas trivial de maintenir cette propriete en presence de churn. Ce travail nous a permis de decouvrir des violations inattendues de la propriete dans les versions publiees de l'algorithme. Sur la base de cette analyse, le protocole IdealPastry est concu et verifie en utilisant l'assistant interactif a la preuve TLAPS pour TLA+. Le protocole LuPastry est obtenu en assouplissant certaines hypotheses de IdealPastry. Il est montre formellement que LuPastry verifie CorrectDelivery sous l'hypothese qu'aucun noeud ne quitte le reseau. Cette hypothese ne peut etre relâchee a cause du risque de perte de connexion du reseau dans le cas ou plusieurs noeuds quittent le reseau en meme temps