figure a

1 Introduction

Smart contracts are a trustless mechanism to enforce financial agreements between many users [46]. The Ethereum blockchain [52] is a popular platform for smart contract development, with most smart contracts written in Solidity. Due to their monetary nature, smart contracts have been the target of many high-profile attacks [14]. Formal verification is a promising technique to ensure the correctness of deployed contracts. However, Solidity smart contracts can address and maintain data for up to \(2^{160}\) users. Analyzing smart contracts with this many users is intractable in general, and calls for specialized techniques [51].

In this paper, we present SmartACE, an automated framework for smart contract verification. SmartACE takes as input a smart contract annotated with assertions, then checks that all assertions hold. This is in contrast to tools that check general patterns on unannotated smart contracts, such as absence of integer overflows (e.g., [47]), or access control policies (e.g., [10]). To ameliorate the state explosion induced by large numbers of users, SmartACE implements local bundle abstractions [51] to reduce verification from arbitrarily many users to a few representative users. SmartACE targets deep violations, that require multiple transactions to observe, using a variety of techniques such as model checking, fuzzing, and symbolic execution. To avoid reinventing the wheel, SmartACE models each contract in LLVM-IR [33] to integrate off-the-shelf analyzers such as SeaHorn  [21], libFuzzer  [34], and Klee  [11].

Fig. 1.
figure 1

A smart contract that implements a simple auction.

Full size image

As an example of the local bundle abstraction, consider in Fig. 1. In , each user starts with a bid of zero. Users alternate, and submit increasingly larger bids, until a designated manager stops the auction. While the auction is not stopped, a non-leading user may withdraw their bid. To ensure that the auction is fair, a manager is not allowed to place their own bid. Furthermore, the role of the manager is never assigned to the zero-account (i.e., the null user at address 0). It follows that satisfies property A0: “All bids are less than or equal to the recorded leading bid.”

In general, can interact with up to \(2^{160}\) users. However, each transaction of interacts with at most the zero-account, the auction itself, the manager, and an arbitrary sender. Furthermore, all arbitrary senders are interchangeable with respect to A0. For example, if there are exactly three active bids \(\{ 2, 4, 8 \}\) then A0 can be verified without knowing which user placed which bid. This is because the leading bid is always 8, and each bid is at most 8. Due to these symmetries between senders, it is sufficient to verify relative to a representative user from each class (i.e., the zero account, the auction itself, the manager, and an arbitrary sender), rather than all \(2^{160}\) users. The key idea is that each representative user corresponds to one or many concrete users [40].

If a representative’s class contains a single concrete user, then there is no difference between the concrete user and the representative user. For example, the zero-account and the auction each correspond to single concrete users. Similarly, the manager refers to a single concrete user, so long as the variable does not change. Therefore, the addresses of these users, and in turn, their bids, are known with absolute certainty. On the other hand, there are many arbitrary senders. Since only compares addresses by equality, the exact address of the representative sender is unimportant. What matters is that the representative sender does not share an address with the zero-account, the auction, nor the manager. However, this means that at the start of each transaction the location of the representative sender is not absolute, and, therefore, the sender has a range of possible bids. To account for this, we introduce a predicate, called an interference invariant, to summarize the bid of each sender. An example interference invariant for is A0 itself.

Fig. 2.
figure 2

A simplified test harness for of Fig. 1

Full size image

Given an interference invariant, A0 can be verified by SeaHorn. To do this, the concrete users in must be abstracted by representative users. The abstract system (see Fig. 2), known as a local bundle abstraction, assigns the zero-account to address 0, the auction to address 1, the manager to address 2, the representative sender to address 3, and then executes an unbounded sequence of transactions (all feasible sequences are included). Before each transaction, the sender’s bid is set to a nondeterministic value that satisfies its interference invariant. If the abstract system and A0 are provided to SeaHorn, then SeaHorn verifies that all states reachable in the abstract system satisfy A0. It then follows from the symmetries between senders that A0 holds for any number of users.

Prior work has demonstrated SmartACE to be competitive with state-of-the-art smart contract verifiers [51]. This paper illustrates the effectiveness of SmartACE by verifying several contracts from the popular OpenZeppelin library. For each contract, we provide specifications in the Scribble language. We report on our experience integrating Scribble with SmartACE, and describe the performance of SmartACE on each specification. As opposed to other case studies (e.g., [2, 10, 16, 17, 23,24,25,26, 30, 32, 35, 37, 45, 47,48,49]), we do not apply SmartACE to contracts scraped from the blockchain. As outlined by the methodology of [16], such studies are not appropriate for tools that require annotated contracts. Furthermore, it is shown in [23] that most contracts on the blockchain are unannotated, and those with annotations are often incorrect. For these reasons, we restrict our case studies to manually annotated contracts.

