Verification of Ethereum Smart Contracts: A Model Checking Approach
Tam Bang, Hoang H. Nguyen, Dung Nguyen, Toan Trieu, Tho Quan · International Journal of Machine Learning and Computing · 2020
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.Besidesthis, 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.