This article is cited in 1 paper

Verifying functional properties of smart contracts using symbolic model-checking

E. S. Shishkin

Infotecs, Scientific Research Department

Abstract: We describe our efforts towards building a tool that automatically verify high-level functional properties of Ethereum smart contracts against its formal specification that can be given using four different methods: an invariant over contract state or three different types of trace properties. A model of runtime system, the source code of smart contract together with its specification is translated into SMT-solver formula and checked for counter example. We tested the method on simplified version of notorious TheDAO smart-contract, called MiniDAO. Our proof-of-concept tool was able to find a functional property violation of MiniDAO in just several seconds. We believe that the proposed method is indeed useful and deserves deeper investigation.

Keywords: symbolic model-checking, smart contracts, blockchain, formal specification.

DOI: 10.15514/ISPRAS-2018-30(5)-16

Bibliographic databases:

•