Константин Савенков / Антон Ампилогов, 3 курс, sec-sem

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

Модератор: staff

Закрыто
Бычков Иван
Аспирант
Сообщения: 179
Зарегистрирован: 23 сен 2008 01:19 pm

Константин Савенков / Антон Ампилогов, 3 курс, sec-sem

Сообщение Бычков Иван »

Тема: Верификация безопасности наблюдаемого поведения информационной системы

Расшифровка темы:
Речь идёт об исследовании применимости верификации в режиме выполнения (runtime verification) для обнаружения атак.

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

Актуальность:

Если рассмотреть подход к обнаружению атак, используемый в СОА "RedSecure", то мы увидим необходимость описывать поведение системы в виде автомата. Такой способ описания не является удобным. Собственно, темпоральные логики когда-то были разработаны именно для того, чтобы избежать ручного построения автомата, распознающего правильное поведение.

Возникает вопрос: можно ли предложить/подобрать некотурую human-friendly логику для описания свойств безопасности (аномального или нормального поведения) информационной системы в рамках формальной модели СОА "RedSecure"? Естественно, при этом нужна не просто логика, но и необхоимый ля её использования инструментарий.

Беглый обзор показал, что существует некоторое количество таких логик (например, EAGLE), осталось их изучить и посмотреть, насколько они применимы на практике.

Постановка задачи на 3 курс:

* Освоение материала по обнаружению атак, верификации программ и темпоральным логикам,

* Освоение материала по runtime verifcation (RV),),

* Обзор работ, где предлагается использование runtime verification для обнаружения атак, а также последних работ в области с анализом их применимости для рассматриваемой задачи.

* Выбор или построение логики для описания свойств безопасности ИС, соотнесение её с автоматами I рода, испльзуемыми в СОА "RedSecure"

* В зависимости от результатов перечисленных выше действий:

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

Понятное дело, это задача не на один курс, всё будет зависеть от усердия студента, да и объём литературы большой.
Антон Ампилогов
Выпускник
Сообщения: 2
Зарегистрирован: 16 дек 2008 10:34 pm

Сообщение Антон Ампилогов »

Отчет о проделанной работе.
Автор: Антон Ампилогов.
Научный руководитель: Константин Савенков.

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

Цель работы:
Сделать возможной верификацию безопасности информационной системы во время
выполнения в рамках СОА "RedSecure".

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

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

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

Проделанная работа:
Были изучены материалы по системам обнаружения атак, в частности по RedSecure.
Просмотрены слайды лекций по верификации.
Прочитано несколько статей на тему Runtime Verification. На часть статей были
написаны резюме, которые можно посмотреть в траке.

Найдена утилита LTL2BA, которая умеет переводить формулы LTL в
* Weak Alternating Automata,
* Generalized Buchi Automata,
* Buchi Automata.
Предполагается использовать Weak Alternating Automata для построения из них автоматов,
использующихся в RedSecure.
Weak Alternating Automata отличается от Alternating Automata тем, что на их состояниях
задан частичный порядок. Фактически, все его состояния можно разбить на несколько
непересекающихся подмножеств, и пронумеровать эти множества так, что переходы в
автомате могут осуществляться только к элементам множества с не меньшим номером,
чем тот, из которого осуществляется переход.

Трудности, которые могут возникнуть при построении переходов:
1. переход осуществляется в объединение двух состояний.
2. переход осуществляется в пересечение двух состояний.
В первом случае автомат должен находиться в одном из состояний, выбирающемся
случайно. Денис Гамаюнов мне дал совет использовать переменную, случайно
выбирающую ноль или один, и в зависимости от значения этой переменной делать
consuming переход в одно из двух состояний.
Во втором случае автомат должен находиться одновременно в обоих состояниях. Это
можно сделать при помощи перехода nonconsuming, и таким образом эмулировать
нахождение автомата в двух состояниях.


Список литературы:
1. Bern Finkerbeiner,Henny Sipma.Checking Finite Traces using Alternating
Automata.//J.Formal Methods in System Design.2004.24.№ 2.P.101-127.
2. Денис Гамаюнов.Обнаружение компьютерных атак на основе анализа поведения
сетевых объектов.
3. Orna Kupferman,Moshe Y.Vardi. Weak Alternating Automata Are Not That Weak.//ACM
Transactions on Computational Logic(TOCL).Volume 3,Issue 2.July 2001.P.408-429.
4. Paul Gastin, Denis Oddoux. Fast LTL to Buchi Automata Translation.//Lecture Notes In
Computer Scines.Vol.2102.Procedings of the 13th International Conference on Computer
Aided Verification. 2001.P. 53-65.
5. Эдмунд М. Кларк, мл. Орна Грамберг, Дорон Пелед.Верификация моделей программ:
Model Checking.M.:Издательство Московского центра непрерывного математического
образования, 2002. 416 с.
6. Klaus Havelund.Using Runtime Analysis to Guide Model Checking of Java
Programs.//SPIN 2000, LNCS 1885.Heidelberg.:Springer-Verlag Berlin,2000. P.245-264.
7. Andreas Morgenstern and Klaus Schneider From LTL to Symbolically Represented
Deterministic Automat.// Lecture Notes in Computer Science. Verification, Model Checking,
and Abstract Interpretation.Vol.4905/2008.,2008.P.279-293.
8. Статья: Применение темпоральных логик для моделирования составных систем.
Закрыто