A refinement-based approach to safe smart contract deployment and evolution

In our previous work, we proposed a verification framework that shifts from the “code is law” to a new “specification is law” paradigm related to the safe evolution of smart contracts. The framework proposed there relaxed the well-established requirement that, once a smart contract is deployed in a blockchain, its code is expected to be immutable. More flexibly, contracts are allowed to be created and upgraded provided they meet a corresponding formal specification that was fixed. In the current paper, we extend this framework to allow specifications to evolve, provided a refinement notion is preserved. We propose a notion of specification refinement tailored for smart contracts and a methodology for checking it. In addition to weakening preconditions and strengthening postconditions and invariants, we allow for the change of data representation and interface extension. Thus, we are able to reason about a significantly wider class of smart contract evolution histories, when contrasted with the original framework. The new framework is centred around a trusted deployer: an off-chain service that formally verifies and enforces the notions of implementation conformance and specification refinement. We have investigated its applicability to the safe deployment and upgrade of contracts implementing widely used Ethereum standards (the ERC20 Token Standard, the ERC3156 Flash Loans, the ERC1155 Multi Token Standard and The ERC721 standard for Non-Fungible Tokens); we handle evolutions possibly involving changes in data representation and interface extensions.