solc-verify: A Modular Verifier for Solidity Smart Contracts

TL;DR

solc-verify is a source-level verification tool for Ethereum smart contracts written in Solidity, enabling automated reasoning about contract correctness and properties through modular analysis and SMT solvers.

Contribution

It introduces a modular verification approach at the Solidity source level, integrating annotations for automated property verification of smart contracts.

Findings

Successfully verified real-world smart contracts.

Effectively identified bugs in Solidity code.

Proved complex properties with minimal user input.

Abstract

We present solc-verify, a source-level verification tool for Ethereum smart contracts. Solc-verify takes smart contracts written in Solidity and discharges verification conditions using modular program analysis and SMT solvers. Built on top of the Solidity compiler, solc-verify reasons at the level of the contract source code, as opposed to the more common approaches that operate at the level of Ethereum bytecode. This enables solc-verify to effectively reason about high-level contract properties while modeling low-level language semantics precisely. The contract properties, such as contract invariants, loop invariants, and function pre- and post-conditions, can be provided as annotations in the code by the developer. This enables automated, yet user-friendly formal verification for smart contracts. We demonstrate solc-verify by examining real-world examples where our tool can effectively find bugs and prove correctness of non-trivial properties with minimal user effort.

Tables

Table 1. Table 1: Etherscan results with different solvers and arithmetic encodings. Each cell represents the number of successfully processed contracts (of 7836 total) and the average execution time per contract.

Encoding	int	bv	mod	mod-overflow
Translated	4096	3919	3926	3926
cvc4	4090 (0.71s)	3837 (0.99s)	3921 (0.72s)	3911 (0.79s)
yices2	3892 (1.15s)	3854 (0.86s)	3903 (0.75s)	3859 (0.87s)
z3	3897 (1.24s)	3831 (1.10s)	3892 (0.87s)	3894 (0.88s)

Full text

1 Introduction

Distributed blockchain-based applications are gaining traction as a secure and trustless alternative to more centralized solutions that require trusted intermediaries such as banks. The focus of early blockchain implementations, such as Bitcoin [34], was to provide the infrastructure for one particular application: digital money (cryptocurrency). Public blockchains allow arbitrary parties to transact with each other in a secure and trustless manner, with no central authority. In this setting a blockchain is a distributed ledger of transactions, where nodes in a peer-to-peer network are processing and validating transactions to maintain integrity. The next step in the evolution of blockchains was to extend the blockchain to a setting where the digital money can also be programmable. This is achieved by generalizing the ledger to allow deployment of programs (termed smart contracts [39]) that operate over ledger data. Blockchains with support for smart contracts provide a general distributed computing platform and allow a set of mutually distrusting parties to execute and enforce their contractual terms (expressed as code) automatically. At the moment, the most popular such platform is the Ethereum blockchain [41, 3].

However, smart contracts are often prone to errors with potentially devastating financial effects (see, e.g., [4] for a survey). The infamous DAO bug [16] is an illustrative example of the difficulties involved in deploying a smart contract. The DAO was a relatively small contract (2KLOC of Solidity code) that was heavily scrutinized by the wider Ethereum community before deployment. Nevertheless, an attacker managed to exploit a subtle reentrancy bug to steal $60M worth of cryptocurrency. Examples such as the DAO highlight the mission-critical nature of smart contracts. Although the code of the contract is usually small by the standards of modern software, if the contract attracts a large amount of investment, the code carries a significant amount of value per line of code. Moreover, since the contract code is stored on the blockchain, once deployed, the code is immutable and making upgrades or bug-fixes is impossible without complex solutions that involve a central authority. There has been a great interest in applying formal methods to verify smart contracts [4, 23, 32]. While there are ongoing projects based on identifying specific vulnerability patterns [8, 22, 40, 29, 35, 13, 20], theorem provers [24, 25, 37], finite automata [30, 1] or SMT [2, 26, 27], they all have limitations in terms of scalability, precision, expressiveness and ease of use.

