ATL Model Checking for Analysis of Ethereum Smart Contracts

Abstract

A blockchain is a growing list of cryptographically secured blocks to maintain shared data on decentralized systems, in order to archive transactions between untrusted participants. Smart contracts are computer programs that automatically execute legal events according to the terms of contracts. Although the Ethereum blockchain has been successfully applied to a number of interesting applications, there have been several events that subtle flaws in smart contracts induce a huge amount of financial loss such as the DAO attack. Accordingly, to analyze smart contracts, we propose a novel formal verification technique to employ ATL (Alternating-time Temporal Logic) model checking. Our methodology represents the interaction between users and smart contracts with a two-player game and verify game properties by using MCMAS that is an efficient ATL model checker.