автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.19, диссертация на тему:Верификация правил фильтрации межсетевых экранов на основе применения метода "проверка на модели"

УДК 004.414.23

005061512 На правах рукописи

/

Полубелова Ольга Витальевна

ВЕРИФИКАЦИЯ ПРАВИЛ ФИЛЬТРАЦИИ МЕЖСЕТЕВЫХ ЭКРАНОВ НА ОСНОВЕ ПРИМЕНЕНИЯ МЕТОДА «ПРОВЕРКИ НА МОДЕЛИ»

Специальность:

05.13.19 — Методы и системы защиты информации, информационная безопасность

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических наук

13 ИЮН 2013

Санкт-Петербург 2013

005061512

Работа выполнена в Федеральном государственном бюджетном учреждении науки Санкт-Петербургском институте информатики и автоматизации РАН.

Научный руководитель: доктор технических наук, профессор, заведующий лабораторией

СПИИРАН Котенко Игорь Витальевич

Официальные оппоненты: доктор технических наук, профессор, заведующий лабораторией

СПИИРАН Воробьев Владимир Иванович

доктор технических наук, профессор, Генеральный директор ООО «Инновационный центр

транспортных исследований» Искандеров Юрий Марсович

Ведущая организация:

Федеральное Государственное унитарное предприятие "Научно-исследовательский институт "Рубин"

Защита состоится «25»июня 2013 г. В 11 часов на заседании диссертационного совета Д.002.199.01 при Федеральном государственном бюджетном учреждении науки Санкт-Петербургском институте информатики и автоматизации РАН по адресу: 199178, Санкт-Петербург, В.О., 14 линия, 39.

С диссертацией можно ознакомиться в библиотеке Федерального государственного бюджетного учреждения науки Санкт-Петербургского института информатики и автоматизации РАН

Автореферат разослан« 22 » мая 2013 г.

Ученый секретарь

диссертационного совета Д.002.199.01

к. т. н. Нестерук Филипп Геннадьевич

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы диссертации.

Системы защиты информации (СЗИ) в компьютерных сетях, основанные на политиках безопасности, широко используются в настоящее время благодаря гибкости в управлении и удобству администрирования. Политика фильтрации, которая является одним из видов политик безопасности, позволяет администратору сети централизованно применять сетевую политику безопасности в выделенном сегменте IP-сети. К программно-аппаратным средствам, обеспечивающим решение этой задачи, относятся межсетевые экраны (МЭ). Политика фильтрации, на основе которой работает МЭ, формируется специалистами, знающими особенности защищаемой сети и используемых МЭ, и базируется на общей политике безопасности компании, закрепленной в регламентирующих документах. Однако эта задача является сложной и подверженной ошибкам из-за важности учета различных зависимостей правил, а также необходимости проверки согласованности новых правил со всей политикой и конфигурацией сети. Эта сложность увеличивается по мере роста размера сети.

Проверка правильности (верификация) правил фильтрации вручную значительно затруднена из-за большого количества правил и их взаимозависимости, и не гарантирует отсутствие ошибок.

Существуют различные подходы к автоматизации верификации правил фильтрации, например, посредством систем доказательства теорем или исчисления событий. Однако большинство из них находятся в стадии исследования. Коммерческие решения, как правило, ориентированы на какие либо специфические программно-аппаратные средства и не обладают достаточной универсальностью.

В данной работе для решения этой задачи предлагается использовать метод "проверки на модели" (Model checking). Согласно определению, Model checking-это метод проверки того, что на данной формальной модели системы заданная логическая формула выполняется (принимает истинное значение). Преимуществами данного метода являются его высокий уровень абстракции при представлении данных, что позволяет построить адекватную, но упрощенную модель сложной системы компьютерной сети, выделяя лишь функции, наиболее важные для верификации правил фильтрации. Кроме того метод разрабатывался на базе строгих формальных теорий, в отличие от различных других методов тестирования и верификации. К недостаткам метода относится вычислительная сложность подхода, но с ростом производительности компьютерных систем, этот недостаток нивелируется. Применение метода "проверки на модели" представляется целесообразным

для эффективного решения задачи верификации правил фильтрации с учетом того, что она не относится к категории систем реального времени.

Для успешного развертывания СЗИ и поддержания ее функционирования требуется проводить регулярный анализ политики фильтрации. Он позволяет выявить и разрешить различные аномалии в политиках, которые могут привести к серьезным нарушениям свойств безопасности и сетевым уязвимостям, таким как блокирование легитимного трафика, разрешение нежелательного трафика, а также передача данных по сети в незашифрованном виде.

Целью исследования является повышение защищенности компьютерной сети за счет использования разработанных моделей, алгоритмов и методики формальной верификации правил фильтрации.

Для достижения данной цели в диссертационной работе поставлены и решены следующие задачи:

1. Анализ способов построения и функционирования межсетевых экранов, возможных аномалий фильтрации и задачи верификации правил фильтрации межсетевых экранов.

2. Анализ методов верификации СЗИ, основанных на политиках безопасности, в том числе метода "проверки на модели".

3. Разработка модели аномалий фильтрации и алгоритмов выявления и стратегий разрешения этих аномалий методом "проверки на модели".

4. Разработка модели компьютерной системы и межсетевых экранов для реализации метода "проверки на модели".

5. Построение архитектуры системы верификации правил фильтрации (СВПФ) межсетевых экранов методом "проверки на модели".

6. Разработка методики верификации правил фильтрации межсетевых экранов методом "проверки на модели" на основе представленных моделей и архитектуры системы верификации.

7. Реализация СВПФ, проведение экспериментов и оценка эффективности методики верификации.

Объектом исследования являются правила фильтрации межсетевых экранов и аномалии в них, а также процессы их обнаружения и разрешения.

Предметом исследования являются методики, модели и алгоритмы верификации правил фильтрации, основанные на методе "проверки на модели".

Научная задача работы - разработка научно-методического аппарата (моделей, алгоритмов и методики) верификации правил фильтрации межсетевых экранов для обнаружения и разрешения аномалий на основе метода "проверки на модели".

Методологическую и теоретическую основу исследования составили научные труды отечественных и зарубежных авторов в областях

верификации политик безопасности, моделирования компьютерных систем, защищенных межсетевыми экранами, компьютерной безопасности.

Методы исследования, использованные в диссертации, относятся к методам системного анализа, теоретико-множественного представления, объектно-ориентированного программирования, моделирования, логико-математического, а также методы сравнения и аналогий.

Основными результатами, выносимыми на защиту, являются:

1. Модель аномалий фильтрации и алгоритмы выявления и разрешения аномалий методом "проверки на модели".

2. Модель компьютерной сети, защищенной межсетевым экраном.

3. Методика верификации правил фильтрации межсетевых экранов на основе метода "проверки на модели".

4. Архитектура и программная реализация системы верификации правил фильтрации межсетевых экранов на основе метода "проверки на модели".

