sGuard: Towards Fixing Vulnerable Smart Contracts Automatically

The concept of smart contracts came into being with Ethereum [6], i.e., a digital currency platform with the capability of executing programmable code. It is subsequently supported by platforms such as RSK [7] and Hyperledger [8]. In this work, we focus on Ethereum smart contracts as it remains the most popular smart contracts platform.

Intuitively speaking, an Ethereum smart contract implements a set of rules for managing digital assets in Ethereum accounts. In the Ethereum platform, there are two type of accounts, i.e., externally owned accounts (EOAs) and contract accounts. Both types of accounts have a 256-bit unique address and a balance which represents the amount of Ether (a.k.a. Ethereum currency unit) in the account. Contract accounts are the ones which are associated with smart contracts that can be used to perform certain predefined tasks. A smart contract is similar to a class in object-oriented programming languages such as Java or C#. It contains persistent data such as storage variables and functions that can modify these variables (including a constructor which initializes them). Functions that are declared public can be invoked from other accounts (either EOAs or other contract accounts) through transactions, i.e., a sequence of function invocations.

The Etherum platform supports multiple programming languages for smart contracts programming. Currently, the most popular one is Solidity, i.e., a Turing-complete programming language. For instance, Figure 1(a) shows a public function in a contract named SmartMesh written in Solidity. Once invoked, the function transfers certain amount of tokens from an account (at address from) to another account (at address to). A Solidity contract is compiled into Ethereum bytecode. With the bytecode, a transaction is then executed by the Ethereum Virtual Machine (EVM) on miners’ machines. In its essence, EVM is a stack-based machine. Its details can be referred to in Section III-A.

Solidity programs have a number of language features which are specific to smart contracts and are often associated with vulnerabilities. For instance, a public function marked with keyword $payable$ is allowed to receive Ether when it is invoked. The amount of Ether received is represented in the value of variable $msg.value$. That is, if an account invokes a $payable$ function of a contract and sets the value of $msg.value$ greater than 0, Ether is transferred from the invoking account to the invoked account. Besides that, Ether can also be sent to other contracts using function $send()$ or $transfer()$ which are globally defined. Note that in such a case, a specific no-name function, called the $fallback$ function, is executed if it is defined in the receiving contract. Note that a $fallback$ function is meant to be a safety valve when a non-existing function is called upon the contract, although it seems to be a source of problems instead. Furthermore, to prevent the harmful exploit of the network such as running infinite loops, each bytecode instruction (called opcode) is associated with a running cost called gas, which is paid from the caller’s account.

Just like traditional programs, smart contracts are subject to code-based vulnerabilities. A variety of vulnerabilities have been identified in real-world smart contracts, some of which have been exploited by attackers and have caused significant financial losses (e.g., [9, 10]). In the following, we introduce two kinds of vulnerabilities through examples.

In the following, we illustrate how sGuard patches smart contracts through the two examples mentioned above. The technical details are presented in Section IV. We remark that sGuard identifies vulnerabilities based on bytecode while patches them based on the corresponding source code. This is because analysis based on the bytecode is more precise than analysis based on the source code (as the former is not affected by bugs or optimizations in the Solidity compiler), whereas patching at the source code is transparent to the users.

A smart contract ${\cal S}$ can be viewed as a finite state machine ${\cal S}=(Var,init,N,i,E)$ where $Var$ is a set of variables; $init$ is the initial valuation of the variables; $N$ is a finite set of control locations; $i\in N$ is the initial control location, i.e., the start of the contract; and $E\subseteq N\times C\times N$ is a set of labeled edges, each of which is of the form $(n,c,n^{\prime})$ where $c$ is an opcode. There are a total of 78 opcodes in Solidity (as of version 0.5.3), as summarized in Table I. Note that each opcode is statically assigned with a unique program counter, i.e., each opcode can be uniquely identified based on the program counter.

