ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ СМАРТ-КОНТРАКТОВ В БАНКОВСКОЙ СФЕРЕ

В современное время смарт-контракты активно применяются в финансовом секторе, в том числе в банковской сфере. Применение смарт-контрактов является одной из перспективных областей автоматизации предоставления банковских услуг. Так британский банк Barclays использовал смарт-контракты для проведения сделок [1].

В то же время смарт-контракты привносят и дополнительные риски за счет основных свойств своей работы. Одним из таких свойств является неизменность, то есть после того, как смарт-контракт попал в блокчейн-сеть, его нельзя изменить [2]. Данное свойство является как и преимуществом смарт-контрактов, что позволяет сторонам точно знать, что параметры не будут изменены, так и недостатком. Например, разработчик может внести уязвимости в работу смарт-контракта или неправильно трактовать спецификации к разработке, что может привести к логическим ошибкам.

Так как смарт-контракты не применяются повсеместно в банковской сфере вопрос верификации смарт-контрактов является важным аспектом обеспечения информационной безопасности

Целью данной работы является составление модели смарт-контракта, для проведения формальной верификации, определение необходимости проведения формальной верификации смарт-контрактов в банковской сфере.

В ходе работы составлена модель, с помощью которой проводилась формальная верификация смарт-контракта, реализующего функцию кредитования, проведено тестирование с использованием инструментов, находящихся в открытом доступе [3].

Формальная спецификация данного контракта имеет следующий вид - смарт-контракт реализует функцию кредитования между представителем банка и клиентом. Представитель банка заполняет данные контракта: сумма долга, процентная ставка, срок кредитования.  В свою очередь клиент обязан выплачивать минимальную сумму платежа, для погашения кредита заемщик должен выплатить остаток по кредиту.

Приведем реализацию функций данного смарт-контракта на языке программирования Solidity:

function getDebt() public view returns(uint, uint, uint)

{

        return (reqAmount, minAmount, paidAmount);

}

function paidDebt() onlyDebtor inState(State.Active) condition(paidAmount < (reqAmount - minAmount)) public payable

  {

paidAmount = paidAmount + minAmount;

debtor.transfer(minAmount);

}

function closeDebt() onlyDebtor inState(State.Active) condition(paidAmount > (reqAmount - minAmount) && paidAmount < reqAmount) payable publiс 

{

state = State.Close;

paidAmount = paidAmount + (reqAmount - paidAmount);

          debtor.transfer(reqAmount - paidAmount);

}

Состоянием смарт-контракта (кредита) охарактеризуем как Active (кредит открыт) и Close (кредит закрыт). 

На основании работы [4], из всех перечисленных данных составлена модель смарт-контракта, рисунок 1, в виде графа переходов состояний, где ребра являются функциями смарт-контракта, вершины являются состояниями смарт-контракта. Причем переход, при вызове функции, возможен при выполнении условий, описанных в спецификации. 

Рисунок 1. Модель смарт-контракта

В результате тестирования смарт-контракта (без ошибок) инструментами, находящимися в открытом доступе, выявлены уязвимости, представленные в таблице 1. Данные уязвимости могут быть исправлены во время разработки программистом. 

Таблица 1. 

Результаты тестирования смарт-контракта

Далее рассмотрены логические ошибки, которые могли быть совершены в процессе разработки программистом, таблица 2, cмарт-контракты с данными ошибками не проходят формальную верификацию с помощью описанной модели.

Таблица 2. 

Логические ошибки

В результате тестирования смарт-контрактов с ошибками, данными инструментами не было выявлено недоступности функций или ошибок выхода значения переменной из допустимых границ, таблица 3.

Таблица 3. 

Результаты тестирования смарт-контрактов с ошибками

Результаты тестирования показывают, что этап формальной верификации является обязательным при разработке смарт-контракта и в дальнейшем его использование в банковской сфере. Следует отметить, так как нет четко сформулированного метода проведения формальной верификации смарт-контрактов, весь процесс формальной верификации стоит регламентировать.

На основе полученных результатов сделаны следующие выводы: рассмотренные инструменты не позволяют выявить ошибки, выявленные формальной верификацией, необходимо проводить формальную верификацию для смарт-контрактов в банковской сфере. В статье рассмотрен вариант проведения формальной верификации смарт-контрактов, выявлена необходимость в использовании формальной верификации при разработке смарт-контрактов в банковской сфере.

Список литературы:

1. Смарт-контракты: аналит. обзор, окт. 2018, Центральный банк РФ. — М.: [не указано], 2018. — 22 с.
2. Андреева Ю. А., Сафарьян О. А. Создание и тестирование смарт-контракта // Молодой исследователь Дона. —   2019 —   № 3 (18). —  С. 84-88.
3. Angelo, Monika Di and Gernot Salzer. A Survey of Tools for Analyzing Ethereum Smart Contracts. // IEEE International Conference on Decentralized Applications and Infrastructures (DAPPCON). —   2019. — P. 69-78.
4. Шишкин Е.С. Проверка функциональных свойств смарт-контрактов методом символьной верификации модели // Труды Института системного программирования РАН. —  2018. — № 30(5). — С. 265-288.