Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

Compositional Verification of Byzantine Consensus

Abstract : Until now, computer-aided proofs of the liveness of byzantine consensus algorithms assumed synchrony to reason in lock steps or the error-prone manual intervention of experts in the proof checker, but could not be automated through model checking. We propose a compositional approach to verify a consensus algorithm, for any number n of processes and any upper bound t < n/3 on the number of byzantine processes. To this end, we identify a fairness property that makes this---otherwise purely asynchronous---byzantine consensus algorithm amenable to model checking. We decompose the algorithm in two parts: an inner broadcast algorithm and an outer decision algorithm. We encode these algorithms using threshold automata, and we formalize their properties in temporal logic. This allows us to automatically check the inner broadcasting algorithm, assuming fairness. For the verification of the outer algorithm, we simplify the automaton of the inner algorithm by relying on its checked properties. We verify in less than 70 seconds, not only the safety of byzantine consensus but also its liveness.
Complete list of metadata

https://hal.archives-ouvertes.fr/hal-03158911
Contributor : Vincent Gramoli Connect in order to contact the contributor
Submitted on : Thursday, March 4, 2021 - 10:59:07 AM
Last modification on : Wednesday, November 3, 2021 - 3:53:03 AM
Long-term archiving on: : Saturday, June 5, 2021 - 6:36:46 PM

File

paper.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-03158911, version 1

Citation

Nathalie Bertrand, Vincent Gramoli, Igor Konnov, Marijana Lazic, Pierre Tholoniat, et al.. Compositional Verification of Byzantine Consensus. 2021. ⟨hal-03158911⟩

Share

Metrics

Record views

190

Files downloads

225