Научная новизна исследования заключается в следующем:

1. Отличительной характеристикой модели аномалий фильтрации является учет основных видов аномалий фильтрации (затенение, обобщение, корреляция и избыточность), а также возможность использования для формальных методов верификации за счет представления на языке линейной темпоральной логики (Linear Temporal Logic, LTL). Алгоритмы выявления и разрешения аномалий отличаются от существующих спецификой метода "проверки на модели", а также возможностью применять различные стратегии разрешения, тогда как в подобных системах реализовано только выявление аномалий.

2. Отличительной особенностью модели компьютерной сети, защищенной межсетевым экраном, является то, что помимо стандартного набора полей, характерных для правил фильтрации, добавляются поля, определяющие временной интервал, в течение которого действует правило. В модели выделены лишь аспекты, касающиеся генерации сетевого трафика и взаимодействия с межсетевыми экранами, что значительно упрощает модель сети, и позволяет повысить эффективность верификации правил фильтрации.

3. Основным отличием данной методики верификации является применение метода "проверки на модели" для верификации политики фильтрации. В отличие от известных, предложенная методика учитывает специфику анализа сетевых устройств, тогда как в существующих работах по верификации политик безопасности, предлагаются решения главным образом для политик авторизации. Основные этапы методики автоматизированы за счет использования разработанных моделей компьютерной сети, аномалий фильтрации и алгоритмов выявления и разрешения аномалий.

4. Отличием архитектура и программная реализация системы верификации правил фильтрации политики безопасности на основе метода «проверки на модели» является наличие в своем составе предложенных методо-ориентированных моделей компьютерной системы, защищенной межсетевым экраном, а также алгоритмов выявления и разрешения аномалий.

Обоснованность и достоверность представленных в диссертационной работе научных положений обеспечивается проведением тщательного анализа состояния научных исследований в данной области, подтверждается согласованностью теоретических результатов с экспериментальными. Эксперименты проводились на программном прототипе. Также проводилась апробация основных теоретических положений в печатных трудах и докладах на научных конференциях.

Теоретическая и практическая значимость исследования. Разработанные модели и алгоритмы выявления и разрешения аномалий, а также методика верификации могут быть использованы для решения задач в области анализа сетевого трафика. В частности, они позволят: верифицировать политики фильтрации в существующих компьютерных сетях, исследовать корректность применения политики фильтрации в компьютерной сети, защищенной межсетевым экраном; повысить эффективность разработки новых политик и редактирования уже используемых, особенно для больших компьютерных сетей, состоящих из множества сегментов; вырабатывать стратегии разрешения различных аномалий фильтрации на основе построенных в процессе верификации контпримеров (описаний некорректных состояний).

Реализация результатов работы. Результаты, полученные в диссертационной работе, были использованы в рамках следующих научно-исследовательских работ: проект Шестой рамочной программы (FP6) Европейского Сообщества "Средства и модели защиты информации, основанные на политике безопасности (POSITIF)", контракт IST-2002-002314, 2003-2007 гг., проект Минобрнауки России «Исследование и разработка методов, моделей и алгоритмов интеллектуализации сервисов защиты информации в критически важных инфраструктурах», государственный контракт № 11.519.11.4008, 2011-2013 гг.; проект Седьмой рамочной программы (FP7) Европейского Сообщества «Управление информацией и событиями безопасности в инфраструктурах услуг (MASSIF)», контракт № 257475, 2010-2013 гг.; «Математические модели и методы комплексной защиты от сетевых атак и вредоносного ПО в компьютерных сетях и системах, основывающиеся на гибридном многоагентном моделировании компьютерного противоборства, верифицированных адаптивных политиках безопасности и проактивном мониторинге на базе интеллектуального анализа данных», грант РФФИ №

10-01-00826-а, 2010-2012 гг.; проект по программе фундаментальных исследований ОНИТ РАН «Архитектура, системные решения, программное обеспечение, стандартизация и информационная безопасность информационно-вычислительных комплексов новых поколений», 2009-2011 гг., в учебном процессе кафедры автоматизированных систем обработки информации и управления Санкт-Петербургского государственного электротехнического университета «ЛЭТИ» им. В.И. Ульянова (Ленина) при подготовке специалистов по специальности "Компьютерная безопасность" и др.

Апробация результатов работы. Основные положения и результаты диссертационной работы докладывались на следующих научных конференциях: IEEE Fourth International Workshop on "Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications" -IDAACS'2011 (Prague, Czech Republic, 15-17 September 2011), XIX Общероссийская научно-техническая конференция «Методы и технические средства обеспечения безопасности информации» (МТСОБИ, Санкт-Петербург, 2011); Санкт-Петербургская межрегиональная конференция «Информационная безопасность регионов России (ИБРР, Санкт-Петербург, 2005, 2006, 2007, 2011)»; XII Санкт-Петербургская Международная Конференция «Региональная информатика-2010» («РИ-2008»); Девятая общероссийская научная конференция «Математика и безопасность информационных технологий» (МаБИТ-2005, МаБИТ-2006, Москва); V Всероссийская научно-практическая конференция «Имитационное моделирование. Теория и практика» (ИММОД, Санкт-Петербург, 2005); Third International Workshop "Information Fusion and Geographical Information Systems" - IF&GIS'07 (St.Petersburg, Russia, May 27-29, 2007); 2007 IEEE Workshop on Policies for Distributed Systems and Networks - Policy'2007 (13-15 June 2007. Bologna, Italy); X Национальная конференция по искусственному интеллекту с международным участием (КИИ-2006); Пятая Общероссийская Конференция "Математика и безопасность информационных технологий" -МаБИТ-06 (Москва, МГУ, 2006) и др.

Публикации. По материалам диссертационной работы опубликовано 26 работ, в том числе 6 статей («Вопросы защиты информации», «Вестник компьютерных и информационных технологий», «Изв. вузов. Приборостроение», «Труды СПИИРАН») из перечня ВАК на соискание ученой степени доктора и кандидата наук.

Структура и объем диссертационной работы. Диссертационная работа объемом 132 машинописных страницы, содержит введение, три главы и заключение, список литературы, содержащий 135 наименований, 6 таблиц, 18 рисунков.

СОДЕРЖАНИЕ РАБОТЫ

Во введении обоснована важность и актуальность темы диссертации, сформулированы цель диссертационной работы и решаемые задачи, определены научная новизна и практическая значимость работы, также представлены основные результаты реализации научных результатов в научно-исследовательских проектах.

В первой главе диссертации рассматриваются различные подходы к верификации политик безопасности, и выделяется метод "проверки на модели". Описываются аномалии фильтрации, их основные типы и алгоритмы обнаружения. Приводится описание требований к верификации компьютерных систем, защищенных межсетевыми экранами. Определяется задача исследования, ее цели и требования к ее реализации.

Вводятся основные определения и классификация аномалий фильтрации. Рассматриваются такие виды аномалий как затенение, обобщение, корреляция и избыточность, вводятся их определения.

