Formal Verification of Consensus Algorithms Tolerating Malicious Faults

Bernadette Charron-Bost 1 Henri Debrat 2 Stephan Merz 2, 3, *
* Auteur correspondant
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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 25 avril 2018 - 10:45:20
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

479

Téléchargements de fichiers

205