Исследование и разработка вероятностных методов верификации систем распределенного реестра тема диссертации и автореферата по ВАК РФ 00.00.00, кандидат наук Федотов Иван Андреевич

• Федотов Иван Андреевич
• кандидат наук
• 2022

Оглавление диссертации кандидат наук Федотов Иван Андреевич

Введение

Глава 1. Обзор технологии распределённого реестра и

особенности ее применения

1.1 Ознакомление с технологией распределенного реестра

1.2 Предпосылки создания технологии распределенного реестра

1.3 Типы сетей на основе технологии распределенного реестра

1.4 Области применения технологии распределенного реестра

1.5 Уязвимости технологии распределенного реестра

1.6 Выводы главы

Глава 2. Верификация систем со стохастическими свойствами.

Моделирование блокчейн систем

2.1 Случайные переменные и распределение вероятности

2.2 Моделирование стохастических систем с дискретным временем

2.3 Спецификация для стохастических систем с дискретным временем

2.4 Способы верификации моделей со стохастическими свойствами

2.4.1 Численные методы вероятностной проверки моделей

2.4.2 Статистическая проверка моделей

2.5 Инструментальные средства верификации с помощью статистической проверки моделей

2.6 Верификация систем распределенного реестра

2.7 Выводы главы

Глава 3. Верификация систем распределенного реестра с

помощью статистической проверки моделей

3.1 Описание моделей атак

3.1.1 Атака DNS

3.1.2 Двойная трата и спам пула памяти

3.1.3 Двойная трата и задержка консенсуса

3.2 Экспериментальная оценка

3.2.1 Атака DNS

3.2.2 Двойная трата и спам пула памяти

3.2.3 Двойная трата и задержка консенсуса

3.3 Анализ экспериментальных результатов

3.3.1 Атака DNS

3.3.2 Двойная трата и спам пула памяти

3.3.3 Двойная трата и задержка консенсуса

3.4 Смежные работы и выводы по проверке моделей атак на блокчейн системы

3.5 Выводы главы

Глава 4. Построение модели и спецификации для протоколов многосторонних соглашений со стохастическими

свойствами

4.1 Использование многосторонних соглашений для достижения консенсуса в системах распределенного реестра

4.1.1 Типы многосторонних соглашений

4.1.2 Примеры использования многосторонних соглашений в платформах распределенного реестра

4.2 Моделирование протоколов консенсуса

4.3 Верификация моделей многосторонних соглашений

4.3.1 Построение спецификации для взвешенного консенсуса

4.3.2 Верификация взвешенного консенсуса

4.3.3 Построение спецификации для консенсуса, заданного в

виде логической формы

4.3.4 Верификация взвешенного консенсуса, заданного в виде конъюнктивной нормальной формы

4.4 Выводы главы

Глава 5. Разработка и применение программного комплекса

верификации и планировки многосторонних соглашений

5.1 Архитектура программного комплекса

5.2 Программный модуль анализа многосторонних соглашений

5.3 Модуль планировки многосторонних соглашений

5.4 Интеграция программного комплекса с платформой Hyperledger Fabric

5.5 Постановка эксперимента для оценки работы интеграции программного комплекса с Hyperledger Fabric

5.6 Анализ результатов эксперимента

5.7 Выводы главы

Заключение

Список сокращений и условных обозначений

Словарь терминов

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

Список рисунков

Список таблиц

Приложение А. Матричное представление моделей консенсуса

в виде цепи Маркова с дискретным временем

Приложение Б. Таблицы измерений для эксперимента по

проверке корректности работы клиента Hyperledger Java Gateway

Введение диссертации (часть автореферата) на тему «Исследование и разработка вероятностных методов верификации систем распределенного реестра»

Введение

В диссертационной работе рассматривается проблема верификации систем распределенного реестра (СРР) со стохастическими параметрами. Также рассматривается задача проверки модели на основе заданной спецификации и решается практическая задача по разработке инструмента по автоматической верификации и проверке моделей промышленных систем распределенного реестра.

Распределенный реестр представляет базу данных, распределенную между несколькими вычислительными устройствами, каждое из которых представляет узел сети [1]. Ключевой особенностью распределенного реестра является отсутствие единого центра управления, а соответственного и единой точки отказа. Каждый узел может предложить новую запись и хранит копию всего реестра. С помощью многостороннего соглашения узлы договариваются о принятии или отклонении записи в реестре. При достижении соглашения хранилище обновляется и каждый узел сохраняет обновлённую версию хранилища.

В работе также рассматривается блокчейн, один из видов распределенного реестра. Помимо перечисленных особенностей распределенного реестра в сети блокчейн транзакции сгруппированы в блоки. Запись в реестр также происходит по блокам. Каждый последующий блок транзакций хранит ссылку на предыдущий. Таким образом, чтобы изменить некоторую запись в прошлом требуется изменить все последующие записи на всех необходимых узлах. В блокчейн можно только добавлять блоки, но не удалять, что делает блокчейн постоянно растущим реестром транзакций. Разработанные алгоритмы верификации могут быть применены как к блокчейн сетям, так и к распределённому реестру вцелом. В работе рассматриваются такие блокчейн сети и платформы, как Hyperledger Fabric [2], Ethereum [3], Bitcoin [4] и другие. Примерами распределенного реестра могут служить такие платформы, как IOTA [5], Hederá Hashgraph [6], Swirilds.

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

ки. В области цепочек поставок СРР выступают связующим звеном между сторонами, среди которых нет доверия. Это также позволяет отслеживать жизненный цикл продукции и обеспечивает прозрачность её передвижения от производителя к поставщику и далее к потребителю. В сфере права собственности СРР используется для отслеживания права обладания определенным активом. Создается цифровая копия актива, которая называется "невзаимозаменяемый токен"или КЕТ, "поп-£и^аЬ1е 1оскеп". Цифровая копия присваивается реально существующему предмету, а в СРР ведется учет права собственности КЕТ [7]. Отслеживание права обладания с помощью СРР применяется в фармацевтике, нефтегазовой отрасли и других областях [8] [9]. Похожая логика используется и в компьютерных играх, и виртуальных аукционах [10]. Цифровые копии реальных предметов могут торговаться на виртуальных биржах или выступать атрибутом компьютерных игр. СРР также используется в качестве платформы для проведения электронных голосований [6]. Прозрачность ведения транзакций исключает возможность фальсификации результатов голосования.

Так как технология распределенного реестра (ТРР) получила активное распространение в областях, связанных с финансами и активами, ошибки в реализациях таких систем могут привести к существенным финансовым потерям. В связи с этим возрастает потребность в повышении надежности и отказоустойчивости систем, использующих распределенный реестр. Более того, многие блокчейн сети, такие как Е^егеиш и В^сот, не позволяют изменять код или параметры системы после развертывания. Если ошибка или уязвимость не выявлена до введения системы или кода в промышленную эксплуатацию, то ошибку уже нельзя будет исправить. Это повышает потребность отлавливания и исправления ошибок на стадии разработки.

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

то валидация отвечает на вопрос: удовлетворяет ли спецификация бизнес требованиям? В текущей работе рассматривается возможность верификации СРР с помощью формальных методов.

Моделирование системы с последующей верификацией позволяет на стадии разработки выявить ошибки и уязвимости [11]. Чтобы проверить, что система удовлетворяет спецификации до развертывания самой системы, можно построить ее модель и проверить, что модель удовлетворяет спецификации. Если модель не удовлетворяет спецификации, можно скорректировать параметры модели и проверить, что модифицированная версия удовлетворяет спецификации. После чего можно также изменить параметры системы. Формальные методы верификации позволяют математически точно определить, что модель удовлетворяет спецификации. После поверки, если модель удовлетворяет спецификации, можно вводить систему в промышленную эксплуатацию. В противном случае можно предложить изменить параметры системы или спецификации таким образом, чтобы модифицированная модель удовлетворяла спецификации. Ввиду того, что технология распределенного реестра начала использоваться в промышленной эксплуатации недавно, методы и инструменты для её верификации представляют открытый вопрос для исследования.