This paper makes the following contributions: (1) the design and implementation of an efficient Solidity smart contract verifier SmartACE, that is available at https://github.com/contract-ace/smartace; (2) a methodology for automatic verification of deep properties of smart contracts, including aggregate properties involving sum and maximum; and (3) a case-study in verification of two OpenZeppelin contracts, and an open-bid auction contract, that are available at https://github.com/contract-ace/verify-openzeppelin.

The rest of this paper is structured as follows. Section 2 presents the high-level architecture of SmartACE. Section 3 describes the conversion from a smart contract to an abstract model. Section 4 describes challenges and benefits in integrating SmartACE with off-the-shelf analyzers. Section 5 reports on a case study that uses SmartACE and Scribble to verify several OpenZeppelin contracts. The performance of SmartACE, and the challenges of integrating with Scribble, are both discussed.

2 Architecture and Design Principles of SmartACE

SmartACE is a smart contract analysis framework guided by communication patterns. As opposed to other tools, SmartACE performs all analysis against a local bundle abstraction for a provided smart contract. The abstraction is obtained through source-to-source translation from Solidity to a harness modelled in LLVM-IR. The design of SmartACE is guided by four principles.

  1. 1.

    Reusability: The framework should support state-of-the-art and off-the-shelf analyzers to minimize the risk of incorrect analysis results.

  2. 2.

    Reciprocity: The framework should produce intermediate artifacts that can be used as benchmarks for off-the-shelf analyzers.

  3. 3.

    Extensibility: The framework should extend to new analyzers without modifying existing features.

  4. 4.

    Testability: The intermediate artifacts produced by the framework should be executable, to support both validation and interpretation of results.

Fig. 3.
figure 3

The architecture of SmartACE for integration with SeaHorn for model checking and libFuzzer for greybox fuzzing.

Full size image
Fig. 4.
figure 4

The analysis and transformations performed by SmartACE.

Full size image

These principles are achieved through the architecture in Fig. 3. SmartACE takes as input a smart contract with Scribble annotations (e.g., contract invariants and function postconditions), and optionally an interference invariant. Scribble processes the annotated smart contract and produces a smart contract with assertions. The smart contract with assertions and the interference invariant are then passed to a source-to-source translator, to obtain a model of the smart contract and its environment in LLVM-IR (see Sect. 3). This model is called a harness. Harnesses use an interface called libVerify to integrate with arbitrary analyzers, and are therefore analyzer-agnostic (see Sect. 4). When an analyzer is chosen, CMake is used to automatically compile the harness, the analyzer, and its dependencies, into an executable program. Analysis results for the program are returned by SmartACE.

The SmartACE architecture achieves its guiding principles as follows. To ensure reusability, SmartACE uses state-of-the-art tools for contract instrumentation (Scribble), build automation (CMake), and program analysis (e.g., SeaHorn and libFuzzer). The source-to-source translation is based on the Solidity compiler to utilize existing source-code analysis (e.g., AST construction, type resolution). To ensure reciprocity, the SmartACE architecture integrates third-party tools entirely through intermediate artifacts. In our experience, these artifacts have provided useful feedback for SeaHorn development. To ensure extensibility, the libVerify interface is used together with CMake build scripts to orchestrate smart contract analysis. A new analyzer can be added to SmartACE by first creating a new implementation of libVerify, and then adding a build target to the CMake build scripts. Finally, testability is achieved by ensuring all harnesses are executable. As shown in Sect. 4, executable harnesses provide many benefits, such as validating counterexamples from model checkers, and manually inspecting harness behaviour.

3 Contract Modelling

This section describes the translation from a smart contract with annotations, to a harness in LLVM-IR. A high-level overview is provided by Fig. 4. First, static analysis is applied to a smart contract, such as resolving inheritance and over-approximating user participation (see Sect. 3.1). Next, the analysis results are used to convert each to LLVM structures and functions (see Sect. 3.2). Finally, these functions are combined into a harness that schedules an unbounded sequence of smart contract transactions (see Sect. 3.3).

3.1 Static Analysis

The static analysis in SmartACE is illustrated by the top row of Fig. 4. At a high-level, static analysis ensures that a bundle conforms to the restrictions of [51], and extracts facts about the bundle required during the source-to-source translation. Bundle facts include a flat inheritance hierarchy [5], the dynamic type of each contract-typed variable, the devirtualization of each call (e.g., [4]), and the representative users (participants) of the bundle. Key design considerations in the analysis follow.

Reducing Code Surface. SmartACE over-approximates conformance checks through syntactic rules. Therefore, it is possible for SmartACE to reject valid smart contracts due to inaccuracies. For this reason, SmartACE uses incremental passes to restrict the code surface that reaches the conformance checker. The first pass flattens the inheritance hierarchy by duplicating member variables and specializing methods. The second pass resolves the dynamic type of each contract-typed variable, by identifying its allocation sites. For example, the dynamic type for state variable in of Fig. 1 is due to the allocation on line 35. The third pass uses the dynamic type of each contract-typed variable, to resolve all virtual calls in the smart contract. For example, at line 52 devirtualizes to method of contract . The fourth pass constructs a call graph for the and methods of each smart contract. Only methods in the call graph are subject to the conformance checker.

