Vulnerable Smart Contract Detection by Means of Model Checking

We are recently witnessing an exponential use of blockchain technology since information infrastructures are increasingly moving from the concept of centralisation to the decentralization ones. Blockchain technology is strictly related to the exchange of sensitive information, and its massive adoption is corresponding to interest from attackers. In this paper, we propose a method to automatically detect whether a Smart Contract (i.e. a contract between two parties concerning the exchange of goods and services, it is executed automatically and is governed by a source code written by a developer, contains clearly conditions accepted by both parties and resides on a distributed and decentralised network of computers) exhibits vulnerability. The proposed method relies on model checking and, through the adoption of μ-Calculus rules, is aimed to detect four different vulnerabilities on Smart Contracts modeled as automata. We preliminary evaluate the proposed method on a dataset composed by 40 (vulnerable and legitimate) contracts, by obtaining a precision ranging from 0.98 to 1 and a recall equal to 1, confirming that the proposed method can be promising in vulnerable Smart Contract detection.