Verifying functional properties of smart contracts using symbolic model-checking
https://doi.org/10.15514/ISPRAS-2018-30(5)-16
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.
References
1. Pettersson J., Edström R. Safer smart contracts through type-driven development. Master’s thesis, Chalmers University of Technology, Department of Computer Science and Engineering, Sweden, 2016.
2. Atzei N., Bartoletti M., Cimoli T. A survey of attacks on ethereum smart contracts (sok). Lecture Notes in Computer Science, vol. 10204, 2017, pp. 164-186.
3. Bhargavan K. et al. Formal verification of smart contracts. In Proc. of the 2016 ACM Workshop on Programming Languages and Analysis for Security, 2016, pp. 91-96.
4. Luu L. et al. Making smart contracts smarter. In Proc. of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016, pp. 254-269.
5. Hirai Y. Defining the ethereum virtual machine for interactive theorem provers. Lecture Notes in Computer Science, vol. 10323, 2017, pp. 520-535.
6. Kalra S. et al. Zeus: Analyzing safety of smart contracts. In Proc. of the Network and Distributed System Security Symposium, 2018.
7. Mueller B. Smashing Ethereum Smart Contracts for Fun and Real Profit. In Proc. of the 9th Annual HITB Security Conference, 2018.
8. Zakrzewski J. Towards verification of Ethereum smart contracts: a formalization of core of Solidity, Lecture Notes in Computer Science, vol. 11294, 2018, pp. 229-247.
9. Solidity github. Available at: https://github.com/ethereum/solidity/blob/develop/docs/grammar.txt, accessed 20.11.2018.
10. Nakamoto S. Bitcoin. A peer-to-peer electronic cash system. 2008. Available at: https://bitcoin.org/bitcoin.pdf, accessed 20.11.2018, accessed 20.11.2018.
11. Gideon Greenspan. Smart contracts and the dao implosion. 2016. Available at: https://www.multichain.com/blog/2016/06/smart-contracts-the-dao-implosion/, accessed 20.11.2018.
12. S. Palladino. The Parity Wallet Hack Explained, https://blog.zeppelin.solutions/on-the-parity-wallet-multisig-hack-405a8c12e8f7, accessed 20.11.2018.
13. J.D. Alois. Ethereum Parity Hack May Impact ETH 500,000 or $146 Million. 2017. Available at: https://www.crowdfundinsider.com/2017/11/124200-ethereum-parity-hack-may-impact-eth-500000-146-million/, accessed 20.11.2018.
14. Jentzsch C. Decentralized autonomous organization to automate governance. 2016. Available at: https://download.slock.it/public/DAO/WhitePaper.pdf, accessed 20.11.2018.
15. Shishkin E. Towards building an environment for reliable smart contracts construction. RusCrypto, 2018.
16. De Moura L., Bjørner N. Z3: An efficient SMT solver. Lecture Notes in Computer Science, vol. 4963, 2008, pp. 337-340.
17. Manna Z., Pnueli A. The temporal logic of reactive and concurrent systems: Specification. Springer-Verlag, 1992, 427 p/
18. Ethereum project. Available at: https://www.ethereum.org/, accessed 20.11.2018.
19. Szabo N. Smart contracts. 1994. Available at: http://www.fon.hum.uva.nl/rob/Courses/InformationInSpeech/CDROM/Literature/LOTwinterschool2006/szabo.best.vwh.net/smart.contracts.html, accessed 20.11.2018.
20. Sheeran M., Singh S., Stålmarck G. Checking safety properties using induction and a SAT-solver. Lecture Notes in Computer Science, vol. 1954, 2000, pp. 127-144.
Review
For citations:
Shishkin E.S. Verifying functional properties of smart contracts using symbolic model-checking. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(5):265-288. (In Russ.) https://doi.org/10.15514/ISPRAS-2018-30(5)-16
Email this article 