Conformance Checking. The syntactic conformance check follows from [51] and places the following restrictions: (1) There is no inline assembly; (2) Mapping indices are addresses; (3) Mapping values are numeric; (4) Address comparisons must be (dis)equality; (5) Addresses never appear in arithmetic operations; (6) Each contract-typed variable corresponds to a single call to .

Participation Analysis. A key step in local analysis is to identify a set of representative users. A representative user corresponds to one or arbitrarily many concrete users. In the case of one concrete user, the corresponding address is either static or dynamic (changes between transactions). Classifying representative users according to this criterion is critical for local analysis. A write of v to abstract location l is said to be strong if v replaces the value at l, and weak if v is added to a set of values at locations referenced by l. It follows that a write to many concrete users is weak, whereas a write to a single concrete user is strong. Furthermore, if the address of the single concrete user is dynamic, then aliasing between representative users can occur. A representative user with weak updates is an explicit participant, as weak updates result from passing arbitrary users as inputs to transactions (e.g.,  ). A representative user with strong updates and a dynamic address is a transient participant, as dynamic addresses are maintained via roles, and may change throughout execution (e.g.,  ). A representative user with strong updates and a static address is an implicit participant, as static addresses are determined by the source text of a contract, independent of transaction inputs and roles (e.g., the zero account). SmartACE implements the algorithm from [51] that uses an intraprocedural taint analysis to over-approximate the maximum number of explicit, transient, and implicit participants. Recall that taint analysis [28] determines whether certain variables, called tainted sources, influence certain expressions, called sinks. In , tainted sources are (a) input address variables, (b) state address variables, and (c) literal addresses, while sinks are (a) memory writes, (b) comparisons, and (c) mapping accesses. An input address variable, , that taints at least one sink is an explicit participantFootnote 1. Similarly, state address variables and literal addresses that taint sinks represent transient and implicit participants, respectively. For example, on Fig. 1, computes 2 explicit participants due to and in the constructor of , 1 transient participant due to in , and 3 implicit participants due to the addresses of the zero-account, , and . This over-approximates true participation in several ways. For example, the constructor of is never influenced by the equality of and , and is always the manager of .

3.2 Source-to-Source Translation

Source-to-source translation relies on the call graph and participants obtained through static analysis. The translation is illustrated by the bottom row of Fig. 4. A translation for Fig. 1 is given in Fig. 5. Note that the C language is used in Fig. 5, rather than LLVM-IR, as C is more human-readable.

Fig. 5.
figure 5

Partial modelling of the types and methods in Fig. 1 as C code (LLVM).

Full size image

Abstract Data Types (ADTs). An ADT is either a or a . Each is translated directly to an LLVM structure. The name of the structure is prefixed by the name of its containing to avoid name collisions. Each is translated to an LLVM structure of the same name, with a field for its address ( ), a field for its balance ( ), and a field for each user-defined member variable. An example is given for at line 3.

Primitive Types. Primitive types include all integer types, along with , , and (unbounded arrays are not yet supported in SmartACE). Integer types are mapped to singleton structures, according to their signedness and bit-width. For example, the type of is mapped to (see line 5). Each type is mapped to the singleton structure , which contains the same underlying type as (see line 6). Each type is mapped to the singleton structure , which contains the same underlying type as (see line 5). Each is treated as an unsigned integer of the nearest containing bit-width. Benefits of singleton structures, and their underlying types, are discussed in Sect. 4.

Functions. Methods and modifiers are translated to LLVM functions. Methods are specialized according to the flattened inheritance hierarchy, and modifiers are specialized to each method. To avoid name collisions, each function is renamed according to the contract that defines it, the contract that is calling it, and its position in the chain of modifiers. For example, the specialization of method for is . Likewise, the specializations of method and its modifier are and , respectively. Extra arguments are added to each method to represent the current call state (see  through to  on line 9). Specifically, is , is , is , is , is , and is . A special argument, , indicates if has been added to a contract’s balance (see line 13, where is set to false). If is true, then the balance is updated before executing the body of the method (see line 30). Multiple return values are handled through the standard practice of output variables. For example, the argument in represents the second return value of .

Statements and Expressions. Most expressions map directly from Solidity to LLVM (as both are typed imperative languages). Special cases are outlined. Each maps to from libVerify, which causes a program failure given argument . Each maps to from libVerify, which reverts a transaction given argument (see line 31). For each statement, the arguments of the event are expanded out, and then a call is made to (see line 12). For each method call, the devirtualized call is obtained from the call graph, and the call state is propagated (see line 13 for the devirtualized called to ). For external method calls, and are reset.

