Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)

Abstract

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