A Survey on Security Verification of Blockchain Smart Contracts <s> B. FORMAL VERIFICATION <s> Smart contracts might encode legal contracts written in natural language to represent the contracting parties’ shared understandings and intentions. The issues and research challenges involved in the validation and verification of smart contracts, particularly those running over blockchains and distributed ledgers, are explored. <s> BIB001 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> B. FORMAL VERIFICATION <s> Blockchain is an integrated technology to ensure keeping record and process transactions with decentralized manner. It is thought as the foundation of future decentralized ecosystem, and collects much attention. However, the maturity of this technology including security of the fundamental protocol and its applications is not enough, thus we need more research on the security evaluation and verification of Blockchain technology This tutorial explains the current status of the security of this technology, its security layers and possibility of application of formal analysis and verification. <s> BIB002
Formal methods provides a powerful technology for the correctness verification of smart contracts. At present, the use of formal methods to verify smart contracts has been widely recognized, and significant results have been achieved in practice. To solve the demands for high assurance contracts, the Ethereum community has turned to formal methods as well  ,  . Besides, using formal methods to validate smart contracts can provide a rigorous mathematical model for the verification of smart contracts. Through the analysis of the model, we can more easily discover the logic errors or other new vulnerabilities. The formal verification of smart contracts tends to be a great potential for development in the future BIB001 , BIB002 . According to the research BIB001 , we summarize the formal verification framework for smart contracts shown in FIGURE 3 . The text agreement of a smart contract made by contract participants needs to fully express the intention of the makers and comply with the law. Then, Implementing formal specification and formal verification on above established contract, which is an iterative process. Through multiple behavioral modeling and attribute modeling of smart contracts, we can validate whether the attributes meet the contract requirement or not. In our survey, we divide the formal verification method of smart contracts into two categories. One is program-based verification and the other one is behavior-based verification. Program-based verification treats smart contracts as codes, it translates the contract codes into formal languages and then identifies vulnerabilities in contracts. This is a verification method for static analysis programs. Behavior-based verification takes into account issues that may be encountered during the execution of smart contracts, such as improper operations and maliciously attacks. By constructing a formal model, it finds out the weak position of the contract, which is a way to dynamically analyze smart contracts. Below we discuss these two aspects in detail.