Rich Specifications for Ethereum Smart Contract Verification

TL;DR

This paper introduces a novel specification methodology and reasoning technique for Ethereum smart contracts that handle unverified code, re-entrancy, and resource transfers, enabling more accurate and modular verification.

Contribution

The paper presents the first specification and verification approach tailored for smart contracts that addresses unverified code, re-entrancy, and resource-based specifications.

Findings

Successfully verified real-world smart contracts using the new approach.

Enabled modular reasoning about multiple interacting contracts.

Provided concise, resource-based specifications that prevent common errors.

Abstract

Smart contracts are programs that execute inside blockchains such as Ethereum to manipulate digital assets. Since bugs in smart contracts may lead to substantial financial losses, there is considerable interest in formally proving their correctness. However, the specification and verification of smart contracts faces challenges that do not arise in other application domains. Smart contracts frequently interact with unverified, potentially adversarial outside code, which substantially weakens the assumptions that formal analyses can (soundly) make. Moreover, the core functionality of smart contracts is to manipulate and transfer resources; describing this functionality concisely requires dedicated specification support. Current reasoning techniques do not fully address these challenges, being restricted in their scope or expressiveness (in particular, in the presence of re-entrant calls), and offering limited means of expressing the resource transfers a contract performs. In this paper, we present a novel specification methodology tailored to the domain of smart contracts. Our specification constructs and associated reasoning technique are the first to enable: (1) sound and precise reasoning in the presence of unverified code and arbitrary re-entrancy, (2) modular reasoning about collaborating smart contracts, and (3) domain-specific specifications based on resources and resource transfers, which allow expressing a contract's behavior in intuitive and concise ways and exclude typical errors by default. We have implemented our approach in 2vyper, an SMT-based automated verification tool for Ethereum smart contracts written in the Vyper language, and demonstrated its effectiveness in succinctly capturing and verifying strong correctness guarantees for real-world contracts.