СРР могут зависеть от стохастических параметров. Например, можно определить вероятность подмены DNS адреса [12] или вероятность того, что транзакция будет принята или отклонена сетью. Это приводит к тому что модель системы также зависит от стохастических параметров, и переходы между состояниями модели могут случаться с определенной вероятностью. Такие системы могут быть описаны в виде различных моделей, например, в виде цепи Маркова или стохастических автоматов [13].

Методы верификации моделей со стохастическими параметрами хорошо изучены. Существуют различные способы представления систем со стохастическими параметрами: Марковский процесс принятия решений, цепь Маркова с дискретным временем, цепь Маркова с непрерывным временем и другие [13]. На данных моделях можно задавать спецификацию в виде линейной временной логики, логики вычислительного дерева с вероятностными операторами [14]. Формальные методы позволяют проверить, что модель удовлетворяет спецификации.

Однако существующие на момент проведения исследования технологии и инструменты не предоставляют возможности верификации СРР со стохастическими свойствами. Авторы выдвинули предположение об использовании метода статистической проверки для верификации СРР [15] [16]. Но данные исследования лишь показывают возможность верификации СРР со стохастическими параметрами, но не предлагают конкретных алгоритмов для этого. Более того, в предлагаемых работах рассматривается только моделирование смарт-контрак-тов и не проведена оценка использования СПМ на промышленных системах.

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

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

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

Вопрос верификации блокчейн систем является актуальным и рассматривается в ведущих исследовательских центрах. В университете Иннополис ведется разработка блокчейн системы 1ппоСЬат с использованием методов формальной верификации. Исследования с использованием доказательства безопасности для блокчейн систем ведутся и в университете ИТМО, где рассматривается

применение блокчейна в системах голосования, а также применение блокчей-на при разработке сетей 5G. Исследования также активно ведутся в институте Макса Планка программного обеспечения в Германии и в университете ETH в Швейцарии, где рассматриваются теоретические вопросы верификации блокчй-ен систем.

В области СРР исследовалась верификация логики программного кода смарт-контрактов, верификация выполнения смарт-контрактов. Проведено исследование по верификации протокола консенсуса, построенного на задаче византийских генералов. В данной диссертационной работе впервые верифицируются другие важные части блокчейн систем: механизм подключения DNS, возможность двойной траты, протоколы консенсуса со стохастическими свойствами. Разработаны алгоритмы для планировки отправки сообщений с целью достижения консенсуса между участниками блокчейн сети. Оптимальный способ отправки сообщений позволяет увеличить вероятность достижения консенсуса. Разработанные алгоритмы реализованы в виде программного комплекса и интегрированы в программный каркас построения и администрирования блокчейн сетей Hyperledger Fabric.

Моделирование и формальные методы верификации позволяют выявлять уязвимости блокчейн систем до введения их в промышленную эксплуатацию. Для анализа существующих решений и программных инструментариев верификации систем распределенного реестра был выбран метод систематического обзора. На основе обзора и требований к системам распределенного реестра для верификации был выбран метод статистической проверки моделей. При разработке программного комплекса применялась парадигма объектно-ориентированного программирования. Для анализа результатов статистического эксперимента прменялся U-тест Мана-Уитни.

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

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

Для достижения поставленной цели необходимо решить следующие задачи:

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

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

3. Разработать алгоритмы построения модели, а также спецификации и оптимизации блокчейн систем.

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

5. Провести серию экспериментов с целью доказательства корректности созданных решений. Провести анализ результатов экспериментов.

Основные положения, выносимые на защиту:

1. Исследованы и систематизированы методы и инструментальные средства для автоматической верификации и тестирования блокчейн систем. Верификация блокчейн систем со стохастическими свойствами выявлено как перспективное направление исследования.

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

3. В рамках задачи верификации протоколов консенсуса разработаны алгоритмы построения моделей разных типов консенсуса в виде Марковской цепи с дискретным временем и спецификации в виде вероятностной линейной временной логики. Верификация протоколов консенсуса позволит определить с какой впероятностью консенсус будет достигнут. Если вероятность мала, ее можно увеличить с помощью отправки сообщений на подтверждение в определенной последовательности. В зависимости от параметров консенсуса вероятность достижения консенсуса может быть увеличена до единицы. Разработан программный комплекс для построения модели, верификации и оптимизации консенсуса, заданных в виде логических формул. Программный комплекс интегрирован в программный каркас Нурег^§ег ЕаЬпс, который используется для построения и администрирования блокчейн сетей. Использование модифицированного программного каркаса Нурег^§ег ЕаЬпс позволяет увеличить вероятность достижения консенсуса до единицы, в зависимости от параметров консенсуса и сети.

Научная новизна:

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

2. Предложены и программно реализованы алгоритмы построения модели консенсуса в виде цепи Маркова с дискретным временем и спецификации в виде линейной временной логики.

3. Показана возможность применения метода статистической проверки моделей для верификации модели взвешенного консенсуса и консенсуса, заданного в виде линейной временной логики.

4. Предложен способ отправки сообщений подтверждения транзакции участникам консенсуса в блокчейн системах со стохастическими параметрами.

Практическая значимость подтверждается в интеграции разработанного программного комплекса с программным каркасом создания блокчейн систем Нурег^§ег ЕаЬпс, который может использоваться в промышленной экс-

плуатации. В работе путем моделирования были выявлены уязвимости блок-чейн систем, которые привели к значительным финансовым потерям в прошлом, и найдены способы их устранения. Разработанные модели можно использовать в системах промышленной эксплуатации. В моделях атак использовались статистические данные из реальных блокчейн систем, а интеграция алгоритмов с программным каркасом Hyperledger Fabric позволяет использовать предложенные алгоритмы в системах промышленной эксплуатации. Теоретические и практические результаты диссертационной работы использованы в рамках работы, проводимой организацией Atomize. Результатом внедрения является проведение испытаний на тестовой сети Hyperledger Fabric с использованием исследовательских наработок. Результаты проведенных исследований также были внедрены в курс "Автоматизация программирования"МФТИ. Внедрение в курс способствует подготовке специалистов в области блокчейн тех Внедрение в курс способствует подготовке специалистов в области блокчейн технологий.

Достоверность результатов подтверждается корректностью применения формальных методов верификации, метода проведения систематического обзора, а также метода статистического анализа экспериментов. По теме исследования в рецензируемых журналах были опубликованы 2 статьи, индексируемых системой Scopus, и 2 статьив журналах перечня ВАК. Также опубликованы 3 тезиса в рамках Всероссийской научной конференции МФТИ.

Апробация работы. Результаты работы были представлены на всероссийских и международных конференциях:

1. Увеличение пропускной способности гибридного алгоритма консенсуса // 61-я Всероссийская научная конференция МФТИ, - Москва, Россия, 2018.

2. Верификация смарт-контрактов на основе статистической проверки моделей // 63-я Всероссийская научная конференция МФТИ. - Москва, Россия, 2020.

3. Статистическая проверка моделей для протоколов консенсуса подтверждения транзакций // 64-я Всероссийская научная конференция МФТИ. - Москва, Россия, 2021.

4. Statistical Model Checking of Common Attack Scenarios on Blockchain // The 9th International Symposium on Symbolic Computation in Software Science. - Linz, Austria, 2021.

5. Towards verification of probabilistic multi-party consensus protocols: Constructing algorithms for verification of multi-party protocols with probabilistic properties // The 5th International Conference on Big Data and Smart Computing. - Yokohama, Japan, 2022.

6. Optimizing multi-party agreement protocols // 4th Conference on Blockchain Research & Applications for Innovative Networks and Services. - Paris, France, 2022.

Личный вклад. Автор лично получил все основные теоретические и практические результаты работы, в частности:

1. Исследовал методы выявления и устранения уязвимостей в блокчейн системах и выявил перспективные направления исследования.

2. Построил модели атак на блокчейн системы и применил метод статистической проверки моделей для верификации и уменьшения вероятности успеха атаки.

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

