Verification of Ethereum Smart Contracts: A Model Checking Approach

Abstract

Ethereum smart contracts based on blockchain technology are powerful and promising applications that provide a global platform for exchanging cryptocurrencies and public services. This technology are garnering a huge impact and is widely adopted in the current times as it can transform the way we transfer and exchange value by passing the need for a middleman and reducing cost. These smart contracts also represent a basis for true ownership of digital assets and a wide range of decentralized applications. Besides this, since Ethereum and its smart contracts are a publicly accessible, unchangeable and distributed platform, they are extremely vulnerable to various forms of attack, with their security becoming a top priority. However, current security-verifying programs tend to provide many technical details which are pretty hard for normal people to understand briefly. To tackle this problem, we designed a process aiming to mitigate these limitations, with our key insight being a combination of semantic structure analysis and symbolic execution on control-flow graphs (CFG for short). This article proposes a new approach for auditing Ethereum smart contracts, applying this technique would benefit both average users without any technical knowledge and security experts as well.