МЕТОДИКА  ВЕРИФИКАЦИИ  ПОЛИТИК  БЕЗОПАСНОСТИ   В  МНОГОУРОВНЕВОЙ  ИНТЕЛЛЕКТУАЛЬНОЙ  СИСТЕМЕ  ОБЕСПЕЧЕНИЯ  КОМПЛЕКСНОЙ  БЕЗОПАСНОСТИ  ЖЕЛЕЗНОДОРОЖНОГО  ТРАНСПОРТА

Котенко  Игорь  Витальевич

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

E-mail:  ivkote@comsec.spb.ru

Саенко  Игорь  Борисович

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

E-mail:  ibsaen@comsec.spb.ru

THE  TECHNIQUE  FOR  VERIFICATION  OF  SECURITY  POLICIES  IN  THE  MULTILEVEL  INTELLIGENT  SYSTEM  OF  INTEGRATED  PROTECTION  OF  RAILWAY  TRANSPORT

Kotenko  Igor  Vitalievich

Ph.D.,  Professor,  Head  of  Laboratory  of  Computer  Security  Problems,  St.  Petersburg  Institute  for  Informatics  and  Automation  of  RAS  (SPIIRAS),  Russia  St.  Petersburg

Saenko  Igor  Borisovich

Ph.D.,  Professor,  Leading  research  scientist  of  Laboratory  of  Computer  Security  Problems,  St.  Petersburg  Institute  for  Informatics  and  Automation  of  RAS  (SPIIRAS),  Russia  St.  Petersburg

Работа  выполнена  при  поддержке  РФФИ  (проекты  13-01-00843,  13-07-13159,  14-07-00697,  14-07-00417)  и  программы  фундаментальных  исследований  ОНИТ  РАН  (проект  2.2)

АННОТАЦИЯ

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

ABSTRACT

The  paper  outlines  a  technique  for  verification  of  security  policies  applied  in  an  intelligent  system  of  integrated  protection  of  railway  transport.  The  stages  of  the  technique  based  on  Model  checking  are  considered.  The  issues  related  to  building  the  models  of  computer  network,  anomalies  and  transitions  used  in  the  verification  technique  are  discussed. 

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

Keywords:  verification;  security  policy;  rail  transport;  security  management. 

Обеспечение  комплексной  безопасности  железнодорожного  транспорта  (ЖТ)  предполагает  внедрение  многоуровневой  интеллектуальной  системы,  обеспечивающей  своевременный  сбор  и  аналитическую  обработку  данных  о  состоянии  ЖТ  и  происходящих  на  нем  событиях  [1,  с.  69;  4,  с.  8],  основанной  на  технологиях,  применяемых  в  системах  мониторинга  и  управления  безопасностью  [2,  с.  28;  3,  с.  8].  Одной  из  важнейших  задач,  решаемых  в  такой  системе,  является  задача  верификации  политик  безопасности,  заключающаяся  в  выявлении  ошибок  в  спецификации  правил  обеспечения  безопасности,  которые  первоначально  вводятся  на  этапе  ввода  интеллектуальной  системы  в  эксплуатацию  и  пополняются  либо  корректируются  в  ходе  эксплуатации  системы  [5,  с.  707].

Одним  из  наиболее  известных  и  широко  распространенных  методов  верификации  политик  безопасности  в  настоящее  время  является  метод  «проверки  на  модели»  (Model  checking),  на  базе  которого  разрабатывается  специальный  верификатор  [5,  с.  706].  С  его  помощью  верификация  политик  безопасности  на  предмет  аномалий  фильтрации  методом  “проверки  на  модели”  сводится  к  следующим  действиям.  Вначале  осуществляется  построение  модели  компьютерной  сети,  в  которой  применяются  политики  безопасности.  Затем  задается  спецификация  этой  сети  с  помощью  линейной  темпоральной  логики.  Модель  компьютерной  сети  предназначена  для  представления  структуры  сети,  ее  основных  элементов  и  сетевых  процессов.  Она  включает  в  себя  два  базовых  компонента:  топологию  сети  и  сетевой  трафик,  контролируемый  политиками  безопасности.  Топология  сети  представляется  расположением  хостов  и  межсетевых  экранов.  Основными  компонентами  модели  сетевого  экрана  являются  сетевые  идентификаторы,  заданные  политики  безопасности,  представленные  в  виде  набора  правил  фильтрации,  а  также  алгоритм  обработки  сетевого  трафика.  В  этом  случае  методика  верификации  правил  политик  безопасности  в  компьютерных  сетях  ЖТ  будет  включать  в  себя  следующие  этапы:  (1)  построение  модели  компьютерной  сети  во  внутреннем  формате  системы  верификации  в  виде  конечного  автомата;  (2)  построение  спецификации  на  проверяемую  систему,  задающей  свойства  корректности  (т.е.  отсутствия  аномалий)  на  языке  темпоральной  логики;  (3)  вычисление  модели  с  помощью  программного  средства  (верификатора);  (4)  обработка  результатов  верификации  и  построенных  контрпримеров,  показывающих,  каким  образом  система  может  перейти  в  некорректное  состояние;  (5)  сравнение  и  оценка  результатов  верификации  в  соответствии  с  требованиями  к  их  эффективности.

