ВКР: Верификация контрактов в криптовалюте Ethereum

1




Введение

Блокчейн – технология для поддержания функционирования распределенных полностью реплицированных баз данных. Впервые эта технология была применена в сети криптовалюты Bitcoin. Сеть Bitcoin состоит из аккаунтов, совершающих друг с другом финансовые сделки, называемые транзакциями. Данные обо всех транзакциях специальным образом собираются в блоки, блоки последовательно связаны друг с другом (отсюда термин блокчейн – цепочка блоков). Процесс сбора транзакций в блоки называется майнингом. Цепочка блоков представляет собой базу данных, содержащую информацию обо всех совершенных финансовых сделках. Так как постоянно совершаются новые транзакции, цепочка блоков постоянно обновляется: в конец последовательности добавляются новые блоки, старые при этом не изменяются (что чрезвычайно важно). Каждый аккаунт хранит собственный экземпляр цепочки блоков. Блокчейн-сеть принимает все необходимые меры, чтобы цепочки на всех аккаунтах были одинаковы. Единая централизованная база данных отсутствует, а значит, невозможно фальсифицировать данные в единственном месте так, чтобы ввести этим в заблуждение все аккаунты сети. Кроме того, аккаунты обмениваются между собой данными без участия посредников (peer-to-peer).

В роли аккаунтов в блокчейн-сети могут выступать онлайн-сервисы. Цепочка блоков может хранить данные не только о балансах и переводах денег, но и любые представляющие интерес данные. Эти возможности блокчейн-технологии успешно используются сетью Ethereum. Также как сеть Bitcoin, сеть Ethereum представляет собой множество аккаунтов, обменивающихся между собой информацией в процессе транзакций. Криптовалюта Ethereum предназначена для совершения аккаунтами финансовых сделок. Существуют аккаунты двух видов: внешние и внутренние. Внешние аккаунты не имеют исходного кода, и все решения об их действиях в сети принимаются человеком извне. Внутренние аккаунты иначе называются контрактами или смарт-контрактами. Каждый внутренний аккаунт представляет собой программу, полностью определяющую действия этого аккаунта в сети.

Как любая программа, контракт может быть подвержен уязвимостям. Уязвимости в кодах контрактов привели к нескольким известным атакам злоумышленников в сети Ethereum с крупными финансовыми потерями. Так, ущерб от атаки TheDAO в июне 2016 года составил $74 млн [14], а за 2017 год было украдено $300 млн [15].

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

Формальная верификация кода – строгое математическое доказательство соответствия кода спецификациям (формальным требованиям). В частности,