4. Разработал и реализовал программный комлпекс для анализа протоколов консенсуса и планирования отправки сообщений на подтверждение в протоколах консенсуса.

Алгоритмы и разработки, представленные в диссертации, опубликованы в следующих рецензируемых журналах:

1. Систематический обзор исследований в области автоматической верификации кода смарт-контрактов / Федотов И., Хританков А. // Программная инженерия, 2020, стр. 3-13. Индексируется базой данных RSCI.

2. Statistical Model Checking of Common Attack Scenarios on Blockchain / Fedotov I., Khritankov A. // EPTCS 342, 2021, стр. 65-77. Индексируется базой данных Scopus.

3. Towards verification of probabilistic multi-party consensus protocols: Constructing algorithms for verification of multi-party protocols with

probabilistic properties / Fedotov I., Khritankov A., Barger A. // ACM, ICSIM, 2022, стр. 100-105. Индексируется базой данных Scopus.

4. Автоматическая верификация многосторонних соглашений и планирование отправки сообщений в системах распределенного реестра / Федотов И., Хританков А., Обидаре М. // Программная инженерия, 2022, стр. 200-213. Индексируется базой данных RSCI.

5. Optimizing multi-party agreement protocols / Fedotov I., Khritankov A., Barger A. // 2022 4th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS), 2022, стр. 55-58.

Глава 1. Обзор технологии распределённого реестра и особенности

ее применения

В данной главе рассмотрим основные понятия ТРР. Глава представляет собой обзор технологии распределенного реестра, а также области применения. Ознакомление с этими темами необходимо для того, чтобы понять, какие части СРР наиболее нуждаются в верификации. После первоначального ознакомления с ТРР коснемся исторических предпосылок создания и внедрения СРР, а также рассмотрим типы сетей и многосторонних соглашений, используемых для принятия или отклонения транзакции. Далее более детально рассмотрим области применения ТРР, так как особенности применения необходимо учитывать при создании алгоритмов и инструмента верификации. Также рассмотрим уязвимости, с которыми может столкнуться разработчик и пользователь.

1.1 Ознакомление с технологией распределенного реестра

Распределённый реестр представляет собой хранилище, в котором данные хранятся в сети децентрализованных узлов [17]. Данные совместно используются, реплицируются и синхронизируются между членами сети. Каждый участник СРР называется узлом. В зависимости от параметров сети каждый узел может хранить либо все записи сети, либо их часть. В последнем случае говорят, что данные шардируются между членами сети. В отличие от централизованных баз данных в распределённом реестре нет единой точки отказа.

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

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

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

В блокчейне можно выделить следующие виды узлов:

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

— Майнер. Также является разновидностью узлов полного вида. Встречается в сетях блокчейн, использующих консенсус вида "Ргоо£-о£-Шогк". Решает сложную математическую функцию, чтобы провалидировать транзакцию, предложенную в сети.

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

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

Алгоритм обработки транзакций в распределённом реестре может быть записан в виде программного кода. В сетях блокчейн, таких как Е^егеиш, подобный код называется смарт-контрактом. Во фреймворке Нурег^§ег ЕаЬпс

(HLF) программный код, в котором заключена логика одобрения, называется чейнкодом. Логика обработки транзакций может быть записана на существующем языке, например, Go или Java. Также известны разработки специального языка для записи логики обработки транзакций, например, Solidity в Ethereum. Вычисления, заключённые в алгоритме обработки транзакций, на каждом узле выполняются независимо. После независимого выполнения узлы сравнивают результаты вычисления между собой.

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

— Доказательство работы, или Proof-of-Work (PoW). В данном виде консенсуса майнеры создают блоки для их включения в сеть блокчейн. Верификация включает в себя решение математической задачи, которая требует значительной вычислительной мощности. Степень сложности решения математической задачи зависит от времени, за которое майнер может сделать новый блок. Например, в сети Bitcoin вычислительная сложность растет с числом блоков, которые уже присутствуют в сети.

— Доказательство владения, или Proof-of-Stake (PoW). Параметры архитектуры сети блокчейн определяют валидаторов. Валидаторы могут меняться каждый раунд подтверждения. Например, валидаторами могут быть узлы, которые имеют больше всего активов в сети, или узлы, которые дольше всего находятся в сети.

Список литературы диссертационного исследования кандидат наук Федотов Иван Андреевич, 2022 год

- г

2 3 4 5 6 7

число обратных переходов

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

— Соответсвует ли результат ожидаемому эффекту? Результат соответсву-ет ожидаемому эффекту. Применение моделей с обратными переходами увеличивает вероятность подтверждения транзакции в сети.

— Можно ли обобщить полученные результаты на другие области применения? Эксперимент был поставлен для верификации и планировки политик одобрения Hyperledger Fabric. Разработанные алгоритмы и программный комплекс можно применять и для других блокчейн сетей, в которых необходимо верифицировать консенсус, а также планировать отпраку сообщений. Таким образом, результат эксперимента можно обобщить на области применения блокчейн технологии, в которых трбуется анализ и планировка консенсуса.

— Является ли эксперимент воспроизводимым? Программный код эксперимента представлен в гит репозитории [151] [140] [141] [154]. Его можно воспроизвести, следуя инструкциям из постановки эксперимента.

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

1.0

3 0.9 >

о

2 08

I

и 0.6

.о

и 0.4

0

1

§ 0.3

о.

си

0.1

о.о -1-1-1-1-1-1-1-1-1-1

2 5 8 11 14 17 20 23 26 29 32

Математическое ожидание числа сообщений

Рисунок 5.11 — График зависимости вероятности достижения консенсуса от математического ожидания числа сообщений для многофакторного эксперимента с двумя организациями.

он может полагаться на гипотезу НО. Использование модели без обратных переходов дает результат, идентичный использованию базовой реализации клиента. Если же пользователь хочет увеличить вероятность подтверждения за счет увеличения числа отправляемых сообщений, то можно полагаться на гипотезы Н1 и Н2. Между статистическими данными симуляции и статистическими данными эксперимента не было найдено статистически значимых различий. При критерии значимости О.О5 можно утверждать, что поведение симуляции модели соответсвует поведению тестовой сети. В симуляции можно видеть, что использование модели с обратными переходами увеличивает вероятность принятия транзакции. Такого же результата стоит ожидать и в реальной сети. Если параметры сети изменились, то пользователю следует пересчитать значения для моделей в модуле анализатора.

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

число обратных переходов

Рисунок 5.12 — График зависимости вероятности достижения консенсуса от числа обратных переходов для многофакторного эксперимента с двумя

организациями.

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

Стоит отметить следующее ограничение в применении разработанной модели в Hyperledger Fabric. Модель предполагает, что организации дают бинарные ответы: транзакция либо подтверждена, либо нет. Также возможно, что организация в силу задержек сети или потери сообщения не отвечает на запрос о подтверждении транзакции. Это равносильно отрицательному ответу. В проводимом эксперименте мы рассматривали вариант с задержками в сети, симулируя задержки с помощью инструмента tc. Однако существует и более широкий спектр ответов, в которых организация предоставляет не бинарный ответ, а результат выполнения чейнкода. В таком случае нельзя определить корректность ответа от организации при последовательной отправке сообщений. Для использования модели в виде классической цепи Маркова необходимо

Рисунок 5.13 — График зависимости математического ожидания числа сообщений от числа обратных переходов для многофакторного эксперимента с

двумя организациями.

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

5.7 Выводы главы