Представляются основные понятия и методы формальной верификации, такие как абдукция, метод автоматического доказательства теорем и метод "проверки на модели".

Для решения поставленной задачи был взят за основу метод "проверки на модели". Этот метод позволяет продемонстрировать, что верифицируемая система обладает желаемыми свойствами, изучая все возможные пути выполнения программы, а если свойства не выполняются, то предоставляет контрпримеры с нарушением свойств.

Сравнительный анализ методов и средств верификации для систем безопасности, основанных на политиках, позволил сформулировать ряд требований к системе верификации (своевременности, обоснованности и ресурсопотреблению).

Сформулирована задача исследования. Она заключается в разработке: (1) модели аномалий фильтрации для каждого типа аномалий, а также алгоритмов их выявления и разрешения; (2) модели компьютерной сети, защищенной межсетевыми экранами; (3) методики верификации, которая позволит верифицировать правила фильтрации политики безопасности на предмет аномалий и предлагать стратегии разрешения этих аномалий; (4) методика верификации должна минимизировать заданную целевую функцию при выполнении требований к своевременности, обоснованности и ресурсопотреблению процесса верификации.

Методика верификации правил фильтрации МЭ задается следующим образом: Р =< б, М > , где С - множество шагов по выполнению этапов верификации правил фильтрации политики безопасности и алгоритмов обнаружения и разрешения аномалий фильтрации на основе метода "проверки на модели", а М - это множество моделей, М =< Мм, Мл >,

где Мы - модель компьютерной сети, защищенной МЭ, Мл - модель аномалий фильтрации, которые интегрированы в методику, позволяющую верифицировать правила фильтрации МЭ и применять стратегии разрешения ко всем обнаруженным аномалиям.

Целью методики является минимизация целевой функции 1псоп<!1з1епсу1пс1еХур(<р) —> ггап, при соблюдении требований к остальным

показателям эффективности верификации правил фильтрации: своевременности, ресурсопотребления и обоснованности. Функция Ысот'ШепсуЫЛех^ показывает противоречивость политики фильтрации МЭ.

ср е Т, где Г: {/: РА/р->Л!>} представляет собой множество всех методик

верификации, /р е РШепщРоНсу, РШепп^РоИсу - множество всех политик фильтрации, ЛЯ - набор подходящих стратегий разрешения аномалий фильтрации, направленных на устранение противоречий. Д5 с /?ело/vingStrategy, где ResolvingStrategy - множество всех возможных стратегий разрешения аномалий. РА^, где РА - аномалии фильтрации, выявленные в некоторой политике фильтрации /р, РИ1егпщАпота1у -множество всех аномалий фильтрации, РА с РИ(ег^Апота1у .

Во второй главе представлены модель аномалий фильтрации, алгоритмы выявления и разрешения аномалий на основе метода "проверки на модели", а также модель компьютерной сети, защищенной МЭ. В работе используется понятие аномалии фильтрации, определяемое как противоречие между двумя правилами фильтрации, при котором одно или более правил политики фильтрации никогда не будут активированы. Такой термин широко используется в работах специалистов из разных стран, занимающихся проблематикой проверки правил фильтрации.

Модель аномалий фильтрации предназначена для формальной спецификации компьютерной сети, защищенной межсетевыми экранами. Спецификация моделируемой системы представляет собой набор темпоральных формул, выражающих некорректные состояния в системе, проверяемые в процессе верификации. Такие формулы выражают наличие аномалий в правилах фильтрации. Они позволяют выполнить анализ корректности применения правила фильтрации для сетевого пакета межсетевого экрана, т.е. насколько согласованно и непротиворечиво применяются правила фильтрации сетевого трафика. Алгоритмы разрешения аномалий строятся на выводимых верификатором контрпримерах, приводящих компьютерную систему к аномалии, и определенных вариантах разрешения.

Модель формализуется с помощью линейной темпоральной логики и определяет свойства, характеризующие состояние верифицируемой системы, для каждого типа аномалии.

Введены обозначения свойств и событий таких состояний системы, нарушение которых приведет к появлению аномалий фильтрации: ta - время

активации правилаип\ ta — время активации правила ит\ td — время деактивации правила ип; td - время деактивации правила ит; ои — приоритет правила ип\ ои - приоритет правила ит; 1и - привилегия правила м„ ; /„ — привилегия правила ит. Также определены следующие логические функции для обозначения состояния системы: IsSubset(un,um) -адресный диапазон правила ип, который является подмножеством диапазона адресов правила ит ; IsIntersection{un,um) - адресный диапазон правила ип, который является пересечением диапазона адресов правила ит; IsEqual(un,um) - адресный диапазон правила ип, который совпадает с диапазоном адресов правила ит .

При формализации различных аномалий фильтрации используется темпоральный оператор G, обозначающий, что формальное утверждение должно выполняться в настоящее время и всегда в будущем:

(1) аномалия затенения:

L = <Ол < > А К. >0JA IsSubset{um, ип) => (/„_ -, = lUm));

(2) аномалия обобщения:

Л = G«X„ <t„J A (tam < ^ ) Л (oUm > о„_) AIsSubset(u„ ,!/„)=> (/„_ -, = )) ;

(3) аномалия корреляции:

