More Web Proxy on the site http://driver.im/

Article

Formal verification of consensus algorithms tolerating malicious faults

Authors:

Bernadette Charron-Bost,

Stephan MerzAuthors Info & Claims

SSS'11: Proceedings of the 13th international conference on Stabilization, safety, and security of distributed systems

Pages 120 - 134

Published: 10 October 2011 Publication History

Abstract

Consensus is the paradigmatic problem in fault-tolerant distributed computing: it requires network nodes that communicate by message passing to agree on 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.

References

[1]

Bar-noy, A., Dolev, D., Dwork, C., Strong, H.R.: Shifting gears: Changing algorithms on the fly to expedite Byzantine agreement. In: Information and Computation, pp. 42-51 (1987).

Digital Library

[2]

Biely, M., Widder, J., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A.: Tolerating corrupted communication. In: Proc. 26th Annual ACM Symposium on Principles of Distributed Computing, PODC 2007, pp. 244-253. ACM, New York (2007).

Digital Library

[3]

Chaouch-Saad, M., Charron-Bost, B., Merz, S.: A reduction theorem for the verification of round-based distributed algorithms. In: Bournez, O., Potapov, I. (eds.) RP 2009. LNCS, vol. 5797, pp. 93-106. Springer, Heidelberg (2009).

Digital Library

[4]

Charron-Bost, B., Merz, S.: Formal verification of a Consensus algorithm in the Heard-Of model. Int. J. Software and Informatics 3(2-3), 273-303 (2009).

[5]

Charron-Bost, B., Schiper, A.: The Heard-Of model: Computing in distributed systems with benign failures. In: Distributed Computing (2009).

[6]

Dwork, C., Lynch, N.A., Stockmeyer, L.: Consensus in the presence of partial synchrony. J. ACM 35(2), 288-323 (1988).

Digital Library

[7]

Elrad, T., Francez, N.: Decomposition of distributed programs into communicationclosed layers. Science Comp. Prog. 2(3) (April 1982).

[8]

Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM 32(2), 374-382 (1985).

Digital Library

[9]

Georgiou, C., Lynch, N.A., Mavrommatis, P., Tauber, J.A.: Automated implementation of complex distributed algorithms specified in the IOA language. Intl. J. Software Tools for Technology Transfer 11(2), 153-171 (2009).

Digital Library

[10]

Hesselink, W.H.: The verified incremental design of a distributed spanning tree algorithm: Extended abstract. Formal Asp. Comput. 11(1), 45-55 (1999).

[11]

Jaskelioff, M., Merz, S.: Proving the correctness of Disk Paxos. Archive of Formal Proofs (2005), http://afp.sourceforge.net/entries/DiskPaxos.shtml

[12]

Lamport, L.: What good is temporal logic? In: Mason, R.E.A. (ed.) Information Processing 1983: Proceedings of the IFIP 9th World Congress, Paris. IFIP, pp. 657-668. North-Holland, Amsterdam (September 1983).

[13]

Lamport, L.: Byzantining Paxos by refinement. Technical report, Microsoft Research (December 2010).

[14]

Lamport, L., Merz, S.: Specifying and verifying fault-tolerant systems. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 41-76. Springer, Heidelberg (1994).

Digital Library

[15]

Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996).

Digital Library

[16]

Nipkow, T., Paulson, L., Wenzel, M.: Isabelle/HOL. A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002).

Digital Library

[17]

Peled, D., Wilke, T.: Stutter-invariant temporal properties are expressible without the next-time operator. Inf. Proc. Letters 63(5), 243-246 (1997).

Digital Library

[18]

Schmid, U., Weiss, B., Rushby, J.M.: Formally verified byzantine agreement in presence of link faults. In: 22nd Intl. Conf. Distributed Computing Systems (ICDCS 2002), Vienna, Austria, pp. 608-616. IEEE Comp. Society, Los Alamitos (2002).

Digital Library

[19]

Tsuchiya, T., Schiper, A.: Model checking of consensus algorithms. In: 26th IEEE Symp. Reliable Distributed Systems (SRDS 2007), Beijing, China, pp. 137-148. IEEE Comp. Society, Los Alamitos (2007).

Digital Library

[20]

