A Survey on Security Verification of Blockchain Smart Contracts <s> 3) SEMANTIC ANALYSIS <s> The adoption of blockchain-based distributed computation platforms is growing fast. Some of these platforms, such as Ethereum, provide support for implementing smart contracts, which are envisioned to have novel applications in a broad range of areas, including finance and the Internet-of-Things. However, a significant number of smart contracts deployed in practice suffer from security vulnerabilities, which enable malicious users to steal assets from a contract or to cause damage. Vulnerabilities present a serious issue since contracts may handle financial assets of considerable value, and contract bugs are non-fixable by design. To help developers create more secure smart contracts, we introduce FSolidM, a framework rooted in rigorous semantics for designing contracts as Finite State Machines (FSM). We present a tool for creating FSM on an easy-to-use graphical interface and for automatically generating Ethereum contracts. Further, we introduce a set of design patterns, which we implement as plugins that developers can easily add to their contracts to enhance security and functionality. <s> BIB001 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 3) SEMANTIC ANALYSIS <s> In this paper, we present a formal verification tool for the Ethereum Virtual Machine (EVM) bytecode. To precisely reason about all possible behaviors of the EVM bytecode, we adopted KEVM, a complete formal semantics of the EVM, and instantiated the K-framework's reachability logic theorem prover to generate a correct-by-construction deductive verifier for the EVM. We further optimized the verifier by introducing EVM-specific abstractions and lemmas to improve its scalability. Our EVM verifier has been used to verify various high-profile smart contracts including the ERC20 token, Ethereum Casper, and DappHub MakerDAO contracts. <s> BIB002 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 3) SEMANTIC ANALYSIS <s> Currently, Bitcoin and Ethereum are the two most popular cryptocurrency systems, especially Ethereum. It permits complex financial transactions or rules through scripts, which is called smart contracts. Since Ethereum smart contracts hold millions of dollars, their execution correctness is crucial against attacks which aim at stealing the assets. In this paper, we proposed a security assurance method for smart contract source code to find potential security risks. It contains two main functions, the first is syntax topological analysis of smart contract invocation relationship, to help developers to understand their code structure clearly; the second is logic risk (which may lead to vulnerabilities) detection and location, and label results on topology diagram. For developers' convenience, we have built a static analysis tool called SASC to generate topology diagram of invocation relationship and to find potential logic risks. We have made an evaluation on 2,952 smart contracts, experiment results proved that our method is intuitive and effective. <s> BIB003 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 3) SEMANTIC ANALYSIS <s> Smart contracts, as a promising and powerful application on the Ethereum blockchain, have been growing rapidly in the past few years. Since they are highly vulnerable to different forms of attacks, their security becomes a top priority. However, existing security auditing techniques are either limited in finding vulnerabilities (rely on pre-defined bug patterns) or very expensive (rely on program analysis), thus are insufficient for Ethereum. To mitigate these limitations, we proposed a novel semantic-aware security auditing technique called S-GRAM for Ethereum. The key insight is a combination of N-gram language modeling and lightweight static semantic labeling, which can learn statistical regularities of contract tokens and capture high-level semantics as well (e.g., flow sensitivity of a transaction). S-GRAM can be used to predict potential vulnerabilities by identifying irregular token sequences and optimize existing in-depth analyzers (e.g., symbolic execution engines, fuzzers etc.). We have implemented S-GRAM for Solidity smart contracts in Ethereum. The evaluation demonstrated the potential of S-GRAM in identifying possible security issues. <s> BIB004
Semantic analysis is another important way to analyze and write a correct contract. Focused on modifying the EVM environment, Hildenbrandt et al.  presented an executable formal specification of the EVM's Bytecode stack-based language called KEVM. It provided a more security environment for the development of the smart contracts, and made the formal analysis of the smart contracts easier. They used the official Ethereum test suite to verify the correctness and performance of the KEVM, which all achieved better results. Daejun et al. BIB002 also proposed a formal verification tool for the EVM Bytecode, which adopted KEVM. Their verification tool had been used to verify various high-profile smart contracts including the ERC20, Ethereum Casper, and DappHub MakerDAO contracts. Focused on developing smart contracts, Zhou et al. BIB003 designed a SASC static analysis tool to generate a syntax topology map of the invocation relationships in smart contracts and mark the locations where risks and vulnerabilities may occur. Liu et al. BIB004 proposed a novel semantic aware security auditing technique called S-gram for Ethereum. They combined the N-gram language to model the static semantic labeling, and predicted potential vulnerabilities by identifying irregular token sequences. Mavridou and Laszka BIB001 introduced FSolidM, a framework rooted in rigorous semantics for designing contracts as FSM. Also, they provided a tool to design the FSM model and verify the correctness of the contracts conveniently. Focused on the published smart contracts, Suiche  designed a decompiler to analyze the syntax and decompile the EVM binary code, so that the readable solidity code was generated. Through static and dynamic analysis of the decompiled code, vulnerabilities in contracts were discovered.