МЕТОДИКА  ВЕРИФИКАЦИИ ПРАВИЛ  ФИЛЬТРАЦИИ МЕТОДОМ  «ПРОВЕРКИ  НА  МОДЕЛИ»

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

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

Е-mail:  ovp@comsec.spb.ru

VERIFICATION  OF  SECURITY  POLICY FILTERING  RULES  BY  MODEL  CHECKING

Olga  Polubelova

Researcher,  Laboratory  of  Computer  Security  Problems  St.  Petersburg  Institute  for  Information  and  Automation  of  RAS,  St.  Petersburg

Работа  выполняется  при  финансовой  поддержке  РФФИ,  программы  фундаментальных  исследований  ОНИТ  РАН,  Министер­ства  образования  и  науки  Российской  Федерации  (государственный  контракт  11.519.11.4008),  при  частичной  финансовой  поддержке,  осуществляемой  в  рамках  проектов  Евросоюза  SecFutur  и  MASSIF,  а  также  в  рамках  других  проектов.

АННОТАЦИЯ

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

ABSTRACT

The  paper  outlines  an  method  to  verification  of  filtering  rules  of  firewalls.  The  method  is  intended  for  detection  and  resolution  of  filtering  anomalies  in  the  specification  of  the  security  policy  of  computer  networks.  It  is  based  on  Model  Checking  technique.  It  uses  temporal  logic  for  the  specification  and  analysis  of  information  flows  in  network.

Ключевые  слова:  сетевая  безопасность;  верификация;  проверка  на  модели;  аномалии  правил  фильтрации.

Keywords:  network  security;  verification;  model  checking;  anomalies  of  filtering  rules.

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

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

Основываясь  на  рассмотренных  работах  [1,  3,  5,  8,  9,  12]  и  ряде  других  работ,  рассмотренных  в  [4,  11],  в  данной  статье  предлагается  методика  верификации  правил  фильтрации  для  обнаружения  таких  аномалий  на  основе  метода  «проверки  на  модели».  Отличительной  особенностью  данной  работы  является  применение  метода  «проверки  на  модели»  для  верификации  правил  фильтрации  политики  безопасности.

Основные  этапы  методики  представлены  на  рисунке  1. 

Рисунок  1.  Основные  этапы  методики  верификации правил  фильтрации

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

Основными  входными  данными  в  предлагаемой  методике  являются  описания  правил  фильтрации  политики  на  языке  описания  политики  (ЯОП)  и  конфигурации  компьютерной  сети  на  языке  описания  системы  (ЯОС),  а  также  выявляемые  аномалии  фильтрации.  ЯОП  и  ЯОС  —  это  xml-подобные  языки,  созданные  на  основе  CIM  [7]. 

На  этапе  трансляции  методики  входные  данные,  включающие  в  себя  описание  политики,  компьютерной  системы  и  аномалий,  преобразуются  во  внутренний  формат  системы  верификации.  На  этапе  построения  модели  строится  общая  модель  для  верификации  правил  фильтрации,  представленная  в  виде  конечного  автомата.  Он  представ­ляет  собой  функционирование  компьютерной  системы,  защищенной  межсетевым  экраном.  На  этапе  вычисления  модели  общая  модель  для  верификации  правил  фильтрации  верифицируется  специальными  программными  средствами,  реализующими  метод  «проверки  на  модели»,  в  данной  работе  —  это  SPIN  [2,  10].  В  процессе  верификации  выявляются  все  некорректные  состояния  системы.  Т.  е.  в  рассматриваемой  методике  таким  состоянием  будет  являться  возникновение  аномалии  фильтрации  при  попытке  применить  правила  фильтрации  на  определенном  наборе  сетевых  пакетов.  Серым  цветом  на  рис.  2  помечено  одно  из  таких  некорректных  состояний.  На  завер­шающем  этапе  полученные  результаты  верификации  интерпрети­руются.  Если  были  обнаружены  аномалии,  то  пользователь  получает  адреса  межсетевых  экранов  и  правила,  приводящие  к  возникновению  аномалии,  а  также  тип  аномалии  и  способ  ее  разрешения.

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

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

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

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

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

Список  литературы:

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

2. Кларк  Э.М.,  Грамберг  О.,  Пелед  Д.  Верификация  моделей  программ.  Model  Checking.  М.:  МЦНМО.  2002.  —  416  с. 

3. Миронов  А.М.  Математическая  теория  программных  систем.  [Электронный  ресурс]  —  Режим  доступа.  —  URL:  http://intsys.msu.ru/staff/mironov/.

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

5. 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,  No.10,  2005.  —  P.  2069—2084.

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

7. Common  Information  Model  (CIM)  Standards.  [Электронный  ресурс]  —  Режим  доступа.  —  URL:  http://www.dmtf.org/standards/cim.

8. Eronen  P.,  Zitting  J.  An  expert  system  for  analyzing  firewall  rules  //  Proceedings  of  the  6th  Nordic  Workshop  on  Secure  IT  Systems  (NordSec  2001),  Copenhagen,  Denmark,  November  2001.  —  P.  100—107.

9. Hari  A.,  Suri  S.,  Parulkar  G.  Detecting  and  Resolving  Packet  Filter  Conflicts  //  Proceedings  of  INFOCOM  2000.  —  P.  1203—1212.

10. Holzmann  G.  The  Spin  Model  Checker  Primer  and  Reference  Manual  //  Addison-Wesley,  2003.  —  608  p.

11. 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.

12. Kowalski  R.A.,  Sergot  M.J.  A  logic-based  calculus  of  events  //  New  Generation  Computing,  Vol.4,  1986.  —  P.  67—94.