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

Первое упоминание о смарт контракте было представлено в 1994 г американским ученым в области информатики, криптографии и права, Ником Сабо.

Смарт-контракт (или умный контракт) представляет собой компьютерный алгоритм для формирования, управления и предоставления информации о владении чем-либо. В более узком смысле под смарт-контрактом понимается набор функций и данных, находящихся по определённому адресу в блокчейне.

Другими словами, смарт-контракт — это договор между несколькими сторонами об установлении юридических прав и обязанностей, которые прописываются в виде программного кода и исполнятся в специальной программной среде.

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

Смарт-контракты обладают следующими свойствами:

Структура смарт-контрактов основана на цикле: «If … then», «If <<условие выполнения контракта>>, «then» <<операция>>. После исполнения контракта происходит запись результата операции в распределенный реестр.
Пример: в случае выигрыша скакуна на конных скачках, смарт-контракт выполняет операцию перевода выигрыша участникам контракта по заранее прописанным в контракте условиям.
Смарт-контракты – договор, реализованный на программном языке, это позволяет минимизировать возможность различной/неправильной интерпретации договора участниками взаимодействия.
Среда запуска и исполнения смарт-контрактов предоставляет надежное окружение, обеспечивающее прозрачность взаимодействия и подлинность отслеживания совершаемых транзакций/операций.

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

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

Однако у смарт-контрактов есть ряд недостатков:

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

Данные недостатки обязывают задуматься о введении дополнительной проверки/тестирования программного кода смарт-контракта для повышения надежности и корректности условий его исполнения.

Одним из способов решения данной задачи является применение формальной верификации смарт-контрактов.

Формальная верификация – формальное моделирование системы, которое позволяет увидеть и проверить правильность функционирования моделируемой системы и подсветить ее слабые стороны.

Формальную верификацию можно воспринимать, как вид тестирования, если грубо – это оценка снизу, верифицирую, мы гарантируем, что система отработает по описанному сценарию и не даст сбоев в логике.

Также формальная верификация может служить мостом для понимания между разработчиком контракта и его заказчиком. Зачастую заказчики хотят быть уверены, что фиксированный смарт-контракт выполняет именно те действия и по тем условиям, о которых договорились стороны договора. Но как в этом убедиться, если стороны договора не владеют языками программирования?

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

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

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

Очевидно, что дополнительная проверка требуется особенно, когда речь идет о финансовых транзакциях или иных действиях, цена ошибок которых достаточна велика. Аудит и тестирование – обычное дело в экономической и инженерной сфере. Технология смарт-контрактов стоит на стыке этих областей, поэтому вполне логично применить к ней повышенные требования надежности и безопасности выполнения операций.

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

Применение формальной верификации и формального моделирования способно сильно сократить временные издержки разработки контрактов за счет проверки их корректности еще на ранних этапах разработки контрактов.

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

Далее планирую статью, где рассмотрю на конкретном примере вариант создания формальной модели для простейшего смарт-контракта.

Не переключайтесь! ?

Формальная верификация смарт-контрактов