Towards Model checking approach for Smart contract validation in the EIP-1559 Ethereum

Abstract

Smart contracts' vulnerabilities are widely dependent on developed code. Due to blockchain immutability, once this code is deployed it cannot be reversed. In this context, formal verification techniques are widely used to check smart contracts' correctness with respect to a given specification. In light of this, we introduce a model checking-based approach for solidity smart contracts and their blockchain environment using the nuXmv model checker. Our model-based approach considers the transaction pricing mechanism set by the Ethereum proposal EIP-1559 [1] and consists of three main steps, respectively, representing a smart contract with its blockchain behavior into an Extended Finite State Machine (EFSM) meanwhile, providing an over-approximation of the contract gas usage following the EIP-1559 proposal, then, encoding the modeled EFSM into nuXmv input language and, finally, specifying safety and liveness properties that will be checked against the model. Our contributions reason about modelling and checking gas usage consumption which makes it failure-aware. We illustrate this approach through a voting case study.