Note that $Var$ includes stack variables, memory variables, and storage variables. Stack variables are mostly used to store primitive values and memory variables are used to store array-like values (declared explicitly with keyword $memory$). Both stack and memory variables are volatile, i.e., they are cleared after each transaction. In contrast, storage variables are non-volatile, i.e., they are persistent on the blockchain. Together, the variables’ values identify the state of the smart contract at a specific point of time. At the Solidity source code level, stack and memory variables can be considered as local variables in a specific function; and storage variables can be considered as contract-level variables.

A concrete trace of the smart contract is an alternating sequence of states and opcodes $\langle s_{0},op_{0},s_{1},op_{1},\cdots\rangle$ such that each state $s_{i}$ is of the form $(pc_{i},S_{i},M_{i},R_{i})$ where $pc_{i}\in N$ is the program counter; $S_{i}$ is the valuation of the stack variables; $M_{i}$ is the valuation of the memory variables; and $R_{i}$ is the valuation of the storage variables. Note that the initial state $s_{0}$ is $(0,S_{0},M_{0},R_{0})$ where $S_{0}$, $M_{0}$ and $R_{0}$ are the initial valuation of the variables defined by $init$. Furthermore, for all $i$, $(pc_{i+1},S_{i+1},M_{i+1},R_{i+1})$ is the result of executing opcode $op_{i}$ given the state $(pc_{i},S_{i},M_{i},R_{i})$ according to the semantic of $op_{i}$. The semantics of opcodes are shown in Figure 3 in form of execution rules, each of which is associated with a specific opcode. Each rule is composed of multiple conditions above the line and a state change below the line. The state change is read from left to right, i.e., the state on the left changes to the state on the right if the conditions above the line are satisfied. Note that this formal semantics is based on the recent effort on formalizing Etherum [12].

Most of the rules are self-explanatory and thus we skip the details and refer the readers to [12]. It is worth mentioning how external calls are abstracted in our semantic model. Given an external function call (i.e., opcode CALL), the execution temporarily switches to an execution of the invoked contract. The result of the external call, abstracted as $res$, is pushed to the stack.

In order to define our problem, we must define the kinds of vulnerabilities that we focus on. Intuitively, we say that a smart contract suffers from certain vulnerability if there exists an execution of the smart contract that satisfies certain constraints. In the following, we extend the concrete traces to define symbolic traces of a smart contract so that we can define whether a symbolic trace suffers from certain vulnerability.

To define symbolic traces, we first extend the concrete values to symbolic values. Formally, a symbolic value has the form of $op(operand_{0},\cdots,operand_{n})$ where $op$ is an opcode and $operand_{0},\cdots,operand_{n}$ are the operands. Each operand may be a concrete value (e.g., an integer number or an address) or a symbolic value. Note that if all operands of an opcode are concrete values, the symbolic value is a concrete value as well, i.e., the result of applying $op$ to the concrete operands. For instance, ADD(5,6) is $11$. Otherwise, the value is symbolic. One exception is that if $op$ is MLOAD or SLOAD, the result is symbolic even if the operands are concrete, as it is not trivial to maintain the concrete content of the memory or storage. For instance, loading a value from address 0x00 from the storage results in the symbolic value SLOAD(0x00) and increasing the value at storage address 0x00 by 6 results in a symbolic value ADD(SLOAD(0x00),0x06). For another instance, the result of symbolically executing SHA3(n,p) is SHA3(MLOAD(n,p)), i.e., the SHA3 hash of the value located from address $n$ to $n+p$ in the memory.

With the above, a symbolic trace is an alternating sequence of states and opcodes $\langle s_{0},op_{0},s_{1},op_{1},\cdots\rangle$ such that each state $s_{i}$ is of the form $(pc_{i},S_{i}^{s},M_{i}^{s},R_{i}^{s})$ where $pc_{i}$ is the program counter; $S_{i}^{s}$, $M_{i}^{s}$ and $R_{i}^{s}$ are the valuations of stack, memory and storage respectively. Note that $S_{i}^{s}$, $M_{i}^{s}$ and $R_{i}^{s}$ may hold symbolic values as well as concrete ones. For all $i$, $(pc_{i+1},S_{i+1}^{s},M_{i+1}^{s},R_{i+1}^{s})$ is the result of executing opcode $op_{i}$ symbolically given the state $(pc_{i},S_{i}^{s},M_{i}^{s},R_{i}^{s})$.