In this paper we present solc-verify, a tool for formal verification of Ethereum smart contracts that integrates seamlessly with developer tools. solc-verify follows the modular software verification approach (e.g., VCC [11], HAVOC [10], and ESC/Java [21]), in the context of Solidity. Given a Solidity contract, annotated with specifications, solc-verify translates the contract into the Boogie intermediate verification language [15, 28], and discharges verification conditions by SMT solvers [7]. Developers can define the expected behavior of their contracts using annotations within the contract code, including assertions, contract and loop invariants, and function pre- and post-conditions. Verification of smart contracts brings domain-specific challenges. To start with, the semantics of Solidity include Ethereum-specific constructs such as the blockchain state, transactions, and data-types not common in general programming languages. As an example, Ethereum smart contracts generally operate on 256-bit integers, making precise reasoning about low-level properties, such as the absence of overflows, infeasible with standard SMT techniques. Furthermore, some common high-level properties of smart contracts, such as “the sum of user balances is always equal to the total supply”, cannot be expressed in first-order logic or in Solidity, and therefore need domain-specific treatment. solc-verify addresses these issues through an SMT-friendly encoding of Solidity into Boogie that is expressive enough to capture the properties of interest, and takes advantage of recent advances in SMT solving to enable effective reasoning. We describe solc-verify through examples and demonstrate how solc-verify can both find non-trivial bugs in real-world examples and prove correctness after the bugs have been fixed (e.g., the BEC token [36] hack). As far as we know, solc-verify is the first tool that allows specification and modular verification of Solidity smart contracts that is practical and automatic. solc-verify is implemented as an add-on to the open-source Solidity compiler and is available on GitHub.111https://github.com/SRI-CSL/solidity

2 Background

Ethereum.

Ethereum [41, 3] is a generic blockchain-based distributed computing platform. The Ethereum ledger is a storage layer for a database of accounts and data associated with those accounts, where each account is identified by its address. Ethereum contracts are usually written in a high-level programming language, most notably Solidity [38], and then compiled into the bytecode of the Ethereum Virtual Machine (EVM). A compiled contract is deployed to the blockchain using a special transaction that carries the contract code and sets up the initial state with the constructor. At that point the deployed contract is issued an address and stored on the ledger. From then on, the contract is publicly accessible and its code cannot be modified. A user (or another contract) can interact with a contract through its public API by calling public functions. This can be done by issuing a transaction with the contract’s address as the recipient. The transaction contains the function to be called along with the arguments, and an execution fee called gas. Optionally, some value of Ether (the native currency of Ethereum) can also be transferred with transactions. The Ethereum network then executes the transaction by running the contract code in the context of the contract instance. During their execution, each instruction costs some predefined amount of gas. If the contract overspends its gas limit, or there is a runtime error (e.g., an exception is thrown, or an assertion is triggered), the entire transaction is aborted and has no effect on the ledger (apart from charging the sender for the used gas).

Solidity.

Figure 2 shows a Solidity contract SimpleBank that illustrates some of the common features that Ethereum contracts use in practice. A contract can have state variables, which define the persistent data that the contract will store on the ledger. The state of SimpleBank consists of a single variable balances, which is a mapping from addresses to 256-bit integers. Further Solidity types include value types, such as Booleans, signed and unsigned integers (of various bit-lengths), addresses, fixed-size arrays, enums, and reference types, to be used with arbitrary-size arrays and structures. Once deployed, an instance of SimpleBank will be assigned its address and since no constructor is provided, its data will be initialized to default values (in this case an empty mapping).

Contracts define functions that can act on their state. Functions can receive data as arguments, perform computation, manipulate the state variables and interact with other accounts. In addition to declared parameters, functions also receive a msg structure that contains the details of the transaction. Our example contract defines two public functions deposit and withdraw. The deposit function is marked as public and payable, meaning that it can be called by anyone and is allowed to receive Ether as part of the call. This function reads the amount of Ether received from msg.value and adds it to the balance of the caller, whose address is available in msg.sender. The withdraw function allows users to withdraw a part of their bank balance. The function first checks that the sender’s balance in the bank is sufficient using a require statement. If the condition of require fails, the transaction is reverted with no effect. Otherwise the function sends the required amount of Ether funds by using a call on the caller address with no arguments (denoted by the empty string). The amount to be transferred is set with the value function. The recipient of the call can be another contract that can perform arbitrary actions on its own (within the gas limits) and can also fail (indicating it in the return value). If call fails, the whole transaction is reverted with an explicit revert, otherwise the balance of the caller is deducted in the mapping as well.

SimpleBank contains a classic reentrancy vulnerability that can be exploited to steal funds from the bank. As the control is transferred to the caller in line 11, before their balance is deducted in line 14, they are free to make another call to withdraw to perform a double (or multiple) spend. Although this flaw seems basic, it is the issue that lead to the loss of funds in the DAO hack [16].

3 Overview and Features

