AN ALGEBRAIC APPROACH TO THE VERIFICATION OF SMART CONTRACTS IN TEAL

Олександр  Летичевський; Володимир  Песчаненко; Максим  Полторацький; Ольга Коннова

doi:10.14308/ite000774

Автор(и)

Олександр Летичевський Інститут кібернетики імені В. М. Глушкова НАН України https://orcid.org/0000-0003-0856-9771
Володимир Песчаненко Херсонський державний університет https://orcid.org/0000-0003-1013-9877
Максим Полторацький Херсонський державний університет https://orcid.org/0000-0001-9861-4438
Ольга Коннова Херсонський державний університет https://orcid.org/0000-0001-5590-9527

DOI:

https://doi.org/10.14308/ite000774

Ключові слова:

блокчейн, смарт-контракти, TEAL, інсерційне моделювання, алгебраїчне програмування, верифікація

Анотація

Блокчейн та смарт-контракти змінили сучасний світ. Вони допомагають забезпечити безпеку та довіру до транзакцій, революціонізують фінанси, логістику, охорону здоров’я та багато інших галузей. Смарт-контракти засновані на програмному коді, тому можуть містити помилки, які призводять до некоректного виконання контракту. Оскільки сфера використання смарт-контрактів часто пов’язана з фінансами, ціна таких помилок може бути досить високою. Крім того, помилки в смарт-контрактах, які вже були надіслані в мережу, неможливо виправити через незмінну природу блокчейна. Цю проблему можна вирішити за допомогою верифікації коду смарт-контракту, який дозволяє розробникам перевірити правильність свого коду та захистити його від можливих помилок і вразливостей.

У цій статті пропонується використання інсерційного моделювання для верифікації коду смарт-контракту для блокчейну Algorand. Цей блокчейн є одним із найшвидших та недорогих блокчейнів, який має розширені можливості смарт-контрактів із низькою комісією за транзакції. Мова, яка використовується для створення смарт-контрактів в Algorand, називається Transaction Execution Approval Language (TEAL).

У цій роботі ми розглядаємо наявні інструменти для перевірки коду TEAL і описуємо можливості, які надає кожен з них. Серед цих інструментів Graviton, Tealer, Algo Builder/runtime. У цій статті ми описуємо особливості мови TEAL, а також наводимо приклади написання смарт-контракту з її використанням.

Ми пропонуємо власну методику верифікації створеного смарт-контракту. Він полягає у використанні алгебраїчного підходу, який реалізовано в рамках системи інсерційного моделювання для перевірки коду смарт-контракту. Такий підхід дозволить нам перевірити код смарт-контракту на досяжність і наявність взаємоблокувань та недетермінізмів.

Завантаження

Дані завантаження ще не доступні.

Показники метрики:

##plugins.generic.paperbuzz.loading##

Посилання

1. Nakamoto, S. (2008). Bitcoin: A peer-to-peer electronic cash system. Decentralized business review.
2. What are smart contracts on blockchain?, IBM. https://www.ibm.com/topics/smart-contracts
3. Jesse Coghlan. (2022, May 03). More than $1.6 billion exploited from DeFi so far in 2022. Cointelegraph. https://cointelegraph.com/news/more-than-1-6-billion-exploited-from-defi-so-far-in-2022
4. The world’s most powerful and sustainable blockchain. https://algorand.com/
5. The smart contract language. Algorand Developer Portal. https://developer.algorand.org/docs/get-details/dapps/avm/teal/
6. Graviton. https://github.com/algorand/graviton
7. Graviton Algorand, https://github.com/algorand/graviton/blob/main/graviton/README.md
8. Tealer. https://github.com/crytic/tealer
9. Vara Prasad Bandaru. (2022, February 09). Detector Documentation. https://github.com/crytic/tealer/wiki/Detector-Documentation#missing-assetcloseto-field-validation
10. Algo Builder. Testing TEAL. //https://algobuilder.dev/guide/testing-teal.html
11. Letichevsky, A., & Gilbert, D. (2000). A model for interaction of agents and environments. In Recent Trends in Algebraic Development Techniques: 14th International Workshop, WADT’99, Château de Bonas, September 15-18, 1999 Selected Papers 14 (pp. 311-328). Springer Berlin Heidelberg.
12. Letichevsky, A. A., & Gilbert, D. R. (1996, October). A universal interpreter for nondeterministic concurrent programming languages. In Fifth Compulog network area meeting on language design and semantic analysis methods.
13. Letichevsky, A., Letychevskyi, O., Peschanenko, V., & Poltorackij, M. (2017, September). An algebraic approach for analyzing of legal requirements. In 2017 IEEE 25th International Requirements Engineering Conference Workshops (REW) (pp. 209-212). IEEE.
14. Letychevskyi, O. O., Peschanenko, V. S., & Poltorackiy, M. Y. (2022). Algebraic approach to the analysis of legal documents. PROBLEMS IN PROGRAMMING, (3-4), 117-127.
15. Letychevskyi, O., Peschanenko, V., Radchenko, V., Poltoratskyi, M., & Tarasich, Y. (2019). Formalization and algebraic modeling of tokenomics projects. In CEUR Workshop Proceedings (pp. 577-584).
16. Letychevskyi, O., Peschanenko, V., Poltoratskyi, M., & Tarasich, Y. (2020). Our approach to formal verification of token economy models. In Information and Communication Technologies in Education, Research, and Industrial Applications: 15th International Conference, ICTERI 2019, Kherson, Ukraine, June 12–15, 2019, Revised Selected Papers 15 (pp. 348-363). Springer International Publishing.
17. Letychevskyi, O. O., Peschanenko, V. S., Poltorackiy, M. Y., Tarasich, Y. H., & Vinnyk, M. O. (2022). Formal semantics and analysis of tokenomics properties. PROBLEMS IN PROGRAMMING, (3-4), 128-138.
18. Letychevskyi, O., Tarasich, Y., Peschanenko, V., Volkov, V., Sokolova, H., & Poltoratskyi, M. (2022, November). Algebraic Modeling as One of the Methods for Solving Organic Chemistry Problems. In Information and Communication Technologies in Education, Research, and Industrial Applications: 17th International Conference, ICTERI 2021, Kherson, Ukraine, September 28–October 2, 2021, Revised Selected Papers (pp. 180-202). Cham: Springer International Publishing.
19. Letychevskyi, O. A., Peschanenko, V., Poltoratskyi, M., & Tarasich, Y. (2020). Platform for Modeling of Algebraic Behavior: Experience and Conclusions. In ICTERI Workshops (pp. 42-57).
20. Jacobson, F., & Andersson Kasche, G. (2022). Tracing of Second-Life Computer Components using Smart Contracts on the Algorand Blockchain: A study on how blockchain technology can benefit the life cycle of computer components.
21. Letichevsky, A. A., Kapitonova, Y. V., Volkov, V. A., Letichevsky, A. A., Baranov, S. N., Kotlyarov, V. P., & Weigert, T. (2005). Systems specification by basic protocols. Cybernetics and Systems Analysis, 41, 479-493.
22. Letichevsky, A., Kapitonova, J., Letichevsky Jr, A., Volkov, V., Baranov, S., Weigert, T.: Basic protocols, message sequence charts, and the verification of requirements specifications. Computer Networks 49(5), 661-675 (2005).