Дослідження верифікації систем розподіленого реєстру
Автор: Думич Матвій Тарасович
Кваліфікаційний рівень: магістр
Спеціальність: Інформаційні мережі зв'язку
Інститут: Інститут телекомунікацій, радіоелектроніки та електронної техніки
Форма навчання: заочна
Навчальний рік: 2023-2024 н.р.
Мова захисту: українська
Анотація: Системи розподіленого реєстру (СРР) набули широкого поширення останнім часом у різних прикладних галузях . У фінансовому секторі СРР використовуються для забезпечення швидких транзакцій без залучення посередників. У класичних транзакціях такими посередниками виступають банки. У галузі ланцюжків поставок СРР виступають сполучною ланкою між сторонами, серед яких немає довіри. Це також дає змогу відстежувати життєвий цикл продукції та забезпечує прозорість її пересування від виробника до постачальника і далі до споживача. Технологія розподіленого реєстру (ТРР) набула активного поширення в галузях, пов’язаних із фінансами та активами, відповідно помилки в реалізаціях таких систем можуть призвести до істотних фінансових втрат [1,2]. У зв’язку з цим зростає потреба в підвищенні надійності та відмовостійкості систем, що використовують розподілений реєстр. Також багато блокчейн-мереж, таких як Ethereum і Bitcoin, не дають змоги змінювати код або параметри системи після розгортання. Якщо помилку або вразливість не виявлено до введення системи або коду в промислову експлуатацію, то помилку вже не можна буде виправити. Це підвищує потребу відловлювання та виправлення помилок на стадії розробки. Існують різні способи виявлення та виправлення вразливостей у програмному забезпеченні, зокрема верифікація, яка дає змогу визначити, що система або модель системи відповідає специфікації [3]. Під час верифікації часто проводять перевірку моделі системи, що виключає необхідність запуску реальної системи. Моделювання системи з подальшою верифікацією дає змогу на стадії розроблення виявити помилки та вразливості. Щоб перевірити, що система задовольняє специфікації до розгортання самої системи, можна побудувати її модель і перевірити, що модель задовольняє специфікації. Якщо модель не задовольняє специфікації, можна скоригувати параметри моделі та перевірити, що модифікована версія задовольняє специфікації. Після чого можна також змінити параметри системи. Формальні методи верифікації дають змогу математично точно визначити, що модель задовольняє специфікації [4,5]. Після перевірки, якщо модель задовольняє специфікації, можна вводити систему в промислову експлуатацію. В іншому разі можна запропонувати змінити параметри системи або специфікації таким чином, щоб модифікована модель задовольняла специфікації. У зв’язку з тим, що технологія розподіленого реєстру є новою, широко застосовна в галузях, пов’язаних із фінансами, а кількість користувачів технології швидко зростає, верифікація систем розподіленого реєстру є важливим напрямом дослідження. З огляду на те, що з’являється дедалі більше користувачів технології розподіленого реєстру, зокрема й більше зловмисників, дослідження верифікації систем розподіленого реєстру зі стохастичними властивостями є актуальним. Метою магістерської кваліфікаційної роботи є підвищення ефективності виявлення вразливостей у процесі верифікації систем розподіленого реєстру.Предмет дослідження – системи розподіленого реєстру. Об’єкт дослідження – процес верифікації для блокчейн-систем. Наукова новизна отриманих результатів полягає у розробці алгоритму побудови моделей різних типів консенсусу у вигляді Марківського ланцюга з дискретним часом, що дозволить визначити з якою імовірністю консенсус буде досягнуто. Практична значимість отриманих результатів полягає у можливості їх використання в системах промислової експлуатації для підвищення виявлення вразливостей блокчейн систем .