Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)
This addresses the state explosion issue in smart contract verification for blockchain applications, offering a semi-automated solution that is relatively complete under moderate assumptions.
The paper tackles the intractable problem of verifying Solidity smart contracts with up to 2^160 users by introducing local bundles, which reduce contracts to sequential programs with a few representative users, achieving order-of-magnitude speedups compared to a state-of-the-art verifier.
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.