Верификация правил фильтрации межсетевых экранов на основе применения метода "проверка на модели" тема диссертации и автореферата по ВАК РФ 05.13.19, кандидат технических наук Полубелова, Ольга Витальевна

• Полубелова, Ольга Витальевна
• кандидат технических наук
• 2013

Оглавление диссертации кандидат технических наук Полубелова, Ольга Витальевна

Содержание

Введение

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Заключение

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

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

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

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

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

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

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

Networklsdl.xml

Filteringspl.xml

Введение диссертации (часть автореферата) на тему «Верификация правил фильтрации межсетевых экранов на основе применения метода "проверка на модели"»

Введение

Системы защиты информации (СЗИ) в компьютерных сетях, основанные на политиках безопасности, не теряют своей популярности благодаря гибкости в управлении и удобству администрирования. Под политикой безопасности понимается совокупность документированных правил, процедур, практических приемов или руководящих принципов в области безопасности информации, которыми руководствуется организация в своей деятельности. Выделяются следующие категории политик безопасности: авторизация, аутентификация, фильтрация сетевого трафика, 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 гг., в учебном процессе кафедры автоматизированных систем обработки информации и управления Санкт-Петербургского государственного электротехнического университета «ЛЭТИ» им. В.И. Ульянова (Ленина) при

и

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

Апробация результатов работы. Основные положения и результаты диссертационной работы докладывались на следующих научных конференциях: 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» («РИ-2010»); Девятая общероссийская научная конференция «Математика и безопасность информационных технологий» (МаБИТ-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) методики верификации, минимизирующей заданную целевую функцию при выполнении требований к своевременности, обоснованности и ресурсопотреблению процесса верификации.

Методика верификации правил фильтрации МЭ задается следующим образом:

Где G - множество шагов по выполнению этапов верификации правил фильтрации политики безопасности и алгоритмов обнаружения и разрешения аномалий фильтрации на основе метода "проверки на модели", а М- это множество моделей, M=<MS,MA>, гдeMv- модель компьютерной сети, защищенной МЭ, МА - модель аномалий фильтрации, которые интегрированы в методику, позволяющую верифицировать правила фильтрации МЭ и применять стратегии разрешения ко всем обнаруженным аномалиям.

Целью разработки методики является минимизация целевой функции: InconsistencyIndex/p {ф) —»min (2)

при соблюдении требований к остальным показателям эффективности верификации правил фильтрации: своевременности, ресурсопотреблению и обоснованности, где функция InconsistencylndexJ^q)) показывает противоречивость политики фильтрации МЭ, методика <реТ, где

представляет собой множество всех методик верификации, jpeFilteringPolicy, где РШегищРоИсу - множество всех политик

Р=< G,M>

