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

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