Tsuchiya, T., Schiper, A.: Using bounded model checking to verify consensus algorithms. In: Taubenfeld, G. (ed.) DISC 2008. LNCS, vol. 5218, pp. 466-480. Springer, Heidelberg (2008).

Digital Library

Cited By

Drăgoi CHenzinger TZufferey D(2016)PSync: a partially synchronous language for fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/2914770.283765051:1(400-415)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837650
Drăgoi CHenzinger TZufferey DBodik RMajumdar R(2016)PSync: a partially synchronous language for fault-tolerant distributed algorithmsProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837650(400-415)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837650
Bérard BLafourcade PMillet LPotop-Butucaru MThierry-Mieg YTixeuil S(2016)Formal verification of mobile robot protocolsDistributed Computing10.1007/s00446-016-0271-129:6(459-487)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1007/s00446-016-0271-1
Show More Cited By

Formal verification of consensus algorithms tolerating malicious faults
1. Software and its engineering
  1. Software creation and management
    1. Software verification and validation
2. Theory of computation

Recommendations

Automatically Tolerating Arbitrary Faults in Non-malicious Settings
LADC '13: Proceedings of the 2013 Sixth Latin-American Symposium on Dependable Computing

Arbitrary faults such as bit flips have been often observed in commodity-hardware data centers and have disrupted large services. Benign faults, such as crashes and message omissions, are nevertheless the standard assumption in practical fault-tolerant ...
Formal development of mechanisms for tolerating transient faults
Rigorous Development of Complex Fault-Tolerant Systems

Transient faults belong to a wide-spread class of faults typical for control systems. These are the faults that only appear for a short period of time and might reappear later. However, even by appearing for a short time, they might cause dangerous ...
Formal Verification of Algorithms for Critical Systems

The authors describe their experience with formal, machine-checked verification of algorithms for critical applications, concentrating on a Byzantine fault-tolerant algorithm for synchronizing the clocks in the replicated computers of a digital flight ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SSS'11: Proceedings of the 13th international conference on Stabilization, safety, and security of distributed systems

October 2011

450 pages

ISBN:9783642245497

Editors:
Xavier Défago
Japan Advanced Institute of Science and Technology, School of Information Science, Ishikawa, Japan
,
Franck Petit
LIP6/INRIA/UPMC Sorbonne Universities, Paris, France
,
Vincent Villain
MIS, University of Picardie Jules Verne, Amiens, France

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 10 October 2011

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

5
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 26 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Drăgoi CHenzinger TZufferey D(2016)PSync: a partially synchronous language for fault-tolerant distributed algorithmsACM SIGPLAN Notices10.1145/2914770.283765051:1(400-415)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2914770.2837650
Drăgoi CHenzinger TZufferey DBodik RMajumdar R(2016)PSync: a partially synchronous language for fault-tolerant distributed algorithmsProceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages10.1145/2837614.2837650(400-415)Online publication date: 11-Jan-2016
https://dl.acm.org/doi/10.1145/2837614.2837650
Bérard BLafourcade PMillet LPotop-Butucaru MThierry-Mieg YTixeuil S(2016)Formal verification of mobile robot protocolsDistributed Computing10.1007/s00446-016-0271-129:6(459-487)Online publication date: 1-Nov-2016
https://dl.acm.org/doi/10.1007/s00446-016-0271-1
Gmeiner AKonnov ISchmid UVeith HWidder J(2014)Tutorial on Parameterized Model Checking of Fault-Tolerant Distributed AlgorithmsAdvanced Lectures of the 14th International School on Formal Methods for Executable Software Models - Volume 848310.1007/978-3-319-07317-0_4(122-171)Online publication date: 16-Jun-2014
https://dl.acm.org/doi/10.1007/978-3-319-07317-0_4
Küfner PNestmann URickmann C(2012)Formal verification of distributed algorithmsProceedings of the 7th IFIP TC 1/WG 202 international conference on Theoretical Computer Science10.1007/978-3-642-33475-7_15(209-224)Online publication date: 26-Sep-2012
https://dl.acm.org/doi/10.1007/978-3-642-33475-7_15

View Options

View options

Media

Figures

Other

Tables

View Table of Contents