Рассмотрим,  каким  образом  формируются  модель  компьютерной  сети  и  модели  для  каждого  типа  аномалий.

Для  построения  модели  компьютерной  сети  в  методе  Model  checking  принято  использовать  модель  Крипке  [6,  с.  10].  Она  состоит  из  множества  состояний,  множества  переходов  между  состояниями  и  функции,  которая  помечает  каждое  состояние  набором  свойств,  истинных  в  этом  состоянии.  Пути  в  модели  Крипке  соответствуют  вычислениям  системы.  Для  описания  параллельных  систем  можно  воспользоваться  формулами  логики  предикатов  первого  порядка,  по  которым  строится  модель  Крипке.  Модели  типов  аномалий,  по  сути,  являются  спецификациями,  задаваемыми  на  языке  темпоральной  логики.  Темпоральные  формулы  отображают  желаемое  поведение  системы.  Иными  словами,  они  выражают  отсутствие  аномалий  в  политиках  безопасности.  Таким  образом,  задача  верификации  представляет  собой  проверку  выполнимости  данных  формул  на  модели  Крипке.  С  помощью  верификатора  проводится  автоматический  анализ  того,  соответствует  ли  модель  заданной  спецификации.  Если  же  модель  не  удовлетворяет  спецификации,  то  определяется  опровергающее  вычисление,  т.  е.  последовательность  действий  модели,  на  которой  нарушается  спецификация.

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

Модель  Крипке  строится  на  основании  формул    первого  порядка  с  учетом  следующих  правил:  множество  состояний  S  есть  множество  всех  оценок  над  множеством  переменных  V;  какова  бы  ни  была  пара  состояний  s  и  s’,  отношение    соблюдается  в  том  и  только  в  том  случае,  когда  формула    обращается  в  True,  после  того,  как  каждой  переменной    присвоено  значение  ,  а  каждой  переменной    –  значение  . 

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

Множество  состояний  будет  определяться  как  ,  где  E  —  множество  сетевых  пакетов  в  модели,  U  —  множество  используемых  в  модели  правил  политики  безопасности,  AF  —  множество  примененных  правил.

Для  построения  системы  переходов  выполняются  следующие  действия:  (1)  для  сетевого  пакета  p  проверяется  возможность  применения  правила  u  до  тех  пор,  пока  все  правила  не  будут  проанализированы.  Если  правило  можно  применить  к  данному  сетевому  пакету,  то  пара  (p,  u)  добавляется  в  массив  пар,  включающих  пакет  и  правило  политики  безопасности;  (2)  когда  сетевой  пакет  p  обработан,  анализируется  пакет  p’,  и  к  нему  начинают  применяться  все  правила  фильтрации;  (3)  проверяется  пара,  включающая  сетевой  пакет  и  примененное  к  нему  правило  (p,  u).  Если  проанализирован  весь  набор  примененных  к  одному  пакету  правил,  то  они  удаляются.

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

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

1.Котенко  И.В.,  Саенко  И.Б.  Предложения  по  созданию  многоуровневой  интеллектуальной  системы  обеспечения  информационной  безопасности  автоматизированных  систем  на  железнодорожном  транспорте  //  Вестник  Ростовского  государственного  университета  путей  сообщения.  Научно-технический  журнал.  —  2013.  —  №  3(51).  —  С.  68—78.

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

3.Котенко  И.В.,  Степашкин  М.В.,  Богданов  В.С.  Архитектуры  и  модели  компонентов  активного  анализа  защищенности  на  основе  имитации  действий  злоумышленников  //  Проблемы  информационной  безопасности.  Компьютерные  системы.  —  2006.  —  №  2.  —  С.  7—24.

4.Котенко  И.В.,  Саенко  И.Б.,  Чернов  А.В.,  Бутакова  М.А.  Построение  многоуровневой  интеллектуальной  системы  обеспечения  информационной  безопасности  для  автоматизированных  систем  железнодорожного  транспорта  //  Труды  СПИИРАН.  —  2013.  —  Вып.  7  (30).  —  С.  7—25.

5.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.  2011.  —  Pp.  706—710.

6.Peled  D.A.,  Clarke  E.M.,  Grumberg  O.  Model  checking.  MIT  Press.  2000.  —  314  p.