Automated construction of predicate abstractions for smart contract validation

Abstract

Verification and validation of smart contracts is crucial, as these programs administer valuable assets. Indeed, there is a proliferation of companies, specialized in smart contract audits that has become a key component of the blockchain ecosystem. Current verification and validation practice is heavily reliant on the insight and experience of auditors. However, there is an increasing rich toolbox that supports their work. In this paper, we show how predicate abstraction can be leveraged to construct models that support smart contract auditing. These models provide auditors with a systematic approach to analyzing and validating the behavior of smart contracts at the function call level. By proposing predicates, auditors can generate alternative perspectives on a contract’s behavior, refine transitions to investigate specific scenarios, and incorporate transient states into the abstraction to uncover reentrancy vulnerabilities. We formally define predicate abstractions for smart contracts and introduce default predicates to support initial exploration. We also present PASCo, a tool that automatically builds an abstract finite state automaton from a set of predicates and a smart contract implementation. We evaluate PASCo on established benchmarks and with an experienced smart contract auditor. Furthermore, we compare its effectiveness in detecting reentrancy vulnerabilities (measured in terms of precision and recall) against 14 state-of-the-art Solidity vulnerability detectors.