Smart Ethereum Virtual Machine - EVM

Abstract

Smart contracts have emerged as a powerful tool for automating complex business logic in a decentralized, secure and transparent manner. The Ethereum Virtual Machine (EVM) is a software platform that enables the execution of smart contracts on the Ethereum blockchain. This study article provides an in-depth analysis of the EVM as a smart contract execution engine. We first provide an overview of the EVM, including its architecture, components, and functionalities. We then discuss the advantages and limitations of the EVM, including its scalability and security issues. 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 trans-action pricing mechanism set by the Ethereum proposal EIP-1559 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-1559proposal, 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.