A symbolic execution engine is one which systematically generate the symbolic traces of a smart contract. Note that different from concrete execution, a symbolic execution would generate two traces given an if-statement, one visits the then-branch and the other visits the else-branch. Furthermore, in the case of an external call (i.e., CALL), instead of switching the current execution context to another smart contract, we can simply use a symbolic value to represent the returned value of the external call.

Intuitively, a vulnerability occurs when there are dependencies from certain critical instructions (e.g., CALL and DELEGATECALL) to a set of specific instructions (e.g., ADD, SUB and SSTORE). Therefore, to define our problem, we first define (control and data) dependency, based on which we define the vulnerabilities.

Figure 4 illustrates an example of control dependency. The source code is shown on the top and the corresponding control flow graph is shown on the bottom. All variables and their symbolic values are summarized in Table II. The source code presents secure steps to transfer _value tokens from msg.sender account to _to account. There are 3 then-branches followed by 2 storage updates. According to the definition, both SSTORE₃ and SSTORE₄ are control-dependent on ISZERO₁, ISZERO₂ and GT₀.

Figure 4 also illustrates an example of data dependency. Opcode ISZERO₁ and ISZERO₂ are data-dependent on SSTORE₃ and SSTORE₄. It has 2 traces, i.e., one trace loads data from storage address SHA3(MLOAD(0x00,0x40)) which is written by SSTORE₁ and SSTORE₂ in another trace.

We say an opcode $op_{j}$ is dependent on opcode $op_{i}$ if $op_{j}$ is control or data dependent on $op_{i}$ or $op_{j}$ is dependent on an opcode $op_{k}$ such that $op_{k}$ is dependent on $op_{i}$.

Let $C$ be a set of critical opcodes which contains CALL, CALLCODE, DELEGATECALL, SELFDESTRUCT, CREATE and CREATE2, i.e., the set of all opcode associated with external calls except STATICCALL. The reason that STATICCALL is excluded from $C$ is that STATICCALL can not update storage variables of the called smart contract and thus is considered to be safe.

A smart contract suffers from intra-function reentrancy vulnerability if and only if at least one of its symbolic traces suffers from intra-function reentrancy vulnerability. The above definition is inspired from the no writes after call (NW) property [4]. It is however more accurate than NW, as it avoids violations of NW which are not considered as reentrancy vulnerability. For instance, the function shown in Figure 5 violates NW, although it is not subject to reentrancy vulnerability. It is because the external call msg.sender.call has no dependency on numWithdraw. In other words, there does not exist a dependency from $op_{c}$ to $op_{s}$.

A smart contract suffers from cross-function reentrancy vulnerability if and only if at least one of its symbolic traces suffers from cross-function reentrancy vulnerability. This vulnerability differs from intra-function reentrancy as the attacker launches an attack through two different functions, which makes it harder to detect. Figure 6 shows an example of cross-function reentrancy. The developer is apparently aware of intra-function reentrancy and thus add the modifier nonReentrant to the function withdraw for preventing reentrancy. However, reentrancy is still possible through function transfer, in which case the attacker is able to double his Ether. That is, the attacker receives Ether at line 10 and illegally transfers it to another account at line 3. Although cross-function reentrancy vulnerabilities were described in Sereum [13] and Consensys [14], our work is the first work to define it formally.

A smart contract suffers from dangerous tx.origin vulnerability if and only if at least one of its symbolic traces suffer from dangerous tx.origin vulnerability. This vulnerability happens due to an incorrect usage of the global variable tx.origin to authorize an user. An attack happens when a user $U$ sends a transaction to a malicious contract $A$, which intentionally forwards this transaction to a contract $B$ that relies on a vulnerable authorization check (e.g., require(tx.origin == owner)). Since tx.origin returns the address of $U$, contract $A$ successfully impersonates $U$. Figure 7 presents an example suffering from dangerous tx.orgin vulnerability, i.e., a malicious contract may impersonate the owner to withdraw all Ethers.

