Home > Archive > 2020 > Volume 10 Number 4 (July 2020) >
IJMLC 2020 Vol.10(4): 588-593 ISSN: 2010-3700
DOI: 10.18178/ijmlc.2020.10.4.977

Verification of Ethereum Smart Contracts: A Model Checking Approach

Tam Bang, Hoang H. Nguyen, Dung Nguyen, Toan Trieu, and Tho Quan

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).

General Information

  • ISSN: 2010-3700 (Online)
  • Abbreviated Title: Int. J. Mach. Learn. Comput.
  • Frequency: Bimonthly
  • DOI: 10.18178/IJMLC
  • Editor-in-Chief: Dr. Lin Huang
  • Executive Editor:  Ms. Cherry L. Chen
  • Abstracing/Indexing: Inspec (IET), Google Scholar, Crossref, ProQuest, Electronic Journals LibraryCNKI.
  • E-mail: ijmlc@ejournal.net

Article Metrics in Dimensions