В пятой главе представлен программный комплекс для верификации и анализа протоколов консенсуса. Программный комплекс интегрирован в программный каркас Hyperledger Fabric. Программный комплекс состоит из двух модулей. Модуль анализа предназначен для построения моделей протоколов консенсуса в виде марковской цепи, а также для вычисления вероятности того, что консенсус будет достигнут. Строятся и верифицируются модели с различными комбинациями обратных переходов. Обратный переход представляет переход к корню дерева, если организация, от которой строится обратный переход не подтвердила транзакцию. По сути обратный переход заново запускает процесс достижения консенсуса. Однако вместе с вероятностью достижения консенсуса увеличивается и математическое ожидания числа сообщений, переданных в сети до достижения консенсуса. Пользователю предлагается выбрать модель с определенной вероятностью достижения консенсуса и математическим ожиданием числа сообщений. После этого выбранная модель передается в модуль планировщика. Модуль планировщика интегрирован в программный каркас Hyperledger Fabric. На основе выбранной модели совершается отправка сообщений участникам консенсуса. С помощью разработанного программного комплекса проведен многофакторный статистический эксперимент с целью выявить, как изменяется вероятность достижения консенсуса с применением разработанного программного комплекса. Данные статистического эксперимента проанализированы с помощью U-критерия Мана-Уитни. Установлено, что при заданном уровне значимости не удалось найти статистически значимых отличий между данными эксперимента и данными, который получились на выходе модуля анализатора. Помимо этого, по результатам модуля анализатора установлено, что использование модели с обратными переходами увеличивает вероятность достижения консенсуса. При заданном уровне значимости можно утверждать, что использование программного комплекса на модели с обратными переходами увеличивает вероятность достижения консенсуса. Таким образом, алгоритмы для верификации и планировки отправки сообщений впервые интегрированы в программный каркас для построения блокчейн сетей

Hyperledger Fabric. Также было установлено, что использование интегрированного программного модуля может увеличить вероятность принятия транзакций.

Заключение

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

— Выявление уязвимостей в сетях, использующих технологию блокчейн;

— Предложение способов для полного устранения уязвимостей или снижения вероятности сценария успеха злоумышленника;

— Верификация и анализ протоколов консенсуса с последующей модификацией условия консенсуса, если модель не удовлетворяет спецификации.

Результаты исследований подтверждают теоретическую и практическую значимость диссертационной работы. В частности, были получены следующие теоретические результаты:

— Предложено использование метода статистической проверки моделей для верификации блокчейн систем;

— Смоделированы наиболее распространенные атаки на блокчейн системы, имеющие стохастические свойства, а также предложены способы снижения вероятности успеха злоумышленника;

— Разработаны алгоритмы построения модели в виде марковской цепи и спецификации в виде вероятностной линейной временной логики для верификации протоколов консенсуса различного типа;

Также можно выделить следующие практические результаты работы:

— Разработан модуль автоматического анализа протоколов консенсуса с использованием метода статистической проверки моделей;

— Разработан модуль планировки отправки сообщений на подтверждение различным участникам консенсуса на основе выбранной модели;

— Проведена интеграция разработанных модулей с платформой построения блокчейн сетей Hyperledger Fabric;

— Поставлен и проведен статистиеский эксперимент, иллюстрирующий преимущество использования разработанного программного комплекса при построении блокчейн сетей;

— Разработанный программный комплекс интегрирован в учебный процесс в рамках курса "Автоматизация программирования".

Основные результаты работы опубликованы в рецензируемых журналах:

1. Систематический обзор исследований в области автоматической верификации кода смарт-контрактов / Федотов И. Хританков А. // Программная инженерия, 2020, стр. 3-13. Индексируется базой данных RSCI. Входит в перечень ВАК.

2. Statistical Model Checking of Common Attack Scenarios on Blockchain / Fedotov I., Khritankov A. // EPTCS 342, 2021, стр. 65-77. Индексируется базой данных Scopus.

3. Towards verification of probabilistic multi-party consensus protocols: Constructing algorithms for verification of multi-party protocols with probabilistic properties / Fedotov I., Khritankov A., Barger A. // ACM, ICSIM, 2022, стр. 100-105. Индексируется базой данных Scopus.

4. Автоматическая верификация многосторонних соглашений и планирование отправки сообщений в системах распределенного реестра / Федотов И., Хританков А., Обидаре М. // Программная инженерия, 2022, стр. 200-213. Индексируется базой данных RSCI. Входит в перечень ВАК.

5. Optimizing multi-party agreement protocols / Fedotov I., Khritankov A., Barger A. // 2022 4th Conference on Blockchain Research & Applications for Innovative Networks and Services (BRAINS), 2022, стр. 55-58.

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

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

сматривалось подмножество бинарных ответов участников, то есть когда участники либо подтверждают, либо отклоняют транзакцию. В широком смысле ответ необязательно должен быть бинарным. Например, участник может вернуть результат запуска кода транзакции, который может представлять не только булевую переменную. В этом случае можно использовать другие модели для стохастических систем, например скрытые цепи Маркова, либо строить цепь Маркова не в виде бинарного дерева, а в виде дерева с множеством переходов из одного узла. Каждый переход может соответсвовать ответу организации, которая присвоена узлу. В-третьих, можно интегрировать модуль отправки сообщений в другие клиенты Hyperledger Fabric, например, клиент Go или Node.js. Это является интересным направлением исследования с точки зрения практической реализации. Для других реализаций клиентов можно провести аналогичные эксперименты, которые были выполнены для клиента Java Gateway, чтобы показать эффективность разработанного программного комплекса. Перечисленные задачи кажутся перспективными и актуальными как в теоретических, так прикладных аспектах.

Список сокращений и условных обозначений

DNSSEC - Domain Name System Security Extensions- расширение безопасности для доменной системы имен.

PRISM - Probabilistic Symbolic Model Checker - символьный программный комплекс для вероятностной проверки моделей.

LTL - Linear Temporal Logic - линейная временная логика.

pLTL - Probabilistic Linear Temporal Logic - вероятностная линейная временная логика.

MLTL - Metric Linear Temporal Logic - метрическая линейная временная логика.

MTL - Metric Temporal Logic - метрическая временная логика.

BIP - Behaviour Interaction Process - поведение, взаимодействие, процесс.

SBIP - Statistical Behaviour Interaction Process - статистическое поведение, взаимодействие, процесс.

DNS - Domain Name System - доменная система имен.

IP-адрес -Internet Protocol адрес, адрес интернет протокола.

BIND - Berkeley Internet Name Domain, интернет-домен Беркли.

TCP - Transmission Control Protocol - протокол управления передачей.

HLF - Hyperledger Fabric.

DDoS - Distributed Denial-of-Service, распределенный отказ сервиса.

PoW - Proof of Work, доказательство работы.

PoS - Proof of Work, доказательство владения.

PoWg - Proof of Work, доказательство веса.

PBFT - Practical byzantine fault tolerance, консенсус практической византийской отказоустойчивоси.

dPBFT - Delegated practical byzantine fault tolerance, делегированный консенсус практической византийской отказоустойчивоси.

API - Application Programming Interface, программный интерфейс приложения.

DTMC - Discrete time Markov chain.

МЦДВ - марковская цепь с дискретным временем.

МЦНВ - марковская цепь с непрерывным временем.

ММПР - марковская модель принятия решений. ТРР - технология распределенного реестра. СРР - система распределенного реестра. ДНФ - дизъюнктивная нормальная форма. КНФ - конъюнктивная нормальная форма. ПВГ - проблема византийских генералов. СПМ - статистическая проверка моделей.

ООП - объектно-ориентированная парадигма программирования.

Словарь терминов

Распределённый реестр - хранилище, в котором данные хранятся в сети децентрализованных узлов.

Блокчейн - распределенный реестр, в котором данные хранятся в виде блоков, и каждый последующий блок содержит ссылку на предыдущий.

Консенсус - соглашение между несколькими сторонами, благодаря которому стороны достигают согласия (или консенсуса) о текущем глобальном состоянии системы.

Майнер - участник блокчейн-сети, который создает блоки и размещает их в сети с соответствием с алгоритмом консенсуса.

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

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

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

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

1. Blockchain / M. Nofer [и др.] // Business & Information Systems Engineering. — 2017. — т. 59, № 3. — с. 183—187.

2. Hyperledger fabric: a distributed operating system for permissioned blockchains / E. Androulaki [и др.] // Proceedings of the thirteenth EuroSys conference. — 2018. — с. 1—15.

