Реферат 2
ВВЕДЕНИЕ 5
1 Основные определения и обозначения 7
2 Описание совместного поведения веб-сервисов при помощи композиции временных автоматов 11
2.1 Построение параллельной композиции временных автоматов 11
2.2 Переход от глобального полуавтомата ко временному автомату композиции 12
2.3 Алгоритм преобразования глобального полуавтомата во временной автомат 16
2.4 Экспериментальные результаты 18
3 Обнаружение веб-уязвимостей при помощи полуавтоматной модели 20
3.1 Построение правого частного 20
3.2 Построение левого частного 21
3.3 Представление данных 23
3.4 Алгоритмы построения правого и левого частного 25
3.5 Обсуждение применения алгоритмов нахождения правого и левого частного для
проверки безопасности веб-сервисов 26
ЗАКЛЮЧЕНИЕ 30
СПИСОК ИСПОЛЬЗОВАННОЙ ЛИТЕРАТУРЫ 31
ПРИЛОЖЕНИЕ А Исходный код программы преобразования глобального полуавтомата во временной автомат 32
ПРИЛОЖЕНИЕ Б Исходный код программы построения левого и правого частного 38
Большое число дискретных систем можно описать с помощью математических моделей - конечного автомата [1] и полуавтомата. Теория автоматов предоставляет богатый набор методов и алгоритмов для работы с данными моделями.
Одними из таких систем являются веб-сервисы, чьё использование в корпоративных и пользовательских приложениях возрастает. Учитывая, что веб-сервисы используются во многих сферах, где недопустима даже возможность неправильного взаимодействия или уязвимости к веб-атакам, необходимы инструменты и способы проверки и обнаружения подобных «слабых мест». С помощью моделей автомата и полуавтомата можно решить ряд возникающих в веб-сервисах задач. В частности - вопрос проверки безопасности веб-сервисов [2], а также проверка корректности взаимодействия клиентской и серверной частей.
Важность защищенности веб-сервисов от атак трудно переоценить, ведь веб-сервисы используются повсеместно. Часто для проведения атаки на веб-сервис злоумышленники используют поля ввода пользовательских данных. Поэтому необходимо проводить проверку и, при необходимости, очистку вводимых пользователями данных.
Наши коллеги из Тайваня предложили использовать модель полуавтомата для обнаружения атак и очистки пользовательских данных [3]. В данной работе мы предлагаем альтернативный способ использования модели полуавтомата. Особенностью нашего способа является возможность отследить, в каком именно поле возможна атака. Зная, какая именно очистка нужна для каждого поля, мы не очищаем больше, чем нужно. Например, нет смысла очищать поля, данные из которых не используются при запросе к базе данных, от SQL-инъекций.
Еще одним важным критерием является корректность совместной работы клиентской и серверной компонент. Описав совместное поведение компонент при помощи формальных моделей, можно с помощью формальных методов построить тест для проверки их совместной работы. В частности, не возникают ли при совместной работе тупики или зацикливания.
Если систему нужно рассматривать с учётом времени, то используется модель временного автомата, а при описании совместной работы нескольких автоматов можно использовать операцию параллельной композиции [4], при которой системы взаимодействуют в режиме диалога, что соответствует взаимодействию между клиентом и сервером.
Одним из инструментов, позволяющих построить параллельную композицию, является BALM-II [5]. Однако, данный инструмент осуществляет параллельную композицию полуавтоматов, выдавая в итоге глобальный полуавтомат. Соответственно, для использования BALM-II с целью построения параллельной композиции необходимо исходные временные автоматы преобразовать в полуавтоматы. В результате параллельной композиции полуавтоматов BALM-II выдаёт глобальный полуавтомат, который нужно преобразовать обратно во временной автомат.
При построении параллельной композиции временных автоматов возможна ситуация, когда автомат, моделирующий совместную работу двух изначальных временных автоматов, имеет бесконечное множество задержек выходных симолов, причем такое множество описывается линейной функцией вида b+kt [6]. Экспериментальная часть работы посвящена изучению того, как часто появляются такие бесконечные множества задержек.
Целью данной бакалаврской работы является разработка и программная реализация алгоритмов для описания совместной работы веб-сервисов с помощью автоматных моделей и проверки их безопасности.
В связи с поставленной целью решаются следующие задачи:
1. Изучить литературу.
2. Описать совместную работу двух временных автоматов.
3. Рассмотреть возможность использования (полу)автоматных моделей для проверки безопасности.
Данная бакалаврская работа посвящена изучению применимости (полу)автоматных моделей для проверки корректности совместной работы веб-сервисов. Под корректностью совместной работы веб-сервисов подразумевается отсутствие тупиков, зацикливаний и возможностей для проведения веб-атак.
При описании веб-сервисов используется модель временного автомата, для которой не существовало инструментов построения параллельной композиции. В связи с этим был программно реализован инструмент построения параллельной композиции временных автоматов. Для его реализации был разработан алгоритм преобразования глобального полуавтомата во временной автомат. Также был реализован скрипт, осуществляющий параллельную композицию временных автоматов. При помощи написанного инструмента был проведён эксперимент. В результате эксперимента было установлено, что в 50% случаев при композиции временных автоматов возникают бесконечные множества задержек выходной реакции, которые можно описать с помощью линейных функций вида b+kt. Также в ходе эксперимента была обнаружена проблема «взрыва числа состояний», связанная с использованием модели полуавтомата.
Для проверки веб-сервисов на безопасность был программно реализован алгоритм построения правого частного двух полуавтоматов. Также был разработан и программно реализован алгоритм построения левого частного двух полуавтоматов. При программной реализации использовалось разработанное ранее и использованное в работе [6] представление полуавтомата. При реализации правого частного использовался алгоритм, предложенный Питером Линцем [7]. Алгоритм получения левого частного был разработан самостоятельно на основе формулы, приведенной в [8]. Также написан скрипт, преобразующий строку в полуавтомат и скрипт, преобразующий алфавит действий из символов в числа. Были успешно осуществлены SQL-инъекции в созданный веб-сервис. На основе успешной SQL-инъекции была проверена корректность работы программ для построения правого и левого частного.
