Сборники трудов ИСП РАН


Проверка функциональных свойств смарт-контрактов методом символьной верификации модели

Шишкин Е.С. (ИнфоТеКС, Москва, Россия)

Аннотация

В статье рассматривается подход к проверке функциональных свойств смарт-контрактов платформы Ethereum методом символьной верификации модели. Описанный подход позволяет верифицировать выполнение 3х видов свойств на трассах ограниченной дли-ны, а также осуществлять проверку выполнимости инварианта. Описана математическая модель среды исполнения смарт-контрактов, проведена формализация выделенных ви-дов свойств в рамках этой модели, описана процедура трансляции всего перечисленного в язык ограничений SMT-решателя. Жизнеспособность предлагаемого подхода иллю-стрируется на примере верификации макетного смарт-контракта MiniDAO, упрощённой версии известного TheDAO. За несколько секунд макет находит контр пример одному нетривиальному функциональному требованию, указывая на ошибку в бизнес-логике смарт-контракта. Насколько нам известно, эта работа - одна из первых попыток описать инструмент, помогающий осуществлять формальную проверку функциональных свойств смарт-контрактов в автоматическом режиме.

Ключевые слова

символьная верификация модели; смарт-контракты; блокчейн; формальная спецификация

Издание

Труды Института системного программирования РАН, том 30, вып. 5, 2018, стр. 265-288.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2018-30(5)-16

Для цитирования

Шишкин Е.С. Проверка функциональных свойств смарт-контрактов методом символьной верификации модели. Труды Института системного программирования РАН, том 30, вып. 5, 2018, стр. 265-288. DOI: 10.15514/ISPRAS-2018-30(5)-16.

Полный текст статьи в формате pdf Вернуться к содержанию тома