Formal Verification of Consensus Algorithms Tolerating Malicious Faults - Inria - Institut national de recherche en sciences et technologies du numérique Access content directly
Conference Papers Year : 2011

Formal Verification of Consensus Algorithms Tolerating Malicious Faults

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.
Fichier principal
Vignette du fichier
main.pdf (335.4 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00639048 , version 1 (08-11-2011)

Identifiers

Cite

Bernadette Charron-Bost, Henri Debrat, Stephan Merz. Formal Verification of Consensus Algorithms Tolerating Malicious Faults. 13th International Symposium on Stabilization, Safety, and Security of Distributed Systems (SSS 2011), Oct 2011, Grenoble, France. pp.120-134, ⟨10.1007/978-3-642-24550-3_11⟩. ⟨hal-00639048⟩
391 View
607 Download

Altmetric

Share

Gmail Facebook X LinkedIn More