Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)

TL;DR

This paper introduces a semi-automated abstraction technique called local bundles for verifying smart contracts with many users, significantly improving verification efficiency by reducing complexity through communication-based abstraction.

Contribution

It presents a novel communication abstraction method that reduces parameterized smart contract verification to manageable sequential analysis, with implementation demonstrating substantial speedups.

Findings

Order-of-magnitude speedups in verification times

Effective abstraction of arbitrarily many users

Relatively complete for safety verification under certain conditions

Abstract

Solidity smart contracts are programs that manage up to 2^160 users on a blockchain. Verifying a smart contract relative to all users is intractable due to state explosion. Existing solutions either restrict the number of users to under-approximate behaviour, or rely on manual proofs. In this paper, we present local bundles that reduce contracts with arbitrarily many users to sequential programs with a few representative users. Each representative user abstracts concrete users that are locally symmetric to each other relative to the contract and the property. Our abstraction is semi-automated. The representatives depend on communication patterns, and are computed via static analysis. A summary for the behaviour of each representative is provided manually, but a default summary is often sufficient. Once obtained, a local bundle is amenable to sequential static analysis. We show that local bundles are relatively complete for parameterized safety verification, under moderate assumptions. We implement local bundle abstraction in SmartACE, and show order-of-magnitude speedups compared to a state-of-the-art verifier.