/с = <?(('.. < ^ ) А <td ) А (0„_ > 0„и ) а

disinter sec П'ои(м„ ,Mm)A —i(IsEqual(ип ,ит ) => (/,_ -, = )) ;

(4) аномалия избыточности:

Л ~ G((ta„ ^ tam ) А < t^ ) А (о„т > 0„я ) AIsInterseCtion(u„ , И J (/„_ = /„_ )) .

Алгоритмы выявления и разрешения аномалий методом "проверки на модели" предназначены для определения последовательности действий, позволяющих обнаружить и разрешить все аномалии в наборе правил фильтрации МЭ компьютерной сети.

Алгоритм выявления аномалий описывается в виде процедуры DETECT-ANOMALY. Входным параметром является массив, содержащий коллекцию пакетов и примененных к ним правил фильтрации. Выходными данными является массив обнаруженных аномалий фильтрации и правила, между которыми возникает данная аномалия. Суть работы алгоритма заключается в

анализе примененных к пакетам правил политики фильтрации и выявлении аномалий на основе условий, специфицированных в модели аномалий фильтрации. Для каждой выявленной аномалии строится контрпример, содержащий путь, по которому система пришла в некорректное состояние.

Алгоритм разрешения аномалий описывается в виде процедуры RESOLVE-ANOMALY. Входным параметром является массив, содержащий коллекцию набор правил, содержащих аномалии, и типы аномалий. Выходными данными является массив правил с разрешенными аномалиями и типы примененных стратегий разрешения. Этот алгоритм позволяет применять различные стратегии разрешения аномалий, основываясь на контрпримерах, сгенерированных алгоритмом выявления аномалий. Выбор стратегии зависит от типа аномалии, например для аномалии избыточности предусмотрена стратегия удаления избыточного правила, а для аномалии затенения предлагается разбить правило, вызывающее аномалию на два, определив для пересекающегося диапазона адресов новую привилегию.

Модель компьютерной сети, защищенной межсетевыми экранами, которая представляет собой параллельную систему с конечным числом состояний, задается моделью Крипке MN. Модель отражает аспекты, имеющие отношение к проверяемым свойствам, и существенные характеристики моделируемой системы, важные для верификации правил фильтрации.

Предлагаемая модель предназначена для представления Структуры компьютерной сети, ее основных элементов и сетевых процессов. В модели для представления компьютерной сети используются такие характеристики, как расположение хостов в защищенной сети, IP-адреса, а основным моделируемым процессом является генерация сетевого трафика в сетевом диапазоне, охватывающим таблицу доступа. Для задачи верификации правил фильтрации из общей топологии выделяется расположение хостов и межсетевых экранов в сети.

Данная модель также включает в себя элементы, предназначенные для представления МЭ и алгоритмов его работы. МЭ моделируется как сетевое устройство, которое контролирует прохождение пакетов через сегменты сети на основе заданной политики фильтрации. Модель поведения МЭ выглядит следующим образом. Весь трафик сопоставляется с правилами доступа последовательно, пока какое-нибудь правило не будет применено.

Политика МЭ - это список правил фильтрации, которые определяют действия для пакетов, удовлетворяющих определенным условиям. Правила состоят из набора полей фильтрации, таких как тип протокола, IP-адрес отправителя, порт отправителя, IP-адрес получателя, порт получателя, а также действие, определяемое для пакета. Поля правила фильтрации представляют собой возможные значения полей сетевого пакета в реальном сетевом трафике. Каждое поле фильтрации может иметь одно значение или диапазон значений. Таким образом, основными компонентами МЭ,

подлежащими моделированию, являются сетевые идентификаторы, заданные наборы правил фильтрации, а также алгоритм обработки сетевого трафика. Заданные в модели ограничения при определении множества октетов и множества сетевых портов обусловлены стандартом TCP/IP для этих полей правила фильтрации.

Для того чтобы описать спецификацию, выражающую свойства моделируемой системы, определяется множество атомарных высказываний. Атомарные высказывания представляют собой присваивание переменным из множества V значений из множества D , которое называется доменом.

Домен D ^ используемый в модели, представляет собой фактические значения для всех типов множеств, описывающих модель компьютерной сети: 0 = {0,...,255} - множество октетов; Н = {0,...,65535} - множество значений приоритетов; А=ОхОхОхО — множество сетевых адресов; М, = IPv4,udp,tcp - множество сетевых протоколов, М2= {deny, accept} -множество привилегий, Р= {0, ...,65535} - множество сетевых портов; F = НхМххАхРхАхРхМ2 - множество правил фильтрации; W = MlxAxPxAxP — множество сетевых пакетов; U a F — множество используемых в модели правил фильтрации, определяющих политику фильтрации, Е с Ж - множество сетевых пакетов в модели, AF с 2<и'Е) -множество применений правил фильтрации.

Переменные моделируемой системы, которые характеризуют ее состояние, определяются так: и - правило фильтрации, р - сетевой пакет. Множество V = {(и,р)} является набором переменных, характеризующих

состояние моделируемой системы. Множество V содержит штрихованные переменные для каждой переменной из множества V и представляет собой значения переменных в следующем состоянии: V ={(и ,/>)}• Такое разделение введено для того, чтобы определять переходы в моделируемой системе. Переменные из множеств V и V принимают значения из конечного множества D .

Множество состояний в модели определяется следующим образом: S = ExUxAF, т.е. на каждом шаге система характеризуется сетевым пакетом, который обрабатывается межсетевым экраном, применяемым правилом межсетевого экрана, парой значений пакета и примененного к нему правила фильтрации.

Для построения системы переходов в модели Крипке выделены следующие виды возможных изменений в системе:

1. Для сетевого пакета р проверяется возможность применения правила и из множества U до тех пор, пока все правила фильтрации не будут проанализированы. Если правило можно применить к данному сетевому

пакету, то пара, состоящая из пакета и примененного правила (р,и), добавляется в массив пар, включающих пакет и правило фильтрации.

2. Сетевой пакет р обработан, и обрабатывается пакет р . К нему начинают применяться все правила фильтрации.

3. Анализируется пара, включающая сетевой пакет и примененное к нему правило (р, и). Если проанализирован весь набор примененных к одному пакету правил, то они удаляются.

Для описания системы переходов используются следующие обозначения: шах(м) - функция для определения достижения максимального значения для индекса правила фильтрации; apply(u,p) - функция для определения применимости правила фильтрации для текущего сетевого пакета; и0 -первое правило фильтрации,' - переход переменной в следующее состояние.

Отношение переходов выражается формулой: Щр,и,р ,и ) = и Ф шах(м) =>/?'= р а и = next (и) л(арр1у(и, р) => (р, и) е А) а и = шах =5>(рФ тах(р) =>/?'= new(p) ли = и0) л apply(u,p) е h

Функция, которая помечает каждое состояние множеством атомарных высказываний, истинных в этом состоянии определяется как

Задача верификации правил фильтрации МЭ на предмет аномалий фильтрации представляет собой проверку выполнимости формул fs,f ,fc,fr

(модель аномалий) на модели Крипке MN (модель компьютерной сети, защищенной МЭ).

В третьей главе рассматривается архитектура СВПФ, методика верификации, а также проводится оценка эффективности методики на основе реализации СВПФ.

Архитектура СВПФ (рис.1) предназначена для построения программной системы, реализующей методику верификации правил фильтрации методом "проверки на модели". Она должна обеспечить отсутствие аномалий в правилах фильтрации. Для решения этой задачи, архитектура СВПФ должна содержать необходимые компоненты, обеспечивающие полное покрытие всех возможных аномалий с точки зрения алгоритмов их поиска и алгоритмов их разрешения.

Провила фильтрации Описание сети

Нарушений свойств корректности (аномалии)

Правила без аномалий

Репозиторий

Аномалия филырзции

разрешенид^

Рис. 1. Архитектура системы верификации правил фильтрации

Архитектура состоит из семи компонентов. Опишем самые существенные из них. Компонент "Менеджер верификации" предназначен для общего управления процессом верификации. Компонент построения модели отвечает за создание модели компьютерной системы на основании описания компьютерной системы, защищенной МЭ, и набора правил фильтрации. Этот компонент также создает структуры обнаружения различных типов аномалий в верифицируемой модели. Компонент "Интерпретатор результатов" преобразует результаты верификации в представление, стандартизированное в СВПФ. Компонент стратегий разрешения аномалий либо применяет автоматические стратегии для разрешения обнаруженных аномалий, либо в интерактивном режиме взаимодействует с пользователем для корректировки политик вручную. Компонент верификации обеспечивает запуск и вычисление верифицируемой модели, а также настройку всех параметров верификации.

