Formal Research On A Consensus Algorithm For Blockchain

Blockchain technology imposes higher requirements on the security of system design and implementation.The traditional software testing methods cannot cover all the state spaces in the operation of distributed network systems,and it is difficult to fully satisfy the security requirements of distributed decentralized systems,and the cost of simulation and emulation methods becomes higher as the expected application scale of distributed systems increases.This paper is the first formal research on the design framework of a consensus mechanism called proof-of-interest in blockchain technology using theorem proving method in formal methods,constructing its logical model in the higher-order logic theorem prover HOL4,and completing the formal verification of some properties.The validation results of this project can guarantee the reliability of this design framework in a specific environment,while the constructed formal model can be borrowed and reused by the formal work of other blockchain projects,laying the foundation for using formal methods to promote the development of blockchain technology.Meanwhile,solutions are given in the modeling process for the problems of node malicious behavior and multi-node communication encountered in the first application of formal methods to blockchain technology and multi-node systems.Four main points are accomplished as follows.(1)Analyze three different common formal methods and introduce their roles in different stages of software development according to their advantages and disadvantages.As well as a detailed analysis and introduction of theorem provers HOL4 in terms of development history and programming languages.(2)A detailed analysis of blockchain technology and consensus mechanism is presented to summarize its working principles and design methods,and an in-depth research on the design framework of proof-of-stake consensus mechanism is conducted.(3)In the HOL4 theorem prover,the modular method is used to formalize and model the design framework of the consensus mechanism of proof of stake.Formal analysis and modeling of network connection state in multi-node environment;Combined with the implementation model,the formalization model of data consistency specification of Proof of Interest is constructed,which lays the foundation for formalization verification.(4)Some property specifications of each module in the formal model of proof of stake are verified in the HOL4 theorem prover,on which the data consistency verification under a specific network model is completed by the theorem prover method,showing the reliability of proof of stake in a specific network environment.It also lays the foundation for proving the data consistency specification in general network environment in the future,and demonstrates the capability and prospect of HOL4 theorem prover in verifying blockchain technology.