Fig. 6.
figure 6

The control-flow of a test harness. Each \(\star \) denotes an optional step.

Full size image

Mappings. Each is translated to an LLVM structure. This structure represents a bounded mapping with an entry for each participant of the contract. For example, if a contract has N participants, then a one-dimensional will have N entries, and a two-dimensional will have \(N^2\) entries. Since types are unnamed, the name of each LLVM structure is generated according to declaration order. For example, of is the first mapping in Fig. 1, and translates to accordingly (see line 1). Accesses to are encapsulated by and (see line 26).

Strings. Each string literal is translated to a unique integer value. This model supports string equality, but disallows string manipulation. Note that string manipulation is hardly ever used in smart contracts due to high gas costs.

Addresses. Implicit participation is induced by literal addresses. This means that the value of a literal address is unimportant, so long as it is unique and constant. For reasons outlined in Sect. 3.3, it is important to set the value of each literal address programmatically. Therefore, each literal address is translated to a unique global variable. For example, translates to .

3.3 Harness Design

A harness provides an entry-point for LLVM analyzers. Currently, SmartACE implements a single harness that models a blockchain from an arbitrary state, and then schedules an unbounded sequence of transactions for contracts in a bundle. A high-level overview of this harness is given in Fig. 6. The harness for in Fig. 1 is depicted in Fig. 7.

Fig. 7.
figure 7

The harness for Fig. 1. Logging is omitted to simplify the presentation.

Full size image

Modelling Nondeterminism. All nondeterministic choices are resolved by interfaces from libVerify. and choose integers of a desired signedness and bit-width. chooses values between (inclusively) and (exclusively). chooses values larger than . In all cases, is an identifier for the call site, and is used for logging purposes.

Address Space. An abstract address space restricts the number of addresses in a harness. It assigns abstract address values to each contract address and literal address symbol. Assume that there are N contracts, M literal addresses, and K non-implicit participants. The corresponding harness has abstract addresses 0 to \((N + M + K - 1)\). Constraints are placed on address assignments to prevent impossible address spaces, such as two literal addresses sharing the same value, two contracts sharing the same value, or a contract having the same value as the zero-account. The number of constraints must be minimized, to simplify symbolic analysis. In SmartACE, the following partitioning is used. is always mapped to abstract address 0 (see line 6). Abstract addresses 1 to N are assigned to contracts according to declaration order (see lines 7–8). Literal addresses are assigned arbitrary values from 1 to \((N+M)\). This allows contracts to have literal addresses. Disequality constraints ensure each assignment is unique. Senders are then chosen from the range of non-contract addresses (see line 16).

Blockchain Model. SmartACE models , , , , and . The block number and timestamp are maintained across transactions by at line 10 and at line 12. Before transaction generation, and may be incremented in lockstep (see lines 29–33). Whenever a method is called, is chosen from the non-contract addresses (e.g., line 16). The value of is also used for (e.g., the second argument on line 22). If a method is , then is chosen by , else is set to 0 (e.g., line 17).

Transaction Loop. Transactions are scheduled by the loop on line 24. The loop terminates if from libVerify returns (this does not happen for most analyzers). Upon entry to the loop, from libVerify provides a hook for analyzer-specific bookkeeping. Interference is then checked and re-applied, provided that returns at line 27. A transaction is picked on line 36 by assigning a consecutive number to each valid method, and then choosing a number from this range. Arguments for the method are chosen using and for integer types, and for bounded types such as , and (see lines 15–19 for an example).

Interference. A harness may be instrumented with interference invariants to enable modular reasoning. Interference invariants summarize the data of all concrete users abstracted by a representative user, relative to the scalar variables in a smart contract (e.g.,  , , and in Fig. 1). An interference invariant must be true of all data initially, and maintained across each transaction, regardless of whether the representative user has participated or not. As illustrated in Fig. 6, interference is checked and then re-applied before executing each transaction. Note that checking interference after a transaction would be insufficient, as this would fail to check the initial state of each user. To apply interference, a harness chooses a new value for each mapping entry, and then assumes that these new values satisfy their interference invariants. To check interference, a harness chooses an arbitrary entry from a mapping, and asserts that the entry satisfies its interference invariant. Note that asserting each entry explicitly would challenge symbolic analyzers. For example, a two-dimensional mapping with 16 participants would require 256 assertions.

Limitations. The harness has three key limitations. First, as gas is unlimited, the possible transactions are over-approximated. Second, there is no guarantee that time must increase (i.e., a fairness constraint), so time-dependent actions may be postponed indefinitely. Third, reentrancy is not modeled [20], though this is sufficient for effectively callback free contracts as defined in [42].

4 Integration with Analyzers