С учетом предложенной архитектуры разработана методика верификации правил фильтрации на основе метода "проверки на модели", которая показана на рис.2.

Действия оператора

Действия системы верификации

| Компоненты системы I верификации

4. Этап интерпретфдии результатов ^

і Интерпретация результатов---'

?—_

Отображение аномалий и стратегий

. J.

5. Этап разрешения аномалий

автоматических стратегии.... ■ ................оператора.....................

I Конец )

г ЦІ

ГіС

Загрузка из репозитория

Стратегии разрешения :

}■ -¡-І Компонент визуализации

І I --------------------------------------------

1} I

Правила фильтрации без аномалий

I

Рис. 2. Методика верификации правил фильтрации на основе метода "проверки на модели"

Основными входными данными в предлагаемой методике являются описания правил фильтрации политики на языке описания политики (ЯОП) и конфигурации компьютерной сети на языке описания системы (ЯОС), а также выявляемые аномалии фильтрации.

На этапе трансляции во внутренний формат оператор загружает входные данные: описание компьютерной сети, защищенной МЭ, а также

правила фильтрации. Далее на этапе построения модели строится общая верифицируемая модель (ОВМ) правил фильтрации, представленная в виде конечного автомата. ОВМ включает в себя модели компьютерной системы, МЭ и аномалий, и инициализируется входными данными во внутреннем формате. На следующем этапе вычисления модели оператор запускает процесс верификации. ОВМ верифицируется специальными программными средствами, реализующими метод "проверки на модели". В процессе верификации выявляются все некорректные состояния системы, которые были заданы в спецификации - аномалии в правилах фильтрации. На этапе интерпретации результатов полученные результаты верификации преобразуются с помощью компонента интерпретации, а затем, с помощью компонента пользовательского интерфейса, представляются оператору. Если были обнаружены аномалии, то пользователь получает адреса межсетевых экранов и правила, приводящие к возникновению аномалии, а также тип аномалии и возможные стратегии разрешения. На завершающем этапе разрешения аномалий оператор выбирает, к каким аномалиям применить автоматическую стратегию разрешения, а какие потребуется корректировать вручную. После корректировки процесс верификации запускается снова, если это необходимо. Выходными данными для данной методики являются правила фильтрации без аномалий.

Для проведения экспериментов и проверки выполнимости поставленных требований к данной методике, на основе вышеописанной архитектуры была сделана программная реализация системы верификации правил фильтрации (СВПФ), написанная на языке Java версии 1.6.29. В качестве компонента верификации использована программная система SPIN версии 6.2. Репозиторий, где хранятся аномалии фильтрации и стратегии разрешения, построен на основе системы управления базами данных MySQL версии 5.6.

Выполнено множество экспериментов по верификации правил фильтрации и разрешения обнаруженных аномалий. Эксперименты проводились на наборах правил, состоящих из 5, 10, 15, 30, 50 и 100 правил. В эти правила были искусственно введены аномалии фильтрации различного типа в количестве от 0 до 20 штук. На основе этих экспериментов рассчитаны показатели целевой функции, а также показатели эффективности (своевременности, ресурсопотребления и обоснованности). Требования к методике были заданы на основе анализа показателей сходных систем верификации, а также с учетом того, что система верификации правил фильтрации не относится к классу систем реального времени.

Для определения показателей своевременности использован метод сетевого планирования. Время реализации методики складывается из времен выполнения ее этапов. Оценка своевременности реализации методики верификации проводилась с помощью СВПФ. Продолжительность описанных этапов зависит от входных параметров. По результатам этих экспериментов можно сделать вывод, что наибольшее влияние на

длительность этапа верификации будет оказывать количество хостов в компьютерной сети и количество межсетевых экранов, что определяет размеры верифицируемых таблиц доступа, тогда как количество аномалий фильтрации в правилах практически не влияет на время верификации.

Временные зависимости длительности верификации правил фильтрации от количества правил фильтрации при учете количества аномалий представлены на рис. 3.

Согласно полученным данным, время верификации растет экспоненциально в зависимости от числа правил. Проведенные эксперименты показали, что предлагаемый подход позволяет выявлять все аномалии правил фильтрации межсетевых экранов, но может эффективно использоваться до определенного количества правил, т.е. применим для компьютерных сетей малых и средних размеров.

Вероятность своевременного выполнения методики верификации для компьютерной сети, защищенной МЭ, с количеством правил до 100 штук при Тдо" = 7 минуты Рсв г < Тдоп составляет 0.9995, что соответствует

предъявляемым требованиям к своевременности.

Показателями обоснованности выступают количество используемых параметров, количество типов выявляемых аномалий, количество возможных стратегий разрешения, а также качество выявления аномалий. Для задания требований к показателям обоснованности был проведен анализ существующих систем, сходных по функциональным характеристикам, но не было найдено систем, являющихся полными аналогами СВПФ. В основном системы верификации статически анализируют конфигурацию сетевых устройств, либо охватывают неполную классификацию аномалий фильтрации. Только одна система (АРУБР) реализует возможность применения стратегий разрешения аномалий. Так как данные программные

системы не выложены в открытом доступе, то их характеристики получены из публикаций, описывающих работу этих систем. Качество выявления аномалий в политике фильтрации определяется вычислением числа ошибок первого рода, числа ошибок второго рода, полнотой, точностью и аккуратностью.

Эксперименты показали, что СВПФ не выдает ложных срабатываний при определении аномалий, достигая максимального показателя качества выявления аномалий фильтрации, как и система АРУБР, но при этом показатель используемых параметров, оценивающий функциональные способность системы, выше на 30% среди рассматриваемых систем, а также показатель возможных стратегий разрешения аномалий, оценивающий эффективность формирования непротиворечивой политики фильтрации, выше на 20%, а показатель количества выявляемых аномалий равен максимальному, что соответствует заданным требования.

Ресурсопотребление характеризует номенклатуру и количество необходимых программных и аппаратных средств, объемы необходимых информационных массивов, кадровые ресурсы и другие ресурсы, затрачиваемые на реализацию процесса верификации правил фильтрации политики безопасности методом "проверки на модели". Проведенные эксперименты показали, что ресурсопотребление соответствует предъявляемым требованиям.

На основе проведенных экспериментов был вычислен показатель противоречивости политики безопасности (целевая функция) 1псоги;1$1епсу1пс1ех(<р). Этот показатель для всех экспериментов равен 0, так

