СИСТЕМА РАСПРЕДЕЛЕННОГО РЕЕСТРА
DISTRIBUTED LEDGER SYSTEM

Изобретение относится к информационным технологиям, а именно к  созданию надежных систем распределенных реестров и может быть использовано для применения в критически важных отраслях промышленности с высокими требованиями к безопасности и среде работы с данными.
На сегодняшний день системы распределенного реестра (СРР) находят свое применение в различных направлениях информационных технологий и в различных секторах экономики, начиная с традиционного для них финансового сектора и заканчивая специфическими применениями в области робототехники, транспорта, связи и многих других.
СРР представляют собой распределенные системы, функционирующие в реальном масштабе времени. К надежности СРР предъявляются особые требования. Это связано с тем, что свойства СРР, с одной стороны, по определению обеспечивают доступ к данным для всех участников системы без ограничений, а также согласованность и целостность данных. С другой стороны, любой дефект в исходном коде СРР может обернуться серьезной уязвимостью для системы в целом ввиду того, что нет единой точки доступа для устранения проблемы.
Одним из основных понятий СРР является понятие смарт-контракта. Смарт-контракт - это функция, реализованная в виде программного обеспечения, аргументами которой являются (1) текущее состояние СРР и (2) данные пользователя, инициировавшего транзакцию в СРР, приводящую к активации данного смарт-контракта. Результатов выполнения смарт-контракта является новое состояние СРР. Понятие состояния СРР будет раскрыто в дальнейшем.
N
k
Из патента № RU2679532 «Система децентрализованного цифрового расчетного сервиса» (G06Q 30/00, G06Q 30/00, G06Q 20/401, 11.02.2019) известно решение, представляющее собой СРР, включающую  серверов банков, каждый из которых содержит автоматизированную банковскую систему с базой данных, распределенный реестр для осуществления финансовых операций напрямую между аккаунтами пользователей без участия систем банка и платежных систем в режиме онлайн, клиентский портал, содержащий модуль доступа к СРР, который хранит публичный и приватный ключи портала,  мобильных устройства клиентов. Недостатками этого известного решения являются отсутствие формальной верификации на всех уровнях работы СРР, что не обеспечивает гарантированной надежности ее работы.В частности, известное решение не содержит специальных механизмов защиты от некорректной логики финансовых операций, ошибок в системе исполнения финансовых операций, ошибок при достижении согласованного состояния распределенного реестра, ошибок в операционном окружении.
В широко распространенной СРР Ethereum были выявлены многочисленные ошибки (уязвимости), связанные с системой исполнения смарт-контрактов. Во многих случаях эти ошибки позволили злоумышленникам совершить хищения цифровых финансовых активов, реализованных на платформе СРР Ethereum.
Традиционные методы обеспечения качества программного обеспечения, такие как тестирование, аудит кода, проектирование по контракту, в принципе не могут гарантировать надежность распределенных систем, работающих в реальном масштабе времени, в том числе СРР. При наличии критических требований по надежности и безопасности таких систем, единственным методом обеспечения качества, включая корректность, надежность, безопасность и безотказность системы, является формальная верификация программного обеспечения.
Методы формальной верификации применяются, начиная с 1990-х годов, для обеспечения надежности программного обеспечения в таких отраслях, как атомная энергетика, аэрокосмическая техника, высокоскоростной железнодорожный транспорт. Так, автоматическая система управления 14-й линией парижского метро (Meteor) была спроектирована и построена на основе метода формальной верификации B. Однако при разработке СРР методы формальной верификации пока применялись недостаточно широко. Известна СРР Tezos с предметно-ориентированным языком смарт-контрактов Archetype, для которого разработаны методы формальной верификации. Однако данные методы охватывают только уровень собственно программной логики смарт-контрактов и не предоставляют гарантий корректного исполнения смарт-контрактов в узлах СРР и их операционном окружении, а также гарантий корректности протокола консенсуса, используемого в СРР.
Задачей и техническим результатом заявляемого решения является создание полностью формально-верифицированной системы распределенного реестра, обеспечивающей надежность исполнения смарт-контрактов и безопасность обработки данных за счет обеспечения доказательства корректности работы смарт-контрактов на всех этапах в среде исполнения, включая операционное окружение. Доказательства корректности функционирования системы верифицируются автоматически в системах компьютерной логики и, таким образом, не допускаются ошибки в работе СРР.
Технический результат достигается тем, что система распределенного реестра (СРР) содержит блок преобразования смарт-контрактов с предметно-ориентированного языка на язык системы компьютерной логики HOL4, блок формальной верификации смарт-контрактов на основе библиотеки теорем и тактик в системе HOL4, блок трансляции смарт-контрактов в абстрактное синтаксическое дерево языка функционального языка программирования CakeML, блок формально-верифицированного компилятора CakeML в машинный код, узлы СРР, каждый из которых содержит верифицированную операционную систему, подсистему исполнения смарт-контрактов, подсистему сетевых взаимодействий, при этом узлы СРР связаны между собой  посредством верифицированного протокола консенсуса.
А также тем, что в качестве верифицированной операционной системы узлов СРР применена формально-верифицированная операционная система seL4.
А также тем, что взаимодействие узлов СРР с внешними системами и базами данных  осуществляется через подсистему взаимодействия, реализованную на фреймворке Erlang/OTP.
А также тем, что протокол консенсуса между узлами СРР верифицирован  методом Model checking.
Сущность заявленного решение поясняется на фиг.1, 2
На фиг.1 изображена схема архитектуры разрабатываемой системы.
На фиг.2 изображено верхнеуровневое представление связей между компонентами узла СРР.
На фигурах введены следующие обозначения:
1 – Блок составления смарт-контракта на предметно-ориентированном языке;
2 – Блок трансляции смарт-контракта с предметно-ориентированного языка на язык системы компьютерной логики HOL4;
3 – Блок транслированного смарт-контракта на языке HOL4;
4 – Блок трансляции смарт-контракта с языка HOL4 в абстрактное синтаксическое дерево языка CakeML;
5 – Блок транслированного смарт-контракта в абстрактное синтаксическое дерево языка CakeML;
6 – Блок верификации программного обеспечения;
7 – Блок библиотеки доказательств и тактик;
8 – Блок формально-верифицированного компилятора CakeML в машинный код;
9 – Блок скомпилированного в машинный код смарт-контракта;
10 – Подсистема исполнения смарт-контракта;
11 – Подсистема сетевых взаимодействий;
12 – Блок верифицированной операционный системы;
13 – Узел системы распределенного реестра;
14 – Блок взаимодействия между узлами СРР посредством верифицированного протокола консенсуса;
15 – Узлы системы СРР;
16 – Подсистема взаимодействия с внешними системами;
17 – Внешние источники (потребители, БД, другие внешние СРР);
18 - Круговой управляющий блок;
19 - Круговое состояние;
20 - Безопасность;
21 - Хранилище блоков;
22 - Синхронизатор;
23 - Алгоритм консенсуса;
24 - Диспетчер соединения;
25 - Диспетчер обнаружения;
26 - Сетевой администратор;
27 - Состояние сети;
28 - Сеть;
29 - Хранилище;
30 - Блок вычисления состояния распределенного реестра.
Все компоненты, необходимые для работы СРР, приведены на фиг. 1. Блок 1 функционально обеспечивает составление смарт-контракта на предметно-ориентированном языке, разработанном для возможности создания смарт-контрактов без понимания технических тонкостей работы СРР, что обеспечивает простоту составления смарт-контракта. Для предметно-ориентированного языка также специфицируется формальная семантика на языке системы компьютерной логики HOL4. HOL4 – это среда, в которой есть все необходимое для формальной верификации, в его основе лежит язык Standard ML. Для доказательства надежности исполнения полученного кода на предметно-ориентированном языке, происходит трансляция кода смарт-контракта из предметно-ориентированного языка в язык HOL4 (блок 2).
Транслированный код на языке HOL4 (блок 3) верифицируется при помощи заранее доказанных теорем посредством обращения к блоку 6 верификации программного обеспечения, который, в свою очередь, взаимодействует с блоком 7, который представляет собой библиотеку доказательств и тактик.  Такой подход возможен, благодаря заданию формальной семантики предметно-ориентированного языка внутри HOL4. Для доказательства используется система верификации (блок 6), которая обращается к библиотеке теорем и тактик (блок 7). Результатом работы блока 6 верификации является код смарт-контракт на языке HOL4, для которого доказана логическая корректность.
На следующем шаге производится генерация абстрактного синтаксического дерева языка CakeML из верифицированного кода смарт-контракта на языке HOL4. CakeML – это язык семейства Standard ML и среда, в которой есть формально-верифицированный компилятор. Для того, чтобы использовать его возможности, необходимо транслировать полученный из блока 3 код на HOL4 во входные данные компилятора CakeML (блок 8). В состав среды CakeML входит библиотека (в составе блока 7), специально разработанная для трансляции кода HOL4 в абстрактное синтаксическое дерево языка CakeML . Транслятор из HOL4 в CakeML (блок 4) использует эту библиотеку и генерирует абстрактное синтаксическое дерево СakeML (блок 5), которое затем компилируется в машинный код при помощи формально-верифицированного компилятора CakeML (блок 8). Применение формально-верифицированного компилятора гарантирует, что полученный машинный код (блок 9) является  корректным.
Узел СРР (блок 13) -- это компонент программного обеспечения СРР, осуществляющий исполнение смарт-контрактов, сетевые взаимодействия с другими узлами СРР, исполнение протокола консенсуса в рамках согласования блоков из транзакций, обеспечение корректности исполнения транзакций, вычисление нового состояния СРР и его сохранение в персистентное хранилище, отправку сообщений в рамках протокола консенсуса, а также за синхронизацию состояния отставшего узла, управление персистентным хранилищем данных, которое используется для хранения данных протокола консенсуса и состояния СРР.
Каждый узел СРР функционирует на физической или виртуальной аппаратной платформе, подключенной к сети Интернет, работающей под управлением формально-верифицированной операционной системы seL4 (блок 12), основанной на архитектуре микроядра. Использование seL4 направлено на исключение потенциальных ошибок функционирования ядра СРР, вызванных некорректным функционированием операционной системы.
Подсистемы исполнения смарт-контрактов (блок 10) и сетевых взаимодействий (блок 11) относятся к узлу СРР и созданы для того, чтобы скомпилированный смарт-контракт мог выполняться в СРР.
Смарт-контракт, представленный в виде машинного кода (блок 9), загружается на узел СРР. Пользователи СРР имеют возможность совершать транзакции, то есть вводить в СРР данные определенного формата, приводящие к активации заданного смарт-контракта. При этом текущее состояние СРР и данные, введенные пользователем, являются аргументами при выполнении данного смарт-контракта.
Результатом выполнения смарт-контакта на узле СРР (блок 13) является изменение состояния этого узла. Под состоянием узла СРР понимаются записи определенного формата, персистентно хранящиеся в памяти узла. Под состоянием СРР в целом понимается единообразное состояние всех правильных узлов СРР, достигаемое в результате применения протокола консенсуса. При этом правильным узлом называется узел, являющийся доступным для сетевых взаимодействий и выполняющий протокол консенсуса, а неисправным узлом -- узел, являющийся недоступным или отклоняющийся от протокола консенсуса. Под протоколом консенсуса понимается алгоритм, выполняемый совокупностью всех (правильных) узлов СРР, приводящий к возникновению единообразного состояния этих узлов после каждой транзакции.
Под i-ой версией системы понимается состояние СРР, полученное после принятия i-ой транзакции и выполнения смарт-контракта, активированного этой транзакией. Формально-верифицированный протокол консенсуса гарантирует, что для любой конечной i-ой версии системы, при числе неисправных узлов, составляющем строго менее половины от числа правильных узлов, все правильные узлы имеют одинаковое согласованное состояние (свойство безопасности), и это состояние изменяется в зависимости от версии системы i (свойство отсутствия тупиков).
На этапе протокола консенсуса транзакции группируются в блоки, что делается исключительно для ускорения принятия транзакций узлами СРР. После принятия блока транзакций в результате работы протокола консенсуса, сохраняются только индивидуальные транзакции с доказательством их согласования в рамках протокола консенсуса. Каждая принятая транзакция из блока транзакций исполняется детерминировано и единообразно на всех правильных узлах СРР, что приводит к увеличению счетчика версий системы i на число выполненных транзакций из принятого блока.
Необходимо отметить, что представленное на фиг. 1 исполнение узла 13 отражает, в том числе, и  исполнение всех остальных узлов СРР 15. Узел 13 приведен для понимания строения всех узлов СРР. Для согласования состояния всех узлов -- участников СРР (блок 15) используется протокол консенсуса, представленный блоком 14, верифицированный при помощи теорем и тактик на HOL4, а также с помощью метода Model checking. Взаимодействие СРР с внешними системами и базами данных (блок 17) осуществляется через подсистему (блок 16), реализованную на фреймворке Erlang/OTP, который обеспечивает высокую надежность исполнения.
На фигуре 2 изображено верхнеуровневое представление связей между компонентами узла СР. Одним из важнейших компонентов узла является протокол консенсуса 14,  работа которого представляется в виде взаимодействия следующих модулей: Круговой управляющий блок 18, Круговое состояние 19, Безопасность 20, Хранилище блоков 21, Синхронизатор 22.
Модуль протокола консенсуса (блок 23) взаимодействует с Сетью (блок 28), Хранилищем СРР (блок 29) и вычисляет состояние СРР (блок 30). Протокол консенсуса включает в себя определенное число раундов обмена сетевыми сообщениями между всеми узлами СРР, с целью достижения одинакового состояния всех правильных узлов. Данный модуль включает в себя компоненты:
- Круговой управляющий блок (блок 18), который ответственен за управление жизненным циклом и за обработку событий протокола консенсуса. Этот блок отвечает за главный цикл обработки сообщений узлом.
- Круговое состояние (блок 19), которое управляет состоянием протокола консенсуса: хранит и обновляет номер текущего раунда, отслеживает голоса узлов СРР, полученные в текущем раунде при формировании консенсуса, генерирует сертификаты кворума при наборе достаточного количества голосов (или событие тайм-аута, если кворум не был достигнут за заданное время), управляет жизненным циклом таймера раунда.
- Безопасность (блок 20) -- это компонент, который ответственен за формирование голоса данного узла СРР при получении блока от лидера раунда в процессе формирования консенсуса. Помимо этого, компонент управляет ЭЦП, т.е подписывает сообщения от имени валидатора, а также проверяет подписи сообщений других валидаторов.
- Хранилище блоков (блок 21) - это компонент, который управляет структурой данных блоков в виде дерева, активирует принятие блока в случае выполнения необходимых условий, а также хранит сертификаты, необходимые для протокола консенсуса и синхронизации.
- Синхронизатор (блок 22) - это компонент, который ответственен за синхронизацию состояния консенсуса и СРР.
Сеть (блок 28) - это компонент, который, в свою очередь, состоит из нескольких субкомпонентов (процессов):
- Диспетчер соединения (блок 24) - это процесс, который отвечает за поддержку соединения с узлами СРР.
- Диспетчер обнаружения (блок 25) - это процесс, который отвечает за получение, передачу и обработку информации об известных узлах СРР.
- Сетевой Администратор (блок 26) - это процесс, который отвечает за исполнение команд отправки сообщений и функций алгоритма консенсуса.
- Состояние сети (блок 27) - это процесс, реализующий  базы данных, в которой хранится информация об известных узлах и текущих соединениях.
Синхронизатор 22 - это компонент, который ответственен за формирование заданий на синхронизацию сетевому слою (Сеть, блок 28) и применение результата к текущему состоянию узла 13.
Таким образом, предлагаемый объект позволяет совершать безопасные и надежные транзакции путем реализации СРР с проверкой полной корректности выполнения на всех этапах выполнения смарт-контракта, а именно:
- трансляция смарт-контракта из предметно-ориентированного языка в HOL4 и его верификация в системе компьютерной логики HOL4 гарантирует логическую корректность смарт-контракта на уровне исходного кода;
- трансляция смарт-контакта из HOL4 в CakeML и далее из CakeML в машинный код исключает ошибки компиляции, то есть гарантирует генерацию корректного машинного кода смарт-контракта;
-  формальная верификация алгоритмов функционирования узла СРР в системе HOL4 гарантирует логическую корректность этих алгоритмов, а реализация узла на CakeML гарантирует генерацию корректного машинного кода узла;
- формальная верификация протокола консенсуса с использованием системы HOL4 и с помощью метода Model checking гарантирует свойства безопасности и отсутствия тупиков в протоколе консенсуса;
- использование формально-верифицированной операционной системы seL4 в качестве основы реализации узла СРР гарантирует отсутствие ошибок, вызванных некорректным функционированием операционной системы.