CMake and libVerify are used to integrate SmartACE with LLVM analyzers. Functions from libVerify, as described in Table 1, provide an interface between a harness and an analyzer (usage of each function is described in Sect. 3). Each implementation of libVerify configures how a certain analyzer should interact with a harness. Build details are resolved using CMake scripts. For example, CMake arguments are used to switch the implementation of primitive singleton structures between native C integers and Boost multiprecision integers. To promote extensibility, certain interfaces in libVerify are designed with many analyzers in mind. A key example is bounded nondeterminism.

In libVerify, the functions and are used as sources of nondeterminism. For example, SeaHorn provides nondeterminism via symbolic values, whereas libFuzzer approximates nondeterminism through randomness. In principle, all choices could be implemented using these interfaces. However, certain operations, such as “increase the current block number,” or “choose an address between 3 and 5,” require specialized implementations, depending on the analyzer. For this reason, libVerify provides multiple interfaces for nondeterminism, such as and . To illustrate this design choice, the implementations of for SeaHorn and libFuzzer are discussed.

The interface returns a value between lo (inclusively) and hi (exclusively). Efficient implementations are given for SeaHorn and libFuzzer in Fig. 8a and Fig. 8b, respectively. The SeaHorn implementation is correct, since failed assumptions in symbolic analysis simply restrict the domain of each symbolic variable. Intuitively, assumptions made in the future can influence choices made in the past. This design does not work for libFuzzer, as failed assumptions in libFuzzer simply halt execution. This is because all values in libFuzzer are concrete. Instead, a value is constructed between lo and hi through modular arithmetic. In contrast, many symbolic analyzers struggle with non-linear constraints such as modulo. Therefore, neither implementation is efficient for both model checking and fuzzing.

Table 1. Summary of the libVerify interface.
Full size table

SmartACE has been instantiated for greybox fuzzing, bounded model checking (BMC), parameterized compositional model checking (PCMC), and symbolic execution. The current version of libVerify supports libFuzzer for fuzzing, SeaHorn for model checking, and Klee for symbolic execution. Other analyzers, such as AFL  [54] and SMACK  [13], can also be integrated by extending libVerify. Each implementation of libVerify offers unique analysis benefits.

Interactive Test Harness. A default implementation of libVerify provides an interactive test harness. Nondeterminism, and the return values for , are resolved through standard input. Events such as are printed to standard output. The hook is used to collect test metrics, such as the number of transactions. As mentioned in Sect. 2, providing an interactive harness improves the testability of SmartACE.

Greybox Fuzzing. Fuzzing is an automated testing technique that explores executions of a program via input generation [38]. In greybox fuzzing, coverage information is extracted from a program to generate a sequence of inputs that maximize test coverage [56]. The harness for greybox fuzzing is instantiated with N participants, and each participant has strong updates. In general, greybox fuzzing is a light-weight technique to test edge-cases in contracts. As opposed to other smart contract fuzzing techniques, SmartACE performs all fuzzing against a local bundle abstraction. This ensures that all implicit participants are in the address space. To illustrate the benefit of local bundle abstractions in fuzzing, consider the property for Fig. 1: “The user with address 100 never places a bid.”. Without a local bundle abstraction, a counterexample requires 101 users (  to  ). With a local bundle abstraction, only 4 users are required (e.g., the zero-account, the two contracts, and ).

Fig. 8.
figure 8

Possible implementations of .

Full size image

Symbolic Execution. Symbolic execution is a sophisticated technique that can be used to find bugs in programs. At a high-level, symbolic execution converts program paths into logical constraints, and then solves for inputs that violate program assertions [12]. Symbolic execution is very precise, but its performance is negatively impacted by the number of paths through a program, which is often unbounded. As in the case of greybox fuzzing, the symbolic execution harness is instantiated with N participants, each with strong updates. Symbolic execution targets deeper violations than greybox fuzzing, at the cost of analysis time.

Table 2. Analysis results for each case study. For bug finding, n is the number of users, FUZ is greybox fuzzing, and SYM is symbolic execution. BMC results marked by \((\dagger )\) were obtained using an additional bound of 5 transactions. Omitted results indicate that a system memory limit was exceeded.
Full size table

BMC. Model checking is a technique that, with little human input, proves properties of a program [15, 43]. In bounded model checking (BMC), properties are proven up to a bound on execution (e.g., on the number of loop iterations or users) [7]. The harness for BMC is instantiated with N participants, each with strong updates. BMC either proves a bundle is safe up to N users, or finds a counterexample using at most N users (e.g., see [29]). As the harness is executable, SmartACE is able to compile and execute counterexamples found by SeaHorn. With SeaHorn, integers can be bit-precise [31], or over-approximated by linear integer arithmetic [8]. The number of transactions can be bounded, or an inductive invariant can be discovered for the transaction loop.