как все возможные аномалии в политике распознаются и разрешаются. Для сходных систем верификации, с которыми выполнялось сравнение, рассчитать показатель противоречивости политики фильтрации невозможно, так как нет возможности провести эксперименты с реальными программными системами. Однако можно сделать вывод, что целевая функция, предлагаемая в данной работе, для этих систем никогда не будет минимальна, так как она зависит от количества выявляемых аномалий, а также предлагаемых стратегий разрешения аномалий, а СВПФ имеет самые высокие показатели этих параметров. В других системах рассматривается меньшее количество аномалий и стратегий их разрешения (кроме системы АР\ТР, которая не предусматривает применение стратегий разрешения), что приводит к тому, что в полученной политике фильтрации останутся не выявленные или неразрешенные аномалии.

Таким образом, цель методики -минимизировать целевую функцию — достигнута при выполнении требований к своевременности, ресурсопотреблению и обоснованности.

ЗАКЛЮЧЕНИЕ

Данная работа предлагает модельно-методический аппарат для верификации правил фильтрации политики безопасности методом проверки на модели.

Основными научными результатами, выносимыми на защиту, являются:

1. Разработанная модель аномалий фильтрации и алгоритмы выявления и разрешения аномалий методом "проверки на модели". Для построения этих моделей применялась линейная темпоральная логика, лежащая в основе метода "проверки на модели".

2. Разработанная модель компьютерной сети, защищенной МЭ, в которой определены модели взаимодействия сетевых устройств компьютерной сети сМЭ.

3. Разработанная архитектура системы верификации правил фильтрации политики безопасности на основе метода «проверки на модели». Она состоит из следующих компонентов: менеджера верификации, транслятора модульного интерфейса, компонента верификации, компонента построения модели, интерпретатора результатов, компонента стратегий разрешения аномалий и компонента пользовательского интерфейса.

4. Разработанная методика верификации правил фильтрации политики безопасности на основе метода «проверки на модели». Представленная методика позволяет повысить защищенность компьютерной сети за счет снижения непротиворечивости политики фильтрации в компьютерных сетях, защищенных МЭ, с большим количеством сетевых сегментов.

С помощью представленной архитектуры и методики реализована система верификации правил фильтрации политики безопасности на основе метода «проверки на модели». Данная система использовалась при проведении экспериментов на основе применения предложенных моделей и методики, что позволило провести анализ данных моделей и оценить эффективность работы методики.

Апробация полученных результатов проводилась на 12 научно-технических конференциях. Основные результаты, полученные автором, опубликованы в 26 научных работах.

ОСНОВНЫЕ ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

Публикации в рецензируемых журналах из перечня ВАК:

Полубелова, О.В. Архитектура и программная реализация. системы верификации правил фильтрации / О.В. Полубелова // Труды СПИИРАН. СПб: Наука. - 2013. - Вып.З (26).

Полубелова, О.В., Котенко, И.В. Верификация правил фильтрации с временными характеристиками методом "проверки на модели" /

О.В. Полубелова, И.В. Котенко // Труды СПИИРАН. - СПб: Наука. - 2012. -Вып.З (22).-С.113-138.

Черватюк, О.В., Котенко, И.В. Верификация правил фильтрации политики безопасности методом "проверки на модели" / О.В. Полубелова // Журнал "Приборостроение". - 2008. - Т.51, № 12. - С.44-49.

Котенко, И.В., Тишков, А.В., Черватюк, О.В., Лакомов, Д.П. Поиск конфликтов в политиках безопасности / И.В. Котенко, А.В. Тишков, О.В. Черватюк, Д.П. Лакомов // Изв. вузов. Приборостроение. - 2006. - Т.49, № 11. -С.45-49.

Котенко, И.В., Полубелова, О.В., Чечулин, А.А. Построение модели данных для системы моделирования сетевых атак на основе онтологического подхода / И.В. Котенко, О.В. Полубелова, А.А. Чечулин// Труды СПИИРАН. СПб.: Наука. - 2013. - Вып.З (26).

Котенко, И.В., Саеико, И.Б., Полубелова, О.В. Перспективные системы хранения данных для мониторинга и управления безопасностью информации / И.В. Котенко, О.В. Полубелова, И.Б. Саенко // Труды СПИИРАН. СПб.: Наука. - 2013. - Вып.2 (25). - С. 113-134.

В других изданиях:

Полубелова, О.В., Саенко, И.Б., Котенко, И.В. Методы представления данных и логического вывода для управления информацией и событиями безопасности / И.В. Котенко, О.В. Полубелова, И.Б. Саенко // Часть 5-й Российской мультиконференции по проблемам управления (МКПУ-2012) -конференция "Информационные технологии в управлении" (ИТУ-2012). 0911 октября 2012 г. Материалы конференции. СПб. - 2012. - С.723-728.

Kotenko, I., Tishkov, A., Chervatuk, О., Sidelnikova, Е. Security Policy Verification Tool for Geographical Information Systems/ I. Kotenko, A. Tishkov, O. Chervatuk, E. Sidelnikova // Information Fusion and Geographical Information Systems. Lecture Notes in Geoinformation and Cartography. Springer. Popovich, Vasily V.; Schrenk, Manfred; Korolenko, Kyrill V. (Eds.). - 2007. - P. 128-146.

Kotenko, I., Chervatuk, O., Sidelnikova, E., Tishkov, A. Multi-module Security Policy Checker / I. Kotenko, O. Chervatuk, E. Sidelnikova, A. Tishkov // Eighth IEEE International Workshop on Policies for Distributed Systems and Networks. - 2007. - C.227.

Котенко, И.В., Тишков, A.B., Черватюк, O.B., Резник, С.А., Сидельникова, Е.В. Система верификации политики безопасности компьютерной сети / И.В. Котенко, А.В. Тишков, О.В. Черватюк, С.А. Резник, Е.В. Сидельникова // Журнал "Вестник компьютерных и информационных технологий". - 2007. - № 11.- С.48-56.

Подписано в печать 21.05.2013г. Формат 60x84 1/16. Бумага офсетная. Печать офсетная. Усл. печ. л. 1,1. Тираж 100 экз. Заказ № 3106.

Отпечатано в ООО «Издательство "JIEMA"» 199004, Россия, Санкт-Петербург, В.О., Средний пр., д. 24 тел.: 323-30-50, тел./факс: 323-67-74 e-mail: izd_lema@mail.ru http://www.lemaprint.ru

Федеральное государственное бюджетное учреждение науки

Санкт-Петербургский институт информатики и автоматизации Российской академии наук

На правах рукописи ГА

04201355136

ПОЛУБЕЛОВА Ольга Витальевна

ВЕРИФИКАЦИЯ ПРАВИЛ ФИЛЬТРАЦИИ МЕЖСЕТЕВЫХ ЭКРАНОВ НА ОСНОВЕ ПРИМЕНЕНИЯ МЕТОДА «ПРОВЕРКА НА

МОДЕЛИ»

Специальность:

05.13.19 — Методы и системы защиты информации, информационная безопасность

Диссертация на соискание ученой степени кандидата технических наук

Научный руководитель: д.т.н., проф. Котенко И. В.

Санкт-Петербург - 2013

Содержание

Введение.....................................................................................................................................4