A smart contract suffers from arithmetic vulnerability if and only if at least one of its symbolic traces suffer from arithmetic vulnerability. Intuitively, this vulnerability occurs when an external call data-depends on an arithmetic operation (e.g., addition, subtraction, or multiplication). For instance, the example in the Figure 2 is vulnerable due to the presence of data dependency between the external call at line 17 and the expression weeklyLimit - getThisWeekBurnedAmount() at line 12. Arithmetic vulnerabilities are the target of multiple tools designed for vulnerability detection. In general, arithmetic vulnerability detection using static analysis often results in high false positive. Therefore, tools such as Securify [4] and Ethainter [5] do not support this vulnerability in spite of its importance. In the above definition, we focus on only critical arithmetic operations to reduce false positives. That is, an arithmetic operation is not considered critical as long as the smart contract does not spread its wrong computation to other smart contracts through external calls. For instance, wrong ERC20 token transfer (e.g., CVE-2018-10376) is not critical because it can be reverted by the contract’s admin, whereas wrong Ether transfer is irreversible.

Note that our definitions of vulnerabilities are based on symbolic traces. Thus, in this first step, we set out to collect a set of symbolic traces $Tr$. As defined in Section III-B, a symbolic trace is a sequence of the form $\langle s_{0},op_{0},\cdots,s_{n},op_{n},s_{n+1}\rangle$. In the following, we focus on symbolic traces that are maximum, i.e., the last opcode $op_{n}$ is either REVERT, INVALID, SELFDESTRUCT, RETURN, or STOP.

Systematically generating the maximum symbolic traces is straightforward in the absence of loops, i.e., we simply apply the symbolic semantic rules iteratively until it terminates. In the presence of loops, however, as the condition to exit the loop is often symbolic, this procedure would not terminate. This is a well-known problem for symbolic execution and the remedy is typically to bound the number of iterations heuristically. Such an approach however does not work in our setting, since we must identify all data/control dependency to identify all potential vulnerabilities. In the following, we establish a bound on the number of iterations on the loops which we prove is sufficient for identifying the vulnerabilities that we focus on.

Given a smart contract ${\cal S}=(Var,init,N,i,E)$, a loop is in general a strongly connected component in ${\cal S}$. Thanks to structural programming, we can always identify the loop heads, i.e., the control location where a while-loop starts or a recursive function is invoked. In the following, we associate each location $n\in N$ with a bound, denoted as $bound(n)$. If $n$ is a loop head, $bound(n)$ intuitively means how many times $n$ has to be visited in at least one of symbolic traces we collect. If $n$ is not part of any strongly connected component, we have $bound(n)=1$. Otherwise, $bound(n)$ is defined as follows.

• •

  If $(n,op_{n},n^{\prime})\in E$ and $n^{\prime}$ is the loop head, $bound(n)=0$ if $op_{n}$ is not an assignment; otherwise $bound(n)=1$.

• •

  If $(n,op_{n},n^{\prime})\in E$, $n^{\prime}$ is not the loop head and there is no $m$ such that $(n,op_{n},m)\in E$, i.e., $n$ is not branching, $bound(n)=bound(n^{\prime})$ if $op_{n}$ is not an assignment; otherwise $bound(n)=bound(n^{\prime})+1$.

• •

  If $(n,op_{n},m_{0})\in E$ and $(n,op_{n},m_{1})\in E$, i.e., $n$ is branching, $bound(n)=bound(m_{1})+bound(m_{2})$.

