Abstract
The Nervos CKB (Common Knowledge Base) is the base layer of a new kind of blockchain. The CKB block synchronization protocol provides a set of rules that participating nodes must obey while synchronizing their blocks. This protocol mainly consists of three parts: connecting header, downloading block and accepting block. In this paper, we model the CKB block synchronization protocol in Coq and verify the correctness of the protocol. Our model takes the communication between nodes and the reliability of implementation into consideration to reflect a more realistic environment faced by the blockchain. We prove the soundness and the completeness of the protocol under several reliability and consistency assumptions. We also prove that without some of these assumptions, the protocol may fail to guarantee the correctness of block synchronization. Our formal verification can ensure the security of the protocol and provide ways to prevent potential attacks.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
The source code of proofs in this paper. https://github.com/H-Bu/CKB-verification
Bhargavan, K., Blanchet, B., Kobeissi, N.: Verified models and reference implementations for the TLS 1.3 standard candidate. In: 2017 IEEE Symposium on Security and Privacy, pp. 483–502. IEEE (2017)
Bitcoin Cash. https://www.bitcoincash.org
CKB block synchronization protocol. https://github.com/nervosnetwork/rfcs/blob/master/rfcs/0004-ckb-block-sync/0004-ckb-block-sync.md
Fiterău-Broştean, P., Janssen, R., Vaandrager, F.: Combining model learning and model checking to analyze TCP implementations. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 454–471. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_25
Havelund, K., Skou, A., Larsen, K.G., Lund, K.: Formal modeling and analysis of an audio/video protocol: an industrial case study using UPPAAL. In: Proceedings Real-Time Systems Symposium, pp. 2–13. IEEE (1997)
Lu, Y., Sun, M.: Modeling and verification of IEEE 802.11i security protocol in UPPAAL for Internet of Things. Int. J. Softw. Eng. Knowl. Eng. 28(11–12), 1619–1636 (2018)
Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008). https://bitcoin.org/bitcoin.pdf
Pîrlea, G., Sergey, I.: Mechanising blockchain consensus. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 78–90. ACM (2018)
Poon, J., Dryja, T.: The bitcoin lightning network: scalable off-chain instant payments (2016). https://www.bitcoinlightning.com/wp-content/uploads/2018/03/lightning-network-paper.pdf
The Nervos Network. https://www.nervos.org
Wood, G.: Polkadot: vision for a heterogeneous multi-chain framework (2016). https://polkadot.network/PolkaDotPaper.pdf
Acknowledgments
This work was partially supported by the Guangdong Science and Technology Department (Grant no. 2018B010107004) and the National Natural Science Foundation of China under grant no. 61772038 and 61532019.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2020 Springer Nature Switzerland AG
About this paper
Cite this paper
Bu, H., Sun, M. (2020). Towards Modeling and Verification of the CKB Block Synchronization Protocol in Coq. In: Lin, SW., Hou, Z., Mahony, B. (eds) Formal Methods and Software Engineering. ICFEM 2020. Lecture Notes in Computer Science(), vol 12531. Springer, Cham. https://doi.org/10.1007/978-3-030-63406-3_17
Download citation
DOI: https://doi.org/10.1007/978-3-030-63406-3_17
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-63405-6
Online ISBN: 978-3-030-63406-3
eBook Packages: Computer ScienceComputer Science (R0)