3. Ethereum: A secure decentralised generalised transaction ledger / G. Wood [и др.] // Ethereum project yellow paper. — 2014. — т. 151, № 2014. — с. 1— 32.

4. Segendorf B. What is bitcoin // Sveri gesRiksbankEconomicReview. — 2014. — т. 2014. — с. 2—71.

5. Silvano W. F., Marcelino R. Iota Tangle: A cryptocurrency to communicate Internet-of-Things data // Future Generation Computer Systems. — 2020. — т. 112. — с. 307—319.

6. Baird L, Harmon M, Madsen P. Hedera: A governing council & public hashgraph network // The trust layer of the internet, whitepaper. — 2018. — т. 1. — с. 1—97.

7. MacDonald-Korth D., Lehdonvirta V., Meyer E. T. The Art Market 2.0: Blockchain and financialisation in visual arts. — 2018.

8. Carter R. A. Forging Stronger Chains // Engineering and Mining Journal. — 2021. — т. 222, № 9. — с. 44—47.

9. Towards Blockchain-based Stainless Steel Tracking / K. Ko [и др.] // 2020 21st Asia-Pacific Network Operations and Management Symposium (APNOMS). — IEEE. 2020. — с. 318—321.

10. Blockchain games: A survey / T. Min [и др.] // 2019 IEEE Conference on Games (CoG). — IEEE. 2019. — с. 1—8.

11. Handbook of model checking. т. 10 / E. M. Clarke [и др.]. — Springer, 2018.

12. Stewart J. DNS cache poisoning-the next generation. — 2003.

13. Norris J. R., Norris J. R. Markov chains. — Cambridge university press, 1998.

14. Pnueli A. The temporal logic of programs // 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). — ieee. 1977. — c. 46—57.

15. Maksimov D., Yakimov I., Kuznetsov A. Statistical model checking for blockchain-based applications // IOP Conference Series: Materials Science and Engineering. t. 734. — IOP Publishing. 2020. — c. 012152.

16. Abdellatif T, Brousmiche K.-L. Formal verification of smart contracts based on users and blockchain behaviors models // 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS). — IEEE. 2018. — c. 1—5.

17. Blockchain technology overview / D. Yaga [h gp.] // arXiv preprint arXiv:1906.11078. — 2019.

18. Merkle tree and Blockchain-based cloud data auditing / A. P. Mohan, A. Gladston [h gp.] // International Journal of Cloud Applications and Computing (IJCAC). — 2020. — t. 10, № 3. — c. 54—66.

19. Survival of the fittest: A natural experiment from crypto exchanges / A. F. Aysan [h gp.] // The Singapore Economic Review. — 2021. — c. 1—20.

20. Ensuring data integrity using blockchain technology / I. Zikratov [h gp.] //

2017 20th Conference of Open Innovations Association (FRUCT). — IEEE.

2017. — c. 534—539.

21. Exploring the attack surface of blockchain: A systematic overview / M. Saad [h gp.] // arXiv preprint arXiv:1904.03487. — 2019.

22. A survey on the security of blockchain systems / X. Li [h gp.] // Future Generation Computer Systems. — 2020. — t. 107. — c. 841—853.

23. Exploring the attack surface of blockchain: A systematic overview / M. Saad [h gp.] // arXiv preprint arXiv:1904.03487. — 2019.

24. Piriou P.-Y, Dumas J.-F. Simulation of stochastic blockchain models //

2018 14th European Dependable Computing Conference (EDCC). — IEEE.

2018. — c. 150—157.

25. Stochastic models and wide-area network measurements for blockchain design and analysis / N. Papadis [h gp.] // IEEE INFOCOM 2018-IEEE Conference on Computer Communications. — IEEE. 2018. — c. 2546—2554.

26. Прохоров Ю., Розанов Ю. Теория вероятностей. т. 2. — М.: Наука, 1973.

27. Ширяев А. Н. Вероятность-1. — МЦНМО, 2007.

28. Веретенников А. Ю., Веретенникова М. А. Об улучшенных оценках и условиях сходимости для цепей Маркова // Известия Российской академии наук. Серия математическая. — 2022. — т. 86, № 1. — с. 98—133.

29. Buchholz P. Structured analysis approaches for large Markov chains // Applied Numerical Mathematics. — 1999. — т. 31, № 4. — с. 375—404.

30. Puterman M. L. Markov decision processes: discrete stochastic dynamic programming. — John Wiley & Sons, 2014.

31. Segala R. Modeling and verification of randomized distributed real-time systems : дис. ... канд. / Segala Roberto. — Massachusetts Institute of Technology, 1995.

32. Sen K., Viswanathan M, Agha G. Model-checking Markov chains in the presence of uncertainties // International Conference on Tools and Algorithms for the Construction and Analysis of Systems. — Springer. 2006. — с. 394— 410.

33. Welch P. H, Barnes F. R. Communicating mobile processes // Communicating Sequential Processes. The First 25 Years. — Springer, 2005. — с. 175—210.

34. XMC: A logic-programming-based verification toolset / C. Ramakrishnan [и др.] // International Conference on Computer Aided Verification. — Springer. 2000. — с. 576—580.

35. Rigorous component-based system design using the BIP framework / A. Basu [и др.] // IEEE software. — 2011. — т. 28, № 3. — с. 41—48.

36. Statistical model checking QoS properties of systems with SBIP / A. Nouri [и др.] // International Journal on Software Tools for Technology Transfer. — 2015. — т. 17, № 2. — с. 171—185.

37. Clarke E. M., Emerson E. A. Design and synthesis of synchronization skeletons using branching time temporal logic // Workshop on logic of programs. — Springer. 1981. — с. 52—71.

38. Clarke E. M., Emerson E. A. Design and synthesis of synchronization skeletons using branching time temporal logic // Workshop on logic of programs. — Springer. 1981. — с. 52—71.

39. Карпенко А. Многозначные логики. — 1997.

40. Галиев Ш. И. Математическая логика и теория алгоритмов // АН Туполева. — 2002.

41. Shoenfield J. R. Mathematical logic. — AK Peters/CRC Press, 2018.

42. Rescher N., Urquhart A. Temporal logic. т. 3. — Springer Science & Business Media, 2012.

43. Clarke E. M., Emerson E. A. Design and synthesis of synchronization skeletons using branching time temporal logic // Workshop on logic of programs. — Springer. 1981. — с. 52—71.

44. Grumberg O, Clarke E., Peled D. Model checking. — 1999.

45. Koymans R. Specifying real-time properties with metric temporal logic // Real-time systems. — 1990. — т. 2, № 4. — с. 255—299.

46. Alur R., Dill D. L. A theory of timed automata // Theoretical computer science. — 1994. — т. 126, № 2. — с. 183—235.

47. Konur S. Real-time and probabilistic temporal logics: An overview // arXiv preprint arXiv:1005.3200. — 2010.

48. Baier C., Katoen J.-P. Principles of model checking. — MIT press, 2008.

49. Buchholz P. A new approach combining simulation and randomization for the analysis of large continuous time Markov chains // ACM Transactions on Modeling and Computer Simulation (TOMACS). — 1998. — т. 8, № 2. — с. 194—222.

50. Teichroew D., Lubin J. F. Computer simulation—discussion of the technique and comparison of languages // Communications of the ACM. — 1966. — т. 9, № 10. — с. 723—741.

51. Jensen A. Markoff chains as an aid in the study of Markoff processes // Scandinavian Actuarial Journal. — 1953. — т. 1953, sup1. — с. 87—91.

52. Malhotra M., Muppala J. K., Trivedi K. S. Stiffness-tolerant methods for transient analysis of stiff Markov chains // Microelectronics Reliability. — 1994. — t. 34, № 11. — c. 1825—1841.

53. Reibman A., Trivedi K. Numerical transient analysis of Markov models // Computers & Operations Research. — 1988. — t. 15, № 1. — c. 19—36.

54. Younes H. L, Simmons R. G. Probabilistic verification of discrete event systems using acceptance sampling // International Conference on Computer Aided Verification. — Springer. 2002. — c. 223—235.