solc-verify is implemented as an extension to the Solidity compiler. It takes a set of Solidity contracts including specification annotations and discharges verification conditions using the Boogie verifier and SMT solvers. An overview of the architecture is shown in Figure 3.

Specification.

Solidity provides only a few error handling constructs (e.g., assert, require) for the programmer to specify expected behavior. Therefore, solc-verify supports in-code annotations to specify contract properties, as illustrated in Figure 2. Annotations are side-effect free Solidity expressions, which can reference any variable in the scope of the annotated element. Contract-level invariants (line 1) must hold before and after the execution of every public function and after the contract constructor. Non-public functions are inlined to a depth of one by default, but can also be specified with pre- and postconditions (lines 6–7). Moreover, loop invariants (line 16) can be attached to loops. As an extension, we also provide a special sum function over collections (arrays and mappings) in the specification language, as seen for example for SimpleBank in Figure 2. The sum function is modeled internally by associating a ghost variable to the collection tracked by the sum: each collection update also updates the ghost variable. This encoding is a sufficient abstraction for our needs.

Correctness.

solc-verify targets functional correctness of contracts with respect to completed222Due to the usage of gas, total and partial correctness are equivalent. Furthermore, currently we do not model gas: running out of gas does not affect correctness as the transaction is reverted. However, we might model it in the future in order to verify liveness properties or to be able to specify an upper bound. transactions and different types of failures. An expected failure is a failure due to an exception deliberately thrown to guard from the user (e.g., require, revert). An unexpected failure is any other failure (e.g., assert, overflow). We say that a contract is correct if all transactions (public function calls) that do not fail due to an expected failure also do not fail due to an unexpected failure and satisfy their specification.

Translation to Boogie.

solc-verify relies on the Solidity compiler that parses the contracts and builds an abstract syntax tree (AST) where names, references and types are resolved. solc-verify then traverses the internal AST and produces a Boogie [15, 28] representation of the program. We discuss the details and properties of the translation in more detail in Section 4.

Boogie and SMT.

Boogie transforms the program into verification conditions (VCs) and discharges them using SMT solvers. By default, Boogie can use z3 [33] and cvc4 [6] but we also extended it to support yices2 [18]. A notable feature of our encoding is that it allows quantifier-free VC generation, permitting to use SMT solvers that do not support quantifiers (e.g., yices2). Boogie reports violated annotations and failing assertions in the Boogie program and solc-verify maps these errors back to the Solidity code using traceability information. The final output of solc-verify is a list of errors corresponding to the original contracts (e.g., line numbers, function names).

4 Translation Details and Properties

The core of solc-verify is a translation from Solidity contracts to the Boogie IVL, supporting a majority of the Solidity language.333The paper and the experiments are based on compiler version v0.4.25, but we keep solc-verify up to date with the latest development branch.

Contracts.

The input of the translation is a collection of contracts to be verified and the output is a single Boogie program with all contracts. solc-verify can reason about single and multiple contracts as well. If the code of all contracts is available, solc-verify can take all available annotations into account when reasoning. However, this can be unsafe as EVM addresses are not typed (any address can be cast to a contract type) and is to be used with care. solc-verify also supports inheritance by relying on the compiler to perform flattening and virtual-call disambiguation.

Types.

solc-verify supports basic Solidity types such as Booleans, integers and addresses. Several modes are provided for modeling arithmetic operations that can be selected by the user. In the simplest mode, integers are unbounded mathematical integers. This mode does not capture the exact semantics of the operations (e.g., overflows) but is scalable and well supported by SMT solvers. Precise arithmetic can be provided by relying on the SMT theory of bitvectors. solc-verify supports this mode but can suffer from scalability issues due to the 256-bit default integer size of Solidity. In order to provide both precision and scalability, solc-verify provides a modular arithmetic mode that encodes arithmetic operations using mathematical integers with range assertions and precise wraparound semantics of all operations. Addresses are modeled with uninterpreted symbols as they can only be queried for equivalence. solc-verify also supports mappings and arrays using SMT arrays [31, 14]. Structures, enumerations and tuples are currently not supported but there are no technical difficulties in supporting them and they are planned in the future. Events (a logging mechanism) are ignored as they are not relevant for functional correctness.444We might model events in the future to be able to specify that an event is expected to be triggered.

State Variables.

State variables are mapped to global variables in Boogie. However, multiple instances of a contract can be deployed to the blockchain at different addresses. Since aliasing of contract storage is not possible, solc-verify models each state variable as a one-dimensional global mapping from contract addresses to their respective type (in essence treating the blockchain as a heap in a Burstall-Bornat model [9]). For example, the state variable x with type int at line 2 of Figure 4 (left) is transformed to the global variable x with mapping type [address]int at line 1 of Figure 4 (right).