PCMC. PCMC is a modular reasoning technique for network verification [40]. Given an interference invariant, PCMC either proves a bundle is safe for any number of users, or finds a counterexample to compositionality (i.e., the interference invariant is inadequate). The harness is instantiated with representative users, and at most the transient and implicit participants are concrete (this is configurable). Increasing the number of concrete participants refines the abstraction, but also increases the size of the state space. As with BMC, integers may be bit-precise or arithmetic, and all counterexamples are executable. If SeaHorn is used as a model checker, then interference invariants are inferred from their initial conditions (i.e., all mapping entries are zero), and their usage throughout the harness. This technique is called predicate synthesis.

5 Case Study: Verifying OpenZeppelin Contracts

We illustrate the effectiveness of SmartACE and Scribble by applying them to analyze the OpenZeppelin libraryFootnote 2. OpenZeppelin is a widely used Solidity library (more than 12’000 stars on GitHub) that implements many Ethereum protocols. From this library, we identify and verify key properties for the and contracts. Properties are specified in the Scribble specification languageFootnote 3. To validate our results, we use fault injection to show that both the harness and the property instrumentation behave as expected. Faults are detected using SeaHorn (bounded in the number of users), libFuzzer, and Klee. To highlight properties not reflected in prior smart contract research, we conclude by verifying two novel properties for from Fig. 1. All evaluations were run on an Intel® Core i7® CPU @ 1.8 GHz 8-core machine with 16 GB of RAM running Ubuntu 20.04. Timing results are given in Table 2.

5.1 Verification of 

A simplified implementation of is presented in Fig. 9. This contract provides a simple access-control mechanism, in which a single user, called the owner, has special privileges. Initially, the owner is the user who creates the contract. At any point during execution, an owner may transfer ownership to another user by calling . An owner may also renounce ownership by calling . When ownership is renounced, the owner is permanently set to and all privileges are lost. These behaviours are captured informally by three properties:

  • O1. If is called successfully, then the new owner is .

  • O2. If ownership changes, then the sender is the previous owner.

  • O3. If ownership changes and has been called at least once, then the new owner is .

O1 is a post-condition for . In Scribble, post-conditions are specified by function annotations. However, function annotations are checked upon function return, using the latest value of each local variable. This means that if was changed during the execution of , then the annotation refers to the newest value of . To overcome this, is used to refer to the original value of . The Scribble annotation is added at line 17 of Fig. 9.

O2 is an assertion for each update to . In Scribble, invariants can be placed on state variable updates using state variable annotations. State variable annotations are checked after each update, even if the update is made during setup in a constructor. However, O2 refers to “ownership changes” which assumes implicitly that some user already owns the contract. Therefore, the invariant should only be checked after construction. This is achieved by adding a flag variable at line 2 that is set to after the constructor has terminated (see line 11). The Scribble annotation is added at line 5 of Fig. 9.

O3 is also an assertion for each update to . However, the techniques used to formalize O2 are not sufficient for O3, as O3 also refers to functions called in the past. To determine if has been called, a second flag variable is added at line 3 that is set to upon entry to at line 22. The Scribble annotation is added at line 6 of Fig. 9.

SmartACE verified each property within 1 s. Furthermore, as does not maintain user-data, verification did not require interference invariants. To validate these results, a fault was injected for each property. Bounded models were then generated using 5 and 500 users to analyze the impact of parameterization. All faults were detected using each of BMC, greybox fuzzing, and symbolic execution. Both BMC and greybox fuzzing were able to detect each fault within 1 s, whereas symbolic execution required up to 90 s per fault. In this case study, the number of users did not impact analysis time.

Fig. 9.
figure 9

A simplified implementation of from OpenZeppelin. All comments are Scribble annotations, and all highlighted lines are instrumentation used in annotations.

Full size image
Fig. 10.
figure 10

A simplified implementation of from OpenZeppelin. All comments are Scribble annotations, and all highlighted lines are instrumentation used in annotations. The field is renamed .

Full size image

5.2 Verification of 

A simplified implementation for is presented in Fig. 10. An escrow is used when a smart contract (the owner) must temporarily hold funds from its users. In the case of , the owner deposits funds on behalf of its users. If some condition is reached (as determined by the owner), the escrow is closed and a beneficiary may withdraw all funds. Otherwise, the owner may enable refunds, and each user can withdraw their funds without the intervention of the owner. In this case study, we consider five properties of :

  • R1 If the state changes, then ownership has not been renounced.

  • R2 If has been called, then all deposits are immutable.

  • R3 If has been called, then has not been called.

  • R4 If has been called, then the balance of the refund escrow is 0, otherwise the balance is the sum of all deposits.

  • R5 If has not been called, then all deposits are increasing.

