A Reduction from Smart Contract Verification to Model Checking

Abstract

We present a reduction from verification of smart contracts to model checking. A smart contract is a computer program written in a language with constructs that correspond to real-world contracts, such as verified sending and accepting digital cash. Model checking is an approach to verification of state-transition systems in which a state is the valuation of a set of variables. A reduction, in our context, is a polynomial-time computable function which guarantees that an input smart contract possesses a property if and only if the output instance of model checking possesses a property to which the former property is mapped. Our focus is smart contracts written to run on the Ethereum blockchain in a language compiled to Ethereum Virtual Machine (EVM) code. Our work is motivated by the importance of checking smart contracts for properties of interest and also by the observation in recent empirical work that establishes that existing verification tools are deficient. Our approach has some distinguishing characteristics from prior approaches, which we discuss in this thesis. We have implemented and carried out a limited empirical assessment of our reduction. We used a dataset of 69 curated smart contracts that contains 115 instances of security vulnerabilities from 10 different classes of such vulnerabilities. Our empirical work suggests that our approach can scale to real-world smart contracts.