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.
Index Terms—Ethereum smart contracts, semantic structure
analysis, symbolic execution, control-flow graph.
The authors are with the Faculty of Computer Science and Engineering, Ho
Chi Minh City University of Technology, Vietnam (e-mail: {bnbaotam,
nhhoang.sdh19, 1652119, 1652614, qttho}@hcmut.edu.vn).
Cite: Tam Bang, Hoang H. Nguyen, Dung Nguyen, Toan Trieu, and Tho Quan, "Verification of Ethereum Smart Contracts: A Model Checking Approach," International Journal of Machine Learning and Computing vol. 10, no. 4, pp. 588-593, 2020.
Copyright © 2020 by the authors. This is an open access article distributed under the Creative Commons Attribution License which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly cited (CC BY 4.0).