通过通信抽象进行智能合约的组合验证（扩展）
Compositional Verification of Smart Contracts Through Communication Abstraction (Extended)
摘要：
Solidity智能合约是在区块链上管理多达2^160个用户的程序。由于状态爆炸，相对于所有用户的智能合约是棘手的。现有的解决方案要么限制用户的数量，以近似的行为，或依赖于手动证明。在本文中，我们提出了本地捆绑，减少合同与任意多个用户的顺序程序与几个代表性的用户。每个代表用户抽象出相对于合约和属性彼此局部对称的具体用户。我们的抽象是半自动的。这些代表依赖于通信模式，并且通过静态分析来计算。每个代表的行为摘要是手动提供的，但默认摘要通常就足够了。一旦获得，局部束服从顺序静态分析。我们表明，局部束是相对完整的参数化安全验证，在适度的假设。我们在SmartACE中实现了本地捆绑抽象，并显示了与最先进的验证器相比的数量级加速。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
