Epistemic model checking of distributed commit protocols with byzantine faults
Pages 51 - 60
Abstract
The notion of knowledge-based program introduced by Halpern and Fagin provides a useful formalism for designing, analysing, and optimising distributed systems. This paper formulates the two phase commit protocol as a knowledge-based program and then an iterative process of model checking and counter-example guided refinement is followed to find concrete implementations of the program for the case of perfect recall semantics in the Byzantine failures context with synchronous reliable communication. We model several different kinds of Byzantine failures and verify different strategies to fight and mitigate them. We address a number of questions that have not been considered in the prior literature, viz., under what circumstances a sender can know that its transmission has been successful, and under what circumstances an agent can know that the coordinator is cheating, and find concrete answers to these questions. The paper describes also a methodology based on temporal-epistemic model checking technology that can be followed to verify the shortest and longest execution time of a distributed protocol and the scenarios that lead to them.
References
[1]
O. Al-Bataineh. Model checking of knowledge in unconditionally secure cryptographic protocols. Master's thesis, School of Computer Science and Engineering, University of New South Wales, 2011.
[2]
O. Al-Bataineh and R. van der Meyden. Epistemic model checking for knowledge-based program implementation: an application to anonymous broadcast. In SecureComm'10, 2010.
[3]
M. Atif. Analysis and verification of two-phase commit and three-phase commit protocols. In Emerging Technologies ICET'09, pages 326--331, 2009.
[4]
K. Baukus and R. van der Meyden. A knowledge based analysis of cache coherence. In 6th Int. Conf. on Formal Engineering Methods, volume 3308 of LNCS, pages 99--114. Springer, 2004.
[5]
A. P. Bernstein, V. Hadzilacos, and N. Goodman. Concurrency control and recovery in database systems. Addison-Wesley, 1987.
[6]
C. Dwork and Y. Moses. Knowledge and common knowledge in a Byzantine environment: crash failures. Information and Computation, 88(2):156--186, 1990.
[7]
R. Fagin, J. Y. Halpern, Y. Moses, and M. Y. Vardi. Reasoning about Knowledge. MIT Press, Cambridge, Mass., 1995.
[8]
P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In Proc. 16th Int. Conf. on computer aided verification (CAV'04), pages 479--483. Springer-Verlag, 2004.
[9]
V. Hadzilacos. A knowledge-theoretic analysis of atomic commitment protocols. PODS '87, pages 129--134. ACM, 1987.
[10]
J. Y. Halpern and L. D. Zuck. A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols. J. ACM, 39(3):449--478, 1992.
[11]
X. Huang and R. van der Meyden. Symbolic synthesis for epistemic specifications with observational semantics. In Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, pages 455--469, 2014.
[12]
W. Janssen and J. Zwiers. Protocol design by layered decomposition. In Proc. FTRTFTS 2nd International Symposium, pages 307--326. LNCS, 1992.
[13]
R. Kurki-Suonio. Towards programming with knowledge expressions. In POPL '86, pages 140--149, New York, NY, USA, 1986. ACM.
[14]
M. Mazer and F. Lochovsky. Analyzing distributed commitment by reasoning about knowledge. Technical report, CRL 90/10, DEC-CRL, 1990.
[15]
Ölveczky Peter Csaba. Formal Modeling and Analysis of a Distributed Database Protocol in Maude. In Proceedings of the 2008 11th IEEE International Conference on Computational Science and Engineering - Workshops, pages 37--44, 2008.
[16]
R. van der Meyden. Finite state implementations of knowledge-based programs. In Proceedings of the 16th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 262--273, London, UK, 1996. Springer-Verlag.
[17]
A. C. Yao. Protocols for secure computations. In Proceedings of the 23rd Annual Symposium on Foundations of Computer Science, SFCS '82, pages 160--164, Washington, DC, USA, 1982. IEEE Computer Society.
Recommendations
Model checking epistemic-probabilistic logic using probabilistic interpreted systems
Model checking is a formal technique widely used to verify security and communication protocols in epistemic multi-agent systems against given properties. Qualitative properties such as safety and liveliness have been widely analyzed in the literature. ...
Abstraction for epistemic model checking of dining cryptographers-based protocols
TARK XIII: Proceedings of the 13th Conference on Theoretical Aspects of Rationality and KnowledgeThe paper describes an abstraction for protocols that are based on multiple rounds of Chaum's Dining Cryptographers protocol. It is proved that the abstraction preserves a rich class of specifications in the logic of knowledge. This result is applied to ...
Checking a Non-Byzantine FT Scheme against Byzantine Faults
IPDPS '02: Proceedings of the 16th International Parallel and Distributed Processing SymposiumProcess duplication for several application processes in combination with appropriate protocols provides byzantine fault tolerance. In contrast, lightweight protocols are often used among duplicated processes that are primarily not able to tolerate ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
Sponsors
- SIGSOFT: ACM Special Interest Group on Software Engineering
- IEEE-CS: Computer Society
Publisher
IEEE Press
Publication History
Published: 27 May 2019
Check for updates
Qualifiers
- Research-article
Conference
ICSE '19
Sponsor:
- SIGSOFT
- IEEE-CS
Upcoming Conference
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 31Total Downloads
- Downloads (Last 12 months)4
- Downloads (Last 6 weeks)1
Reflects downloads up to 24 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in