The first three properties are not parameterized and can be formalized using the same techniques as in the previous case study (Sect. 5.1). R4 is formalized using the operator and a contract invariant, as illustrated on lines 1–2 of Fig. 10. In Scribble, is used to track the sum of all elements in a mapping, without checking for integer overflow. Note that a contract invariant was required, as R4 must be checked each time receives payment. R5 is formalized using a new technique, as illustrated on line 10 of Fig. 10. The key observation is that R5 is equivalent to, “For every address ,if has not been called, then is less than or equal to .” Then, does not satisfy R5 if and only if there exists some witnessing address that violates the new formulation. Therefore, R5 can be checked by non-deterministically selecting a witness, and then validating its deposits across each transactions. In Fig. 10, line 15 non-deterministically selects a witness via user input, and line 10 validates each deposit made on behalf of the witness. Therefore, the annotation on line 10 is equivalent to R5.

Since maintains user-data, all verification required interference invariants (see Sect. 3.3). SmartACE verified each property within 17 s using predicate synthesis. For R1 to R4, all users were abstract, whereas R5 required concrete transient participants to reason exactly about . For comparison, SmartACE was then used to verify each property with user-provided interference invariants. It was found that a “trivial” interference invariant, that includes all deposits, was sufficient to verify each property within 12 s. As in the previous case study, faults were then injected, and detected using 5 and 500 users. With 5 users, BMC required up to 5 s, greybox fuzzing required up to 26 s, and symbolic execution required up to 454 s. However, with 500 users, BMC increased to 33 min, fuzzing increased to 5 min, and symbolic execution exceeded system resource limits for most properties. In this case study, reducing the number of users significantly reduced analysis time.

5.3 Verification of 

Recall from Fig. 1. In this case study the following two properties are formalized and verified:

  • A1. The maximum bid equals leadingBid and is at most the sum of all bids.

  • A2. Any pair of non-zero bids are unequal.

A1 involves the maximum element of bids, and is not addressed by existing smart contract analyzers. The challenge in verifying A1 is that the exact value of max(bids) depends on all previous writes to bids. Specifically, each time the largest bid is overwritten by a smaller bid, the value of max(bids) must be set to the next largest bid. However, if the maximum bid is monotonically increasing, then max(bids) is equal to the largest value previously written into bids. This motivates a formalization that approximates max(bids). In this formalization, two variables are added to Auction. The first variable tracks the largest value written to bids (see line 19 in Fig. 11). The second variable is so long as max(bids) is monotonically increasing (see line 20 in Fig. 11). Together, these two variables help formalize A1, as illustrated by lines 1–2 in Fig. 11.

Fig. 11.
figure 11

An annotated version of from Fig. 1. All comments are Scribble annotations, and all highlighted lines are instrumentation used in annotations.

Full size image

A2 compares two arbitrary elements in , and cannot be reduced to pre- and post-conditions. However, the technique used for R5 in Sect. 5.2 generalizes directly to A2 as shown on line 3 in Fig. 11. In the formalization, there are now two instantiated users: u and v. On line 11, an assertion is added to ensure that these users are unique (i.e., a “pair” of users).

SmartACE verified each property within 246 s using predicate synthesis. For A1, all users were abstract, whereas A2 required concrete transient participants to reason exactly about and . For comparison, SmartACE was then used to verify each property with user-provided interference invariants. Unlike in the previous study (Sect. 5.2), a trivial interference invariant was insufficient to prove A1. However, the discovery of a non-trivial invariant was aided by counterexamples. Initially, the trivial invariant was used, and a counterexample was returned in which each user’s initial bid was larger than 0. This suggested that each element of must be bounded above, which motivated a second invariant: . This new invariant was shown to be compositional, and adequate to prove A1. Using the provided interference invariants, each property was verified within 56 s.

As in the previous case studies, faults were then injected, and detected using 5 and 500 users. With 5 users, BMC required up to 4 s, greybox fuzzing required up to 4 s, and symbolic execution required up to 533 s. However, with 500 users, BMC increased to 73 min, fuzzing increased to 6 min, and symbolic execution exceeded system resource limits for A1. As in Sect. 5.2, reducing the number of users significantly reduced analysis time.

5.4 Discussion

Inter-transactional Analysis. SmartACE is an inter-transactional verification tool. That is, SmartACE verifies properties across unbounded sequences of transactions. In contrast, intra-transactional verification tools (e.g., [2, 26]) verify pre- and post-conditions for single transactions. Inter-transactional verification is a more challenging problem, as it requires an invariant for contract state between transactions. In our study, inter-transactional verification was required to support properties involving calls made in the past (e.g., O3 and R3), and to eliminate unreachable contract states (e.g., the interference invariant used to prove A1). While there are many techniques for inter-transactional verification (e.g., [23, 37, 42, 44, 45, 50]), we believe that the SmartACE approach is unique in its level of automation and its ability to handle parameterization in the number of contract users.