Functions.

Each function in Solidity is translated to a procedure in Boogie with an additional implicit receiver parameter [5] called _this, which identifies the address of the contract instance. As an example, consider the set function of the Solidity contract A in Figure 4. Updating x in the Boogie program becomes an update of the map x using the receiver parameter _this. Consider also the call a.set(x) in the Solidity function setXofA. The Boogie program first gets the address of the A instance corresponding to the current B instance using a[_this]. Then it passes this address to the receiver parameter of the function set.

Functions can be declared view (cannot write state) or pure (cannot read or write state), but these restrictions are checked by the compiler. Additional user-defined function modifiers are a language feature of Solidity to alter or extend the behavior of functions. In practice, modifiers are commonly used to weave in extra checks and instructions to functions. For example, the pay function in Figure 5 (left) includes the modifier onlyOwner (defined in line 4), which performs an extra check before calling the actual function (denoted by the placeholder _). solc-verify simply inlines statements of all modifiers of a function to obtain a single Boogie procedure (e.g., pay procedure in Figure 5 right).

Statements and expressions.

Most of the Solidity statements and expressions can be directly mapped to a corresponding statement or expression in Boogie with the same semantics, including variable declarations, conditionals, while loops, calls, returns, indexing, unary/binary operations and literals. There are also some statements and expressions that require a simple transformation, such as mapping for loops to while loops or extracting nested calls and assignments within expressions to separate statements using fresh temporary variables. solc-verify currently does not support inline assembly and creating new contracts from within another contract (new expressions). Furthermore, the availability of some arithmetic operations depends on the expressiveness of the underlying domain (e.g., bitwise operations).

Transactions.

Solidity includes Ethereum-specific functions and variables to query and manipulate balances and transactions. Some examples can be seen in Figure 5 (left) with the corresponding translation in Figure 5 (right). Each address is associated with its balance, which can be queried using the balance member of the address. Correspondingly, solc-verify keeps track of the balances in a global mapping from addresses to integers (line 1 of Figure 5 right).

Solidity offers the msg.sender field within functions (line 5 of Figure 5 left) to access the caller address. solc-verify maps this to Boogie by adding an extra parameter _msg_sender of type address to each procedure. When a procedure calls another, the current receiver address (_this) is passed in as the sender.

Solidity functions marked with the payable keyword (line 8 of Figure 5 left) are capable of receiving Ether when called. The amount of Ether received can be queried from the msg.value field. solc-verify models this in Boogie by including an extra parameter _msg_value and updating the global balances map at the beginning of the corresponding Boogie procedure (line 6 of Figure 5 right). When calling a payable function in Solidity, the amount of Ether to be transferred can be set with the special value function (e.g., line 11 of Figure 2). solc-verify translates this to Boogie by reducing the balance of the caller before making the call and passing the value as the _msg_value argument.

The functions send and transfer are dedicated functions to transfer Ether between addresses. solc-verify inlines these functions by manipulating the global mapping of balances directly. If the recipient is a contract, a special fallback function is executed, but the gas passed is limited to raising events, which is irrelevant for functional correctness.555Gas costs of certain write operations were about to change with Constantinople, allowing a reentrancy attack, but it was reverted with the St. Petersburg upgrade [19]. For example, the transfer in line 12 of Figure 5 (left) is mapped to lines 11–13 on the right. The sender not having enough funds is an expected transaction failure, which is modeled with an assumption.

The function call can call a function by its name on any address and can also pass arbitrary data. Since there can be an unknown code behind the called address, solc-verify treats such cases as an external call that can perform arbitrary computation.666Contract invariants are also checked before external calls as they can perform a callback to the contract. solc-verify does not support low-level function calls such as callcode and delegatecall as it is considered dangerous and would require encoding of the EVM details (contract layout, EVM semantics).

Error handling.

Solidity exceptions will undo all changes made to the global state by the current call. Deliberately thrown exceptions (require, revert, throw) are therefore mapped to assumptions in Boogie, which stop the verifier without reporting an error. Assertions are mapped to Boogie assertions, causing a reported error when their condition evaluates to false.

Detection of overflows.

Neither the EVM nor Solidity performs any checking of the results of arithmetic operations by default. Due to the wraparound semantics of integers, this allows unexpected overflows and underflows to occur undetected (e.g., the infamous BEC token [36]).

