Formal Verification of Blockchain Byzantine Fault Tolerance
作者： Vincent Gramoli , Pierre Tholoniat
DOI:
关键词: Byzantine fault tolerance 、 Listing (computer) 、 Model checking 、 Correctness 、 Blockchain 、 Simple (philosophy) 、 Consensus algorithm 、 Formal verification 、 Theoretical computer science 、 Computer science
摘要: … returns at the correct processes before returning at a Byzantine process; however, we cannot distinguish a correct process from a Byzantine process that acted correctly. We are thankful …
arxiv.org
harvard.edu
springer.com参考文章(38)
Bernadette Charron-Bost, Henri Debrat, Stephan Merz, Formal verification of consensus algorithms tolerating malicious faults international conference on stabilization safety and security of distributed systems. ,vol. 6976, pp. 120- 134 ,(2011) , 10.1007/978-3-642-24550-3_11
Chris Newcombe, Why Amazon Chose TLA ABZ 2014 Proceedings of the 4th International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z - Volume 8477. pp. 25- 39 ,(2014) , 10.1007/978-3-662-43652-3_3
Igor Konnov, Helmut Veith, Josef Widder, SMT and POR Beat Counter Abstraction: Parameterized Model Checking of Threshold-Based Distributed Algorithms computer aided verification. pp. 85- 102 ,(2015) , 10.1007/978-3-319-21690-4_6
Piotr Berman, Juan A. Garay, Asymptotically Optimal Distributed Consensus (Extended Abstract) international colloquium on automata languages and programming. pp. 80- 94 ,(1989) , 10.1007/BFB0035753
Christian Cachin, Klaus Kursawe, Victor Shoup, Random oracles in constantipole: practical asynchronous Byzantine agreement using cryptography (extended abstract) principles of distributed computing. pp. 123- 132 ,(2000) , 10.1145/343477.343531
Cynthia Dwork, Nancy Lynch, Larry Stockmeyer, Consensus in the presence of partial synchrony Journal of the ACM. ,vol. 35, pp. 288- 323 ,(1988) , 10.1145/42282.42283
Martin Biely, Ulrich Schmid, Bettina Weiss, Synchronous consensus under hybrid process and link failures Theoretical Computer Science. ,vol. 412, pp. 5602- 5630 ,(2011) , 10.1016/J.TCS.2010.09.032
Annu John, Igor Konnov, Ulrich Schmid, Helmut Veith, Josef Widder, Parameterized model checking of fault-tolerant distributed algorithms by abstraction formal methods in computer-aided design. pp. 201- 209 ,(2013) , 10.1109/FMCAD.2013.6679411
Ramakrishna Kotla, Lorenzo Alvisi, Mike Dahlin, Allen Clement, Edmund Wong, Zyzzyva ACM Transactions on Computer Systems. ,vol. 27, pp. 1- 39 ,(2009) , 10.1145/1658357.1658358
Gabriel Bracha, Sam Toueg, Asynchronous consensus and broadcast protocols Journal of the ACM. ,vol. 32, pp. 824- 840 ,(1985) , 10.1145/4221.214134