Глава 1 Системный анализ задачи верификации правил фильтрации межсетевых экранов для защищенных систем, основанных на политиках безопасности, методом "проверки на модели"..........................................................17

1.1 Роль и место верификации правил фильтрации в задаче управления сложными системами на основе политики безопасности......................................................................17

1.2 Анализ аномалий фильтрации и способов их разрешения...........................................20

1.3 Анализ методов и средств верификации политики безопасности...............................23

1.4 Требования к системам верификации правил фильтрации методом «проверки на модели»....................................................................................................................................30

1.5 Постановка задачи исследования....................................................................................33

Выводы по 1 главе...................................................................................................................38

Глава 2 Модели и алгоритмы верификации правил фильтрации на основе метода "проверки на модели"..........................................................................................41

2.1 Модель аномалий фильтрации.........................................................................................43

2.2 Алгоритмы выявления и разрешения аномалий методом "проверки на модели"......46

2.3 Модель компьютерной сети, защищенной межсетевыми экранами............................51

Выводы по 2 главе...................................................................................................................56

Глава 3 Методика верификации правил фильтрации межсетевых экранов методом "проверки на модели" и оценка ее эффективности..............................58

3.1 Архитектура системы верификации правил фильтрации.............................................58

3.2 Методика верификации правил фильтрации межсетевых экранов методом "проверки на модели"................................................................................................................................61

3.3 Реализация системы верификации правил фильтрации и оценка эффективности методики...................................................................................................................................64

3.4 Предложения по практическому использованию полученной методики для анализа защищенности компьютерной сети.......................................................................................90

3.4.1 Верификация таблицы доступа межсетевого экрана..............................................90

3.4.2 Разрешение аномалий................................................................................................91

Выводы по главе 3...................................................................................................................92

Заключение...............................................................................................................................95

Список литературы и электронных ресурсов.............................................................98

Приложение 1. Глоссарий.................................................................................................113

Приложение 2. Копии документов, подтверждающих внедрение.....................118

Приложение 3. Пример политики фильтрации с включенными аномалиями фильтрации различного типа, используемый при проведении

экспериментов......................................................................................................................123

Приложение 4. Пример описания верифицируемой системы, а также

политики фильтрации на внутреннем языке............................................................125

Networklsdl.xml...................................................................................................................125

Filteringspl.xml.....................................................................................................................129

Введение

Системы защиты информации (СЗИ) в компьютерных сетях, основанные на политиках безопасности, не теряют своей популярности благодаря гибкости в управлении и удобству администрирования. Под политикой безопасности понимается совокупность документированных правил, процедур, практических приемов или руководящих принципов в области безопасности информации, которыми руководствуется организация в своей деятельности. Выделяются следующие категории политик безопасности: авторизация, аутентификация, фильтрация сетевого трафика, IPSec и операционные правила.

Политика фильтрации позволяет администратору сети централизованно применять сетевую политику безопасности в выделенном сегменте IP-сети. К программно-аппаратным средствам, обеспечивающим решение этой задачи, относятся межсетевые экраны (МЭ). Настройка МЭ дает возможность разрешить или запретить пользователям как доступ из внешней сети к соответствующим службам хостов или к хостам, находящихся в защищаемом сегменте, так и доступ пользователей из внутренней сети к соответствующим ресурсам внешней сети. МЭ работают на основе политик фильтрации, представленных в виде множества правил фильтрации. Политика фильтрации формируется специалистами, знающими особенности защищаемой сети и используемых МЭ, на основе общей политики безопасности компании, закрепленной в регламентирующих документах. Однако эта задача является сложной и подверженной ошибкам из-за важности учета различных зависимостей правил, а также необходимости проверки согласованности новых правил со всей политикой. Эта сложность увеличивается по мере роста размера сети. Например, согласно статистическим исследованиям международной ассоциации компьютерной безопасности (International

Computer Security Association, ICSA), до 70% всех МЭ уязвимы из-за неправильной конфигурации и настройки. Определенную долю в этих ошибках составляют и противоречия в правилах фильтрации МЭ. Так например, в работе известного специалиста по МЭ Авишай Вулома, которое посвящено исследованию множества межсетевых экранов в локальных сетях многих предприятий, показано, что все МЭ были уязвимы и имели различные ошибки конфигурирования. Также исследованиями проблем конфигурирования политики фильтрации занимаются многие ученые из разных стран: Ehab S. Al-Shaer [47-49], А. Wool [103, 104], R. Oliveira [108, 109], J. G. Alfaro [53, 54], R. Marmorstein [100-102], M. G. Gouda [74, 75], E. Lupu [55], P. Eronen [72], L. A. Lymberopoulos [97], T. Bourdier [60], S. Hinrichs [78], M. Johnson [83]. В данной работе используется понятие аномалии фильтрации, определяемое как противоречие между двумя правилами фильтрации, при котором одно или более правил политики фильтрации никогда не будут активированы. Такой термин широко используется в работах многих ученых и специалистов из разных стран, занимающихся проблематикой настройки правил фильтрации.

Таким образом, для успешного развертывания СЗИ и поддержания ее функционирования требуется проводить регулярный анализ политики фильтрации. Он позволяет выявить и разрешить различные конфликты и аномалии в политиках, которые могут привести к серьезным нарушениям свойств безопасности и сетевым уязвимостям, таким как блокирование легитимного трафика, разрешение нежелательного трафика, а также передача данных по сети в незашифрованном виде. Анализ правил вручную значительно затрудняется с ростом размера компьютерной сети, а также не гарантирует отсутствие ошибок.

Существуют различные подходы автоматизации процесса верификации правил фильтрации, например, посредством систем доказательства теорем или исчисления событий. Однако большинство из них находятся в стадии исследования. Коммерческие решения, как правило, ориентированы на какие

либо специфические программно-аппаратные средства и не обладают достаточной универсальностью.

В данной работе предлагается метод "проверки на модели" (Model checking) для решения этой задачи [51, 56]. Согласно определению, Model checking —это метод проверки того, что на данной формальной модели системы заданная логическая формула выполняется (принимает истинное значение). Для верификации этим методом, компьютерная сеть, защищенная МЭ, представляется упрощенной моделью ее вычислений - системой переходов с конечным числом состояний, некоторой разновидностью конечного автомата. Требуемые свойства этой модели (т.е. отсутствие аномалий фильтрации) выражаются точно и недвусмысленно формулами темпоральной логики. Проверка модели сводится к исчерпывающему анализу всего пространства состояний модели системы.

К недостаткам метода относится вычислительная сложность подхода, но с ростом производительности компьютерных систем, этот недостаток нивелируется. Преимуществами данного метода являются его высокий уровень абстракции при представлении данных, что позволяет построить адекватную, но упрощенную модель сложной системы компьютерной сети, выделяя лишь функции, наиболее важные для верификации правил фильтрации. Также метод "проверки на модели" позволяет исследовать динамическое поведение системы, не включаясь в процесс функционирования сети. Кроме того метод разрабатывался на базе строгих формальных теорий, в отличие от различных других методов тестирования и верификации.

