A Survey on Security Verification of Blockchain Smart Contracts <s> 1) THE SOLUTION FOR A SPECIFIC VULNERABILITY <s> Ethereum contracts can be designed to function as fully decentralized applications called DAPPs that hold financial assets, and many have already been fielded. Unfortunately, DAPPs can be hacked, and the assets they control can be stolen. A recent attack on an Ethereum decentralized application called The DAO demonstrated that smart contract bugs are more than an academic concern. Ether worth hundreds of millions of US dollars was extracted by an attacker from The DAO, sending the value of its tokens and the overall exchange price of ether itself tumbling. We present two market-based techniques for insuring the ether holdings of a DAPP. These mechanisms exist and are managed as part of the core programming of the DAPP, rather than as separate mechanisms managed by users. Our first technique is based on futures contracts indexed by the trade price of ether for DAPP tokens. Under fairly general circumstances, our technique is capable of recovering the majority of ether lost from theft with high probability even when all of the ether holdings are stolen; and the only cost to DAPP token holders is an adjustable ether withdrawal fee. As a second, complementary, technique we propose the use of Gated Public Offerings (GPO) as a mechanism that mitigates the effects of attackers that exploit DAPP withdrawal vulnerabilities. We show that using more than one public offering round encourages attackers to exploit the vulnerability early, or depending on certain factors, to delay exploitation (possibly indefinitely) and short tokens in the market instead. In both cases, less ether is ultimately stolen from the DAPP, and in the later case, some of the losses are transferred to the market. <s> BIB001 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) THE SOLUTION FOR A SPECIFIC VULNERABILITY <s> Callbacks are essential in many programming environments, but drastically complicate program understanding and reasoning because they allow to mutate object's local states by external objects in unexpected fashions, thus breaking modularity. The famous DAO bug in the cryptocurrency framework Ethereum, employed callbacks to steal $150M. We define the notion of Effectively Callback Free (ECF) objects in order to allow callbacks without preventing modular reasoning. An object is ECF in a given execution trace if there exists an equivalent execution trace without callbacks to this object. An object is ECF if it is ECF in every possible execution trace. We study the decidability of dynamically checking ECF in a given execution trace and statically checking if an object is ECF. We also show that dynamically checking ECF in Ethereum is feasible and can be done online. By running the history of all execution traces in Ethereum, we were able to verify that virtually all existing contracts, excluding the DAO or contracts with similar known vulnerabilities, are ECF. Finally, we show that ECF, whether it is verified dynamically or statically, enables modular reasoning about objects with encapsulated state. <s> BIB002 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) THE SOLUTION FOR A SPECIFIC VULNERABILITY <s> Smart contracts enabled a new way to perform cryptocurrency transactions over blockchains. While this emerging technique introduces free-of-conflicts and transparency, smart contract itself is vulnerable. As a special form of computer program, smart contract can hardly get rid of bugs. Even worse, an exploitable security bug can lead to catastrophic consequences, e.g., loss of cryptocurrency/money. In this demo paper, we focus on the most common type of security bugs in smart contracts, i.e., reentrancy bug, which caused the famous DAO attack with a loss of 60 million US dollars. We presented ReGuard, an fuzzing-based analyzer to automatically detect reentrancy bugs in Ethereum smart contracts. Specifically, ReGuard performs fuzz testing on smart contracts by iteratively generating random but diverse transactions. Based on the runtime traces, ReGuard further dynamically identifies reentrancy vulnerabilities. In the preliminary evaluation, we have analyzed 5 existing Ethereum contracts. ReGuard automatically flagged 7 previously unreported reentrancy bugs. A demo video of ReGuard is at https://youtu.be/XxJ3_-cmUiY. <s> BIB003 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) THE SOLUTION FOR A SPECIFIC VULNERABILITY <s> Termination of smart contracts is crucial for any blockchain system's security and consistency, especially for those supporting Turing-complete smart contract languages. Resource-constrained blockchain systems, like Ethereum and Hyperledger Fabric, could prevent smart contracts from terminating properly when the pre-allocated resources are not sufficient. The Zen system utilizes the dependent type system of the programming language F* to prove the termination of smart contracts for all inputs during compilation time. Since the smart contract execution usually depends on the current blockchain state and user inputs, this approach is not always successful. In this work, we propose a lazy approach by statically proving conditional termination and non-termination of a smart contract to determine input conditions under which the contract terminates or not. Prior to the execution of the smart contract, the proof-carrying blockchain system will check that its current state and the contract's input satisfy the termination conditions in order to determine if the contract is qualified (i.e., eventually terminating) to run on the chain. <s> BIB004 </s> A Survey on Security Verification of Blockchain Smart Contracts <s> 1) THE SOLUTION FOR A SPECIFIC VULNERABILITY <s> The capability of executing so-called smart contracts in a decentralised manner is one of the compelling features of modern blockchains. Smart contracts are fully fledged programs which cannot be changed once deployed to the blockchain. They typically implement the business logic of distributed apps and carry billions of dollars worth of coins. In that respect, it is imperative that smart contracts are correct and have no vulnerabilities or bugs. However, research has identified different classes of vulnerabilities in smart contracts, some of which led to prominent multi-million dollar fraud cases. In this paper we focus on vulnerabilities related to integer bugs, a class of bugs that is particularly difficult to avoid due to some characteristics of the Ethereum Virtual Machine and the Solidity programming language. In this paper we introduce Osiris -- a framework that combines symbolic execution and taint analysis, in order to accurately find integer bugs in Ethereum smart contracts. Osiris detects a greater range of bugs than existing tools, while providing a better specificity of its detection. We have evaluated its performance on a large experimental dataset containing more than 1.2 million smart contracts. We found that 42,108 contracts contain integer bugs. Besides being able to identify several vulnerabilities that have been reported in the past few months, we were also able to identify a yet unknown critical vulnerability in a couple of smart contracts that are currently deployed on the Ethereum blockchain. <s> BIB005
Some studies have given different solutions to specific vulnerabilities. Bissias et al. BIB001 proposed a mechanism for recovering stolen assets for DAPP applications such as DAO, which greatly reduced the losses caused by attacks. Marcus et al.  proposed to eliminate some artifacts of Kademlia protocol, raising the threshold for attackers. This countermeasure has been added to geth1.8 (a standalone client of Go Ethereum) to against eclipse attacks. Liu et al. BIB003 proposed the ReGuard, a tool for detecting reentrant vulnerabilities, which dynamically identified reentrant vulnerabilities in contracts through fuzzing and automatically flaged reentrant errors generated. As the same, Shelly et al. BIB002 proposed a notion of Effectively Callback Free (ECF) objects, which dealt with the callback bugs in contracts, such as reentrancy. Le et al. BIB004 ensured the normal execution of the contract by calculating the execution model and statically proving the input conditions that guaranteed the termination or non-termination of the contract. Torres et al. BIB005 designed a framework to accurately find integer bugs in Ethereum smart contracts called Osiris. They evaluated the tool's performance on a large experimental dataset containing more than 1.2 million smart contracts, which found that 42,108 contracts contain integer bugs.