Compositional verification of smart contracts through communication abstraction

DOI10.1007/978-3-030-88806-0_21zbMATH Open1497.68321arXiv2107.08583OpenAlexW3206384689MaRDI QIDQ2145351FDOQ2145351

Authors: Scott Wesley, Maria Christakis, Richard Trefler, Valentin Wüstholz, Arie Gurfinkel, Jorge Navas 

Publication date: 17 June 2022

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.

Full work available at URL: https://arxiv.org/abs/2107.08583

Recommendations

• Verification-Led Smart Contracts
• Formal verification of atomicity requirements for smart contracts
• EthVer: formal verification of randomized Ethereum smart contracts
• Formal verification of Ethereum smart contracts using Isabelle/HOL
• Quantitative analysis of smart contracts

Mathematics Subject Classification ID

Cryptography (94A60) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Cites Work

• All for the price of few (parameterized verification through view abstraction)
• Reasoning about systems with many processes
• Verification, Model Checking, and Abstract Interpretation
• An axiomatic proof technique for parallel programs
• On Reasoning About Rings
• Title not available (Why is that?)
• Title not available (Why is that?)
• Parameterized compositional model checking
• Towards efficient parameterized synthesis
• Verification, Model Checking, and Abstract Interpretation
• Model Checking Software

Cited In (5)

• Formal verification of Ethereum smart contracts using Isabelle/HOL
• Formal verification of atomicity requirements for smart contracts
• Verification-Led Smart Contracts
• \textit{CCOM}: cost-efficient and collusion-resistant oracle mechanism for smart contracts
• SSCalc: a calculus for Solidity smart contracts

Uses Software

• SeaHorn
• Manticore
• solc-verify
• VerX

This page was built for publication: Compositional verification of smart contracts through communication abstraction

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2145351)