Correct-by-Design Interacting Smart Contracts and a Systematic Approach for Verifying ERC20 and ERC721 Contracts With VeriSolid
Keerthi Nelaturu, Anastasia Mavridou, Emmanouela Stachtiari, Andreas Veneris, Áron Lászka
Abstract
Blockchain-based smart contracts enable the creation of decentralized applications, which often handle assets of considerable value. While the underlying platforms guarantee the correctness of smart-contract execution, they cannot ensure that the code of a contract is correct. Today, as evidenced by a number of recent security breaches, developers still have a hard time making contracts that work properly.Even though these incidents often exploit contract interaction, prior work on smart-contract verification, vulnerability discovery, and secure development typically considers only individual contracts in isolation. To address this gap, we introduce the <sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">VeriSolid</small> framework for the formal verification of contracts that are specified using a abstract state machine based model with rigorous operational semantics. Our model-based approach allows developers to reason about and verify the behavior of a set of interacting contracts at a high level of abstraction. <sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">VeriSolid</small> allows the generation of Solidity code that is functionally and behaviorally equivalent to verified models, which enables the creation of correct-by-design smart contracts. We additionally introduce a graphical notation (called <italic xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">deployment diagrams</i> ) for specifying possible interactions between contract types. Based on this notation, we present a framework for the automated verification, generation, and deployment of contracts that conform to a deployment diagram. To demonstrate the applicability of <sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">VeriSolid</small> , we translate existing Ethereum Improvement Proposal (EIP) specifications to temporal properties for two of the most popular contract interfaces: ERC20 and ERC721. We also show you how to write code for the ERC20 and ERC721 interfaces in a way that is safe, and we do this by using <sc xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">VeriSolid</small> . We evaluate our framework on 726 contracts that are currently deployed on the Ethereum blockchain, which include 267 ERC20 and 459 ERC721 contracts. Our experiments indicate that 18% of ERC20 contracts and 4% of ERC721 contracts fail to satisfy the EIP specifications.