55. Legay A., Delahaye B., Bensalem S. Statistical model checking: An overview // International conference on runtime verification. — Springer. 2010. — c. 122—135.

56. Younes H. L. S. Verification and planning for stochastic processes with asynchronous events. — Carnegie Mellon University, 2004.

57. Teichroew D., Lubin J. F. Computer simulation—discussion of the technique and comparison of languages // Communications of the ACM. — 1966. — t. 9, № 10. — c. 723—741.

58. Ulam S., Richtmyer R. D., Neumann J. von. Statistical methods in neutron diffusion // LAMS-551, Los Alamos National Laboratory. — 1947. — c. 1—22.

59. Legay A., Delahaye B., Bensalem S. Statistical model checking: An overview // International conference on runtime verification. — Springer. 2010. — c. 122—135.

60. Sen K., Viswanathan M, Agha G. Statistical model checking of blackbox probabilistic systems // International Conference on Computer Aided Verification. — Springer. 2004. — c. 202—215.

61. Wald A. Sequential tests of statistical hypotheses // The annals of mathematical statistics. — 1945. — t. 16, № 2. — c. 117—186.

62. Larsen K. G., Skou A. Bisimulation through probabilistic testing // Information and computation. — 1991. — t. 94, № 1. — c. 1—28.

63. Younes H. L. Ymer: A statistical model checker // International Conference on Computer Aided Verification. — Springer. 2005. — c. 429—433.

64. Sen K., Viswanathan M., Agha G. Vesta: A statistical model-checker and analyzer for probabilistic systems // Second International Conference on the Quantitative Evaluation of Systems (QEST'05). — IEEE. 2005. — с. 251—252.

65. How fast and fat is your probabilistic model checker? an experimental performance comparison / D. N. Jansen [и др.] // Haifa verification conference. — Springer. 2007. — с. 69—85.

66. Kwiatkowska M., Norman G., Parker D. PRISM 4.0: Verification of probabilistic real-time systems // International conference on computer aided verification. — Springer. 2011. — с. 585—591.

67. Kwiatkowska M, Norman G., Parker D. PRISM: Probabilistic symbolic model checker // International Conference on Modelling Techniques and Tools for Computer Performance Evaluation. — Springer. 2002. — с. 200—204.

68. Hagerup T, Rub C. A guided tour of Chernoff bounds // Information processing letters. — 1990. — т. 33, № 6. — с. 305—308.

69. Rigorous component-based system design using the BIP framework / A. Basu [и др.] // IEEE software. — 2011. — т. 28, № 3. — с. 41—48.

70. AlTurki M, Meseguer J. PVeStA: A parallel statistical model checking and quantitative analysis tool // International Conference on Algebra and Coalgebra in Computer Science. — Springer. 2011. — с. 386—392.

71. Uppaal 4.0 / G. Behrmann [и др.]. — 2006.

72. COSMOS: a statistical model checker for the hybrid automata stochastic logic / P. Ballarini [и др.] // 2011 Eighth International Conference on Quantitative Evaluation of SysTems. — IEEE. 2011. — с. 143—144.

73. Legay A., Delahaye B., Bensalem S. Statistical model checking: An overview // International conference on runtime verification. — Springer. 2010. — с. 122—135.

74. НОВИКОВ Е. М. Возможности и ограничения инструментов верификации моделей программ // Труды Института системного программирования РАН. — 2022. — т. 33, № 6. — с. 7—14.

75. Федотов И., Хританков А. Систематический обзор исследований в области автоматической верификации кода смарт-контрактов // Программная инженерия. — 2020. — т. 11, № 1. — с. 3—13.

76. Гратинский В. А., Новиков Е. М., Захаров И. С. Экспертная оценка результатов верификации инструментов верификации моделей программ // Труды Института системного программирования РАН. — 2020. — т. 32, № 5. — с. 7—20.

77. Formal verification of workflow policies for smart contracts in azure blockchain / Y. Wang [и др.] // Working Conference on Verified Software: Theories, Tools, and Experiments. — Springer. 2019. — с. 87—106.

78. Boogie: A modular reusable verifier for object-oriented programs / M. Barnett [и др.] // International Symposium on Formal Methods for Components and Objects. — Springer. 2005. — с. 364—387.

79. Formal modeling and verification of smart contracts / X. Bai [и др.] // Proceedings of the 2018 7th international conference on software and computer applications. — 2018. — с. 322—326.

80. Implementing statecharts in PROMELA/SPIN / E. Mikk [и др.] // Proceedings. 2nd IEEE Workshop on Industrial Strength Formal Specification Techniques. — IEEE. 1998. — с. 90—101.

81. Nehai Z, Piriou P.-Y, Daumas F. Model-checking of smart contracts // 2018 IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData). — IEEE. 2018. — с. 980—987.

82. Ahrendt W, Pace G. J., Schneider G. Smart contracts: a killer application for deductive source code verification // Principled Software Development. — Springer, 2018. — с. 1—18.

83. The KeY platform for verification and analysis of Java programs / W. Ahrendt [и др.] // Working Conference on Verified Software: Theories, Tools, and Experiments. — Springer. 2014. — с. 55—71.

84. Towards verifying ethereum smart contract bytecode in Isabelle/HOL / S. Amani [и др.] // Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs. — 2018. — с. 66—77.

85. Hirai Y. Defining the ethereum virtual machine for interactive theorem provers // International Conference on Financial Cryptography and Data Security. — Springer. 2017. — с. 520—535.

86. VeriSolid: Correct-by-design smart contracts for Ethereum / A. Mavridou [и др.] // International Conference on Financial Cryptography and Data Security. — Springer. 2019. — с. 446—465.

87. Шишкин Е. С. Проверка функциональных свойств смарт-контрактов методом символьной верификации модели // Труды Института системного программирования РАН. — 2018. — т. 30, № 5.

88. S-gram: towards semantic-aware security auditing for ethereum smart contracts / H. Liu [и др.] // 2018 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE). — IEEE. 2018. — с. 814—819.

89. Meurers D. Natural language processing and language learning // Encyclopedia of applied linguistics. — 2012. — с. 4193—4205.

90. Somin S., Gordon G., Altshuler Y. Network analysis of erc20 tokens trading on ethereum blockchain // International Conference on Complex Systems. — Springer. 2018. — с. 439—450.

91. Remix documentation. — 2022. — https://remix-ide.readthedocs.io/en/ latest/.

92. Intellij Solidity overview. — 2022. — https://plugins.jetbrains.com/plugin/ 9475-solidity/.

93. Clarke E., Donze A., Legay A. Statistical model checking of mixed-analog circuits with an application to a third order A- £ modulator // Haifa Verification Conference. — Springer. 2008. — с. 149—163.

94. Clarke E., Donze A., Legay A. On simulation-based probabilistic model checking of mixed-analog circuits // Formal Methods in System Design. — 2010. — т. 36, № 2. — с. 97—113.

95. Statistical model checking in biolab: Applications to the automated analysis of t-cell receptor signaling pathway / E. M. Clarke [и др.] // International Conference on Computational Methods in Systems Biology. — Springer. 2008. — с. 231—250.

96. Statistical abstraction and model-checking of large heterogeneous systems / A. Basu [h gp.] // Formal Techniques for Distributed Systems. — Springer, 2010. — c. 32—46.

97. Imeri A., Agoulmine N., Khadraoui D. Smart Contract modeling and verification techniques: A survey // 8th International Workshop on ADVANCEs in ICT Infrastructures and Services (ADVANCE 2020). — 2020. — c. 1—8.

98. Fedotov I., Khritankov A. Statistical model checking of common attack scenarios on blockchain // arXiv preprint arXiv:2109.02803. — 2021.

99. Blockchain attacks analysis and a model to solve double spending attack / A. Begum [h gp.] // International Journal of Machine Learning and Computing. — 2020. — t. 10, № 2. — c. 352—357.

