Способ повышения надежности системы распределенного реестра
системы распределённого реестра (СРР) смарт-контракты лидирующий исследовательский центр (ЛИЦ) информационные технологии сквозные цифровые технологии
Изобретение относится к информационным технологиям, а именно к созданию надежных систем распределенных реестров и может быть использовано для применения в критически важных отраслях промышленности с высокими требованиями к безопасности и среде работы с данными. 
Согласно способу повышения надежности системы распределенного реестра, выполняется составление смарт-контракта на предметно-ориентированном языке, для которого реализована формальная семантика на языке системы компьютерной логики HOL4, осуществление трансляции смарт-контракта с предметно-ориентированного языка на язык HOL4, осуществление верификации полученного смарт-контракта на языке HOL4 посредством обращения к блоку верификации программного обеспечения, связанного с библиотекой доказательств и тактик, осуществление трансляции верифицированного смарт-контракта с языка HOL4 в абстрактное синтаксическое дерево функционального языка программирования CakeML, осуществление передачи абстрактного синтаксического дерева смарт-контракта в компилятор языка CakeML для трансляции смарт-контракта в машинный код, размещаемый в узле СРР, при этом верификацию процесса компиляции смарт-контракта осуществляют путем повторного использования предварительно формально-верифицированного компилятора языка CakeML, осуществление передачи скомпилированного смарт-контракта в подсистему исполнения смарт-контрактов, подсистему сетевых взаимодействий и выполнение скомпилированного смарт-контракта в каждом узле системе распределенного реестра, причем в основе реализации и функционирования узла СРР лежит формально-верифицированная операционная система seL4, а  узел СРР реализуется на языке CakeML, алгоритмы функционирования узла формально верифицируются с использованием системы компьютерной логики HOL4, машинный код узла СРР и генерируется с использованием формально-верифицированного компилятора языка CakeML, взаимодействие между узлом и остальными узлами СРР осуществляется посредством протокола консенсуса, верифицированного при помощи библиотеки доказательств и тактик в системе HOL4.
Задачей и техническим результатом заявляемого решения является создание полностью формально-верифицированной системы распределенного реестра, обеспечивающей надежность исполнения смарт-контрактов и безопасность обработки данных за счет обеспечения доказательства корректности работы смарт-контрактов на всех этапах в среде исполнения, включая операционное окружение. Доказательства корректности функционирования системы верифицируются автоматически в системах компьютерной логики и, таким образом, не допускаются ошибки в работе СРР.
реализация смарт-контрактов, безопасная обработка данных
Алексей
Дудниченко
Викторович
Руководитель центра
Отсутствует
Отсутствует
-
-
РОССИЯ
Кирилл
Семенихин
Владимирович
Директор
РОССИЯ
20.53.23
Средства передачи информации
20.53.21
Средства выдачи информации
28.21.19
Теория кодирования
28.27.15
Оптимизация надежности
28.27.27
Методы оценки надежности
01.02.ET
COMPUTER SCIENCE, INFORMATION SYSTEMS
01.02.EX
COMPUTER SCIENCE, THEORY & METHODS
01.02.EW
COMPUTER SCIENCE, SOFTWARE ENGINEERING
Леонид
Меркин
Альбертович
Разработка технического решения
РОССИЯ
Руслан
Резин
Маратович
Разработка технического решения
РОССИЯ
Николай
Васильев
Константинович
Разработка технического решения
РОССИЯ
ФОНД НТИ
ФОНД ПОДДЕРЖКИ ПРОЕКТОВ НАЦИОНАЛЬНОЙ ТЕХНОЛОГИЧЕСКОЙ ИНИЦИАТИВЫ
1167700062529
Организация
Организации, учрежденные юридическими лицами или гражданами, или юридическими лицами и гражданами совместно
Фонды
АНО ВО "Университет Иннополис"
Автономная некоммерческая организация высшего образования "Университет Иннополис"
1121600006142
Организация
Организации, учрежденные юридическими лицами или гражданами, или юридическими лицами и гражданами совместно
Автономные некоммерческие организации