In general, overflows can be detected by checking the result of every operation after it has been computed. However, reporting every such overflow would result in an overwhelming number of false alarms. For example, it is common practice for Solidity developers to perform arithmetic operations first, and then check for overflows manually after the fact (see, e.g., line 10 of Figure 2). This practice of overflow detection is an integral part of the SafeMath library [17] that is used in almost all deployed contracts on the Ethereum blockchain and is part of Solidity best practices [12].

To reduce the number of false overflow reports, solc-verify uses the following approach. Whenever an arithmetic computation is performed, it computes the overflow condition that captures whether the overflow has occurred (i.e., if the result of the computation in modular arithmetic is different from the result over unbounded integers). However, instead of immediately checking this condition, it is accumulated in a dedicated Boolean overflow-detection variable. solc-verify then checks for overflow at the end of every basic block with an assertion. This “delayed checking” gives space to developer to perform manual checking for the overflow (in which case the assertion will not trigger) and will avoid the false alarms. For example, the potential overflow in line 9 of Figure 2 is not reported because in the very next line the programmer guards the overflow and reverts the transaction.

5 Examples and Experiments on Real World Contracts

To demonstrate solc-verify we first discuss the coverage of currently-supported language features and scalability by examining the (unannotated) contracts currently deployed on the Ethereum blockchain. We also pick a subset of the unannotated contracts and manually check what solc-verify can report on them. Finally, we examine two contracts that had been exploited in the past, and show how solc-verify could have found the issues, with minimal annotation burden, and prove that the fixed versions of the contracts are correct.

5.1 Language Coverage

To analyze the coverage of currently-supported language features and the scalability of solc-verify, we collected 37531 contracts available on Etherscan.777http://csl.sri.com/users/dejan/contracts.tar.gz These contracts were compiled with various versions of the Solidity compiler and not all of them are supported by version 0.4.25 that solc-verify used at the time of writing the paper. We therefore selected 7836 contracts that do compile. The results of running solc-verify on the selected contracts is shown in Table 1. Columns correspond to different arithmetic modes, with the last column representing modular arithmetic with overflow checking enabled. The first row shows that roughly 50% of the contracts can be successfully translated to Boogie in each mode. Contracts that cannot be translated contain constructs not yet handled by solc-verify, such as structures, enumerations or special transaction and blockchain members. Some features (e.g., exponentiation) also depend on the arithmetic mode, resulting in slight differences in feature coverage. The remaining three rows show the number of contracts for which solc-verify terminates within 10s with a given SMT solver as a backend. Note, that the effectiveness of the different SMT solvers on this set of contracts should be taken with a grain of salt. For example, the bitvector encoding seems to be nearly as efficient as modular arithmetic. However, this is because the assertions in these contracts do not depend on complex (e.g., nonlinear) arithmetic. With more complex invariants, the bitvector encoding becomes infeasible for reasoning, as we demonstrate it with the BEC token example later in this section. The takeaway of these results is that the average execution time per contract is around a second, meaning that solc-verify is applicable and effective for a significant amount of real-world contracts, but scalability might depend on the complexity of the properties.

5.2 Unannotated Contracts

The contracts available at Etherscan are not annotated and solc-verify can only consider assert and require statements, and overflows as implicit specification. Furthermore, the ground truth about the contracts (whether they are correct or not) is unknown. Nevertheless, we systematically selected a subset of the contracts and manually checked the results given by solc-verify.

We took all 3897 contracts that solc-verify could translate and process with z3 in integer mode. At the first glance we discovered that a majority of the contracts (2754) use the popular SafeMath library [17], which has just recently adopted the proper usage of assert and require.888For discussion, see https://github.com/OpenZeppelin/openzeppelin-solidity/issues/1120. We updated these contracts to properly guard against user input with require (instead of assert). Afterwards, we checked for assertion failures and overflows using solc-verify.

Assertion checking.

Surprisingly, only 88 contracts (out of the 3897) contain assertions. solc-verify reported an error for 80 contracts, which we all checked manually. Out of those errors, 78 are clearly false alarms caused by a bad specification – the developer wrote assert where require should have been used – and fit into one of the following categories:

• •

Enforcing input validity with assertion (e.g., input arrays are of equal size).

• •

Enforcing time locks with an assertion (e.g., now > 100).

• •

Enforcing success of functions calls with an assertion (e.g. addr.call()).

• •

Enforcing permissions with an assertion (e.g., checking msg.sender).

