Горбатюк С. О. Методи модельного розроблення та аналізування кібербезпеки для інформаційних систем логістики

Загальна проблема дослідження полягає у перевірці властивостей безпеки розподілених систем, що використовуються для вирішення відповідних задач у системах міжнародної логістики, за допомогою перевірки моделей (model checking) та алгебраїчного підходу з інсерційним моделюванням. Іншою актуальною проблемою є задача виявлення та протидії випадкам шахрайства, особлива увага приділяється даній проблемі ще на стадії розробки високонадійних систем за допомогою модельного способу розробки логістичних систем. Метою роботи є вирішення науково-прикладної проблеми створення методології для технології модельного способу розробки для високонадійних розподілених систем, зокрема для систем логістики. Для досягнення вказаної мети необхідно розв'язати наступні взаємопов'язані задачі: – провести аналіз існуючих моделей, методів і технологічних засобів, які дозволяють створити інструментарій та методологію для використання розподілених систем, зокрема технології блокчейн в логістичних системах; – провести аналіз властивостей безпеки та можливих атак в логістичних системах – визначити теоретичні основи базових понять інсерційного моделювання для логістичних агентів в певному діючому середовищі; – запропонувати архітектурно-структурні рішення, алгоритми та програмно-апаратні засоби формування і відображення взаємодії логістичних агентів та безперервного контролю за їх розміщенням та поведінками з метою дотримання безпеки функціонування; – запропонувати рішення, методи кібербезпеки та алгоритми верифікації для перевірки властивостей цілісних логістичних систем, таких як безпека та життєдіяльність; - визначити використання алгебраїчного та інсерційного підходу на стадіях модельного способу розробки для процедур верифікації, тестування; - розглянути методи безпеки в логістичних системах, захисту від атак зловмисника та шахрайства та методи аналізу вразливостей; - розглянути методи аналізу безпеки в системах на основі блокчейн платформ на основі інсерційного підходу; - побудувати приклад модельної розробки логістичної системи. Перший розділ дисертації присвячено виявленню та вивченню глобальних проблем, які накопичились в сучасній системі міжнародної логістики, та які можуть бути вирішені за допомогою застосування технології блокчейн та методів модельної розробки систем. Проаналізовано приклади на напрямки прогресивних шляхів використання розподілених систем та смарт-контрактів на їх основі в міжнародній логістиці передовими логістичними операторами, науковими та державними установами. Розглянуто методологію проектування логістичних систем з врахуванням необхідності дотримання властивостей безпеки та надійності протидії шахрайству та атакам зловмисників. При розробці високонадійних систем, критичних до безпеки, є доцільним використання модельного способу розробки, тому проаналізовано процедуру валідації та верифікації артефактів на всіх етапах розробки таких систем. У другому розділі розкрито основи використання алгебраїчного підходу та інсерційного моделювання при формальній верифікації та формалізації за допомогою тестування на основі моделей. Наведено приклад застосування на практиці алгебри поведінок на прикладі діючої закритої логістичної системи фермерського господарства, наведено приклади запису моделей поведінок агентів. Розглянуто основні властивості безпеки, що перевіряються в логістичній системі фермерського господарства. Приклад застосування у фермерському господарстві розширено до більш широкого застосування у відкритій системі міжнародної логістики. У третьому розділі проаналізовано проблеми безпеки в проектуванні логістичної блокчейн платформи. Описано інсерційну семантику блокчейн-системи та в розумних контрактах (Smart Contracts,) змодельовано дії зловмисників у цих системах, формалізовано атаки DAO для розумних контрактів. Запропоновано принципи дій для запобігання атакам при проектуванні блокчейн систем. Четвертий розділ описує два приклади використання модельного методу розробки: приклад побудови логістичної системи для фермерського господарства, яка використовує моделювання на рівні моделей вимог та другий - приклад формалізації вимог та подальше розроблення для логістичної системи, що визначає та супроводжує функціонування ланцюжка постачання. Розглянуто схему документообігу при мультимодальному міжнародному перевезенні, запропоновано використання модельного способу розробки контракту для мономодального перевезення на блокчейн платформі з метою мінімізації ризиків для учасників та запобіганню дій шахраїв. Описані в дисертаційному дослідженні підходи до побудови логістичних систем є універсальними, та можуть використовуватись, за умови адаптації, до логістичних систем будь-якої складності та масштабу, як для закритих, так і для відкритих систем національного та міжнародного рівня.