Research On The Formal Specification Of Ethereum Smart Contracts Based On Operational Semantics

At present,the digital economy is evolving to the era of programmable economy.Smart contracts play an important role in promoting the programmable economy,but its application is facing various problems.In blockchain applications,due to the immutability of the blockchain,smart contracts cannot be changed once they are online.Once a hacker incident occurs,the consensus of the entire community is needed to roll back the transaction,and it is unrealistic to roll back the transaction every time it is attacked.With the generalization of platform-level applications,the amount involved in smart contracts has increased exponentially.If there are loopholes in its code,the loss to users is huge and irreversible.Since the rollback is unrealistic due to the unchangeable launch,and the loss is large,blockchain application development requires rigorous detection methods to obtain sufficient security.Formal methods are special technologies based on mathematical logic,which can truly improve the automation and accuracy of smart contract security verification.Formal description is the first step to realize smart contract security verification.A good formal language description as a basis can truly help improve the efficiency,quality and feasibility of smart contracts in formal verification.Aiming at the security issues of Ethereum smart contracts,this article will focus on the process of formalizing smart contracts using operational semantics.This article focuses on the formal modeling of Ethereum smart contracts,combined with the characteristics of the solidity programming language,proposes a formal contract model for Ethereum smart contracts,and applies the formal model to major security vulnerabilities that pose a serious threat to smart contracts.In the formal analysis,the specific research content is as follows:(1)Conduct a general analysis of Ethereum smart contracts,and propose a formal model suitable for general smart contracts.The formal contract model of the smart contract is composed of three parts: the formal model of the contract system,the state-assisted model,and the rule modeling.The basic framework of the model is defined according to the characteristics of the smart contract programming language,and multiple sets of rewrite rules are used to define smart contract execution rules,and abstract The state machine assists in realizing the state transition of contract execution,and the model has practical significance for the security of smart contracts.(2)A detailed analysis of the serious security vulnerabilities of Ethereum smart contracts.This article analyzes the causes and attack methods of reentrant vulnerabilities,integer overflow vulnerabilities,and insufficient gas vulnerabilities,respectively,and combines the formal contract model to target each vulnerabilities.A specific modeling method is proposed to solve the modeling difficulties of the above-mentioned vulnerabilities.It is verified through experiments that the instances with security vulnerabilities do have security risks under the formal description method proposed in this paper.The formal description method proposed in this article implements the strict specification of the behavior logic of smart contracts,clarifies the state changes of the contract,keeps the key behavior semantics consistent with the source code,and the formal semantics can automatically execute the content,and solves the description in the smart contract security verification.Problems such as obscure language and single vulnerability detection.