In order to detect those security issues on Ethereum smart contracts, Luu et al. build a symbolic execution tool called Oyente[15] to find potential bugs pre-deploy. Oyente ran on 19,366 smart contracts and found that 8,833 contracts potentially have bugs. These contracts currently have a total balance of about 3,068,654 million Ethers, approximately equivalent to 30 million USD.
From a different perspective, K. Bhargavan et al.[16] outline a framework to analyze and formally verify Ethereum smart contracts using F*[17], a functional programming language targeted at program verification. The F* language comes with a rich type system to generate automated queries for a SMT solver that can then statically verify such properties of contracts.
Other than Oyente, there are many alternative tools for smart contract security check-ing. Motivated by the security issues and recurring financial losses in smart contracts, A.Dika[18] provide a taxonomy of all known security issues and security code analy-sis tools used to identify smart contract vulnerabilities. Based on previous attacks on Ethereum smart contracts, they also categorizes all known vulnerabilities within their ar-chitectural and severity level. By assessing their effectiveness and accuracy, they conduct the investigation of security code analysis tools on Ethereum. They analyze four ma-jor Ethererum smart contracts security detecting tools, Oyente, Securify[19], Remix, and SmartCheck[20]. We can tell from the research result that there are overall inconsisten-cies between the tools on different security properties. SmartCheck obviously is the most effectiveness tool. Whereas in terms of accuracy, Oyente give the best performance. Also, they propose future improvements within the user interfaces, interpretation of results, and additional vulnerability checks.
There are several other approaches to analyze security of smart contracts. Not only using source code, some existing tools turn to find out the problems from EVM bytecode.
Porosity[21] is a decompiler for EVM bytecode that generates readable Solidity syntax contracts. Enabling static and dynamic analysis of such compiled contracts.
‧
KEVM[22], the first fully executable formal semantics of the bytecode in which smart contracts are executed. The K framework, a semantic definition of EVM for use in verifying properties of smart contracts, not only passes the official test suite for EVM implementations, but also reveals ambiguities and potential sources of error in the existing on-paper formalization of EVM semantics. These properties make it an ideal formal reference implementation.
S.Amani et al.[23] extend an existing EVM formalisation in Isabelle/HOL by a sound program logic at the level of bytecode. They target unstructured bytecode rather than a high-level programming language. They structure bytecode sequences into blocks of straight-line code and create a program logic to reason about these.
To promote the development of secure smart contracts, A.Mavridou et al.[24] have created the FSolidM framework, that allows developers to define contracts as finite state machines (FSMs)[25] with strict and clear semantics. It provides an user friendly editor for specifying FSMs, a code generator for creating smart contracts, and a set of plugins that developers may add to their FSMs to enhance security and functionality. There goal is to helps developers to create smart contracts that are secure by design.
For some popular scripting languages used in existing cryptocurrencies such as Bitcoin, Nxt[26] and Ethereum, Seijas, Pablo Lamela et al.[27] survey different approaches, and give an overview of critiques of existing languages. They also cover technologies that might be used to strengthen extensions and innovations in scripting and contracts, including technologies for verification, such as zero knowledge proofs[28], proof-carrying code[29]
and static analysis, as well as approaches to making systems more efficient, e.g. Merkelized Abstract Syntax Trees[30].
Cryptocurrency is a virtual form of money but it create a total different transacting method due to the power of blockchain. However, same as concrete currency, trust be-tween user and blockchain system has to be established to make sure people won’t have to face the situation that their money were stolen due to system vulnerability. Public blockchain may be the most used chain in recent ecosystem because of the ability for
‧
every person to join the network. To use public chain, user has to obey those basic rules created by the creator of public chain. So there might be some limitation to prevent any unintentional mistakes or malicious attack. The transaction amounts and total capital will be rich in public blockchain. That is why hackers might try to get benefit from it.
Rather using public chain, an enterprise or a group of company might be interested to using private chain as there blockchain infrastructure. Unlike public chain, private chain only allowed specific user, such as company’s employee, to access the network. Transac-tion and total capital will be relatively low because of less participants, but the flexibility is higher so there might be less restriction. Although more customizable, the problem of exceeding the limitation of blockchain system might happened.
Based on previous research, we want to check whether a smart contract contains any positive cycle that might cause EVM stack to overflow during execution. EVM stack has 1,024 frames. When EVM execute an instruction, it will push or pop certain instructions.
By keep executing the part of positive cycle in a smart contract, stack size will eventually exceed the upper bound and cause an exception which makes smart contract terminate with all data rolling back to initial state. But, to make a stack overflow, we need enough gas to consume for the execution. During creation of private chain, gas limit can be customize to any possible number. So in a private chain environment with enormous gas limit, it is possible that stack overflow occur in a smart contract. So our approach is to use static analysis strategies to find out the stack increment and estimate gas consumption when execute positive cycle.
3 Motivating Example
We propose automatic model checking techniques on smart contracts. Our model checking approach benefits from soundness like formal reasoning approaches, as well as automation like symbolic execution approaches. This is achieved by conducting automatic reachabil-ity analysis on the opcode-level control flow graphs along with arithmetic and string automata.
‧
‧
國立 政 治 大 學
‧
N a tio na
l C h engchi U ni ve rs it y
The automata associated with each program point characterize all potential values of target variables on executions up to that program point. The reachability analysis may not terminate when such states are infinite, but when it terminates, the automata represent a fixpoint of reachable states on values of target variables. We can then apply automata operations for checking properties that are related to target variables.
Compared to symbolic executions on observable paths, our objective is to have a sound approach to compute all potential status and behaviors of smart contracts. This is achieved by conducting the reachability analysis on the control flow graphs that abstract all potential execution paths. This challenges our opcode analysis to having a sound approximation on flows but tight enough to prevent a high false positive rate.
In this section, we will use a short example to demonstrate how we analysis smart contract. Contract SimpleM ember is an example code written in high-level language, Solidity.
3.1 Cycle Detection
For the first step, we compile above example source code into opcode and use the opcode to construct control flow graph. After running the analysis program, our analyzer’s algorithm reveal that one cycle is contained in the example source code, starting from line 21 to 30.
Figure 1 is the output of the analyzer, which is a control flow graph of the cycle part. A cycle may cause some unexpected things to happen during the execution. That is to say, if the code of that cycle part is executing multiple times, an exception might appear and make the whole process stopped. We will use the control flow graph of the cycle path for further analyze and finally we will calculate the stack size usage and gas consumption to confirm our hypothesis.