(О

T = {f'-FA/P->RS}

(3)

фильтрации, ДО- набор подходящих стратегий разрешения аномалий фильтрации, направленных на устранение противоречий. ДО с ResolvingStrategy, где Ке8оЬищ8№Ше£у- множество всех возможных стратегий разрешения аномалий. РА/Г, где - аномалии фильтрации,

выявленные в некоторой политике фильтрации /р, ЕШегищАпота1у -множество всех аномалий фильтрации, ГА/г с ЕШег^АпотЫу.

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

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

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

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

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

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

На основе проведенных экспериментов был вычислен показатель противоречивости политики безопасности (целевая функция) Inconsistency IndexJp{(p). Этот показатель для всех экспериментов равен 0, так как все возможные аномалии в политике распознаются и разрешаются. Для сходных систем верификации, с которыми выполнялось сравнение, рассчитать показатель противоречивости политики фильтрации невозможно,

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

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

Заключение диссертации по теме «Методы и системы защиты информации, информационная безопасность», Полубелова, Ольга Витальевна

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

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

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

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

4. Проведенные эксперименты показали эффективность работы системы верификации правил фильтрации. Все виды аномалий обнаруживаются. При этом время работы составляет несколько минут на наборах по 50 правил. Это характерно для компьютерных систем средних размеров.

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

Заключение

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

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

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

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

3. Разработана архитектура системы верификации правил фильтрации политики безопасности на основе метода «проверки на модели».

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

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

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

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

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

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

Список литературы диссертационного исследования кандидат технических наук Полубелова, Ольга Витальевна, 2013 год

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

1. Анфилатов В. С. Системный анализ в управлении / В. С. Анфилатов, А.

A. Емельянов, А. А. Кукушкин ; ред. А. А. Емельянова. - Москва : Финансы и статистика, 2005. - 361 с.

2. Астахов А. Анализ защищенности корпоративных автоматизированных систем [Электронный ресурс] / А. Астахов. — Электрон, текстовые дан. и граф. дан.— [Б. м. : б. и.]. — Режим доступа: http: // www.jetinfo.ru / 2002/7/ 1 /articleL7.2002.html (по состоянию на 01.01.2006).

3. Боговик A.B. Теория управления в системах военного назначения. Учебник. A.B. Боговик, С.С.Загорулько, И.С.Ковалев, И.В.Котенко,

B.В.Масановец / Под редакцией И.В.Котенко. М.: МО РФ, 2001. 312 с.

4. ГОСТ 24.701-86. Эффективность автоматизированных систем управления. Основные положения. Введ. 1987-07-01. М.: Изд-во стандартов, 1986. 11 с.

5. ГОСТ Р 51904-2002. Программное обеспечение встроенных систем. Общие требования к разработке и документированию.

6. ГОСТ Р 50922-96. Защита информации. Основные термины и определения. Введ. 1997-07-01. М.: Изд-во стандартов, 1996. 11 с.

7. ГОСТ Р ИСО 9000 «Системы менеджмента качества. Основные положения и словарь. Введен 15 августа 2001 г. № 332-ст. М.: Изд-во стандартов, 2001.

8. Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем // СПб.: БХВ, 2009. 560 с.

9. Карпов Е.А. Основы теории управления в системах военного назначения. Часть I. Учебное пособие. Е.А. Карпов, И.В.Котенко, А.В.Боговик, И.С.Ковалев, А.Н.Забело, С.С.Загорулько, В.В.Олейник / Под редакцией А.Ю.Рунеева и И.В.Котенко. СПб.: ВУС, 2000. 192 с.

10. Вигерс К. И.: Разработка требований к программному обеспечению — Русская Редакция, 2004, ISBN 5-7502-0240-2.

11. Карпов Е.А. Основы теории управления в системах военного назначения. Часть II. Учебное пособие. Е.А.Карпов, И.В.Котенко, А.В.Боговик, И.С.Ковалев, А.Н.Забело, С.С.Загорулько, В.В.Олейник / Под редакцией А.Ю.Рунеева и И.В.Котенко. СПб.: ВУС, 2000. 200 с.

12. Котенко И.В. Теория и практика построения автоматизированных систем информационной и вычислительной поддержки процессов планирования связи на основе новых информационных технологий. Монография. СПб.: ВАС, 1998. 404 с.

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

14. Котенко И.В., Саенко И.Б., Полубелова О.В., Чечулин A.A. Технологии управления информацией и событиями безопасности для защиты компьютерных сетей // Проблемы информационной безопасности. Компьютерные системы. № 2, 2012. С. 57-68.

15. Котенко И.В., Саенко И.Б., Полубелова О.В., Чечулин A.A. Применение технологии управления информацией и событиями безопасности для защиты информации в критически важных инфраструктурах // Труды СПИИРАН. Вып.1 (20). СПб.: Наука, 2012. С. 27-56.

16. Котенко И.В., ТишковА.В., Сидельникова Е.В., Черватюк О.В. Проверка правил политики безопасности для корпоративных компьютерных сетей // Защита информации. Инсайд, № 5, 2007. С.46-49; № 6, 2007. С.52-59.

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

18. Котенко И.В., ТишковА.В., Черватюк О.В., Резник С. А., Сидельникова Е.В. Система верификации политики безопасности

компьютерной сети // Вестник компьютерных и информационных технологий, № 11, 2007. С.48-56.

19. Котенко И.В., Юсупов P.M. Перспективные направления исследований в области компьютерной безопасности // Защита информации. Инсайд, № 2, 2006. С.46-57.

20. Миронов A.M. Математическая теория программных систем. http://intsys.msu.ru/staff/mironov/

21. Национальный стандарт РФ «Защита информации. Основные термины и определения» (ГОСТ Р 50922-2006).

22. Новиков Ф. А. Дискретная математика для программистов: Учебное издание для вузов. 3-е изд. П.: «Питер», 2008.

23. Основы сетевого планирования и управления в физической культуре и спорте, http:// books.ifmo.ru/ book/ pdf /51.pdf

24. Основы защиты информации / В. А. Герасименко, А. А. Малюк. М.: МИФИ, 1997. 539 с.

25. Официальное руководство по iptables (Iptables Tutorial 1.1.19) Электронный ресурс. / Режим доступа: http://www.opennet.ru/docs/RUS/iptables/ свободный. — Загл. с экрана.

26. Перечень российских рецензируемых научных журналов, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученых степеней доктора и кандидата наук, (редакция 17.06.2011 г.). http://vak.ed.gov.ru/ru/ help desk/ list/.

27. Полубелова O.B. Верификация правил фильтрации политики безопасности методом «проверки на модели» // Методы и технические средства обеспечения безопасности информации. Материалы XX Общероссийской научно-технической конференции. 27 июня - 1 июля 2011 года. Санкт-Петербург. Издательство Политехнического университета. 2011. С.87-88.

28. Полубелова О.В., Котенко И.В. Верификация правил фильтрации с временными характеристиками методом "проверки на модели" // Труды СПИИРАН. Вып.З (22). СПб.: Наука, 2012. С.113-138.

29. Полубелова О.В., Котенко И. В., Саенко И.Б., Чечулин A.A. Применение онтологического подхода и логического вывода для управления информацией и событиями безопасности // Системы высокой доступности, № 2, 2012. С. 100-108.

30. Полубелова О.В. Применение онтологического подхода и логического вывода для управления информацией и событиями безопасности // Четырнадцатая Международная конференция "РусКрипто'2012". Московская область, г.Солнечногорск, 28-30 марта 2012 г. http://www.ruscrypto.ru/

31. Полубелова О.В., Котенко И.В., Саенко И.Б. Онтологический подход к построению интеллектуальных сервисов хранения и обработки событий безопасности // Труды Конгресса по интеллектуальным системам и информационным технологиям «IS&IT' 12». Научное издание в 4-х томах. М.: Физматлит, 2012. Т. 2. С.394-399.

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

33. Полубелова О.В. Применение линейной темпоральной логики для верификации правил фильтрации политики безопасности методом «проверки на модели» // XIII Санкт-Петербургская Международная Конференция "Региональная информатика-2012" ("РИ-2012"). Материалы конференции. СПб., 2012. С. 121.

34. [правил присоединения ведомственных] Постановление Правительства РФ «Об утверждении правил присоединения ведомственных и

выделенных сетей электросвязи к сети электросвязи общего пользования» от 19.10.96 №1254.

35. Российская Федерация. Законы. Закон Российской Федерации «О безопасности». Федеральный Закон «О федеральной службе безопасности» Федер. закон: в ред. от 24 декабря 1993 г. №2288 и от 30 декабря 1999 г. №226-ФЗ. М.: Ось-89, 2005. 48 с. ISBN 5-98534-290-5.

36. Российская Федерация. Законы. Закон Российской Федерации «Об участии в международном информационном обмене» [Текст] : [федер. закон : от 04.07.96 №85-ФЗ]. — [Б. м. : б. и.].

37. Руководящий документ Гостехкомиссии России «Безопасность информационных технологий. Концепция оценки соответствия автоматизированных систем требованиям безопасности информации» (проект, первая редакция) [Электронный документ] / Электрон, текстовые дан. и граф. дан.— [Б. м. : б. и.]. — Режим доступа: http: //www.fstec.ru /_Нсеп / 015.pdf (по состоянию на 01.01.2006).

38. Руководящий документ Гостехкомиссии России «Средства вычислительной техники. Межсетевые экраны. Защита от несанкционированного доступа. Показатели защищенности от несанкционированного доступа к информации» [Текст]. — М.: ГТК РФ,

1997. — 18 с.

39. Саенко И.Б., Котенко И.В., Полубелова О.В. Применение онтологического подхода для построения модели уязвимостей на основе стандарта SCAP // Методы и технические средства обеспечения безопасности информации. Материалы XXI Общероссийской научно-технической конференции. 24 - 29 июня 2012 года. Санкт-Петербург. Издательство Политехнического университета. 2012. С.74-76.

40. Сборник руководящих документов по защите информации от несанкционированного доступа [Текст]. — М.: Гостехкомиссия России,

1998.

41. Система. Большая Советская Энциклопедия, http:// bse.sci-lib.com/ article 102619.html.

42. Система сетевого планирования и управления. Методические указания, http:// www.nntu.scinnov.ru/ RUS/ fakyl/ VECH/ metod/ orgprodl/part5.htm

43. Специальные требования и рекомендации по технической защите конфиденциальной информации (СТР-К). Решение Коллегии Гостехкомиссии России №7/02.03.01 г. http:// www.confidentiality.strongdisk.ru (по состоянию на 01.01.2011).

44. Тишков А.В., Котенко И.В., Черватюк О.В., Лакомов Д.П., Резник С.А., Сидельникова Е.В. Обнаружение и разрешение конфликтов в политиках безопасности компьютерных сетей // Труды СПИИРАН, Выпуск 3, Том 2. СПб.: Наука, 2006. С. 102-114.

45. Федеральная программа РФ по усилению борьбы с преступностью на 1994-1995 гг., утвержденная Указом Президента РФ от 24.05.94 №1016, 1994.

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

47. Al-Shaer Е., Adel El-Atawy, Taghrid Samak. Automated pseudo-live testing of firewall configuration enforcement. IEEE Journal on Selected Areas in Communications V. 27(3). 2009. P. 302-314.

48. Al-Shaer E., Hamed, H., Boutaba, R., Hasan, M.: Conflict classification and analysis of distributed firewall policies. IEEE Journal on Selected Areas in Communications, Vol.23(10) (2005)

49. Al-Shaer E.; Will Marrero; Adel El-Atawy; Khalid ElBadawi. Network configuration in a box: Towards end-to-end verification of network reachability and СВПФигку // Proceedings - International Conference on Network Protocols, ICNP. 2009. P. 123-132.

50. Alur, R., Anand, H., Grosu, R., Ivancic, F., etc. Mocha User Manual. JMocha Version 2.0. http://embedded.eecs.berkeley.edu/research/mocha/doc/j-doc/

51. E. M. Clarke and H. Schlingloff. Model checking. In A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning (Volume II), chapter 24, pages 1635-1790. Elsevier Publishers B.V., 2000.

52. Al-Tawil K., Ibrahim A. Al-Kaltham. Evaluation and testing of internet firewalls. Int. Journal of Network Management 9(3): 1999. P. 135-149.

53. Alfaro J. G., N. Boulahia-Cuppens • F. Cuppens. Complete analysis of configuration rules to guarantee reliable network Security policies. // International Journal of Information Security (IJIS), Vol 7, No 2,2008.-C. 103-122.

54. Alfaro J. G., Cuppens F., N. Cuppens-Boulahia. Management of Exceptions on Access Control Policies. IIIFIP International Federation for Information Processing, Springer Boston, 2007.

55. Arosha K B, Antonis Kakas, Emil C Lupu, Ra Russo. Using Argumentation Logic for Firewall Policy Specification and Analysis. // 17th IFIP/IEEE International Workshop on Distributed Systems: Operations and Management, Dublin, Ireland, 2006, C. 185-196.

56. Baier C., Katoen J.-P. Principles of Model Checking // The MIT Press, 2008. P. 984.

57. Bandara A.K., A.S.Kakas, E.C.Lupu, and A.Russo, "Using Argumentation Logic for Firewall Policy Specification and Analysis," 17th IFIP/IEEE International Workshop on Distributed Systems: Operations and Management. DSOM 2006, 2006. pp. 185-196.

58. Bartal Y., Alain Mayer, Kobbi Nissim, Avishai Wool. Firmato A Novel Firewall managment tool. // ACM Transactions on Computer Systems, Vol. 22, No. 4. IEEE CS Press, 2004. -C.381-420.

59. Benthem J. M. and A. T. Meulen Handbook of Logic and Language // Eds., North-Holland, 1997.

60. Bourdier T.. Formal analysis of firewalls using tree automata techniques. // INRJA Nancy Research Center-PAREO Team 615, France, 2010.

61. Braghin, C.; Sharygina, N.; Barone-Adesi, K. A Model Checking-based Approach for Security Policy Verification of Mobile Systems, Formal Aspects of Computing Journal, Springer, 2010

62. "Check Point Visual Policy Editor Data Sheet." http://www.checkpoint.com/products/downloads/vpe datasheet.pdf

63. Chen F.; Alex X. Liu; Jeehyun Hwang; Tao Xie. First step towards automatic correction of firewall policy faults // ACM Transactions on Autonomous and Adaptive Systems. V. 7(2). 2012.

64. "Cisco Secure Policy Manager 2.3 Data Sheet." http://www.cisco.com/warp/public/cc/pd/sqsw/sqppmn/prodlit/spmgr ds.pdf

65. Cobb. S. "ICSA Firewall Policy Guide v2.0." NCSA CBnOurity White Paper Series, 1997.

66. Common Information Model (CIM) Standards. http://www.dmtf.org/standards/cim

67. Conrad S., Campbell L.A., Cheng B.H.C., Deng M. A requirements patterns-driven approach to specify systems and check properties, International SPIN workshop, 2003. Vol. 2648. P. 18-33.

68. Cuppens F., Nora Cuppens-Boulahia, Joaquin Garcia-Alfaro. Detection and Removal of Firewall Misconfiguration. // Proceedings of the 2005 IASTED International Conference on Communication, Network and Information Security 1,2005. C. 154-162.

69. G. Delia Penna and B. Intrigila and I. Melatti and E. Tronci and M. Venturini Zilli. Finite horizon analysis of Markov chains with the Murphi verifier. Journal on Software Tools and Technology Transfer, 8(4-5):397^l09, 2006.

70. El-Atawy A., Ibrahim K., Hamed H., Al-Shaer E. Policy Segmentation for Intelligent Firewall Testing, Proceedings of the First Workshop on Secure Network Protocols, Boston, Massachusetts, 2005. P.67-72.

71. Eppstein D., and S. Muthukrishnan. "Internet Packet Filter Management and Rectangle Geometry." Proceedings of 12th Annual

72. Eronen P. and Jukka Zitting. An Expert System for Analyzing Firewall Rules. // Proc. 6th Nordic Worksh. Secure IT Systems, Technical report IMM-TR-2001-14, Denmark, 2001. C. 100107.

73. Firewall wizards security mailing list. Электронный ресурс. / Режим доступа: http://honor.icsalabs.com/mailman/listinfo/firewall-wizards свободный. — Загл. с экрана.

74. Gouda M. G.. Linear-Time Verification of Firewalls. // ICNP 2009: Princeton, USA, 2009. C. 133-140.

75. Gouda M. G., Alex X. Liu. A model of statefull firewalls and its properties. // In Proceedings of the IEEE International Conference on Dependable Systems and Networks (DSN'05), Japan, June 2005.

76. Hamed H., Al-Shaer E. Taxonomy of Conflicts in Network Security Policies, IEEE Communications Magazine, March 2006. Vol. 44, No. 3. P. 134-141.

77. Hari A., S. Suri, G. Parulkar. Detecting and Resolving Packet Filter Conflicts. // INFOCOM 2000. Nineteenth Annual Joint Conference of the IEEE Computer and Communications Societies, Vol.3, 2000.-C. 1203-1212.

78. Hinrichs S.. Integrating changes to a hierarchical policy model. // In Proceedings of 9th IFIP/IEEE International Symposium on Integrated Network Management, Nice, France, 2005. C. 441-454.

79. Holzmann G. The Spin Model Checker, IEEE Transactions on Software Engineering, May 1997. Vol. 23, No. 5. P.279-295.

80. Hwang J. H.; Tao Xie; Fei Chen; Alex X. Liu. Systematic structural testing of firewall policies // IEEE Transactions on Network and Service Management.V. 9(1). 2012. P. 1-11.

81. IETF Policy Framework (policy) Working Group. http://www.ietf.org/html.charters/policy-charter.html

82. Jajodia S., Samarati P., Sapino M.L., Subrahmanian V.S. Flexible support for multiple access control policies, ACM Transaction Database Systems. Vol.26, No.2, 2001. P. 214-260.

83. Johnson M., John Karat, Clare-Marie Karat, Keith Grueneberg. Optimizing a Policy Authoring Framework for Security and Privacy Policies. // Proceedings of the Sixth Symposium on Usable Privacy and Security, Vol. 485, Article No: 8, July 2010.

84. Jurjens J., Guido Wimmel. Specification-Based Testing of Firewalls (2001) // In proceeding of the 4th International Conference of perspectives of System Informatics (PSI'02). 2002. P. 308-316.

85. J.-P. Katoen and M. Khattri and I. S. Zapreev. A Markov reward model checker. In 2nd International Conference on Quantitative Evaluation of Systems (QEST), pages 243-244. IEEE Computer Society Press, 2005.

86. Kotenko I., Polubelova O. Verification of Security Policy Filtering Rules by Model Checking // Proceedings of IEEE Fourth International Workshop on "Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications" (IDAACS'2011). Prague, Czech Republic, 15-17 September 2011. P. 706-710.

87. Kotenko I., Olga Polubelova, Igor Saenko. Data Repository for Security Information and Event Management in service infrastructures. Proceedings of 9th International Joint Conference on e-Business and Telecommunications (ICETE 2012). International Conference on Security and Cryptography (SECRYPT 2012). Rome, Italy, 24-27 July, 2012. P.308-313. (на английском).

88. Kotenko I., Olga Polubelova, Igor Saenko. Hybrid Data Repository Development and Implementation for Security Information and Event Management. Proceedings of the Work in Progress Session held in connection with the 20th Euromicro International Conference on Parallel, Distributed and network-based Processing (PDP 2012). Garching/Munich, February 2012. SEA-Publications. SEA-SR-31. 2012. P.29-30. (на английском).

89. Kotenko I., Olga Polubelova, Igor Saenko. The Ontological Approach for SIEM Data Repository Implementation. 2012 IEEE International Conference on Green Computing and Communications, Conference on Internet of Things,

and Conference on Cyber, Physical and Social Computing. Besançon, France, September 11-14, 2012. Los Alamitos, California. IEEE Computer Society. 2012. P. 761-766. (на английском).

90. Kotenko I., Olga Polubelova. Verification of Security Policy Filtering Rules by Model Checking. Proceedings of IEEE Fourth International Workshop on "Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications" (IDAACS'2011). Prague, Czech Republic, 15-17 September 2011. P. 706-710. ISBN 978-1-4244-4882-1. (на английском).

91. Kowalski, R.A., Sergot, M.J.: A logic-based calculus of events. New Generation Computing, V.4 (1986) pages?

92. M. Kwiatkowska and G. Norman and D. Parker. Modelling and verification of probabilistic systems. In P. Panangaden and F. van Breugel, editors, Part 2 of Mathematical Techniques for Analyzing Concurrent and Probabilistic Systems, volume 23 of CRM Monograph Series. AMS Press, 2004.

93. [LTL patterns] http://patterns.projects.cis.ksu.edu/documentation/patterns/ltl.shtml

94. Liu A. X. and Mohamed G. Gouda. Complete redundancy detection in firewalls. // Department of Computer Sciences, The University of Texas at Austin, Austin, Texas, USA, 2005.

95. Liu A. X., Mohamed G. Gouda, Huibo H. Ma, Anne HH. Ngu. Firewall Queries. // OPODIS 2004, LNCS 3544, Springer-Verlag Berlin Heidelberg, 2005. С. 197-212.

96. Lupu E., M. Sloman. Conflict Analysis for Management Policies. // Proceedings of the fifth IFIP/IEEE international symposium on Integrated network management (IM'97), San-Diego, USA, 1997.-C. 430-443.

97. Lymberopoulos L. A.. An Adaptive Policy Based Framework for Network Management. // Journal of Network and Systems Management, Vol. 11, 2003. C. 277 - 303.

98. Manna Z., Pnueli A. Temporal Verification of Reactive Systems: Safety // Springer-Verlag, New York, 1995. P. 530.

99. Manna Z., A. Pnueli A.: The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1992.

100. Mannorstein R., Phil Kearns. A Tool for Automated Iptables Firewall Analysis. // USENIX 2005 Annual Technical Conference, FREENIX Track, Anaheim, CA, 2005. C. 71-81.

101. Marmorstein R. Formal Analysis of Firewalls. // Department of Math and Computer Science, Longwood University, September 2005.

102. Marmorstein R., Phil Kearns. Firewall analysis with policy-based host classification. // Proceedings of the 20th Large Installation System Administration Conference (LISA '06), Washington DC, 2006.-C. 41-51.

103. Mayer A. J., Avishai Wool, Elisha Ziskind. Offline firewall analysis. Int. J. Inf. Sec. 5(3). 2006. P. 125-144.

104. Mayer A., Avishai Wool, Elisha Ziskind. Fang. A firewall analysis engine. // In Proceedings, IEEE Symposium on Security and Privacy, IEEE CS Press, 2000. C. 177-187.

105. McMillan K. L.. A technique of state space search based on unfoldings. Formal Methods in System Design, 6(l):45-65, 1995.

106. Merz S. and N. Navet (editors). Modeling and Verification of Real-Time Systems: Formalisms and Software Tools. ISTE Ltd, 2008.

107. Microsoft Encyclopedia of Security / M. Tulloch. Washington : Microsoft Press, 2003. 416 p.

108. Oliveira R., S. Lee, H. Kim. Automatic detection of firewall misconfigurations using firewall and network routing policies. // Carnegie Mellon University, 2009.

109. Oliveira R., Sihyung Lee, Hyong S. Kim. Automatic Detection of Firewall Misconfigurations Using Firewall and Network Routing Policies. // Carnegie Mellon University, 2009.

110. On-The-Fly, LTL Model Checking with SPIN, http://netlib.bell-labs.com/netlib/spin/whatispin.html

111. RFC 1817 CIDR and Classful Routing. Электронный ресурс. / Режим доступа: http://www.faqs.org/rfcs/rfcl817.html/ - свободный. - Загл. с экрана.

112. RFC 4632 Classless Inter-domain Routing (CIDR): The Internet Address Assignment and Aggregation Plan. Электронный ресурс. / Режим доступа: http://t001s.ietf.0rg/html//rfc4632/ -свободный. - Загл. с экрана.

113. Parker D. Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham, UK, 2002.

114. Pham H. Т., Ninh-Thuan Truong , Viet-Ha Nguyen Analyzing RBAC Security Policy of Implementation Using AST, Proceedings of the 2009 International Conference on Knowledge and Systems Engineering (KSE '09), 0ct'2009.

115.Pozo S., A.J. Varela-Vaca, Rafael M. Gasca. MDA-Based Framework for Automatic Generation of Consistent Firewall ACLs with NAT. // In Proc. 9th International Conference on Computational Science and Its Applications (ICCSA), Korea, 2009. C. 130-144.

116. Rasmussen J. I. and K. G. Larsen and K. Subramani. On using priced timed automata to achieve optimal scheduling. Formal Methods in System Design, 29(1):97-114, 2006.

117. Rothmaier G., Kneiphoff Т., KrummH. Using SPIN and Eclipse for Optimized High-Level Modeling and Analysis of Computer Network Attack Models, Lecture Notes in Computer Science, Springer-Verlag, 2005. Vol. 3639. P.236-250.

118. Ruys Т. C. and E. Brinksma. Managing the verification trajectory. International Journal on Software Tools for Technology Transfer, 4(2):246-259, 2003.

119. Sebastiani R. and S. Tonetta. "More deterministic" vs. "smaller" Buchi automata for efficient LTL model checking. In 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods

(CHARME), volume 2860 of Lecture Notes in Computer Science, pages 126— 140. Springer-Verlag, 2003.

120. Sirjani M. Formal specification and verification of concurrent and reactive systems, Ph.D. Thesis. Sharif University of Technology, 2004. 175 p.

121. Schneider K. Verification of Reactive Systems: Formal Methods and Algorithms.Springer-Verlag, 2004.

122. Staunstrup J. and H. R. Andersen and H. Hulgaard and J. Lind-Nielsen and K. G. Larsen and G. Behrmann and K. Kristoffersen and A. Skou and H. Leerberg and N. B. Theilgaard. Practical verification of embedded software. IEEE Computer, 33(5):68-75, 2000.

123. Tauriainen H.. Nested emptiness search for generalized B'uchi automata. Research Report A79, Helsinki University of Technology, Laboratory for Theoretical Computer Science, 2003.

124. Thirioux X.. Simple and efficient translation from LTL formulas to B'uchi automata. Electronic Notes in Theoretical Computer Science, 66(2), 2002.

125. Tretmans G. J. and K. Wijbrans and M. Chaudron. Software engineering with formal methods: the development of a storm surge barrier control system. Formal Methods in System Design, 19(2): 195-215, 2001.

126. Tripakis S. and S. Yovine. Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design, 18(l):25-68, 2001.

127. Uribe T., S. Cheung. Automatic analysis of firewall and network intrusion detection system configurations. // Journal of computer security, Vol. 15, 2007. C. 691-715.

128. Vardi M. Y. Branching versus linear time: Final showdown. In 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2031 of Lecture Notes in Computer Science, pages 1-22. Springer-Verlag, 2001.

129. Volzer H. and D. Varacca and E. Kindler. Defining fairness. In 16th International Conference on Concurrency Theory (CONCUR), volume 3653

of Lecture Notes in Computer Science, pages 458^72. Springer-Verlag, 2005.

130. Wang F. Efficient verification of timed automata with BDD-like data structures.Journal on Software Tools and Technology Transfer, 6(l):77-97, 2004.

131. Westerinen, A., Strassner, J., Scherling, M., Quinn, B., Herzog, S., Huynh, A., Carlson, M., Perry, J., Waldbusser, S.: Terminology for Policy-Based Management (RFC 3198). [Online]. Available: www.rfc-archive.org/getrfc.php?rfc=3198

132. Yu T.; Dhivya Sivasubramanian; Tao Xie. Security policy testing via automated program code generation // ACM International Conference Proceeding Series. 2009.

133. Yuan L., J. Mai, Z. Su, H. Chen, C. Chuah, and P. Mohapatra. FIREMAN: a toolkit for firewall modeling and analysis. // In Proc. IEEE Symposium on Security and Privacy, 2006. C. 199

134. Zhang N., RyanM. D., GuelevD. Evaluating Access Control Policies Through Model Checking, 8th Information Security Conf. (ISC'05). Singapore: Lecture Notes in Computer Sei. Springer-Verlag. Vol. 3650, 2005. P. 446^60.

135. Zhang L.; Xiaoxing Ma; Jian Lu; Tao Xie; Nikolai Tillmann; Peli De Halleux. Environmental modeling for automated cloud application testing // IEEE Software. V. 29(2). 2012. P. 30-35.