Применение метода "проверки на модели" представляется целесообразным для эффективного решения задачи верификации правил фильтрации с учетом того, что она не относится к категории систем реального времени.

Цслыо исследования является повышение защищенности компьютерной сети за счет использования разработанных моделей, алгоритмов и методики формальной верификации правил фильтрации.

Для достижения данной цели в диссертационной работе поставлены и решены следующие задачи:

1. Анализ способов построения и функционирования межсетевых экранов, возможных аномалий фильтрации и задачи верификации правил фильтрации межсетевых экранов.

2. Анализ методов верификации СЗИ, основанных на политиках безопасности, в том числе метода "проверки на модели".

3. Разработка модели аномалий фильтрации, алгоритмов выявления и стратегий разрешения этих аномалий методом "проверки на модели".

4. Разработка модели компьютерной системы и межсетевых экранов для реализации метода "проверки на модели".

5. Построение архитектуры системы верификации правил фильтрации (СВПФ) межсетевых экранов методом "проверки на модели".

6. Разработка методики верификации правил фильтрации межсетевых экранов методом "проверки на модели" на основе представленных моделей и архитектуры системы верификации.

7. Реализация СВПФ, проведение экспериментов и оценка эффективности методики верификации.

Объектом исследования являются правила фильтрации межсетевых экранов и аномалии в них, а также процессы их обнаружения и разрешения.

Предметом исследования являются методики, модели и алгоритмы верификации правил фильтрации, основанные на методе "проверки на модели".

Научная задача работы - разработка научно-методического аппарата (моделей, алгоритмов и методики) верификации правил фильтрации межсетевых экранов для обнаружения и разрешения аномалий на основе метода "проверки на модели".

Методологическую и теоретическую основу исследования составили научные труды отечественных и зарубежных авторов в областях верификации политик безопасности, моделирования компьютерных систем, защищенных межсетевыми экранами, компьютерной безопасности.

Методы исследования, использованные в диссертации, относятся к методам системного анализа, теоретико-множественного представления, объектно-ориентированного программирования, моделирования, логико-математическим, а также методам сравнения и аналогий.

Основными результатами, выносимыми на защиту, являются:

1. Модель аномалий фильтрации и алгоритмы выявления и разрешения аномалий методом "проверки на модели".

2. Модель компьютерной сети, защищенной межсетевым экраном.

3. Методика верификации правил фильтрации межсетевых экранов на основе метода "проверки на модели".

4. Архитектура и программная реализация системы верификации правил фильтрации межсетевых экранов на основе метода "проверки на модели".

Научная новизна исследования заключается в следующем:

1. Отличительной характеристикой модели аномалий фильтрации является учет основных видов аномалий фильтрации (затенение, обобщение, корреляция и избыточность), а также возможность использования для формальных методов верификации за счет представления на языке линейной темпоральной логики (Linear Temporal Logic, LTL) [98, 99]. Алгоритмы выявления и разрешения аномалий отличаются от существующих спецификой метода "проверки на модели", а также возможностью применять различные стратегии разрешения, тогда как в подобных системах реализовано только выявление аномалий.

2. Отличительной особенностью модели компьютерной сети, защищенной межсетевым экраном, является то, что помимо стандартного набора полей, характерных для правил фильтрации, добавляются поля,

определяющие временной интервал, в течение которого действует правило. В модели выделены лишь аспекты, касающиеся генерации сетевого трафика и взаимодействия с межсетевыми экранами, что значительно упрощает модель сети и позволяет повысить эффективность верификации правил фильтрации.

3. Основным отличием данной методики верификации является применение метода "проверки на модели" для верификации политики фильтрации. В отличие от известных, предложенная методика учитывает специфику анализа сетевых устройств, тогда как в существующих работах по верификации политик безопасности предлагаются решения главным образом для политик авторизации. Основные этапы методики автоматизированы за счет использования разработанных моделей компьютерной сети, аномалий фильтрации и алгоритмов выявления и разрешения аномалий.

4. Отличием архитектуры и программной реализации системы верификации правил фильтрации политики безопасности на основе метода «проверки на модели» является наличие в ее составе предложенных методо-ориентированных моделей компьютерной системы, защищенной межсетевым экраном, а также алгоритмов выявления и разрешения аномалий.

Обоснованность и достоверность представленных в диссертационной работе научных положений обеспечивается проведением тщательного анализа состояния научных исследований в данной области, подтверждается согласованностью теоретических результатов с экспериментальными. Эксперименты проводились на программном прототипе. Также проводилась апробация основных теоретических положений в печатных трудах и докладах на научных конференциях.

Теоретическая н практическая значимость исследования. Разработанные модели и алгоритмы выявления и разрешения аномалий, а также методика верификации могут быть использованы для решения задач в области анализа сетевого трафика. В частности, они позволят: верифицировать политики фильтрации в существующих компьютерных сетях; исследовать корректность применения политики фильтрации в

компьютерной сети, защищенной межсетевым экраном; повысить эффективность разработки новых политик и редактирования уже используемых, особенно для больших компьютерных сетей, состоящих из множества сегментов; вырабатывать стратегии разрешения различных аномалий фильтрации на основе построенных в процессе верификации контрпримеров (описаний некорректных состояний).

Реализация результатов работы. Результаты, полученные в диссертационной работе, были использованы в рамках следующих научно-исследовательских работ: проект Шестой рамочной программы (FP6) Европейского Сообщества "Средства и модели защиты информации, основанные на политике безопасности (POSITIF)", контракт IST-2002-002314, 2003-2007 гг., проект Минобрнауки России «Исследование и разработка методов, моделей и алгоритмов интеллектуализации сервисов защиты информации в критически важных инфраструктурах», государственный контракт № 11.519.11.4008, 2011-2013 гг.; проект Седьмой рамочной программы (FP7) Европейского Сообщества «Управление информацией и событиями безопасности в инфраструктурах услуг (MASSIF)», контракт № 257475, 2010-2013 гг.; «Математические модели и методы комплексной защиты от сетевых атак и вредоносного ПО в компьютерных сетях и системах, основывающиеся на гибридном многоагентном моделировании компьютерного противоборства, верифицированных адаптивных политиках безопасности и проактивном мониторинге на базе интеллектуального анализа данных», грант РФФИ № 10-01-00826-а, 2010-2012 гг.; проект по программе фундаментальных исследований ОНИТ РАН «Архитектура, системные решения, программное обеспечение, стандартизация и информационная безопасность информационно-вычислительных комплексов новых поколений», 2009-2011 гг., в учебном процессе кафедры автоматизированных систем обработки информации и управления Санкт-Петербургского государственного электротехнического университета «ЛЭТИ» им. В.И. Ульянова (Ленина) при

и

подготовке специалистов по специальности "Компьютерная