|
This article is cited in 1 scientific paper (total 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.
Citation:
E. S. Shishkin, “Verifying functional properties of smart contracts using symbolic model-checking”, Proceedings of ISP RAS, 30:5 (2018), 265–288
Linking options:
https://www.mathnet.ru/eng/tisp373 https://www.mathnet.ru/eng/tisp/v30/i5/p265
|
Statistics & downloads: |
Abstract page: | 374 | Full-text PDF : | 328 | References: | 29 |
|