Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)

Solidity smart contracts are distributed programs that facilitate information flow between users. Users alternate and execute predefined transactions, that each terminate within a predetermined number of steps. Each user (and contract) is assigned a unique, $160$-bit address, that is used by the smart contract to map the user to that user’s data. In theory, smart contracts are finite-state systems with $2^{160}$ users. However, in practice, the state space of a smart contract is huge—with at least $2^{2^{160}}$ states to accommodate all users and their data (conservatively counting one bit per user). In this paper, we consider the challenge of automatically verifying Solidity smart contracts that rely on user data.

A naive solution for smart contract verification is to verify the finite-state system directly. However, verifying systems with at least $2^{2^{160}}$ states is intractable. The naive solution fails because the state space is exponential in the number of users. Instead, we infer correctness from a small number of representative users to ameliorate state explosion. To restrict a contract to fewer users, we first generalize to a family of finite-state systems parameterized by the number of users. In this way, smart contract verification is reduced to parameterized verification.

For example, consider {Auction} in \cref{Fig:Auction} (for now, ignore the highlighted lines). In \mbox{\code{Auction},} each user starts with a bid of $0$. 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\footnote{For simplicity of presentation, we do not use Ether, Ethereum’s␣native␣currency.}.␣\code{Auction}␣satisfies␣\prop{1}:␣‘‘\emph{Once␣\mbox{\code{stop()}}␣is␣called,␣all␣bids␣are␣immutable}.’’␣\prop{1}␣␣␣␣␣␣␣␣is␣satisfied␣since␣\mbox{\code{stop()}}␣sets␣\code{stopped}␣to␣true,␣no␣function␣␣␣␣␣␣␣␣sets␣\code{stopped}␣to␣false,␣and␣while␣\code{stopped}␣is␣true␣neither␣␣\mbox{\code{bid()}}␣nor␣\mbox{\code{withdraw()}}␣is␣enabled.␣Formally,␣\prop{1}␣is␣initially␣true,␣and␣remains␣true␣due␣to␣\prop{1b}:␣‘‘\emph{Once␣␣␣␣␣␣\mbox{\code{stop()}}␣is␣called,␣\code{stopped}␣remains␣true}.’’␣\prop{1}␣is␣said␣␣␣␣␣␣␣␣to␣be␣inductive␣relative␣to␣its␣\emph{inductive␣strengthening}␣\prop{1b}.␣A␣␣␣␣␣\emph{Software␣Model␣Checker␣(SMC)}␣can␣establish␣\prop{1}␣by␣an␣exhaustive␣␣␣␣␣search␣for␣its␣inductive␣strengthening.␣However,␣this␣requires␣a␣bound␣on␣the␣␣␣number␣of␣addresses,␣since␣a␣search␣with␣all␣$2^{160}$␣addresses␣is␣intractable.␣␣␣␣␣␣␣␣␣␣␣␣␣␣␣␣A␣bound␣of␣at␣least␣four␣addresses␣is␣necessary␣to␣represent␣the␣zero-account␣␣␣(i.e.,␣a␣null␣user␣that␣cannot␣send␣transactions),␣the␣smart␣contract␣account,␣␣the␣manager,␣and␣an␣arbitrary␣sender.␣However,␣once␣the␣arbitrary␣sender␣submits␣␣␣␣␣␣␣␣a␣bid,␣the␣sender␣is␣now␣the␣leading␣bidder,␣and␣cannot␣withdraw␣its␣bid.␣To␣␣␣␣enable␣\mbox{\code{withdraw()},}␣a␣fifth␣user␣is␣required.␣It␣follows␣by␣applying␣␣␣␣␣␣␣the␣results␣of~\cite{KaiserKroening2010},␣that␣a␣bound␣of␣five␣addresses␣is␣also␣␣␣␣␣␣␣␣sufficient,␣since␣users␣do␣not␣read␣each␣other’s bids, and adding a sixth user does not enable additional changes to \mbox{\code{leadingBid}~\cite{KaiserKroening2010}}. The bounded system, known as a harness, in \cref{Fig:Harness} assigns the zero-account to address 0, the smart contract account to address 1, the manager to address 2, the arbitrary senders to addresses 3 and 4, and then executes an unbounded sequence of arbitrary function calls. Establishing \prop{1} on the harness requires finding its inductive strengthening. A strengthening such as \prop{1b} (or, in general, a counterexample violating \prop{1}) can be found by an SMC, directly on the harness code. The above bound for \prop{1} also works for checking all control-reachability properties of \code{Auction}. This, for example, follows by applying the results of~\cite{KaiserKroening2010}. That is, \code{Auction} has a \emph{Small Model Property (SMP)}~(e.g.,~\cite{KaiserKroening2010,AbdullaHH13}) for such properties. However, not all contracts enjoy an SMP. Consider \prop{2}: ‘‘\emph{The sum of all active bids is at least \code{leadingBid}}.’’ \code{Auction} satisfies \prop{2} since the leading bid is never withdrawn. To prove \code{Auction} satisfies \prop{2}, we instrument the code to track the current sum, through the highlighted lines in \cref{Fig:Auction}. With the addition of \code{\_sum}, \code{Auction} no longer enjoys an SMP. Intuitively, each user enables new combinations of \code{\_sum} and \code{leadingBid}. As a proof, assume that there are $N$ users (other than the zero-account, the smart contract account, and the manager) and let $S_N = 1 + 2 + \cdots + N$. In every execution with $N$ users, if \code{leadingBid} is $N + 1$, then \code{\_sum} is less than $S_{N + 1}$, since active bids are unique and $S_{N + 1}$ is the sum of $N + 1$ bids from $1$ to $N + 1$. However, in an execution with $N + 1$ users, if the $i$-th user has a bid of $i$, then \code{leadingBid} is $N + 1$ and \code{\_sum} is $S_{N + 1}$. Therefore, increasing $N$ extends the reachable combinations of \code{\_sum} and \code{leadingBid}. For example, if $N = 2$, then $S_3 = 1 + 2 + 3 = 6$. If the leading bid is $3$, then the second highest bid is at most $2$, and, therefore, $\mathsol{\_sum} \le 5 < S_3$. However, when $N = 3$, if the three active bids are $\{ 1, 2, 3 \}$, then \code{\_sum} is $S_3$. Therefore, instrumenting \code{Auction} with \code{\_sum} violates the SMP of the original \code{Auction}. Despite the absence of such an SMP, each function of \code{Auction} interacts with at most one user per transaction. Each user is classified as either the zero-account, the smart contract, the manager, or an arbitrary sender. In fact, all arbitrary senders are indistinguishable with respect to \prop{2}. For example, if there are exactly three active bids, $\{ 2, 4, 8 \}$, it does not matter which user placed which bid. The leading bid is $8$ and the sum of all bids is $14$. On the other hand, if the leading bid is $8$, then each participant of \code{Auction} must have a bid in the range of $0$~to~$8$. To take advantage of these classes, rather than analyze \code{Auction} relative to all $2^{160}$ users, it is sufficient to analyze \code{Auction} relative to a representative user from each class. In our running example, there must be representatives for the zero-account, the smart contract account, the manager, and an (arbitrary) sender. The key idea is that each representative user can correspond to one or \emph{many} concrete users. Intuitively, each representative user summarizes the concrete users in its class. 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,␣the␣smart␣contract␣account,␣and␣the␣manager␣each␣␣␣␣␣correspond␣to␣single␣concrete␣users.␣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␣senders␣are␣indistinguishable␣from␣each␣other,␣the␣␣␣␣␣precise␣address␣of␣the␣representative␣sender␣is␣unimportant.␣What␣matters␣is␣␣␣␣that␣the␣representative␣sender␣does␣not␣share␣an␣address␣with␣the␣zero-account,␣the␣smart␣contract␣account,␣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␣that␣is␣true␣of␣all␣initial␣bids,␣and␣holds␣␣inductively␣across␣all␣transactions.␣We␣provide␣this␣predicate␣manually,␣and␣use␣␣␣␣␣␣␣␣it␣to␣over-approximate␣all␣possible␣bids.␣An␣obvious␣predicate␣for␣␣␣␣␣␣\code{Auction}␣is␣that␣all␣bids␣are␣at␣most␣\mbox{\code{leadingBid},}␣but␣this␣␣predicate␣is␣not␣strong␣enough␣to␣prove␣\prop{2}.␣For␣example,␣the␣␣␣␣␣␣representative␣sender␣could␣first␣place␣a␣bid␣of␣$10$,␣and␣then␣(spuriously)␣␣␣␣withdraw␣a␣bid␣of␣$5$,␣resulting␣in␣a␣sum␣of␣$5$␣but␣a␣leading␣bid␣of␣$10$.␣A␣␣␣stronger␣predicate,␣that␣is␣adequate␣to␣prove␣\prop{2},␣is␣given␣by␣$\theta_U$:␣‘‘\emph{Each␣bid␣is␣at␣most␣\mbox{\code{leadingBid}.}␣If␣a␣bid␣is␣not␣␣␣\mbox{\code{leadingBid},}␣then␣its␣sum␣with␣\code{leadingBid}␣is␣at␣most␣␣␣␣␣␣␣␣\mbox{\code{\_sum}.}}’’␣␣␣␣␣␣␣␣␣Given␣$\theta_U$,␣\prop{2}␣can␣be␣verified␣by␣an␣SMC.␣This␣requires␣a␣new␣␣␣␣␣␣␣harness,␣with␣representative,␣rather␣than␣concrete,␣users.␣The␣new␣harness,␣␣␣␣␣\cref{Fig:Harness}␣(now␣including␣the␣highlighted␣lines),␣is␣similar␣to␣the␣SMP␣harness␣in␣that␣the␣zero-account,␣the␣smart␣contract␣account,␣and␣the␣manager␣␣␣account␣are␣assigned␣to␣addresses␣0,␣1,␣and␣2,␣respectively,␣followed␣by␣an␣␣␣␣␣unbounded␣sequence␣of␣arbitrary␣calls.␣However,␣there␣is␣now␣a␣single␣sender␣␣␣␣that␣is␣assigned␣to␣address~3␣(line~\ref{line:harness-instr-sender}).␣That␣is,␣␣the␣harness␣uses␣a␣fixed␣configuration␣of␣representatives␣in␣which␣the␣fourth␣␣␣representative␣is␣the␣sender.␣Before␣each␣function␣call,␣the␣sender’s bid is set to a non-deterministic value that satisfies $\theta_U$ (lines~\ref{line:harness-instr-start}--\ref{line:harness-instr-end}). If the new harness and \prop{2} are provided to an SMC, the SMC will find an inductive strengthening such as, ‘‘\emph{The leading bid is at most the sum of all bids}.’’ The harness in \cref{Fig:Harness} differs from existing smart contract verification techniques in two ways. First, each address in \cref{Fig:Harness} is an abstraction of one or more concrete users. Second, \code{msg.sender} is restricted to a finite address space by lines~\ref{line:harness-instr-sender-start}~to~\ref{line:harness-instr-sender}. If these lines are removed, then an inductive invariant must constrain all cells of \code{bids}, to accommodate \code{bids[msg.sender]}. This requires quantified invariants over arrays that is challenging to automate. By introducing lines~\ref{line:harness-instr-sender-start}~to~\ref{line:harness-instr-sender}, a quantifier-free predicate, such as our $\theta_U$, can directly constrain cell \code{bids[msg.sender]} instead. Adding lines \ref{line:harness-instr-sender-start}--\ref{line:harness-instr-sender} makes the contract finite state. Thus, its verification problem is decidable and can be handled by existing SMCs. However, as illustrated by \prop{2}, the restriction on each user must not exclude feasible counterexamples. Finding such a restriction is the focus of this paper. In this paper, we present a new approach to smart contract verification. We construct finite-state abstractions of parameterized smart contracts, known as \emph{local bundles}. A local bundle generalizes the harness in \cref{Fig:Harness}, and is constructed from a set of representatives and their predicates. When a local bundle and a property are provided to an SMC, there are three possible outcomes. First, if a predicate does not over-approximate its representative, a counterexample to the predicate is returned. Second, if the predicates do not entail the property, then a counterexample to verification is returned (this counterexample refutes the proof, rather than the property itself). Finally, if the predicates do entail the property, then an inductive invariant is returned. As opposed to deductive smart contract solutions, our approach finds inductive strengthenings automatically~\cite{HajduJovanovic2019,ZhongCheang2020}. As opposed to other model checking solutions for smart contracts, our approach is not limited to pre- and post-conditions~\cite{KalraGoel2018}, and can scale to $2^{160}$ users~\cite{Kolb2020}. Key theoretical contributions of this paper are to show that verification with local bundle abstraction is an instance of Parameterized Compositional Model Checking (PCMC)~\cite{NamjoshiTrefler2016} and the automation of the side-conditions for its applicability. Specifically, \cref{Thm:SafetyCheck} shows that the local bundle abstraction is a sound proof rule, and a static analysis algorithm (\code{PTGBuilder} in \cref{sec:communication}) computes representatives so that the rule is applicable. Key practical contributions are the implementation and the evaluation of the method in a new smart contract verification tool \smartace, using \seahorn~\cite{GurfinkelKahsai2015} for SMC. \smartace takes as input a contract and a predicate. Representatives are inferred automatically from the contract, by analyzing the communication in each transaction. The predicate is then validated by \seahorn, relative to the representatives. If the predicate is correct, then a local bundle, as in \cref{Fig:Harness}, is returned. The rest of the paper is structured as follows. \cref{Sec:Background} reviews parameterized verification. \cref{Sec:SyntaxSemantics} presents MicroSol, a subset of Solidity with network semantics. \cref{sec:communication} relates user interactions to representatives. We formalize user interactions as \emph{Participation Topologies (PTs)}, and define \emph{PT Graphs (PTGs)} to over-approximate PTs for arbitrarily many users. Intuitively, each PTG over-approximates the set of representatives. We show that a PTG is computable for every MicroSol program. \cref{sec:locality} defines local bundles and proves that our approach is sound. \cref{sec:eval} evaluates \smartace and shows that it can outperform \verx, a state-of-the-art verification tool, on all but one \verx benchmark.