100. An overview of blockchain security analysis / H. Wang [h gp.] // China Cyber Security Annual Conference. — Springer, Singapore. 2018. — c. 55—72.

101. Attack surface definitions: A systematic literature review / C. Theisen [h gp.] // Information and Software Technology. — 2018. — t. 104. — c. 94—103.

102. Fedotov I., Khritankov A. SBIP models. — 2021. — https://github.com/ 1vanan/SBIP_models.

103. Abhishta A., Rijswijk-Deij R. van, Nieuwenhuis L. J. Measuring the impact of a successful DDoS attack on the customer behaviour of managed DNS service providers // ACM SIGCOMM Computer Communication Review. — 2019. — t. 48, № 5. — c. 70—76.

104. Herzberg A., Shulman H. DNSSEC: Security and availability challenges // 2013 IEEE Conference on Communications and Network Security (CNS). — IEEE. 2013. — c. 365—366.

105. Shocking Blockchain's Memory with Unconfirmed Transactions: New DDoS Attacks and Countermeasures / M. Saad [h gp.] // Blockchain for Distributed Systems Security. — 2019. — c. 205.

106. Karame G. O, Androulaki E., Capkun S. Double-spending fast payments in bitcoin // Proceedings of the 2012 ACM conference on Computer and communications security. — 2012. — c. 906—917.

107. Average time to mine a block in minutes. — 2021. — URL: https://data. bitcoinity.org/bitcoin/block_time/5y?f=m10&t=l.

108. Tampering with the delivery of blocks and transactions in bitcoin / A. Gervais [h gp.] // Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security. — 2015. — c. 692—705.

109. BIP 2.0: Statistical Model Checking Stochastic Real-Time Systems / B. L. Mediouni [h gp.] // International Symposium on Automated Technology for Verification and Analysis. — Springer. 2018. — c. 536—542.

110. Approximate probabilistic model checking / T. Herault [h gp.] // International Workshop on Verification, Model Checking, and Abstract Interpretation. — Springer. 2004. — c. 73—84.

111. Bitcoin Monitoring. — 2021. — URL: https://dsn.tm.kit.edu/bitcoin/.

112. Sobti R., Geetha G. Cryptographic hash functions: a review // International Journal of Computer Science Issues (IJCSI). — 2012. — t. 9, № 2. — c. 461.

113. Houy N. The economics of Bitcoin transaction fees // GATE WP. — 2014. — t. 1407.

114. Abdellatif T., Brousmiche K.-L. Formal verification of smart contracts based on users and blockchain behaviors models // 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS). — IEEE. 2018. — c. 1—5.

115. Architecture of the hyperledger blockchain fabric / C. Cachin [h gp.] // Workshop on distributed cryptocurrencies and consensus ledgers. t. 310. — Chicago, IL. 2016. — c. 1—4.

116. Kar A. K., Rakshit A. Flexible pricing models for cloud computing based on group decision making under consensus // Global Journal of Flexible Systems Management. — 2015. — t. 16, № 2. — c. 191—204.

117. A survey on decentralized consensus mechanisms for cyber physical systems / U. Bodkhe [h gp.] // IEEE Access. — 2020. — t. 8. — c. 54371—54401.

118. Approximate consensus in stochastic networks with application to load balancing / N. Amelina [h gp.] // IEEE Transactions on Information Theory. — 2015. — t. 61, № 4. — c. 1739—1752.

119. An overview of blockchain technology: Architecture, consensus, and future trends / Z. Zheng [h gp.] // 2017 IEEE international congress on big data (BigData congress). — Ieee. 2017. — c. 557—564.

120. Lamport L, Shostak R., Pease M. The Byzantine generals problem // Concurrency: the Works of Leslie Lamport. — 2019. — c. 203—226.

121. Bamakan S. M. H, Motavali A., Bondarti A. B. A survey of blockchain consensus algorithms performance evaluation criteria // Expert Systems with Applications. — 2020. — t. 154. — c. 113385.

122. Prashant B., Makrant I., Mansi M. Migration from POW to POS for Ethereum. —.

123. Practical byzantine fault tolerance / M. Castro, B. Liskov [h gp.] // OsDI. t. 99. — 1999. — c. 173—186.

124. Bach L. M., Mihaljevic B., Zagar M. Comparative analysis of blockchain consensus algorithms // 2018 41st International Convention on Information and Communication Technology, Electronics and Microelectronics (MIPRO). — Ieee. 2018. — c. 1545—1550.

125. GossipSub: Attack-resilient message propagation in the Filecoin and ETH2. 0 networks / D. Vyzovitis [h gp.] // arXiv preprint arXiv:2007.02754. — 2020.

126. Algorand: Scaling byzantine agreements for cryptocurrencies / Y. Gilad [h gp.] // Proceedings of the 26th symposium on operating systems principles. — 2017. — c. 51—68.

127. Nakamoto S. Bitcoin: A peer-to-peer electronic cash system // Decentralized Business Review. — 2008. — c. 21260.

128. King S. Primecoin: Cryptocurrency with prime number proof-of-work // July 7th. — 2013. — t. 1, № 6.

129. Vasin P. Blackcoin's proof-of-stake protocol v2 // URL: https://blackcoin. co/blackcoin-pos-protocol-v2-whitepaper. pdf. — 2014. — t. 71.

130. King S., Nadal S. Ppcoin: Peer-to-peer crypto-currency with proof-of-stake // self-published paper, August. — 2012. — t. 19, № 1.

131. Endorsement in hyperledger fabric / E. Androulaki [и др.] // 2019 IEEE International Conference on Blockchain (Blockchain). — IEEE. 2019. — с. 510—519.

132. Sukhwani H. Performance modeling & analysis of hyperledger fabric (permissioned blockchain network) : дис. ... канд. / Sukhwani Harish. — Duke University, 2019.

133. Fast probabilistic consensus with weighted votes / S. Müller [и др.] // Proceedings of the Future Technologies Conference. — Springer. 2020. — с. 360—378.

134. Duda J. Exploiting statistical dependencies of time series with hierarchical correlation reconstruction // arXiv preprint arXiv:1807.04119. — 2018.

135. Corani G., Benavoli A. A Bayesian approach for comparing cross-validated algorithms on multiple data sets // Machine Learning. — 2015. — т. 100, № 2. — с. 285—304.

136. Fedotov I., Khritankov A., Barger A. Towards automated verification of multiparty consensus protocols // arXiv preprint arXiv:2112.02397. — 2021.

137. Goubault-Larrecq J., Plaisted D. Normal form transformations // Handbook of Automated Reasoning. — 2001. — т. 1. — с. 273.

138. Agha G., Palmskog K. A survey of statistical model checking // ACM Transactions on Modeling and Computer Simulation (TOMACS). — 2018. — т. 28, № 1. — с. 1—39.

139. Abdellatif T., Brousmiche K.-L. Formal verification of smart contracts based on users and blockchain behaviors models // 2018 9th IFIP International Conference on New Technologies, Mobility and Security (NTMS). — IEEE. 2018. — с. 1—5.

140. Fedotov I., Obidare M. consensus-analyzer. — 2021. — https://github.com/ 1vanan/consensus-analyzer.

141. Fedotov I. consensus-scheduler. — 2021. — https://github.com/1vanan/ consensus-scheduler.

142. Hyperledger application. — 2022. — https://hyperledger-fabric.readthedocs. io/en/release-2.2/write_first_app.html.

143. Test network. — 2022. — https://github.com/hyperledger/fabric-samples/ tree/main/test-network.

144. Asset transfer basic. — 2022. — https://github.com/hyperledger/fabric-samples/tree/main/asset-transfer-basic.

145. Oueslati S., Roberts J., Sbihi N. Flow-aware traffic control for a content-centric network // 2012 Proceedings IEEE INFOCOM. — IEEE. 2012. — c. 2417—2425.

146. Traffic control Linux. — 2022. — https://linux.die.net/man/8/tc.

147. Fabric Gateway Java. — 2022. — https://github.com/hyperledger/fabric-gateway-java.

