Проверка функциональных свойств смарт-контрактов методом символьной верификации модели
https://doi.org/10.15514/ISPRAS-2018-30(5)-16
Аннотация
В статье рассматривается подход к проверке функциональных свойств смарт-контрактов платформы Ethereum методом символьной верификации модели. Описанный подход позволяет верифицировать выполнение 3х видов свойств на трассах ограниченной длины, а также осуществлять проверку выполнимости инварианта. Описана математическая модель среды исполнения смарт-контрактов, проведена формализация выделенных видов свойств в рамках этой модели, описана процедура трансляции всего перечисленного в язык ограничений SMT-решателя. Жизнеспособность предлагаемого подхода иллюстрируется на примере верификации макетного смарт-контракта MiniDAO, упрощённой версии известного TheDAO. За несколько секунд макет находит контр пример одному нетривиальному функциональному требованию, указывая на ошибку в бизнес-логике смарт-контракта. Насколько нам известно, эта работа - одна из первых попыток описать инструмент, помогающий осуществлять формальную проверку функциональных свойств смарт-контрактов в автоматическом режиме.
Список литературы
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. Доступно по ссылке: https://github.com/ethereum/solidity/blob/develop/docs/grammar.txt, дата обращения 20.11.2018.
10. Nakamoto S. Bitcoin. A peer-to-peer electronic cash system. 2008. Доступно по ссылке: https://bitcoin.org/bitcoin.pdf, дата обращения 20.11.2018, дата обращения 20.11.2018..
11. Gideon Greenspan. Smart contracts and the dao implosion. 2016. Доступно по ссылке: https://www.multichain.com/blog/2016/06/smart-contracts-the-dao-implosion/, дата обращения 20.11.2018.
12. S. Palladino. The Parity Wallet Hack Explained, https://blog.zeppelin.solutions/on-the-parity-wallet-multisig-hack-405a8c12e8f7, дата обращения 20.11.2018.
13. J.D. Alois. Ethereum Parity Hack May Impact ETH 500,000 or $146 Million. 2017. Доступно по ссылке: https://www.crowdfundinsider.com/2017/11/124200-ethereum-parity-hack-may-impact-eth-500000-146-million/, дата обращения 20.11.2018.
14. Jentzsch C. Decentralized autonomous organization to automate governance. 2016. Доступно по ссылке: https://download.slock.it/public/DAO/WhitePaper.pdf, дата обращения 20.11.2018.
15. Е. Шишкин. О построении среды для конструирования гарантированно надёжных смарт-контрактов. Материалы конференции РусКрипто’2018, 2018. Доступно по ссылке: https://www.ruscrypto.ru/resource/archive/rc2018/files/03_Shishkin.pdf, дата обращения 20.11.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. Доступно по ссылке: https://www.ethereum.org/, дата обращения 20.11.2018.
19. Szabo N. Smart contracts. 1994. Доступно по ссылке: http://www.fon.hum.uva.nl/rob/Courses/InformationInSpeech/CDROM/Literature/LOTwinterschool2006/szabo.best.vwh.net/smart.contracts.html, дата обращения 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.
Рецензия
Для цитирования:
Шишкин Е.С. Проверка функциональных свойств смарт-контрактов методом символьной верификации модели. Труды Института системного программирования РАН. 2018;30(5):265-288. https://doi.org/10.15514/ISPRAS-2018-30(5)-16
For citation:
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
Послать статью по эл. почте 