АЛГЕБРАЇЧНИЙ ПІДХІД ДО АНАЛІЗУ СМАРТ-КОНТРАКТІВ НА TEAL

Анотація

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

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

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

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