148. McKnight P. E., Najab J. Mann-Whitney U Test // The Corsini encyclopedia of psychology. — 2010. — c. 1—1.

149. Shi N.-Z, Tao J. Statistical hypothesis testing: theory and methods. — World Scientific Publishing Company, 2008.

150. Hyperledger Fabric Test Network Installation. — 2022. — https://hyperledger-fabric.readthedocs.io/en/release-2.2/install.html.

151. Fabric Java Application. — 2022. — https://github.com/1vanan/fabric-application-java.

152. Fedotov I. consensus-experiment. — 2022. — https://github.com/1vanan/ consensus-experiment.

153. Feldt R., Magazinius A. Validity threats in empirical software engineering research-an initial survey. // Seke. — 2010. — c. 374—379.

154. Experiment resources and results. — 2022. — https://github.com/1vanan/ fabric-application-java/tree/main/consensus-analysis.

155. Rabiner L, Juang B. An introduction to hidden Markov models // ieee assp magazine. — 1986. — t. 3, № 1. — c. 4—16.

Список рисунков

2.1 Графическое представление свойств непрерывной случайной величины ................................................................29

2.2 Пример марковской цепи принятия решений с вознаграждениями 34

2.3 Модель процесса покупки актива......................................36

3.1 Атака на кэш DNS......................................................56

3.2 Атака двойной траты с задержкой консенсуса ......................60

3.3 Атака двойной траты ..................................................61

3.4 Атака двойной траты с заполнением пула памяти ..................65

3.5 Зависимость вероятности от времени для модели DNS атаки. ... 68

3.6 Зависимость вероятности от времени для модели двойной траты

со спамом пула памяти......................... 70

3.7 Зависимость вероятности от времени для модели двойной траты

с задержкой консенсуса......................... 71

4.1 Модель взвешенного консенсуса ......................................87

4.2 Зависимость пороговой вероятности от вероятности принятия транзакции организацией 3 ............................................89

4.3 Модель с двумя организациями ........................................90

4.4 Модель с двумя организациями ........................................93

5.1 Модель с двумя организациями....................100

5.2 График зависимости вероятности достижения консенсуса от математического ожидания числа сообщений, переданных в сети

до подтверждения транзакции .................... 116

5.3 График зависимости вероятности подтверждения транзакции от числа обратных переходов ....................... 117

5.4 График зависимости математического ожидания числа сообщений от числа обратных переходов .............. 118

5.5 График зависимости вероятности достижения консенсуса от математического ожидания числа сообщений для

многофакторного эксперимента с тремя организациями.......120

5.6 График зависимости вероятности достижения консенсуса от

числа обратных переходов для многофакторного эксперимента с

тремя организациями..........................121

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

5.8 График зависимости вероятности достижения консенсуса от математического ожидания числа сообщений для многофакторного эксперимента с участием тремя

организациями с правилом подтверждения всех трех организаций. 123 5.9 График зависимости вероятности достижения консенсуса от

числа обратных переходов для многофакторного эксперимента с

тремя организациями с правилом одобрения всех организаций. . . 124

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

5.11 График зависимости вероятности достижения консенсуса от математического ожидания числа сообщений для

многофакторного эксперимента с двумя организациями......126

5.12 График зависимости вероятности достижения консенсуса от числа обратных переходов для многофакторного эксперимента с двумя организациями..........................127

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

Список таблиц

1 Сравнение алгоритмов консенсуса.................. 79

2 Зависимость порога веса от порога вероятности .......... 90

3 Матричное представление модели Маркова с дискретным временем для консенсуса из трех организаций с вероятностями отклонения близкими к нулю......................153

4 Матричное представление модели Маркова с дискретным временем для консенсуса из двух организаций с вероятностями отклонения близкими к нулю......................153

5 Матричное представление модели Маркова с дискретным временем для консенсуса из трех организаций с вероятностями отклонения близкими к нулю и обратными переходами.......154

6 Матричное представление модели Маркова с дискретным временем для консенсуса из двух организаций для мультифакторного эксперимента....................154

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

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

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

10 Вероятность достижения консенсуса и соответсвующие значения среднего числа сообщений, рассчитанные для разных моделей

для мультифакторного эксперимента с двумя организациями . . . 163

Приложение А

Матричное представление моделей консенсуса в виде цепи Маркова

с дискретным временем

Таблица 3 — Матричное представление модели Маркова с дискретным временем для консенсуса из трех организаций с вероятностями отклонения близкими к нулю.

- Ох Оу С>2' Оз Оз' Оз'' Оз'' 1х ¡2 1з 14 к 16 1х 18

Ох 0 0.07 0.93 0 0 0 0 0 0 0 0 0 0 0 0

О2 0 0 0 0.01 0.99 0 0 0 0 0 0 0 0 0 0

Оу 0 0 0 0 0 0.01 0.99 0 0 0 0 0 0 0 0

Оз 0 0 0 0 0 0 0 0.02 0.98 0 0 0 0 0 0

03' 0 0 0 0 0 0 0 0 0 0.02 0.98 0 0 0 0

Оз" 0 0 0 0 0 0 0 0 0 0 0 0.02 0 .98 0 0

О3''' 0 0 0 0 0 0 0 0 0 0 0 0 0 0.02 0.98

0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

¿2 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

13 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

/4 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

1ъ 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

16 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

17 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

18 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0

Таблица 4 — Матричное представление модели Маркова с дискретным временем для консенсуса из двух организаций с вероятностями отклонения близкими к нулю.

- 02 Оз Оз' /1 ¡2 1з /а

02 0 0.01 0.99 0 0 0 0

Оз 0 0 0 0.02 0.98 0 0

Оз> 0 0 0 0 0 0.02 0.98

11 0 0 0 0 0 0 0

¡2 0 0 0 0 0 0 0

13 0 0 0 0 0 0 0

1а 0 0 0 0 0 0 0

Таблица 5 — Матричное представление модели Маркова с дискретным временем для консенсуса из трех организаций с вероятностями отклонения близкими к нулю и обратными переходами.

- 01 02 Оу 17 18

о1 0.07 0.93 0 0 0

02 0 0.01 0.99 0 0

Оуп 0 0 0 0.02 0.98

¡7 0 0 0 0 0

18 0 0 0 0 0

Таблица 6 — Матричное представление модели Маркова с дискретным временем для консенсуса из двух организаций для мультифакторного эксперимента.

- 01 02 02' 11 ¡2 1з /4

О1 0 0.1 0.98 0 0 0 0

02 0 0 0 0.3 0.7 0 0

02' 0 0 0 0 0 0.3 0.7

11 0 0 0 0 0 0 0

¡2 0 0 0 0 0 0 0

1з 0 0 0 0 0 0 0

1а 0 0 0 0 0 0 0

Приложение Б

Таблицы измерений для эксперимента по проверке корректности работы клиента Hyperledger Java Gateway

Таблица 7 — Вероятность достижения консенсуса и соответсвующие значения среднего числа сообщений, рассчитанные для разных моделей для консенсуса из трех организаций с правилом одобрения большинства

Вероятность Число сообщений

0.9931 3

0.9932 3

0.9964 3

0.995 3

0.9926 3.2

0.9946 3

0.9963 3.15

0.9965 3.09

0.9965 3.01

0.9951 3

0.9927 3.2

0.9946 3

0.9964 3.15

0.9965 3.09

0.9984 3.01

0.9962 3.21

0.9979 3.01

0.9963 3.15

1 3.1

0.9947 3.21

0.9965 3.01

0.9984 3.15

0.9965 3.09

0.9942 3.21

0.996 3.38

0.9962 3.31

0.9978 3.15

0.9965 3.09

0.9985 3.01

0.99636 3.21

Вероятность Число сообщений

0.9979 3.01

0.9964 3.15

1 3.1

0.9948 3.21

0.9965 3.01

0.9985 3.15

0.9965 3.09

0.9942 3.21

0.9961 3.38

0.9962 3.31

0.9978 3.15

0.9965 3.09

0.9983 3.22

1 3.02