Solidity smart contract allow developers to formalize financial agreements between users. Due to their monetary nature, smart contracts have been the target of many high-profile attacks. Brute-force verification of smart contracts that maintain data for up to 2160 users is intractable. In this paper, we present SmartACE, an automated framework for smart contract verification. To ameliorate the state explosion induced by large numbers of users, SmartACE implements local bundle abstractions that reduce verification from arbitrarily many users to a few representative users. To uncover deep bugs spanning multiple transactions, SmartACE employs a variety of techniques such as model checking, fuzzing, and symbolic execution. To illustrate the effectiveness of SmartACE, we verify several contracts from the popular OpenZeppelin library: an access-control policy and an escrow service. For each contract, we provide specifications in the Scribble language and apply fault injection to validate each specification. We report on our experience integrating Scribble with SmartACE, and describe the performance of SmartACE on each specification.
CITATION STYLE
Wesley, S., Christakis, M., Navas, J. A., Trefler, R., Wüstholz, V., & Gurfinkel, A. (2022). Verifying Solidity Smart Contracts via Communication Abstraction in SmartACE. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 13182 LNCS, pp. 425–449). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-94583-1_21
Mendeley helps you to discover research relevant for your work.