Formal Verification of Consensus Algorithms Tolerating Malicious Faults

Bernadette Charron-Bost 1 Henri Debrat 2 Stephan Merz 2, *
* Auteur correspondant
2 VERIDIS - VERIfication pour les systèmes DIStribués
Inria Nancy - Grand Est, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications : UMR7503
Abstract : Consensus is the paradigmatic problem in fault-tolerant distributed computing: it requires network nodes that communicate by message passing to agree on a common value even in the presence of (benign or malicious) faults. Several algorithms for solving Consensus exist, but few of them have been rigorously verified, much less so formally. The Heard-Of model proposes a simple, unifying framework for defining distributed algorithms in the presence of communication faults. Algorithms proceed in communication-closed rounds, and assumptions on the faults tolerated by the algorithm are stated abstractly in the form of communication predicates. Extending previous work on the case of benign faults, our approach relies on the fact that properties such as Consensus can be verified over a coarse-grained, round-based representation of executions. We have encoded the Heard-Of model in the interactive proof assistant Isabelle/HOL and have used this encoding to formally verify three Consensus algorithms based on synchronous and asynchronous assumptions. Our proofs give some new insights into the correctness of the algorithms, in particular with respect to transient faults.
Type de document :
Communication dans un congrès
Xavier Défago and Franck Petit and Vincent Villain. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. Springer, 6976, pp.120-134, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-24550-3_11〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00639048
Contributeur : Stephan Merz <>
Soumis le : mardi 8 novembre 2011 - 09:40:53
Dernière modification le : mercredi 20 février 2019 - 01:15:09
Document(s) archivé(s) le : dimanche 4 décembre 2016 - 11:20:58

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Bernadette Charron-Bost, Henri Debrat, Stephan Merz. Formal Verification of Consensus Algorithms Tolerating Malicious Faults. Xavier Défago and Franck Petit and Vincent Villain. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. Springer, 6976, pp.120-134, 2011, Lecture Notes in Computer Science. 〈10.1007/978-3-642-24550-3_11〉. 〈hal-00639048〉

Partager

Métriques

Consultations de la notice

575

Téléchargements de fichiers

267