Formal Modeling And Analysis Of Smart Contracts Based On Blockchain

As a decentralized distributed ledger,blockchain can reliably record the transaction process and maintain the agreement reached by the parties.Transaction records on the blockchain are hard to tamper with and transaction history of it can be traced.With the rapid development of blockchain,blockchain technology has been widely used in many aspects of society,such as finance,Internet and cloud computing.Smart contracts can express the agreement reached by both parties in the form of a program,which allows a trusted transaction without a third-party supervisor.Blockchain provides a stable operating platform for smart contracts.Smart contracts are also widely used in blockchain technology because of its simple and efficient characteristics.However,with the rapid development of smart contracts,the number of attacks is also growing.In June 2016,the DAO was attacked.Hackers stole more than 3 million ETH from the resource pool through the smart contract vulnerability.Therefore,it has become increasingly important to ensure the security and reliability of smart contracts.At present,there are two methods to verify the security of smart contracts,including correctness verification and security assurance.The correctness verification mainly checks whether the transaction behavior between smart contracts and clients conforms to the corresponding specifications.Security assurance detects the vulnerability in the code of smart contracts.The thesis mainly examines the safety of smart contracts from the perspective of the correctness verification.In the thesis,model checking technology is applied to the transaction process of the blockchain,and the functional safety of smart contracts are formally modeled and analyzed.According to the behavior characteristics of smart contracts in the transaction process,we build its formal model,and propose a general method for modeling smart contracts and clients through the basic specification of the transaction scenario.Then the method is applied to a specific blockchain transaction case.By analyzing the behavior characteristics of smart contracts and clients in the transaction process,the thesis builds their formal models.Secondly,the thesis uses the Promela language to realize the formal models of smart contracts and clients from the code level.The Promela model not only realizes the internal behaviors of smart contracts and clients,but also the behaviors of smart contracts interacting with clients.Finally,the Promela model is formally verified and analyzed by the model checking tool SPIN.SPIN runs the Promela model and simulates the message passing between the processes.Then,SPIN verifies the correct properties extracted from the specification of the transaction scenario in order to check whether these properties are satisfied in the model.Through formal analysis,it can check whether the behaviors of smart contracts and clients in the transaction process comply with the corresponding transaction specifications and verify the correctness of smart contracts.