Automation. SmartACE is a fully-automated tool for inter-transactional verification, with optional user-guidance (i.e., user-provided interference invariants). Many other tools rely on semi-automated approaches, such as user-provided contract invariants (i.e., [23, 50]) or predicate abstractions (i.e., [42]). Of the fully-automated tools (i.e., [37, 44, 45]), neither address the state explosion problem. Furthermore, [45] is designed for the harder problem of liveness checking, whereas [37, 44] rely on less optimized model checking techniques than in SeaHorn.

Parameterization. SmartACE is based on the hypothesis that existing smart contract verifiers struggle to scale due to the impact of users on the size of the state space. This aligns with bug finding results for , , and . In the case of , user-data was not maintained, and as expected, the number of users had no noticeable impact on analysis time. In contrast, both and maintain user-data and are significantly impacted by the number of users. For BMC, analysis time increased from seconds to hours, whereas symbolic execution became infeasible. Greybox fuzzing was less impacted by the number of users, which likely reflects that greybox fuzzing is coverage-based, as opposed to symbolic.

Integration Challenges. Two major challenges were encountered while integrating SmartACE with Scribble. The first challenge came from . When Scribble instruments , extra ghost state is added such as which is used to track all updated fields in the mapping. The purpose of this ghost state is to support quantification, but it is not required for summation. However, this state is not supported by SmartACE, and also adds overhead for dynamic analysis. To support in SmartACE, this state was manually removed. The second challenge came with formalizing the predicate: “function has been called at least once.” Formally, this predicate is expressed by , and is supported by other smart contract verification tools such as [42, 45]. However, these specifications are not supported by Scribble. As shown in Sect. 5.1, both and can be instrumented manually with flag variables. However, manual instrumentation is more error-prone than well-tested automated instrumentation. We conclude that SmartACE can integrate with Scribble, but that further improvements are needed for the integration to become seamless. Furthermore, these improvements would benefit all users of Scribble, as opposed to only SmartACE.

6 Related Work

Inter-transactional Verification. There are many tools for inter-transactional verification. Manual approaches, such as [6, 19, 27] provide proof-assistants for end-users to verify properties. These tools are versatile, but are also time consuming and are aimed at verification engineers rather than developers. Semi-automated approaches, such as [23, 50], require end-users to manually provide contract invariants. In VerX  [42], contract invariants are discovered automatically, but an end-user must provide an adequate predicate abstraction. Automated approaches, such as [37, 44, 45], do not offer solutions to parameterization, and instead rely on the underlying solvers to reduce symmetries.

Reusing Off-the-Shelf Tools. SmartACE is not the first smart contract analyzer to leverage existing analyzers for more widely used languages. For example, prior work has applied SeaHorn for gas estimation [36], and intra-transactional verification [2, 26]. Other smart contract analyzers have reduced to Datalog for checking access control patterns [10], detecting gas exploits [17], and implementing general pattern checks [48]. In [49], SMACK is used to detect non-deterministic payment bugs. In [29], TLA+ is used to perform inter-transactional analysis with a reduced number of users. SmartACE is the first application of off-the-shelf tools to unbounded inter-transactional verification.

Bug Finding. There are multiple tools for smart contract symbolic execution (e.g., [32, 35, 39, 47, 55]) and fuzzing (e.g., [18, 24, 25, 53]). A major challenge for such tools is finding deep violations across many transactions. In [55], a static analysis technique is introduced to eliminate uninteresting transaction sequences. In [47], a learning-based approach is used to train accurate fuzzers from symbolic execution. We suspect that SmartACE would also benefit from such techniques.

Parameterized Verification. Parameterized systems form a rich field of research, as outlined in [9]. In general, verifying a parameterized system is undecidable [3]. However, local bundle abstraction is an instance of PCMC [40], and is decidable (for finite-state systems) relative to an interference invariant. Furthermore, the discovery of interference invariants in SmartACE is an instance of [22]. Though this paper is restricted to safety properties, local bundle abstractions are known to extend to \(\text {CTL}^{*}\) [41]. Abdualla et al. [1] propose a somewhat similar notion of view abstraction to abstract interfering processes in a network, though this abstraction has not been applied to smart contracts.

7 Conclusion

We presented SmartACE, a communication-aware smart contract framework with support for multiple off-the-shelf analyzers. The framework is based on parameterized smart contract verification, and can verify properties for arbitrarily many users. We reported on verifying two widely used smart contracts from the OpenZeppelin library. We then applied SmartACE to a simple open-bid auction to highlight limitations of existing smart contract analyzers, and how they are alleviated by SmartACE. We show that in practice, SmartACE is appropriate for fully-automated smart contract analysis.

During the implementation and evaluation of SmartACE, several challenges were encountered. At the implementation stage, we observed that many analyzers handle value selection and non-determinism using incompatible techniques. To overcome this incompatibility, we introduced libVerify to separate the details of an analyzer from the harness design. At the evaluation stage, we identified limitations in Scribble and suggested improvements. We also proposed manual solutions that can be used to circumvent the limitations of Scribble.