Методи та засоби побудови автоматизованої освітньої програмної системи для кібербезпеки (кіберполігону) : дисертація на здобуття наукового ступеня доктора філософії
Loading...
Date
2026
Authors
Бабич, Трохим
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
Дисертація на здобуття наукового ступеня доктора філософії за спеціальністю 122 "Комп’ютерні науки" (12 – Інформаційні технології). – Національний університет "Києво-Могилянська академія", Київ, 2026. У дисертаційній роботі розв’язано важливу наукову задачу побудови автоматизованих освітніх програмних систем для практико-орієнтованого навчання у предметних областях з підвищеними вимогами до ізоляції середовищ виконання. Особливим випадком таких систем виступає кіберполігон як автоматизоване освітнє програмне середовище, що забезпечує автоматизоване розгортання ізольованих лабораторних завдань з кібербезпеки і автоматизовану перевірку коректності їх виконання. Актуальність роботи зумовлена кадровим розривом у галузі кібербезпеки, що зафіксований ENISA і ISC2 і перевищує чотири мільйони фахівців у глобальному масштабі і близько трьохсот тисяч позицій тільки у країнах Європейського Союзу. Класична академічна модель підготовки структурно не спроможна забезпечити необхідний приріст кваліфікованих фахівців за прийнятний час; для України ця проблема додатково загострилася у зв’язку з повномасштабним вторгненням Російської Федерації. Дисертаційна робота присвячена розробленню моделей, методів і архітектурних рішень для побудови такого класу програмних систем з гарантованими властивостями цілісності моделі знань, безпеки конкурентного розгортання, поліморфної оркестрації гетерогенних виконавчих середовищ і доведеної автоматизованої перевірки коректності виконання навчальних завдань. Розглянуто архітектурні рішення академічних кіберполігонів (DETER, CRATE, KYPO, CyRIS, SecGen), комерційних платформ (Hack The Box, TryHackMe, RangeForce) і гібридних академічно-комерційних платформ (UWF Cyber Range). Встановлено, що ні академічні, ні комерційні рішення не пропонують інтегрованої архітектури з композиційними інваріантами, яка б одночасно поєднувала формалізовану модель каталога компетентностей з перевірюваними інваріантами, поліморфну агентську оркестрацію і автоматизовану перевірку коректності виконання навчальних завдань. Систематизовано термінологію предметної області з акцентом на чіткому розмежуванні понять верифікації (формальне математичне доведення) і перевірки коректності (експериментальне порівняння), сервісу блокувань через Redis і класичного розподіленого взаємного виключення Lamport-стилю, програмної системи як абстрактного класу і програмної платформи Colo як конкретного артефакту реалізації. Сформовано модель каталога компетентностей як типізований орієнтований граф з трьома інваріантами (повноти покриття, ациклічності передумов і замикання передумов) над таксономіями NICE Workforce Framework і MITRE ATT&CK, з’єднаними через шар лабораторних завдань. Інваріанти формалізовано як предикати першого порядку, що перевіряються на рівні схеми та завантаження каталога. Доведено теорему про властивості цільового профілю за інваріантами каталога (Теорема 3.1), яка стверджує, що цільовий профіль робочої ролі NICE є непорожнім, замкненим за транзитивним замиканням передумов і зберігає порядок покриття за умов виконання усіх трьох інваріантів. Сформульовано задачу мінімального покриття бракуючих компетентностей (MCCP) як варіант задачі покриття множин з обмеженнями типізованого графа. Доведено NP-важкість задачі. Запропоновано жадібний евристичний алгоритм поліноміальної складності 𝑂(|𝑇|⋅|𝑅|⋅𝑑𝑚𝑎𝑥) з доведеною верхньою межею якості наближення 𝐻(|𝑅|), де 𝐻 - гармонійна функція. Розроблено метод стисненого інверсного індексу на основі структури даних RoaringBitmap для масштабованого зіставлення профілів компетентностей. Доведено теорему про складність операцій композиції 𝑂(𝐵+𝐴), де 𝐴 - сумарна кількість верхньорівневих ключів двох бітмапів, 𝐵 - сума розмірів контейнерів під спільними ключами. Розроблено поліморфний агентський протокол для гетерогенних виконавчих середовищ (контейнерних Docker і віртуальних машинних QEMU/KVM) через єдиний REST API і спільний абстрактний інтерфейс драйвера, з адаптивним автоматом станів активності IDLE/ACTIVE/FAST. Розв’язано задачу безпечного конкурентного розгортання ізольованих середовищ через комбінацію сервісу блокувань на основі атомарної операції SET NX у Redis (за паттернами Chubby і ZooKeeper, з індивідуальним ключем блокування) і ACID-транзакції бази даних з блокуванням рядка сесії розгортання LabRun через SELECT FOR UPDATE. Доведено теорему (Теорема 4.1) про збереження інваріанта квоти при паралельному розгортанні, яка гарантує, що для будь-якого користувача у будь-який момент часу кількість активних сесій не перевищує визначену квоту. Розроблено протокол поетапного оновлення зі збереженням стану (англ. stateful canary deployment) для довготривалих ізольованих навчальних сесій зі спільним станом у реляційній і кеш-базах даних. Доведено теорему (Теорема 4.2) про збереження активних сесій під час оновлення програмної системи у нормальному режимі без покладання на маршрутизацію з прив’язкою сесій через клієнтські cookie. Розроблено архітектуру програмної платформи Colo як інтегрованої реалізації запропонованих моделей і методів. Платформа складається приблизно з 70 тисяч рядків програмного коду на мові Python з застосуванням фреймворку Django, 26 тисяч рядків JavaScript і 13 тисяч рядків HTML-шаблонів. Реалізовано 106 шаблонів лабораторних завдань і сімейство протокольно повних файлів remote_solver.py для автоматизованої перевірки коректності виконання. Розроблено формалізовану мову опису лабораторних завдань як предметно-орієнтовану мову (DSL) з валідацією через JSON-схему і детермінованою генерацією ключів на основі SHA-256 із індивідуальним для пари (user,lab) початковим значенням (seed), ключованим серверним секретним ключем через HMAC-SHA256 (що забезпечує криптографічну непередбачуваність ключа без зберігання у БД); той самий механізм підтримує два режими відповіді - CTF-флаг або змістовну відповідь (індикатор компрометації, поле SIEM, класифікаційний вердикт) з анти-чіт-вплетенням лише голого значення. Створено SDK з п’ятьма категоріями генераторів часу виконання (crypto, forensics, stego, binary, network) для рандомізації завдань. Реалізовано повноцінну інтеграцію з системами управління навчанням через стандарт LTI 1.3 з підтримкою Deep Linking, Assignment-Grade Service і Names and Roles Provisioning Service. Експериментально перевірено коректність запропонованих рішень. Метрики продуктивності у контрольованому режимі теплого кешу (образ присутній у локальному кеші, вимірювання на dev-середовищі): медіана часу розгортання контейнерних завдань - 4,2 секунди, віртуальних машинних - 3,0 секунди швидким NBD-шляхом (загальна медіана VM-розгортань 86 секунд через бімодальний розподіл, §5.6.1; завдяки механізму NBD-ін’єкції, що дозволяє ін’єктувати ключі-флаги у файлову систему образу до запуску гостьової операційної системи); у режимі холодного старту (з підтягуванням образу з реєстру) медіана розгортання контейнерних завдань - близько 77 секунд (§5.6.1). Стрес-тест безпеки конкурентного розгортання з 100 паралельних запитів від одного користувача з квотою 1 підтверджує теоретичну гарантію: рівно одна сесія створилася, 99 - відхилено з очікуваною помилкою. У 47 операціях розгортання за період експлуатації лютий-травень 2026 жодна активна сесія не була втрачена через перемикання версій (95-відсоткова довірча межа ймовірності втрати - 7,6 % на одну операцію за інтервалом Уілсона). Перевірка коректності виконання remote_solver.py показала 100 % успішність відтворення сценаріїв розв’язання для завдань з реалізованим remote_solver. Практичне значення одержаних результатів. Платформу Colo впроваджено у навчальний процес бакалаврської програми з кібербезпеки факультету інформатики Національного університету "Києво-Могилянська академія" і у програму перенавчання ветеранів повномасштабного російського вторгнення компанії Sheriff Company; практичну підготовку, підтверджену актами впровадження (Додаток Б), пройшли 66 здобувачів НаУКМА за 2025-2026 навчальний рік і 36 ветеранів Sheriff Company - разом 102 особи, а у версії V2 платформи станом на 2026-05-20 зафіксовано 4 042 розгортання ізольованих середовищ. Формалізована мова опису лабораторних завдань і SDK уможливлюють додавання нових завдань незалежними авторами з автоматизованою перевіркою якості їх виконання. Перспективними напрямами подальших досліджень є: формальне дослідження стійкості моделі компетентностей до оновлень редакцій таксономій NICE і MITRE ATT&CK з автоматичним переносом профілів засвоєних компетентностей здобувачів при зміні структури каталога; адаптація запропонованих моделей і методів до суміжних напрямів кібербезпекової освіти (безпека промислових систем керування ICS/SCADA, безпека Інтернету речей, безпека хмарних інфраструктур, цифрова форензика); розширення каталога лабораторних завдань до промислових масштабів (500-1000 шаблонів) і дослідження поведінки MCCP-розв’язувача у нових режимах розрідженості каталога.
Description
PhD thesis to obtain the degree of Doctor of Philosophy in the Programme Subject Area 122 "Computer Science" (12 – Information Technologies). – National University of Kyiv-Mohyla Academy, Kyiv, 2026. This dissertation solves an important scientific problem of building automated educational software systems for practice-oriented learning in subject areas with elevated requirements for execution environment isolation. A special case of such systems is the cyber range as an automated educational software environment that provides automated deployment of isolated cybersecurity laboratory tasks and automated checking of their completion correctness. The relevance of the work is driven by the cybersecurity workforce gap documented by ENISA and ISC2, which exceeds four million specialists globally and approximately three hundred thousand positions within European Union countries alone. The classical academic training model is structurally incapable of providing the required growth of qualified specialists in a reasonable timeframe; for Ukraine, this problem has been additionally aggravated by the full-scale Russian invasion. The dissertation is dedicated to developing models, methods, and architectural solutions for building such a class of software systems with guaranteed properties of knowledge model integrity, concurrent deployment safety, polymorphic orchestration of heterogeneous execution environments, and provably automated correctness checking of educational task completion. The architectural solutions of academic cyber ranges (DETER, CRATE, KYPO, CyRIS, SecGen), commercial platforms (Hack The Box, TryHackMe, RangeForce), and hybrid academic-commercial platforms (UWF Cyber Range) have been analyzed. It has been established that neither academic nor commercial solutions offer an integrated architecture with compositional invariants that simultaneously combines a formalized competency catalog model with verifiable invariants, polymorphic agent orchestration, and automated correctness checking of educational task completion. The terminology of the subject area has been systematized with emphasis on clear distinction between verification (formal mathematical proof) and correctness checking (experimental comparison), between Redis-based lock service and the classical distributed mutual exclusion in the Lamport style, between the software system as an abstract class and the Colo software platform as a concrete implementation artifact. A model of the competency catalog has been formed as a typed directed graph with three invariants (coverage completeness, prerequisite acyclicity, and prerequisite closure) over the NICE Workforce Framework and MITRE ATT&CK taxonomies, joined through the laboratory task layer. The invariants have been formalized as first-order predicates that are checked at the catalog schema and data-loading level. A theorem on the properties of the target profile under the catalog invariants has been proven (Theorem 3.1), stating that the target profile of a NICE work role is non-empty, closed under the transitive closure of prerequisites, and order-preserving under the conditions of all three invariants. The Minimum Competency Coverage Problem (MCCP) has been formulated as a variant of the set cover problem with typed-graph constraints. The NP-hardness of the problem has been proven. A greedy heuristic algorithm of polynomial complexity 𝑂(|𝑇|⋅|𝑅|⋅𝑑𝑚𝑎𝑥) has been proposed, with a proven upper bound on approximation quality 𝐻(|𝑅|), where 𝐻 is the harmonic function. A method of compressed inverted index based on the RoaringBitmap data structure has been developed for scalable matching of competency profiles. A theorem on the complexity of composition operations 𝑂(𝐵+𝐴) has been proven, where 𝐴 is the total number of upper-level keys of two bitmaps, 𝐵 is the sum of container sizes under common keys. A polymorphic agent protocol has been developed for heterogeneous execution environments (containerized Docker and virtual machine QEMU/KVM) through a unified REST API and a common abstract driver interface, with an adaptive activity state machine IDLE/ACTIVE/FAST. The problem of safe concurrent deployment of isolated environments has been solved through the combination of a Redis-based lock service using the atomic SET NX operation (following the Chubby and ZooKeeper patterns, with a per-user lock key) and an ACID database transaction with row-level locking of the deployment-session row (LabRun) through SELECT FOR UPDATE. A theorem has been proven (Theorem 4.1) on the preservation of the user quota invariant under concurrent deployment, guaranteeing that for any user at any moment in time the number of active sessions does not exceed the defined quota. A stateful canary deployment protocol has been developed for long-running isolated educational sessions with shared state in relational and cache databases. A theorem has been proven (Theorem 4.2) on the preservation of active sessions during software system update in the normal operation mode without reliance on sticky routing of client cookies. The architecture of the Colo software platform has been developed as an integrated implementation of the proposed models and methods. The platform consists of approximately 70 thousand lines of program code in Python using the Django framework, 26 thousand lines of JavaScript, and 13 thousand lines of HTML templates. 106 laboratory task templates have been implemented, along with a family of protocol-complete remote_solver.py files for automated correctness checking. A formalized domain-specific language for laboratory task description has been developed with JSON Schema validation and deterministic generation of execution keys based on SHA-256 with a per-(user, lab) seed parameter keyed by a server secret via HMAC-SHA256 (ensuring both deterministic per-student uniqueness and cryptographic unpredictability - a key cannot be recomputed without the server SECRET_KEY - with stateless verification and without storing the key). The same mechanism backs two answer modes - a CTF flag or a meaningful value (indicator of compromise, SIEM field, triage verdict) graded with an anti-cheat invariant that weaves in only the bare value, never a literal COLO_FLAG token. An SDK with five categories of runtime generators (crypto, forensics, stego, binary, network) for task randomization has been created. Full integration with learning management systems has been implemented through the LTI 1.3 standard with support for Deep Linking, Assignment-Grade Service, and Names and Roles Provisioning Service. The correctness of the proposed solutions has been experimentally verified. Performance metrics in controlled warm-cache mode (image present in the local cache, measured on the dev environment): the median deployment time for containerized tasks is 4.2 seconds and for virtual machine tasks 3.0 seconds via the fast NBD path (overall VM deployment median 86 seconds due to a bimodal distribution, Section 5.6.1; the NBD-injection mechanism that allows injecting flag keys into the image file system before launching the guest operating system); in cold-start mode (pulling the image from the registry) the median deployment time for containerized tasks is about 77 seconds (Section 5.6.1). A stress test of safe concurrent deployment with 100 parallel requests from a single user with a quota of 1 confirms the theoretical guarantee: exactly one session was created, 99 were rejected with the expected error. In 47 deployment operations over the exploitation period February-May 2026, no active session was lost due to the canary swap (95-percent confidence upper bound on the probability of loss is 7.6 % per operation by the Wilson score interval). Correctness checking of the remote_solver.py suite showed 100 % success in reproducing solution scenarios for tasks with an implemented solver. Practical significance of the obtained results. The Colo platform has been implemented in the educational process of the Bachelor’s program in cybersecurity at the Faculty of Informatics of the National University of Kyiv-Mohyla Academy and in the retraining program for veterans of the full-scale Russian invasion at Sheriff Company; practical training confirmed by implementation acts (Appendix B) was completed by 66 NaUKMA students (2025-2026 academic year) and 36 Sheriff Company veterans - 102 persons in total, while version V2 of the platform recorded 4,042 isolated-environment deployments as of 2026-05-20. The formalized laboratory task description language and SDK enable independent authors to add new tasks with automated quality checking of their completion. Promising directions for further research are: formal study of the resilience of the competency model to taxonomy edition updates (NICE, MITRE ATT&CK) with automatic transfer of learner competency profiles upon catalog structure changes; adaptation of the proposed models and methods to adjacent areas of cybersecurity education (industrial control systems security ICS/SCADA, Internet of Things security, cloud infrastructure security, digital forensics); expansion of the laboratory task catalog to industrial scale (500-1000 templates) and study of the MCCP solver behavior in new catalog sparsity regimes.
Keywords
автоматизована освітня програмна система, кіберполігон, кібербезпека, інформаційна безпека, вразливості, практико-орієнтоване навчання, онтологія каталога компетентностей, типізований орієнтований граф, метод аналізу ієрархій, автомат станів, розподілені обчислення, LTI інтеграція, TLS протокол, рекомендаційна система навчальної траєкторії, теорія складності, дисертація, automated educational software system, cyber range, cybersecurity, information security, vulnerabilities, practice-oriented training, competency catalog ontology, typed directed graph, analytic hierarchy process, state machine, distributed computing, LTI integration, TLS protocol, learning trajectory recommender system, complexity theory
Citation
Бабич Т. А. Методи та засоби побудови автоматизованої освітньої програмної системи для кібербезпеки (кіберполігону) : дисертація на здобуття наукового ступеня доктора філософії / Бабич Трохим Анатолійович ; наук. кер. Глибовець Андрій Миколайович ; Національний університет "Києво-Могилянська академія", Міністерство освіти і науки України. - Київ : [б. в.], 2026. - 225 с. : схеми, табл. - Містить додатки.