Intuitively, the bound of a loop head is computed based on the number of branching statements and assignment statements inside the loop. That is, the bound of a loop head $n$ can be computed by traversing the CFG in the reverse order, i.e., from the exiting nodes of the loop to $n$. Every execution path maintains a bound, which equals to the number of assignment statements in that path. If two execution paths meet at a branching statement then the new bound is set to the sum of their bounds. In our implementation, the bounds for every node $n\in N$ are statically computed using a fixed-point algorithm, with a complexity of $\mathcal{O}((\#N)^{2})$ where $\#N$ is the number of nodes. Once the bounds are computed, we systematically enumerate all maximum symbolic traces such that each loop head $n$ is visited at most $bound(n)$ times. It is straightforward to see that this procedure always terminates and returns a finite set of symbolic traces.

The following establishes the soundness of our approach, i.e., using the bounds, we are guaranteed to never miss any of the 4 kinds of vulnerabilities that we focus on.

We sketch the proof in the following. All vulnerabilities in Section III are defined based on control/data dependency between opcodes. That means we always have a vulnerable trace, if there is, one as long as the set of symbolic traces we collect exhibit all possible dependency between opcodes. To see that all dependencies are exhibited in the traces we collect, we distinguish two cases. All control dependency between opcodes are identified as long as all possible branches in the smart contract are executed. This condition is satisfied based on the way we collect traces in $Tr$. This argument applies to data dependency between opcodes which do not belong to any loop as well. Next, we consider the data dependency between opcodes inside a loop. Note that with each loop iteration, there are two possible cases: no new data dependency is identified (i.e., the data dependency reaches fixed point) or at least 1 new dependency is identified. If the loop contains $n$ assignments, in the worst case, all of these opcodes depend on each other and we need a trace with $n$ iterations to identify all of them. Based on how we compute the bound for the loop heads, the trace is guaranteed to be in $Tr$. Thus, we establish that the above lemma is proved.

It is well-known that symbolic execution engines may suffer from the path explosion problem. sGuard is not immune as well, i.e., the number of symbolic paths explored by sGuard is in general exponential in the loop bounds. Existing symbolic execution engines address the problem by allowing users to configure a bound $K$ which is the maximum number of times any loop is unrolled. In practice, it is highly non-trivial to know what $K$ value should be used. Given the impact of $K$, i.e., the number of paths are exponential in the value of $K$, existing tools often set $K$ to be a small number by default, such as 3 in sCompile [16] and 5 in Manticore [17]; and it is unlikely that users would configure it differently. While having a large $K$ leads to the path explosion problem, having a small $K$ leads to false negatives. For instance, with $K=3$, the overflow vulnerabilities due to the two expressions $m=n+1$, $n=x+1$ in the Figure 8 would be missed as this bound is not sufficient to infer dependency from variable $x$ on $m$ and $n$. In contrast, sGuard automatically identifies a loop bound for each loop which guarantees that no vulnerabilities are missed. In Section V, we empirically evaluate whether the path explosion problem occurs often in practice.

Given the set of symbolic traces $Tr$, we then identify dependency between all opcodes in every symbolic trace in $Tr$, with the aim to check whether the trace suffers from any vulnerability. In the following, we present our approach to capture dependency from symbolic traces.

Given a symbolic trace $Tr$, an opcode $op_{i}$, we aim to identify a set of opcodes $dp$ in $Tr$ such that: (soundness) for all $op_{k}$ in $dp$, $op_{i}$ depends on $op_{k}$; and (completeness) for all $op_{k}$ in $Tr$, if $op_{i}$ depends on $op_{k}$ then $op_{k}\in dp$. To identify $dp$, we systematically identify all opcodes that $op_{i}$ is control-dependent on in $Tr$, all opcodes that $op_{i}$ is data-dependent on in $Tr$ and then compute their transitive closure.

To systematically identify all control-dependency, we build a control flow graph (CFG) from $Tr$ (as shown in Algorithm 2). Afterwards, we build a post-dominator tree based on the CFG using a workList algorithm [18]. The result is a set $PD(op_{i})$ which are the opcodes that post-dominate $op_{i}$. The set of opcodes which $op_{i}$ control-depend on in the symbolic trace $tr$ is then systematically identified as the following.

where $succs(op)$ returns successors of $op$ according to CFG.

Identifying the set of opcodes which $op_{i}$ is data-dependent on is more complicated. Data dependency arises from 3 data sources, i.e., stack, memory and storage. In the following, we present our over-approximation based algorithm which traces data-flow on these data sources in order to capture data dependency. Although an opcode typically reads and writes data to the same data source, an opcode may write data to a different data source in some cases. That makes data-flow tracing complicated, i.e., data flows from stack to memory through MSTORE, memory to stack through MLOAD, stack to storage through SSTORE and storage to stack through SLOAD. Since only assignment opcodes (i.e., SWAP, MSTORE, and SSTORE) create data dependency, we thus design an algorithm to identify data-dependency based on the assignment opcodes in $tr$. The details are presented in the Algorithm 3, which takes a symbolic trace $tr$ and opcode $op_{i}$ as input and returns a set of opcodes that $op_{i}$ is data-dependent on.

Algorithm 3 systematically identifies those opcodes in $tr$ which taint $op_{i}$. An opcode $op_{j}$ is said to taint another opcode $op_{i}$ if $op_{i}$ reads data from stack indexes written by $op_{j}$, or there exists an opcode $op_{t}$ such that $op_{j}$ taints $op_{t}$ and $op_{t}$ taints $op_{i}$. For each $op_{j}$ that taints $op_{i}$, there are three possible dependency cases.

• •

  Stack dependency: $op_{i}$ is data-dependent on $op_{j}$ if $op_{j}$ is an assignment opcode (i.e., SWAP) (lines 3-4)

• •

  Memory dependency: $op_{j}$ is data-dependent on $op_{k}$ if $op_{j}$ reads data from memory which was written by the assignment opcode $op_{k}$ (i.e., MSTORE) (lines 5-7)

• •

  Storage dependency: $op_{j}$ is data-dependent on $op_{k}$ if $op_{j}$ reads data from storage which was written by the assignment opcode $op_{k}$ (i.e., SSTORE) (lines 8-12)

Note that the algorithm is recursive, i.e., if $op_{k}$ is added into the set of opcodes to be returned, a recursive call is made to further identify those opcode that $op_{k}$ is data-dependent on (lines 7 and 12). Further note that since storage is globally accessible, the analysis may be cross different traces in $Tr$ (line 11).

Algorithm 3 in general over-approximates. For instance, because memory and storage addresses are likely symbolic values, a reading address and a writing address are often incomparable, in which case we conservatively assume that the addresses may be the same. In other words, $R(op_{j})\cap W(op_{k})\neq\emptyset$ is true if either $R(op_{j})$ or $W(op_{k})$ is a symbolic address.

Once the dependencies are identified, we check whether each symbolic $tr$ suffers from any of the vulnerabilities defined in Section III-C and then fix the smart contract accordingly. In general, a smart contract is fixed as follows. Given a vulnerable trace $tr$, according to our definitions in Section III-C, there must be an external call $op_{c}\in C$ in $tr$. Furthermore, there must be some other opcode $op$ that $op_{c}$ depends on which together makes $tr$ vulnerable (e.g., if $op$ is SSTORE, $tr$ suffers from reentrancy vulnerability; if $op$ is ADD, SUB, MUL or DIV, $tr$ suffers from arithmetic vulnerability). The idea is to introduce runtime checks right before $op$ so as to prevent the vulnerability. According to the type of vulnerability, the runtime checks are injected as follows.

• •

  To prevent intra-function reentrancy vulnerability, we add a modifier nonReentrant to the function $F$ containing $op$. Note that the nonReentrant modifier works as a mutex which blocks an attacker from re-entering $F$. To prevent cross-function reentrancy vulnerability, we add the modifier nonReentrant to the function containing $op$. The details of the fixing algorithm are presented in Algorithm 4 which takes a vulnerable trace $tr$ and the dependency relation $dp$ as inputs.

• •

  To fix dangerous tx.origin vulnerability, we replace $op$ (i.e., ORIGIN) with msg.sender which returns address of the immediate account that invokes the function.

• •

  To fix arithmetic vulnerability, we replace $op$ (i.e., ADD, SUB, MUL, DIV, or EXP) with a call to a safe math function which checks for overflow/underflow before performing the arithmetic operation.