A Survey on Security Verification of Blockchain Smart Contracts <s> 1) PROGRAM-BASED FORMAL VERIFICATION <s> Smart contracts are programs running on cryptocurrency (e.g., Ethereum) blockchains, whose popularity stem from the possibility to perform financial transactions, such as payments and auctions, in a distributed environment without need for any trusted third party. Given their financial nature, bugs or vulnerabilities in these programs may lead to catastrophic consequences, as witnessed by recent attacks. Unfortunately, programming smart contracts is a delicate task that requires strong expertise: Ethereum smart contracts are written in Solidity, a dedicated language resembling JavaScript, and shipped over the blockchain in the EVM bytecode format. In order to rigorously verify the security of smart contracts, it is of paramount importance to formalize their semantics as well as the security properties of interest, in particular at the level of the bytecode being executed. In this paper, we present the first complete small-step semantics of EVM bytecode, which we formalize in the F* proof assistant, obtaining executable code that we successfully validate against the official Ethereum test suite. Furthermore, we formally define for the first time a number of central security properties for smart contracts, such as call integrity, atomicity, and independence from miner controlled parameters. This formalization relies on a combination of hyper- and safety properties. Along this work, we identified various mistakes and imprecisions in existing semantics and verification tools for Ethereum smart contracts, thereby demonstrating once more the importance of rigorous semantic foundations for the design of security verification techniques. <s> BIB001 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) PROGRAM-BASED FORMAL VERIFICATION <s> This paper reports on the development and verification of a novel formal symbolic process virtual machine (FSPVM) for verifying the reliability and security of Ethereum smart contracts, denoted as FSPVM-E, completely in Coq proof assistant. It adopts execution-verification isomorphism (EVI), an extension of Curry-Howard isomorphism (CHI), as its fundamental theoretical framework. The current version of FSPVM-E is constructed on a general, extensible, and reusable formal memory (GERM) framework, an extensible and universal formal intermediate programming language Lolisa, which is a large subset of the Solidity programming language using generalized algebraic datatypes, and the corresponding formally verified interpreter of Lolisa, denoted as FEther. It supports the ERC20 standard and can automatically simultaneously symbolically execute the smart contract programs of Ethereum and verify their reliability and security properties using Hoare logic in Coq. In addition, this work, contributes to solving the problems of automation, inconsistency and reusability in higher-order logic theorem proving. <s> BIB002 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) PROGRAM-BASED FORMAL VERIFICATION <s> In recent publications, we presented a novel formal symbolic process virtual machine (FSPVM) framework that combined higher-order theorem proving and symbolic execution for verifying the reliability and security of smart contracts developed in the Ethereum blockchain system without suffering the standard issues surrounding reusability, consistency, and automation. A specific FSPVM, denoted as FSPVM-E, was developed in Coq based on a general, extensible, and reusable formal memory (GERM) framework, an extensible and universal formal intermediate programming language, denoted as Lolisa, which is a large subset of the Solidity programming language that uses generalized algebraic datatypes, and a corresponding formally verified interpreter for Lolisa, denoted as FEther, which serves as a crucial component of FSPVM-E. However, our past work has demonstrated that the execution efficiency of the standard development of FEther is extremely low. As a result, FSPVM-E fails to achieve its expected verification effect. The present work addresses this issue by first identifying three root causes of the low execution efficiency of formal interpreters. We then build abstract models of these causes, and present respective optimization schemes for rectifying the identified conditions. Finally, we apply these optimization schemes to FEther, and demonstrate that its execution efficiency has been improved significantly. <s> BIB003 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) PROGRAM-BASED FORMAL VERIFICATION <s> Blockchain technology has increasing attention in research and across many industries. The Ethereum blockchain offers smart contracts, which are small programs defined, executed, and recorded as transactions in the blockchain transaction history. These smart contracts run on the Ethereum Virtual Machine (EVM) and can be used to encode agreements, transfer assets, and enforce integrity conditions in relationships between parties. Smart contracts can carry financial value, and are increasingly used for safety-, security-, or mission-critical purposes. Errors in smart contracts have led and will lead to loss or harm. Formal verification can provide the highest level of confidence about the correct behaviour of smart contracts. In this paper we extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. We structure bytecode sequences into blocks of straight-line code and create a program logic to reason about these. This abstraction is a step towards control of the cost and complexity of formal verification of EVM smart contracts. <s> BIB004 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) PROGRAM-BASED FORMAL VERIFICATION <s> The recent growth of the blockchain technology market puts its main cryptocurrencies in the spotlight. Among them, Ethereum stands out due to its virtual machine (EVM) supporting smart contracts, i.e., distributed programs that control the flow of the digital currency Ether. Being written in a Turing complete language, Ethereum smart contracts allow for expressing a broad spectrum of financial applications. The price for this expressiveness, however, is a significant semantic complexity, which increases the risk of programming errors. Recent attacks exploiting bugs in smart contract implementations call for the design of formal verification techniques for smart contracts. This, however, requires rigorous semantic foundations, a formal characterization of the expected security properties, and dedicated abstraction techniques tailored to the specific EVM semantics. This work will overview the state-of-the-art in smart contract verification, covering formal semantics, security definitions, and verification tools. We will then focus on EtherTrust [1], a framework for the static analysis of Ethereum smart contracts which includes the first complete small-step semantics of EVM bytecode, the first formal characterization of a large class of security properties for smart contracts, and the first static analysis for EVM bytecode that comes with a proof of soundness. <s> BIB005
The essence of a smart contract is the program that is executed on the blockchain. Verifying the correctness of the program is a key part of ensuring the safety and reliability of smart contracts. There are both successful practical cases and theoretical studies on program-based verification of smart contracts. At the 3rd Global Blockchain Summit in 2017, a blockchain formal verification team of the University of Electronic Science and Technology presented the VaaS (Verification as a service) as a EOS formal verification platform. Except for the EOS blockchain platform, VaaS also supports other common platforms such as Ethereum and Fabric. The principle of VaaS platform is to translate programs written in the Solidity scripting language into the Coq code, thus establishing a standard formal model for smart contracts, and then verify the correctness of the smart contract by verifying the correctness of the Coq language. Similarly, Bhargavan et al.  proposed a verification method based on programming language. They translated the Solidity language into an F* language to check if the contract was correct. In most cases we can only get the binary code running on the Ethereum, and we cannot get the source code of the smart contract. So in the absence of source code, they decompiled the binary files on Ethereum into F* language [58] , and analyzed whether at least some of the attributes to be reached by the contract were satisfied. The complete F* language for any smart contract had not yet been implemented because of huge work. Moreover, for the same contract, it was so hard to verify whether the F* language translated by Solidity language consistented with the decompiled binary code. Furthermore, Grishchenko et al. BIB001 also used the F* language proof assistant to successfully validate the official Ethereum test suite. Yang and Lei BIB002 , BIB003 proposed a novel formal symbolic process virtual machine (FSPVM) to verify the reliability and security properties of smart contracts which based on Hoare logic in Coq. It used an extensible formal intermediate programming language Lolisa and the corresponding formally verified interpreter of Lolisa. After verification, they found that it supported the ERC20 standard and could solve the problems in higher-order logic theorem proving. Hirai  proposed a formal verification method based on Ethereum Bytecode. In the process of translating one language into another, there may be cases where the meaning expressed in the translated language not be consistent with that before translation. So he proposed using the Isabelle/HOL to verify the binary Ethereum code. To illustrated his method, first, he obtained the binary instructions of a small contract called ''deed''. Then he translated the list of instructions into an AVL tree. Last, he analyzed the AVL tree in a theorem proving environment with the Isabelle proof assistant. This verification method is generic to all Ethereum smart contracts. Amani et al. BIB004 also used the Isabelle proof assistant to verify the binary Ethereum code. The principle of the method is to organize the bytecode sequences into linear code blocks and create a logic program, where each block is processed as a set of instructions. Each part of the verification is validated in a single trusted logical framework from the perspective of bytecode. Grishchenko et al. BIB005 focused on the EtherTrust [62] , a framework for the static analysis of Ethereum smart contracts. It also analyzed the EVM Bytecode of the contracts statically together with a proof of soundness.