Specification is law : safe creation and upgrade of ethereum smart contracts

Abstract

Smart contract evolution is crucial for the success of decentralized applications, and current methods and processes are not well suited to handle these drivers of change, as the knowledge about the software is predominantly stored in informal documents. In addition, they are the building blocks of the ”code is law” paradigm: the smart contract’s code indisputably describes how its assets are to be managed - once it is created, its code is typically immutable. Faulty smart contracts present the most significant evidence against the practicality of this paradigm; they are well-documented and resulted in assets worth vast sums of money being compromised. To address this issue, the Ethereum community proposed (i) tools and processes to audit/analyse smart contracts, and (ii) design patterns implementing a mechanism to make contract code mutable. Individually, (i) and (ii) only partially address the challenges raised by the ”code is law” paradigm. In this work, we combine elements from (i) and (ii) to create a systematic framework that moves away from ”code is law” and gives rise to a new ”specifica- tion is law” paradigm. It allows contracts to be created and upgraded but only if they meet a corresponding formal specification. We explain how formal verification techniques can be used to ensure safety properties of smart contracts during their evolution. Although formal verification methods have the potential of being used in several application fields, we focus on ensuring compliance with its specifications. The process consists of three phases: Formal requirements specification, verification, and deployment. All steps are planned and executed in an integrated way and together they form a framework capable of fostering safe evolution and make it more reliable and secure. The framework is centered around a trusted deployer: an off-chain service that formally verifies and enforces specification conformance. We have proto- typed this framework, and investigated its applicability to contracts implementing three widely used Ethereum standards: the ERC20 Token Standard, ERC3156 Flash Loans and ERC1155 Multi Token Standard, with promising results.