In this section, we briefly recall Parameterized Compositional Model Checking (PCMC) [NamjoshiTrefler2016]. We write $\mathbf{u}=(u_{0},\ldots,u_{n-1})$ for a vector of $n$ elements, and $\mathbf{u}_{i}$ for the $i$-th element of $\mathbf{u}$. For a natural number $n\in\mathbb{N}$, we write $[n]$ for $\{0,\ldots,n-1\}$.

This section provides network semantics for MicroSol, a subset of Solidity²²2https://docs.soliditylang.org/. Like Solidity, MicroSol is an imperative object-oriented language with built-in communication operations. The syntax of MicroSol is in Fig. 3. MicroSol restricts Solidity to a core subset of communication features. For example, MicroSol does not include inheritance, cryptographic operations, or mappings between addresses. In our evaluation (LABEL:sec:eval), we use a superset of MicroSol, called MiniSol (see LABEL:Appendix:MiniSol), that extends our semantics to a wider set of smart contracts. Throughout this section, we illustrate MicroSol using {Auction} in \cref{Fig:Auction}. A MicroSol \emph{smart contract} is similar to a class in object-oriented programming, and consists of variables, and transactions (i.e., functions) for users to call. A transaction is a deterministic sequence of operations. Each smart contract user has a globally unique identifier, known as an \emph{address}. We view a smart contract as operating in an SCUN: the control process executes each transaction sequentially, and the user processes are contract users that communicate with the control process. Users in the SCUN enter into a transaction through a synchronized action, then the control process executes the transaction as an internal action, and finally, the users are updated through synchronized actions. For simplicity of presentation, each transaction is given as a global transition. A constructor is a special transaction that is executed once after contract creation. Calls to \code{new} (i.e., creating new smart contracts) are restricted to constructors. \code{Auction} in \cref{Fig:Auction} is a smart contract that defines a constructor (line~\ref{line:constructor}), three other functions (lines~\ref{line:bid}, \ref{line:withdraw}, and~\ref{line:stop}), and four state variables (lines~\ref{line:vars-start}--\ref{line:vars-end}). MicroSol has four types: \emph{address}, \emph{numeric} (including \code{bool}), \emph{mapping}, and \emph{contract reference}. Address variables prevent arithmetic operations, and numeric variables cannot cast to address variables. Mapping and contract-reference variables correspond to dictionaries and object pointers in other object-oriented languages. Each typed variable is further classified as either \emph{state}, \emph{input}, or \emph{local}. We use \emph{role} and \emph{data} to refer to state variables of address and numeric types, respectively. Similarly, we use \emph{client} and \emph{argument} to refer to inputs of address and numeric types, respectively. In \code{Auction} of \cref{Fig:Auction}, there is $1$ role \mbox{(\code{manager}),} $2$ contract data \mbox{(\code{leadingBid}} and \mbox{\code{stopped}),} $1$ mapping \mbox{(\code{bids})}, $1$ client common to all transactions \mbox{(\code{msg.sender})}, and at most $1$ argument in any transaction \mbox{(\code{amount}).} Note that in MicroSol, \emph{user} denotes any user process within a SCUN. A \emph{client} is defined relative to a transaction, and denotes a user passed as an input. \newcommand{\tran}{\mathit{tr}} \newcommand{\cM}{\mathcal{M}} \paragraph{Semantics of MicroSol.} Let $\cC$ be a MicroSol program with a single transaction $\tran$ (see \appendixcite{Appendix:Lts} for multiple transactions). An $N$-user \emph{bundle} is an $N$-user network of several (possibly identical) MicroSol programs. The semantics of a bundle is an LTS, $\lts( \cC, N ) \gets ( S, P, f, s_0 )$, where $S_C \gets \control( \cC, [N] )$ is the set of control states, $S_U \gets \user( \cC, [N] )$, is the set of user states, $s_{\bot}$ is the error state, $S \subseteq \left( S_C \cup \{ s_{\bot} \} \right) \times (S_U)^N$ is the set of LTS states, $P \gets \inputs( \cC, [N] )$ is the set of actions, $f: S \times P \rightarrow S$ is the \emph{transition function}, and $s_0$ is the initial state. We assume, without loss of generality, that there is a single control process\footnote{Restrictions place on \code{new} ensure that the number of MicroSol smart contracts in a bundle is a static fact. Therefore, all control states are synchronized, and can be combined into a product machine.}. Let $\bbD$ be the set of $256$-bit unsigned integers. The state space of a smart contract is determined by the address space, $\cA$, and the state variables of $\cC$. In the case of $\lts( \cC, N )$, the address space is fixed to $\cA = [N]$. Assume that $n$, $m$, and $k$ are the number of roles, data, and mappings in $\cC$, respectively. State variables are stored by their numeric indices (i.e., variable~$0$, $1$, etc.). Then, $\control( \cC, \cA ) \subseteq \cA^n \times \bbD^m$ and $\user( \cC, \cA ) \subseteq \cA \times \bbD^k$. For $c = ( \vx, \vy ) \in \control( \cC, \cA)$, $\role( c, i ) = \vx_i$ is the $i$-th role and $\data( c, i ) = \vy_i$ is the $i$-th datum. For $u = (z, \vy) \in \user( \cC, \cA )$, $z$ is the address of $u$, and $\rec( u ) = \vy$ are the mapping values of $u$. Similarly, actions are determined by the address space, $\cA$, and the input variables of $\tran$. Assume that $q$ and $r$ are the number of clients and arguments of $\tran$, respectively. Then $\inputs( \cC, \cA ) \subseteq \cA^q \times \bbD^r$. For $p = (\vx, \vy) \in \inputs( \cC, \cA )$, $\client( p, i ) = \vx_i$ is the $i$-th client in $p$ and $\args( p, i ) = \vy_i$ is the $i$-th argument in $p$. For a fixed $p$, we write $f_p( s, \vu )$ to denote $f( (s, \vu), p )$. The initial state of $\lts( \cC, N )$ is $s_0 \gets (c, \vu) \in \control( \cC, [n] ) \times \user( \cC, [n] )^N$, where $c = ( \vec{0}, \vec{0} )$, $\forall i \in [N] \cdot \rec(\vu_i) = \vec{0}$, and $\forall i \in [N] \cdot \id( \vu_i ) = i$. That is, all variables are zero-initialized and each user has a unique address. An $N$-user transition function is determined by the (usual) semantics of $\tran$, and a \emph{bijection} from addresses to user indices, $\cM: \cA \rightarrow [N]$. If $\cM( a ) = i$, then address $a$ belongs to user $\vu_i$. In the case of $\lts( \cC, N )$, the $i$-th user has address $i$, so $\cM(i) = i$. We write $f \gets \bbrackfn{\cC}_{\cM}$, and given an action $p$, $f_p$ updates the state variables according to the source code of $\tran$ with respect to $\cM$. If an \code{assert} fails or an address is outside of $\cA$, then the error state $s_{\bot}$ is returned. If a \code{require} fails, then the state is unchanged. Note that $f$ preserves the address of each user. For example, $\lts(\text{Auction}, 4) = (S, P, f, s_0)$ is the $4$-user bundle of \code{Auction}. Assume that $(c, \vu)$ is the state reached after evaluating the constructor. Then $\role( c, 0 ) = 2$, $\data( c, 0 ) = 0$, $\data( c, 1 ) = 0$, and $\forall i \in [4] \cdot \rec( \vu_i )_0 = 0$. That is, the manager is at address 2, the leading bid is 0, the auction is not stopped, and there are no active bids. This is because variables are zero-indexed, and \code{stopped} is the second numeric variable (i.e., at index 1). If the user at address $3$ placed a bid of $10$, this corresponds to $p \in P$ such that $\client( p, 0 ) = 3$ and $\args( p, 0 ) = 10$. A complete LTS for this example is in \appendixcite{Appendix:Lts}. \paragraph{Limitations of MicroSol.} MicroSol places two restrictions on Solidity. First, addresses are not numeric. We argue that this restriction is reasonable, as address manipulation is a form of pointer manipulation. Second, \code{new} must only appear in constructors. In our evaluation (\cref{sec:eval}), all calls to \code{new} could be moved into a constructor with minimal effort. We emphasize that the second restriction does not preclude the use of abstract interfaces for arbitrary contracts.