Аналітичний огляд доповідей міжнародної конференції «математичні моделі, методи та архітектури для захисту комп`ютерних мереж» (mmm-acns-2010)
Попередні міжнародні конференції MMMACNS, проведені в 2001, 2003, 2005 і 2007 рр., Продемонстрували гострий інтерес дослідних організацій і вчених усього світу до тематики використання формальних методів, моделей і розробці перспективних архітектурних рішень для забезпечення безпеки інформаційних ресурсів в комп`ютерних мережах. Досвід їх організації показав, що проведення подібної конференції в Санкт-Петербурзі стимулює розробку нових результатів і плідні обміни думками між різними школами (зарубіжними і російськими) в області захисту інформації, полегшує поширення нових ідей і просуває дух співпраці між дослідниками в міжнародному масштабі. Тому вирішено регулярно проводити цю конференцію.
Конференція була організована СПІІРАН і Університетом Бінгхемтона - державним університетом штату Нью-Йорк (США). Фінансову підтримку конференції забезпечили Європейське управління воздушнокосміческіх досліджень і розробок США, Управління наукових досліджень ВМС США і Російський фонд фундаментальних досліджень. Міжнародний програмний комітет, що включав відомих фахівців по темі конференції з 18 країн Європи, Австралії та Америки, виступав гарантом високого наукового рівня конференції.
Відео: Лекція 7. Класична схема побудови мережі
На конференції було зареєстровано 67 учасників. Статистичні дані про приналежність учасників до різних областей діяльності такі: число учасників з університетського середовища - 29- з наукових організацій - 26- з комерційних організацій - 6 з державних установ - 6.
Дебар (Франція) виступив з доповіддю на тему «Залежності сервісів при забезпеченні безпеки інформаційних систем». з Франції представив модель залежностей інформаційних послуг, розроблену з метою забезпечення адміністраторів безпеки системою підтримки прийняття кількісних рішень для розгортання та управління політиками безпеки. Дана система дозволяє визначати найбільш критичні місця в політиках безпеки і скорочує в цілому витрати на управління безпекою інформаційних систем.
Автор докладно розглянув стан справ в області моделювання залежностей послуг, вимоги, що пред`являються до моделювання залежностей, і обгрунтував необхідність розробки уявлення сервісних залежностей, яке включає інформацію не тільки про їх розмір, а й про привілеї.
Була запропонована нова формальна модель залежностей. Спочатку автор розглянув просту модель послуг. Потім представив її розширення за допомогою поняття привілеї, а також механізми поділу привілеїв, що задаються предикатами Credential і Trust. З використанням мови аналізу і проектування AADL (Architecture Analysis and Design Language) були показані різні варіанти представлення залежностей. Автор ввів такі характеристики залежностей: тип (type), режим (mode) і вплив (impact). Можливими типами залежностей є: «з боку сервісу» (serviceside), «з боку користувача» (userside) і проксі (proxy). Сервіс має чотири операційних режиму: запуск (start mode), очікування запиту (idle mode), обробка запиту (request mode) і останов (stop mode). Вплив залежностей відображається послідовностями станів деградації провідного сервісу, які змінюють доступ до даних за допомогою залежного сервісу.
На закінчення свого виступу доповідач зупинився на питаннях реалізації запропонованої моделі залежностей послуг та її застосування для оцінки наслідків поширення атак в мережі.
У доповіді Д. Гольманна (Німеччина) «Безпечні додатки без безпечних інфраструктур» були розглянуті приклади атак прикладного рівня, проти яких не можна забезпечити захист на рівні інфраструктури Інтернету. До числа таких атак, зокрема, автор відносить: атаки «SQLін`екціі», міжсайтовий скриптинг (СrossSite Scripting), міжсайтовий підробку запиту (CrossSite Request Forgery), атаки «отруєння кешу» (Cache Poisoning), атаки «зв`язування DNS» (DNS Rebinding ) і атаки «людини в середині» (Manin theMiddle). Останній вид атаки грунтується на застосуванні протоколу SSL / TLS, що дозволяє встановити захищене тунельний з`єднання між клієнтом і веб-сервера.
Доповідач показав, що розгортання захищеної інфраструктури не є достатньою умовою для захисту критично важливих додатків. Додатки можна захищати, не покладаючись на безпеку сервісів, що надаються інфраструктурою. Отже, розгортання захищеної інфраструктури не є необхідною умовою для захисту критично важливих додатків. У той же час це є єдино необхідною умовою забезпечення обчислювальної цілісності (execution integrity) самої інфраструктури, а також її доступності. Доступність є первинним властивістю, яка вимагається від комунікаційної інфраструктури. Інші сервіси безпеки, такі, як конфіденційність, цілісність і автентичність, ця інфраструктура не спроможна досягти.
Доповідач зробив висновок, що останнім часом акцент в моніторингу безпеки все більше зміщується від захищених операційних систем (1980-ті рр.) І веб-браузер (1990е рр.) На прикладні
додатки. У зв`язку з цим досить актуальна задача створення безпечних додатків «безбезопасних» інфраструктур. Відповідальність за забезпечення безпеки в цьому випадку все в більшій мірі покладається на розробників даних програм і кінцевих користувачів. Однак фахівці зазначених категорій рідко добре підготовлені для вирішення даного завдання.
Багато найпростіші види помилок, наприклад, переповнення буфера, можуть бути попереджені при використанні типізованих мов замість традиційних, таких як C і C ++. Мови Java, Scheme і ML є прикладами мов, в яких принаймні принципово не може мати місце переповнення буфера. Однак залишаються загрози, пов`язані з використанням недоліків програмування на більш високому рівні, наприклад, атаки класу «SQLін`екціі». Таким чином, наступне покоління мов програмування має ґрунтуватися на системах типізації, які можуть висловлювати і виконувати політики безпеки конкретних додатків.
В основу мов системного програмування наступного покоління автор пропонує покласти застосування так званих «витончених» (refinement) типів даних, тобто типів, що мають форму
«X: T», де T - тип, а P (x) - предикат над значеннями типу T.
Однак основна проблема використання витончених типів даних полягає в знаходженні способів перевірки типів.
Автор наводить приклад системи Coq, що відноситься до класу «помічників доказів» (Proof Assistants), яка забезпечує потужний уніфікований спосіб написання наступних алгоритмів:
а) програм;
б) специфікацій і моделей, що охоплюють бажані властивості програм, від простої типізації та властивостей безпеки аж до повної коректності;
в) формальних машіннопроверяемих доказів того, що програма відповідає своїй специфікації.
На закінчення був представлений приклад розробленої мови Ynot, що є розширенням Coq, який базується на теорії типів Хоара (Hoare Type Theory - HTT), і наведені результати побудови на його основі верифицированной програмної системи.
Доповідач завершив свій виступ твердженням, що мова програмування, вбудований в Coq, є високорівневим, подібно до мови ML. Для багатьох додатків це є ідеальним випадком. Однак в той же час для багатьох завдань системного програмування, наприклад програмування гіпервізора або драйверів пристроїв, вона є мовою надто високого рівня. Таким чином, необхідна розробка низкоуровневой середовища програмування, яка може ефективно замінити мову C.
У доповіді Б. Пренеля (Бельгія) «Криптографія для безпеки мереж: невдачі, успіхи і проблеми» були розглянуті сучасні криптографічні алгоритми, які використовуються для забезпечення безпеки обчислювальних мереж. У доповіді обговорювався сучасний стан широкого кола криптографічних алгоритмів, що застосовуються в мережевих додатках, і був зроблений висновок, що дуже часто проблеми безпеки мереж ідентифікуються з даними алгоритмами і їх реалізаціями.
