Formal Analysis And Verification Of Blockchain Consensus Protocol Based On Model Checking

Blockchain technology has attracted extensive attention because of the introduction of bitcoin.With the development of recent years,the application of blockchain technology is no longer limited to bitcoin and other digital currencies,and more application scenarios have been developed.A large number of digital assets are managed through the blockchain,making the blockchain vulnerable to hacker attacks,and security issues hinder the development of the blockchain.The consensus protocol is the core technology of the blockchain,and most of the known attacks on the blockchain system are aimed at the consensus protocol.Only by ensuring the security of the consensus protocol can the blockchain be more reliable and widely used.Formal method is one of the most powerful methods to analyze the security of network protocols.Among them,model checking,based on the state space search to traverse all the states in the process of protocol execution,finds potential vulnerabilities,and then ensure the security of the protocol.In this thesis,the security of blockchain consensus protocol is studied.PBFT(Practical Byzantine Fault Tolerance),a typical blockchain consensus protocol,is selected as the research object,and the security of PBFT is analyzed by formal method.The main work of this thesis is as follows:(1)An abstract modeling method for the PBFT consensus protocol is proposed,which simplifies the number of entities in the implementation of the protocol the message structure,and assumes that the cryptographic system used by the protocol is complete.Extending the modeling method proposed by Maggi,and defining message transmission channels for different stages of protocol execution.Abstract and simplify the PBFT protocol interaction process to solve the problem that the PBFT consensus protocol communication process is too complicated to be analyzed by formal methods.(2)A Byzantine node model construction method for the security analysis of the PBFT consensus protocol is proposed.Analyzing the damage caused by Byzantine nodes to the consensus process during the implementation of PBFT protocol,and we can divide the behavior of the Byzantine node into sending true messages,not sending messages,replay messages,and forged messages.(3)Abstract the security properties of PBFT conformance protocol and view change protocol.Use the LTL formula to characterize,use the model checking tool SPIN to analyze and verify,and analyze the security of the PBFT protocol in the presence of Byzantine nodes.Taking the number of honest nodes and Byzantine nodes participating in the execution of the agreement as independent variables,the upper limit of the number of Byzantine nodes that the agreement can tolerate is given.In summary,the protocol abstract modeling method and the Byzantine node model construction method proposed in this article are of reference significance for the formal method to analyze the security of the PBFT consensus protocol;it is proposed to change the number of nodes participating in the execution of the protocol to explore the fault tolerance of the protocol.The upper limit method can be applied to the fault tolerance analysis of such consensus protocols.