Visible to the public Formal Modeling and Verification of Blockchain System

TitleFormal Modeling and Verification of Blockchain System
Publication TypeConference Paper
Year of Publication2018
AuthorsDuan, Zhangbo, Mao, Hongliang, Chen, Zhidong, Bai, Xiaomin, Hu, Kai, Talpin, Jean-Pierre
Conference NameProceedings of the 10th International Conference on Computer Modeling and Simulation
Conference LocationNew York, NY, USA
ISBN Number978-1-4503-6339-6
KeywordsBlockchain protocols, Collaboration, composability, compositionality, formal methods, formal verification, model-checking, policy-based governance, privacy, protocol verification, pubcrawl

As a decentralized and distributed secure storage technology, the notion of blockchain is now widely used for electronic trading in finance, for issuing digital certificates, for copyrights management, and for many other security-critical applications. With applications in so many domains with high-assurance requirements, the formalization and verification of safety and security properties of blockchain becomes essential, and the aim of the present paper. We present the model-based formalization, simulation and verification of a blockchain protocol by using the SDL formalism of Telelogic Tau. We consider the hierarchical and modular SDL model of the blockchain protocol and exercise a methodology to formally simulate and verify it. This way, we show how to effectively increase the security and safety of blockchain in order to meet high assurance requirements demanded by its application domains. Our work also provides effective support for assessing different network consensus algorithms, which are key components in blockchain protocols, as well as on the topology of blockchain networks. In conclusion, our approach contributes to setting up a verification methodology for future blockchain standards in digital trading.

Citation Keyduan_formal_2018