• •

Enforcing correct result of arithmetic operations with an assertion.

As described in the Solidity documentation [38] assert should only be used to check for internal errors and invariants, and all cases highlighted above should use require instead. After replacing the spurious assertions with require, solc-verify reports no false alarms.

The 2 reported errors worth discussing in more detail are illustrated in Figure 6. The example on the left is a pre-sale contract that accepts Ether until a sale cap is reached. The invariant of the contract, i.e. that (raised <= max) is enforced with a (stronger) assertion at the beginning of function. It could be argued that this fits within the mentioned prescribed usage for the assert construct. However, as solc-verify performs modular analysis, and nothing is assumed about the state before a function call, it will report such an assertion as a potential error. To fix this, the invariant (raised <= max) should be specified as a contract invariant, and require should be used to check the stronger precondition at function entry (followed by an assert at the end of the function).

The example on the right is a token transfer function. The function checks whether the sender has enough balance, and then it transfers the tokens to the recipient. Finally, the assertion checks that no overflow has occurred using an assert statement on the result of the addition. As is, solc-verify reports an error because increasing the balance of the recipient might overflow. As argued above, if the purpose of the assertion is to guard against overflows require should be used instead. On the other hand, one could argue that for fixed-cap tokens such an overflow should never occur since no address can hold enough tokens to trigger the overflow. This assumption can be explicitly specified, i.e., by stating a contract invariant sum(balances) <= cap. With this invariant, solc-verify avoids the false alarm by inferring that overflow is no longer possible.

Overflow checking.

We also checked for overflows and manually verified the results for the 68 contracts (out of 3897) that have at least 100 transactions. solc-verify reports 33 alarms of which 29 are false and 4 can be considered as real. All false alarms are due to implicit assumptions on the magnitude of used numbers. There are 20 false alarms due to missing range assumptions for array lengths causing false overflow alarms for loop counters. For example, in a loop for (uint i = 0; i < array.length; i++) {} solc-verify reports that i++ might overflow. It is reasonable to assume that array lengths remain small due to the gas costs associated with growing an array. Other false alarms are caused by implicit assumptions on Ether balances or time. For example, it is assumed that a counter for the total amount of Ether received by a contract, or multiplying msg.value by 20000 cannot overflow because the amount of Ether is limited. Similarly, adding days or even weeks to the current timestamp will not overflow any time soon. We plan to include such implicit assumptions to a limited extent but, in general, it is best if the developer explicitly specifies them. The four issues found that could be considered real are the following:

• •

A pre-sale contract sets the hardCap in its constructor based on a cap provided as argument with hardCap = cap*(10**18). Although the constructor is only called once by the deployer, providing a large cap can result in an unintentional overflow.

• •

A crowd-sale contract sets the unit cost based on the argument perEther by calculating unitCost = 1 ether / (perEther*10**8). The problematic function is guarded so that it can only be called by the contract owner. Nevertheless, overflow can happen and can lead to an inconsistent unit price.

• •

A utility contract for mass distribution of tokens has a function to transfer an array of values to an array of recipients as a batch. The total amount transferred is kept accumulated in a contract counter and can overflow. However, as the counter is not used otherwise, the overflow might be benign.

• •

A food store contract first calculates the cost based on the bundles ordered, by computing cost = bundles * price, where bundles is provided by the caller. The function then checks if msg.value >= cost holds, but this check can be bypassed with the overflow, opening the door for a potential exploit.

5.3 Annotated Contracts

While solc-verify can find violations to implicit specifications in unannotated contracts, its main target is to allow developers to check custom, high-level properties by the means of annotations. We demonstrate this by annotating two contracts, finding bugs and proving the correctness of the fixed versions.

Reentrancy detection (DAO).

Reentrancy is a common source of vulnerabilities and the cause of the infamous DAO bug [16]. As explained in Section 2, the SimpleBank contract presented in Figure 2 suffers from the same reentrancy bug. Using solc-verify, the developer can specify the consistency of the bank contract state through a contract-level invariant, and solc-verify can detect the bug. For example, we can annotate the contract with a property sum(balances) == this.balance. As the balance of the contract is deducted before the external call, the contract invariant is violated and solc-verify reports a (real) error. However, if the user fixes the issue by first reducing the balance of the recipient in the mapping and then transferring the amount, the invariant will hold before making the external call and solc-verify proves the specification successfully. For both the buggy and correct versions of the contract, the verification with solc-verify is instant.

Overflow detection (BEC token).