Конечно-автоматные алгоритмы проверки безопасного функционирования веб-сервисов тема диссертации и автореферата по ВАК РФ 00.00.00, кандидат наук Широкова Екатерина Владимировна

• Широкова Екатерина Владимировна
• кандидат наук
• 2025

Оглавление диссертации кандидат наук Широкова Екатерина Владимировна

Введение

1 Основные определения и обозначения

1.1 Веб-сервис

1.2 Конечные автоматы и отношения между ними

1.3 Конечные полуавтоматы

1.4 Параллельная композиция конечных автоматов

1.4.1 Построение композиции конечных автоматов на основе перехода к полуавтоматам

1.4.2 Построение композиции конечных автоматов на основе дерева достижимости

1.5 Описание поведения веб-сервисов и их композиций с использованием операции параллельной композиции автоматов-компонентов

2 Проверка безопасности и робастности веб-сервисов

2.1 Краткий обзор известных подходов к проверке безопасности взаимодействия компонентов сложных систем

2.2 Проверка на наличие тупиковых ситуаций работы веб-сервиса на основе композиции конечных автоматов и проекций автоматных компонентов

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

2.4 Проверка робастности веб-сервиса

2.4.1 Проверка робастности веб-сервиса на основе композиции конечных автоматов

2.4.2 Прагматичный подход к проверке робастности веб-сервисов

2.5 Выбор реализаций серверного приложения, которые могут робастно взаимодействовать с заданным клиентским приложением

2.6 Синтез безопасного серверного приложения веб-сервиса

2.6.1 Параллельные автоматные уравнения (неравенства)

2.6.2 Система параллельных автоматных уравнений (неравенств)

2.6.3 Синтез серверного приложения, которое может взаимодействовать с различными клиентами и при работе с каждым клиентом предоставлять одинаковый уровень сервиса

2.6.4 Синтез серверного приложения, которое может взаимодействовать с заданным клиентом и при работе с данным клиентом предоставлять различные уровни сервиса

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

3 Проверка безопасности веб-сервисов на основе параллельных композиций временных / расширенных автоматов

3.1 Проверка безопасности веб-сервисов на основе параллельных композиций временных автоматов

3.1.1 Временной автомат

3.1.2 Параллельная композиция временных автоматов

3.1.3 Проверка безопасности веб-сервисов

3.2 Проверка безопасности веб-сервисов на основе параллельных композиций расширенных автоматов

3.2.1 Расширенный автомат

3.2.2 Параллельная композиция расширенных автоматов

3.2.3 Построение бинарной параллельной композиции двух расширенных автоматов, где один из автоматов является встроенным компонентом

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

4 Проверка уязвимости веб-сервисов к атакам на основе решения полуавтоматных уравнений относительно операции конкатенации

4.1 Описание наиболее популярных видов атак на веб-сервисы

4.2 Описание известного подхода к обнаружению уязвимостей веб-сервисов к атакам на основе решения полуавтоматных уравнений относительно операции

конкатенации

4.3 Способы решения полуавтоматных уравнений относительно операции конкатенации

4.4 Описание эксперимента по поиску уязвимостей веб-сервиса «ТГУ.Расписание»

4.5 Полуавтомат с таймаутами

4.6 Построение конечно-автоматной абстракции полуавтомата с таймаутами

4.7 Решение уравнений над полуавтоматами с таймаутами на основе конечно -автоматных абстракций

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

Заключение

Список использованной литературы

Приложение А Акт об использовании результатов диссертационной работы в

ООО «Томские транспортные линии»

Приложение Б Акт об использовании результатов диссертационной работы в ООО «Сибирский дом «Кондитерский»

Введение диссертации (часть автореферата) на тему «Конечно-автоматные алгоритмы проверки безопасного функционирования веб-сервисов»

Введение

Актуальность темы исследования. Предоставление различных услуг с использованием сети Интернет способствует появлению большого количества веб-сервисов, т.е. программных систем, обеспечивающих взаимодействие между поставщиком сервиса и клиентом [37, 38, 95]. Клиентское приложение отправляет на сервер запрос, удовлетворяющий правилам протокола передачи данных, который обрабатывается сервером. После обработки запроса или ряда запросов сервер отправляет клиенту ответ, который является результатом обработки запроса, например, запрашиваемой информацией или сообщением об ошибке.

В случае если функциональность одного веб-сервиса не удовлетворяет разработчика, то можно скомбинировать несколько существующих сервисов вместе, т.е. построить композицию веб-сервисов [36].

Реализации веб-сервисов обычно являются кроссплатформенными, поскольку не важно, где физически располагаются компоненты сервиса и/или язык, на котором написан тот или иной модуль сервисной системы. Соответственно, сервисные компоненты могут быть реализованы разными разработчиками, которые обычно не делятся деталями реализации. В связи с этим важной становится не только проверка функциональности сервисных компонентов [37, 67], но и проверка робастности и безопасности как отдельных сервисов, так и их композиций [67, 69, 72, 75, 76, 102]. Такая проверка позволяет убедиться в том, что при использовании реализации стороннего разработчика, даже если будет отправлен «неверный» запрос, система не будет «разрушена» и такой клиент не сможет «добраться» до данных, которые ему не предназначены. Система должна или не принимать недопустимые входные данные, или обрабатывать их путем создания соответствующих сообщений для пользователя. В настоящее время в сети Интернет в свободном доступе находится очень много сервисов, и, соответственно, возникает вопрос о безопасном выборе компонентов при разработке композиционного сервиса.

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

Степень разработанности темы исследования. Несмотря на большое число различных публикаций, задачи проверки робастности и безопасности веб -сервисов решены только для ряда частных случаев [22, 59, 69, 71, 72, 73, 75, 76, 80, 102].

Для эффективного решения задач проверки робастности и безопасности (композиций) веб-сервисов необходимо определить математическую модель, используемую для описания поведения компонентов и системы в целом, и правила совместного функционирования элементов системы. В настоящее время в качестве таких моделей активно используются модели с конечным числом состояний, в частности, конечно-автоматные модели [1, 5, 15, 16, 40, 56, 70, 90]. В этом случае ряд задач анализа многокомпонентных веб-сервисов можно свести к решению таких задач для композиций конечных автоматов, для которых существуют хорошо разработанные методы и алгоритмы решения [15, 90]. Однако далеко не все такие методы и алгоритмы адаптированы для решения задач анализа веб-сервисов.

Целью работы является разработка и применение методов и алгоритмов анализа (композиций) конечных автоматов для проверки робастности и безопасности (многокомпонентных) веб-сервисов.

Для достижения поставленной цели необходимо решить следующие задачи:

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

а) алгоритм для проверки наличия недопустимых входных последовательностей на входе каждого компонента композиции;

б) алгоритм проверки неопределенных переходов компонента, если на входе компонента могут появиться входные последовательности, не описанные в руководстве для пользователя.

2. Исследовать возможность применения конечно-автоматных алгоритмов для выбора безопасного компонента в многокомпонентной системе.

3. Адаптировать алгоритм решения бинарных полуавтоматных уравнений, который используется для проверки уязвимости веб-сервисов, для решения уравнений относительно полуавтоматов с таймаутами, поскольку для описания семейства небезопасных входных последовательностей могут потребоваться временные аспекты.

4. Провести предварительные исследования возможности использования предложенных алгоритмов для проверки робастности / безопасности для реальных веб-сервисов.

Научная новизна.

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

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

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

автоматов, в которых области определения контекстных переменных и входных параметров автоматов-компонентов могут быть бесконечными.

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

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

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

Положения, выносимые на защиту.

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

2. Алгоритм построения тестовых последовательностей для проверки поведения бинарной параллельной композиции (временных) автоматов на входных последовательностях, инициирующих неопределенные входные последовательности для частичных автоматов, компонентов композиции.

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

тупиковых ситуаций в многокомпонентной композиции веб-сервисов (если это возможно).

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

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

Реализация и внедрение результатов работы. Исследования, результаты которых представлены в данной работе проводились в рамках следующих проектов:

1) НИР "Исследование и разработка вероятностных, статистических и логических методов и средств оценки качества компонентов телекоммуникационных систем" в рамках проектной части госзадания РФ № 739.

2) Проект РНФ № 16-49-03012 "Надежность, безопасность и доверие в системах, используемых в качестве сервисов: масштабируемые решения для эффективного анализа и менеджмента".

Результаты работы были использованы на предприятиях ООО «Томские транспортные линии» (Томск) и ООО «Сибирский дом «Кондитерский» (Томск) для проверки производственных веб-сервисов на наличие тупиковых ситуаций, робастности, а также на наличие возможностей осуществления XSS атак (межсайтовый скриптинг) и SQL-инъекций (приложения А и Б).

Апробация работы. Основные положения и результаты, представленные в работе, обсуждались на следующих конференциях:

Российская конференция с международным участием «Новые информационные технологии в исследовании сложных структур» (Алтай, Россия,

2012; Алтай, Россия, 2014; Екатеринбург, Россия, 2016; Алтай, Россия, 2018; Томск, Россия, 2020; Байкал, Россия, 2022);

Международная научно-практическая конференция «Актуальные проблемы радиофизики» (Томск, Россия, 2012 и 2013);

Международная конференция «IEEE Сибирская конференция по управлению и связи» (Омск, Россия, 2015);

Международная конференция «IEEE East-West Design & Test Symposium» (Ереван, Армения, 2016; Казань, Россия, 2018);

Международная конференция «International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices» (Алтай, Россия, 2017);

Международная конференция «International Conference of Young Professionals in Electron Devices and Materials» (Алтай, Россия, 2021);

Международная конференция «Spring/Summer Young Researchers' Colloquium on Software Engineering» (Москва, Россия, 2022);

Международная конференция студентов, аспирантов и молодых ученых «Перспективы развития фундаментальных наук» (Томск, Россия, 2023).

Публикации. По теме диссертации Е. В. Широковой опубликовано 15 работ, в том числе 4 статьи в журналах, включенных в Перечень рецензируемых научных изданий, в которых должны быть опубликованы основные научные результаты диссертаций на соискание ученой степени кандидата наук, на соискание ученой степени доктора наук (из них 1 статья в российском научном журнале, входящим в Web of Science) [11, 13, 30, 33], 5 публикаций в сборниках материалов международных конференций, представленных в изданиях, входящих в Scopus [47, 48, 64, 65, 87], 6 статей в сборниках материалов международных и всероссийских (в том числе с международным участием) научных конференций [9, 10, 12, 14, 31, 32].

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка использованной литературы, двух приложений. Список использованной литературы включает 103 наименования, 69 из них на

иностранном языке. Диссертация содержит 28 рисунков, 1 таблицу. Объем диссертации составляет 131 страницу.

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

Первая глава содержит основные определения и обозначения, которые используются в работе. В разделе 1.1 приводятся определение и описание работы веб-сервисов, используемых для предоставления различных услуг через Интернет. В случае, если функциональность одного веб-сервиса не удовлетворяет пользователя, то можно скомбинировать несколько существующих сервисов вместе. Результат такой комбинации называется композицией веб-сервисов. Композиция сервисов может быть организована методами оркестровки или хореографии [36]. При оркестровке веб-сервисы находятся под контролем так называемого дирижера, который координирует взаимодействие веб-сервисов, участвующих в композиции. Вызванные веб-сервисы «не знают», что они участвуют в композиции. При хореографии каждый веб-сервис, участвующий в композиции, должен точно «знать» когда начинать активность и с кем он должен взаимодействовать. В некотором смысле организация композиции веб-сервисов методом оркестровки похожа на параллельную композицию систем переходов [90], где компоненты взаимодействуют в режиме диалога. Мы воспользуемся таким формальным описанием, когда поведение сервисов-компонентов описано автоматными моделями.

В разделе отмечается, что в веб-сервисах могут присутствовать компоненты от различных разработчиков [22], которые обычно не делятся деталями реализации, и достаточно часто функциональность таких компонентов описана недостаточно. В связи с этим важно проверять безопасность и робастность используемых объектов (веб-сервисов). Веб-сервис является безопасным, если на его компоненты могут поступать только определенные в их спецификациях входные данные. При взаимодействии компонентов веб-сервисов не должно

возникать зацикливаний и тупиковых ситуаций. Если сервис не является безопасным, то важно проверить его робастность [58]. Такая проверка позволяет убедиться в том, что даже если пользователем будет отправлен «неверный» запрос, то система не будет "разрушена", и такой пользователь не сможет «добраться» до данных, которые ему не предназначены. Веб-сервис должен или не принимать недопустимые входные данные, или обрабатывать их путем создания соответствующих сообщений для пользователя.

В настоящей диссертации для анализа работы веб-сервисов адаптируются конечно-автоматные методы, часто используемые для анализа веб-сервисов и их композиций [17, 90], и соответственно, в разделах 1.2-1.5 приводятся определения конечного автомата, конечного полуавтомата, бинарной композиции конечных автоматов, примеры использования автоматных моделей и их композиций для описания поведения веб-сервисов.

Инициальным конечным автоматом или просто конечным автоматом [1, 5, 15, 16, 77, 90] называется пятёрка 5 = (Я I, O, Ts, so), где £ - непустое конечное множество состояний с выделенным начальным состоянием so, I - непустое множество входных символов, называемое входным алфавитом, О - непустое множество выходных символов, называемое выходным алфавитом, с I х £ х £ х О - отношение переходов. Автомат называется полностью определенным, если из каждого его состоянии для каждого входного действия существует, по крайней мере, один переход. В противном случае автомат называется частичным. Автомат называется детерминированным, если из каждого его состоянии для каждого входного действия существует не более одного перехода. В противном случае автомат называется недетерминированным. Инициальные автоматы описывают поведение систем с известным начальным состоянием и используются для описания поведения систем, которые преобразуют последовательности в одном (входном) алфавите I в последовательности в другом (выходном) алфавите О. Для анализа различных характеристик веб-сервисов также используются конечные полуавтоматы, в которых действия не обязательно

разделяются на входные и выходные. Конечным полуавтоматом [15, 90, 56] называется пятёрка Р = J, Tp, p0, Fp), где P - непустое конечное множество состояний с выделенным начальным состоянием p0 и подмножеством Fp финальных состояний. J - алфавит, Tp с J х P х P - отношение переходов.

Для представления веб-сервиса в виде композиции других, более простых в некотором смысле компонентов, необходимо определить операцию композиции. В настоящей работе мы используем параллельную композицию [15, 90], которая достаточно адекватно описывает поведение взаимодействующих сервисных систем, поскольку последние обычно также работают в диалоговом режиме. Таким образом, компоненты некоторой системы, поведение которых описано конечными автоматами, взаимодействуют в режиме диалога посредством обмена слов в их языках. Соответственно, в каждый момент времени активным является только один компонент, и такое функционирование можно описать с использованием операции параллельной композиции автоматов-компонентов при так называемой «медленной» внешней среде. При подаче внешнего входного сигнала на один из компонентов этот компонент вырабатывает внешний или внутренний выходной сигнал. Если компонент вырабатывает внутренний сигнал, то компоненты работают в режиме диалога, пока компоненты не перестанут обмениваться внутренними сигналами. После этого композиция готова обработать следующий внешний входной сигнал. Задача построения параллельной композиции классических конечных автоматов хорошо изучена. В настоящей диссертации для построения композиции автоматов применяется подход на основе перехода к полуавтоматам [15, 90], а также подход на основе построения дерева достижимости [50].

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

символы могут поступать только на клиентское приложение, в то время как серверное приложение является встроенным компонентом [22].

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

Если при проверке безопасности работы веб-сервиса предполагается, что компоненты описываются частичными автоматами, то необходимо исследовать, какие входные последовательности безопасны, т.е. не приводят к тупиковым ситуациям (deadlock), то есть ситуациям, когда на компоненты композиции могут поступить входные последовательности, на которых их поведение не определено; или к зацикливаниям (осцилляциям) (livelock), то есть ситуациям, когда на компоненты композиции могут поступить входные последовательности, которые инициируют бесконечный диалог между компонентами композиции. В случае, если известно, что композиция, описывающая взаимодействие компонентов веб-сервиса, не является безопасной, то необходимо осуществить проверку робастности веб-сервиса. Реализация компонента (композиции) называется робастной, если при подаче неопределенных входных данных генерируется специальное сообщение либо реализация компонента (композиции) не принимает такие последовательности.

Задача проверки безопасности многокомпонентных систем изучалась в различных работах. Раздел 2.1 содержит краткий обзор известных подходов. Например, в [2, 3, 43, 90] для проверки безопасности предлагается рассматривать глобальную модель всей системы. Так как построение глобального автомата композиции, описывающей взаимодействие компонентов системы, является

довольно трудоемкой задачей, то интересной является задача проверки безопасности композиции без построения такого автомата. В работах [6-8] предлагаются условия, позволяющие определять осцилляции в параллельной композиции автоматов без построения глобального автомата.

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

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

Для случая, когда при взаимодействии компонентов веб-сервиса возникают тупиковые ситуации, в разделе 2.3 предлагается способ решения этой проблемы. Сначала предлагается определить недопустимые для серверного приложения

входные последовательности, а затем можно «ограничить» клиентское приложение. Это приведет к тому, что клиентское приложение не будет генерировать внутренние последовательности, которые являются недопустимыми для серверного приложения.

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

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

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

соответствующее безопасное приложение (раздел 2.6). Задача синтеза одного из компонентов бинарной безопасной композиции может быть решена с помощью автоматных уравнений [15, 18, 41, 86, 90, 100, 101]. Особый интерес представляют живые (compositionally progressive) решения уравнения [4, 17, 51], поскольку в этом случае композиция известного компонента с живым детерминированным решением уравнения является полностью определенным автоматом, т.е. композиция не содержит осцилляций.

В случае, когда необходимо синтезировать компонент системы, который должен работать в различных контекстах и, при работе в каждом контексте предоставлять свой уровень сервиса, задачу синтеза такого компонента можно свести к решению системы параллельных автоматных уравнений, если поведение всех компонентов системы описано конечными автоматами [15]. Задача нахождения наибольшего (живого) решения автоматного уравнения имеет экспоненциальную сложность относительно размеров автоматов, коэффициентов уравнений [17]. В то же время, общее решение системы уравнений является пересечением наибольших решений уравнений. Также необходимо проверить работу каждой комбинации клиент-сервер на отсутствие тупиковых ситуаций. В связи с этим интересной является задача о возможности сведении системы автоматных неравенств (уравнений) к решению одного неравенства (уравнения), для решения которого можно использовать более практические методы нахождения решения, т.е. обойтись без нахождения наибольшего живого решения, а в некоторых случаях и без построения наибольшего решения уравнения [17].

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

Список литературы диссертационного исследования кандидат наук Широкова Екатерина Владимировна, 2025 год

Список использованной литературы

1. Агибалов Г. П. Лекции по теории конечных автоматов. / Г. П. Агибалов, А. М. Оранов // Томск : Издательство ТГУ. - 1984. - 185 с.

2. Бурдонов И. Б. Теория соответствия для систем с блокировками и разрушениями / И. Б. Бурдонов, А. С. Косачев, В. В. Кулямин. - М. : ФИЗМАТЛИТ, 2008. - 412 с.

3. Бурдонов И. Б. Семантики взаимодействия с отказами, дивергенцией и разрушением. Часть 1. Гипотеза о безопасности и безопасная конформность / И. Б. Бурдонов, А. С. Косачев // Вестник Томского государственного университета. Управление, вычислительная техника и информатика, - № 4. - 2010. - С. 124-133.

4. Бушков В. Г. К описанию прогрессивных решений параллельного автоматного уравнения / В. Г. Бушков // Прикладная дискретная математика. -2008. - № 1 (1). - С. 120-125.

5. Гилл А. Введение в теорию конечных автоматов / А. Гилл. - М. : Издательство Наука, 1966. - 272 с.

6. Григорьева А. В. Исследование осцилляций в автоматных композициях / А. В. Григорьева // Труды 7-й и 8-й конференций студенческого научно-исследовательского инкубатора. - Томск : Томское университетское издательство. - 2007. - С. 35-37.

7. Григорьева А. В. Исследование тупиков и зацикливаний при взаимодействии дискретных систем / А. В. Григорьева // Выпускная квалификационная работа. - Томск. - 2007.

8. Григорьева А. В. К пассивному тестированию взаимодействующих элементов телекоммуникационных систем / А. В. Григорьева // Наука. Технологии. Инновации : Материалы всероссийской научной конференции молодых ученых в 7-ми частях. - Новосибирск : Изд-во НГТУ. - 2006. - Часть 1. - 193 с.

9. Дарусенкова (Широкова) Е. В. К анализу безопасной работы параллельной композиции частичных автоматов / Е. В. Дарусенкова (Широкова) //

Новые информационные технологии в исследовании сложных структур : материалы 11-й международной конференции, 06-10 июня 2016 г. - Томск : Издательский Дом ТГУ. - 2016. - С. 49-50.

10. Дарусенкова (Широкова) Е. В. К построению параллельной композиции расширенных автоматов / Е. В. Дарусенкова (Широкова), С. А. Прокопенко, Н. В. Шабалдина // Новые информационные технологии в исследовании сложных структур : материалы Двенадцатой конф. с междунар. участием. Томск, 04-08 июня 2018 г. - Томск : Издательский Дом ТГУ. - 2018. - С. 81-82.

11. Дарусенкова (Широкова) Е. В. Оценка робастности как параметра качества композиции веб-сервисов / Е. В. Дарусенкова (Широкова), О. В. Кондратьева // Известия вузов. Физика. - 2013. - № 9/2. - С. 162-164.

12. Дарусенкова (Широкова) Е. В. Сведение решения системы параллельных автоматных неравенств к решению одного неравенства / Е. В. Дарусенкова (Широкова) // Тезисы докладов десятой российской конференции с международным участием «Новые информационные технологии в исследовании сложных структур». - Томск : Издательский Дом ТГУ. - 2014. - с. 37-38.

13. Дарусенкова (Широкова) Е. В. Тестирование робастности веб-сервисов на основе композиций конечных автоматов / Е. В. Дарусенкова (Широкова), О. В. Кондратьева // Известия вузов. Физика. - 2012. - № 9/2. - С. 339-340.

14. Дарусенкова (Широкова) Е. В. Тестирование робастности веб-сервисов / Е. В. Дарусенкова (Широкова), О. В. Кондратьева // Тезисы докладов девятой российской конференции с международным участием «Новые информационные технологии в исследовании сложных структур». - Томск : Изд-во НТЛ. - 2012. - С. 32.

15. Евтушенко Н. В. Недетерминированные автоматы: анализ и синтез. Ч. 2. Решение автоматных уравнений : учебное пособие / Н. В. Евтушенко, М. В.

Рекун, С. В. Тихомирова // Томск : Томский государственный университет. - 2009.

- 111 с.

16. Евтушенко Н. В. Недетерминированные автоматы: анализ и синтез. Ч. 1. Отношения и операции : учебное пособие / Н. В. Евтушенко, А. Ф. Петренко, М. В. Ветрова. - Томск : Томский государственный университет. - 2006. - 142 с.

17. Жарикова С. В. Метод нахождения прогрессивного решения системы автоматных уравнений / С. В. Жарикова // Доклады V Сибирской научной школы-семинара с международным участием "Компьютерная безопасность и криптография" - SYBECRUPT'06. - 2006. - С. 20-24.

18. Жарикова С. В. Решение автоматных уравнений в различных приложениях / С. В. Жарикова, Н. В. Евтушенко // Вестник Красноярского государственного университета. - 2004. - № 3. - С. 35-39.

19. Карибский В. В. Основы технической диагностики / В. В. Карибский, П. П. Пархоменко, Е. С. Согомонян, В. Ф. Халчев. - М. : Энергия. - 1976. - 464 с.

20. Коломеец А. В. Алгоритмы синтеза проверяющих тестов для управляющих систем на основе расширенных автоматов : диссертация на соискание ученой степени кандидата технических наук. / А. В. Коломеец. - Томск.

- 2010. - 129 с.

21. Кондратьева О. В. Параллельная композиция конечных автоматов с таймаутами / О. В. Кондратьева, Н. В. Евтушенко, А. Р. Кавалли // Вестник Томского государственного университета. Управление, вычислительная техника и информатика. - 2014. - № 2. - С. 73-81.

22. Никитин А. Л. Тестирование робастности многомодульных систем на основе автоматной модели / А. Л. Никитин // Труды 7-й и 8-й конференций студенческого научно-исследовательского инкубатора. - Томск : Томское университетское издательство. - 2011. - С. 121-124.

23. Пакет построения тестов для конечных детерминированных автоматов [Электронный ресурс]. - [Томск], 2020. // URL: http://fsmtestonline.ru (дата обращения: 05.10.2022).

24. Сервис расписания Томского государственного университета [Электронный ресурс]. - [Томск], 2021 // URL: http://schedule.tsu.ru (дата обращения: 20.05.2021).

25. Твардовский А. С. О возможностях автоматного описания параллельной композиции временных автоматов / А. С. Твардовский, А. В. Лапутенко // Труды Института системного программирования РАН. - 2018. - Т. 30, № 1. - С. 25-40.

26. Тейбор Р. Реализация XML Web-служб на платформе Microsoft. NET / Р. Тейбор. - М. : Вильямс. - 2002. - 464 с.

27. Тихомирова С. В. Оптимизация многокомпонентных дискретных систем на основе решения автоматных уравнений : диссертация на соискание ученой степени кандидата технических наук / С. В. Тихомирова. - Томск, 2008. -145 с.

28. Трахтенброт Б. А. Конечные автоматы (поведение и синтез) / Б. А. Трахтенброт, Я. М. Барздинь // Москва : изд-во «Наука». - 1970. - 400 с.

29. Форостьянова М. С. Мутационное тестирование систем, описанных в языке XML, с использованием древовидных автоматов / М. С. Форостьянова // Известия высших учебных заведений. Физика. - 2013. - Т. 56, № 9/2. - С. 193-195.

30. Широкова Е. В. К построению параллельной композиции расширенных автоматов / Е. В. Широкова, С. А. Прокопенко, Н. В. Шабалдина // Вестник Томского государственного университета. Управление, вычислительная техника и информатика. - 2019. - № 48. - С. 83-91. - DOI: 10.17223/19988605/48/10.

31. Широкова Е. В. О решении уравнений для полуавтоматов с таймаутами относительно операции конкатенации / Е. В. Широкова // Перспективы развития фундаментальных наук : сборник трудов XX Международной конференции студентов, аспирантов и молодых ученых (Томск, 25-28 апреля 2023 г.): в 7 т. Т.7 : IT-технологии и электроника. - Томск : Издательство Томского политехнического университета. - 2023. - С. 163-165.

32. Широкова Е. В. Проверка разрешимости уравнений относительно конкатенации для полуавтоматов с таймаутами / Е. В. Широкова, Н. В. Евтушенко // Новые информационные технологии в исследовании сложных структур : материалы четырнадцатой международной конференции, 19-24 сентября 2022 года. - Издательский дом Томского государственного университета. - 2022. - С. 69-70.

33. Широкова Е. В. Синтез безопасных компонентов веб-сервисов на основе решения автоматных уравнений / Е. В. Широкова, Н. В. Евтушенко // Научно-практический журнал "Современная наука: актуальные проблемы теории и практики", серия «Естественные и технические науки». - № 8. - Август 2023. -С. 143-150. - DOI: 10.37882/2223-2982.2023.08.38.

34. Яковлева Т. И. Синтез тестов для расширенных автоматов при ограничении на длину входной последовательности: дипломная работа / Т. И. Яковлева. - Томск. - 2010.

35. Aho A. V. The Theory of Parsing, Translation, and Compiling, Volume I : Parsing / A. V. Aho, J. D. Ullman // Prentice Hall. - 1972. - 1002 p.

36. Albreshne A. Web Servises Orchestration and Composition / A. Albreshne, P. Fuhrer, J. Pasquier // Hewlett-Packard's Dev. Resour. Organ. - 2009. - P. 46-52.

37. Al-Masri E. Quality of web services dataset [Electronic resource] -[Washington], 2007 / E. Al-Masri, Q. H. Mahmoud // 2007. - URL: http://www.uoguelph.ca/~qmahmoud/qws/index.html (access date: 21.02.2021).

38. Al-Masri E.-Investigating web services on the world wide web / E. Al-Masri, Q. H. Mahmoud // Proceedings of the 17th International conference on World Wide Web. - 2008. - P. 795-804.

39. Alur R. A theory of timed automata / R. Alur, D. L. Dill // Theoretical computer science, 126 : 2. - 1994. - P. 183-235.

40. Bochmann G. V. Protocol testing: review of methods and relevance for software testing / G. V. Bochmann, A. Petrenko // Proceedings of the 1994 international

symposium on Software testing and analysis. - Washington, United States. - 1994. - P. 109-124.

41. Bochmann G. V. Using logic to solve the submodule construction problem / G. V. Bochmann // Discrete Event Dynamic Systems. - 2013. - P. 27-59

42. Bresolin D. Deterministic timed finite state machines : Equivalence checking and expressive power / D. Bresolin, K. El-Fakih, T. Villa, N. Yevtushenko // Proceedings of the 5th International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2014. - Verona, Italy. - September 10-12, 2014. - P. 203-216.

43. Burdonov I. B. Theory of correspondence for systems with blocking and destructions / I. B. Burdonov, A. S. Kosachev, V. V. Kulyamin // - Moscow: Fizmatlit. -2008. - 412 p.

44. Campeanu C. A Formal Study of Practical Regular Expressions / C. Campeanu, K. Salomaa, S. Yu // International Journal of Foundations of Computer Science 14 (6). - 2003. - P. 1007-1018.

45. Castagnetti G. Solving parallel equations with BALM-II / G. Castagnetti, M. Piccolo, T. Villa, N. Yevtushenko, A. Mishchenko, R. Brayton // Technical Report No UCB/EECS-2012-181, Electrical Engineering and Computer Sciences University of California at Berkeley. - 2012. - 32 p.

46. Cox R. Regular Expression Matching Can Be Simple And Fast (but is slow in Java, Perl, PHP, Python, Ruby, ...) [Electronic resource] - [Cambridge], 2007 / R. Cox // 2007. - URL: https://swtch.com/~rsc/regexp/regexp1.html (access date: 03.10.2022).

47. Darusenkova (Shirokova) E. Deriving a module of a multiagent system via Finite State Machine equation solving / E. Darusenkova, N. Yevtushenko, T. Villa // Труды XI Международной IEEE Сибирской конференции по управлению и связи SIBC0N-2015. - г. Омск. - 2015.

48. Darusenkova (Shirokova) E. Towards parallel composition of partial finite state machines: checking safety property step-by-step [Electronic resource] - [Yerevan],

2016 / E. Darusenkova, N. Shabaldina // Proceedings of the IEEE East-West Design & Test Symposium (EWDTS). - Yerevan, Armenia, 2016. - URL: http://doi. ieeecomputersociety.org/10.1109/EWDTS.2016.7807689 (access date: 03.10.2022).

49. El-Fakih K. Distinguishing Experiments for Timed Non-Deterministic Finite State Machines / K. El-Fakih, M. Gromov, N. Shabaldina N. Yevtushenko // Acta Cybernetica, 21 : 2. - 2013. - P. 205-222.

50. El-Fakih K. FSM Based Interoperability Testing Methods / K. El-Fakih, V. Trenkaev, N. Spitsyna, N. Yevtushenko // Lecture notes in Computer Science 2978. -2004. - P. 60-75.

51. El-Fakih K. Progressive solutions to FSM equations / K. El-Fakih, N. Yevtushenko // Lecture Notes in Computer Science. - Vol. 5148. - Springer, Berlin, Heidelberg. - 2008. - P. 274-282.

52. Gromov M. Using BALM-II for deriving parallel composition of timed finite state machines with outputs delays and timeouts : work-in-progress / M. Gromov, N. Shabaldina // System Informatics. - № 8. - 2016. - P. 33-42.

53. Gromov M. L. Derivation of the Cascade Parallel Composition of Timed Finite State Machines Using BALM-II / M. L. Gromov, N. V. Shabaldina // Automatic Control and Computer Sciences. - Vol. 51, № 7. - 2017. - P. 507-515.

54. Hartmanis J. Algebraic structure theory of sequential machines / J. Hartmanis, R. E. Stearns // N. J. : Prentice-Hall Inc. Englewood Cliffs. - 1966. - 210 p.

55. Holzmann G. J. Design and validation of computer protocols / G. J. Holzmann // Prentice-Hall, Englewood Cliffs. - 1991. - 500 p.

56. Hopcroft J. Introduction to automata theory, Languages, and Computation / J. Hopcroft, R. Motwani, J. Ullman // Addison-Wesley. - 2001. - 521 p.

57. IBM Web Sphere Service Registry and Repository. - [S. l.], 2015. - URL: http://www.ibm.com/developerworks/downloads/ws/wsrr (access date: 03.10.2022).

58. IEEE_STD610_12-1990 - Glossary of Software Engineering Terminology. - [S. l.], 1990. - URL: http://www.informatik.htw-dresden.de/~hauptman/SEI/IEEE_

Standard_Glossary_of_Software_Engineering_Terminology°/o20.pdf (access date: 15.11.2022).

59. Jimenez W. Software Vulnerabilities, Prevention and Detection Methods. A Review / W. Jimenez, A. Mammar, A. R. Cavalli // Security in model-driven architecture. - Nethderlands. - 2009. - Article number 215995. - 12 p. - URL: https://www.researchgate.net/publication/253704494_Software_Vulnerabilities_Prevent ion_and_Detection_Methods_A_Review_1 (access date: 10.11.2022).

60. Kam T. Synthesis of FSMs: functional optimization / T. Kam, T. Villa, R. Brayton, A. Sangiovanni-Vincentelli // N. Y. : Kluwer Academic Publishers. - 1997. -282 p.

61. Kari L. Insertion and Deletion of Words: Determinism and Reversibility / L. Kari // Mathematical Foundations of Computer Science. - Springer, Berlin, Heidelberg. - 1992. - P. 315-326.

62. Kari L. Maximal and Minimal Solutions to Language Equations / L. Kari, G. Thierrin // Journal of computer and system sciences. - Volume 53. - 1996. - P. 487496.

63. Kari L. On language equations with invertible operations / L. Kari // Theoretical Computer Science. - Volume 132. - 1994. - P. 129-150.

64. Kolomeets A. Checking Robustness of Web Services based on Solving Automata Equations / A. Kolomeets, E. Shirokova, M. Gromov, N. Yevtushenko // 2021 IEEE 22nd International Conference of Young Professionals in Electron Devices and Materials (EDM). - 2021. - P. 499-502. - DOI: 10.1109/EDM52169.2021.9507669.

65. Kolomeets A. V. Using Models of Finite Transition Systems for Checking Web-Service Security / A. V. Kolomeets, N. V. Shabaldina, E. V. Darusenkova (Shirokova), N. V. Yevtushenko // 18th International Conference of Young Specialists on Micro/Nanotechnologies and Electron Devices EDM 2017: proceedings Erlagol, June 29 - July 03, 017. - Novosibirsk: NSTU publisher. - 2017. - P. 151-154.

66. Kondratyeva O. Parallel composition of nondeterministic finite state machines with timeouts / O. Kondratyeva, N. Yevtushenko, A. Cavalli // Journal of Control and Computer Science of Tomsk State University, 2:27. - 2014. - P. 73-81.

67. Kondratyeva O. Timed FSM strategy for optimizing web service compositions w.r.t. the quality and safety issues / O. Kondratyeva // Doctoral thesis. -Paris Saclais. - 2015. - 125 p.

68. Kushik N. Studying the optimal height of the EFSM equivalent for testing telecommunication protocols / N. Kushik, M. Forostyanova, S. Prokopenko, N. Yevtushenko // Proc. of the International Conference on Advances in Computing, Communication and Information Technology. - 2014. - P. 159-163.

69. Laranjeiro N. A robustness testing approach for SOAP Web services / N. Laranjeiro, M. Vieira, H. Madeira // Journal of Internet Services and Applications. -Volume 3, Issue 2. - 2012. - P. 215-232.

70. Lee D. Principles and Methods of Testing Finite State Machine / D. Lee, M. Yannakakis // A Survey, Proceedings of the IEEE 84. - Volume. 8. - 1996. - P. 1090-1123.

71. Lei B. Robustness testing for software components / B. Lei, X. Li, Z. Liu, C. Morisset, V. Stolz. // UNU-IIST. - 2009. - P. 7-38.

72. Lei B. Robustness testing for software components / B. Lei, X. Li, Z. Liu, C. Morisset, V. Stolz // Science of Computer Programming. - Volume 75, Issue 10. -2010. - P. 879-897.

73. Lin C. H. Optimal Sanitization Synthesis for Web Application Vulnerability / C. H. Lin, F. Yu, C. Y. Shueh, Y. F. Chen, B. Y. Wang, T. Bultan // Repair, ISST. -2016. - P. 189-200.

74. Linz P. An Introduction to Formal Languages and Automata / P. Linz // Jones & Bartlett Learning. - 2011. - 427 p.

75. Martin E. Automated Robustness Testing of Web Services / E. Martin, S. Basu, T. Xie // Proceedings of the 4th International Workshop on SOA And Web Services Best Practices. - Portland. - 2006. - P. 25-30.

76. Martins E. Passive approach for robustness testing of communication protocols [Electronic resource] - [Paris], 2008 / E. Martins, A. Morais, A. Cavalli // 2008. - URL: http://www.ic.unicamp.br/~cmrubira/seminario/apresent-eliane.pdf (access date: 02.03.2022).

77. Moore E. F. Gedanken-experiments on Sequential Machines / E. F. Moore // Automata Studies, Annals of Mathematical Studies. - Volume 34. - 1956. - P. 129153.

78. OASIS, Web Services Business Process Execution Language. - [S. l.], 2007. - URL: http://docs.oasis-open.org/wsbpel/2.0/wsbpel-v2.0.pdf (access date: 09.01.2022).

79. Online-community for the Universal Description, and Integration OASIS Standard. - [S. l.], 2013. - URL: http://uddi.xml.org/uddi-org/ (access date: 05.07.2022).

80. OWASP (Open Worldwide Application Security Project). - [S. l.], 2022. -URL: https://www.owasp.org/index.php/Main_Page (access date: 10.07.2022).

81. OWASP Top Ten Web Application Security Risks. - [S. l.], 2022. - URL: https://owasp.org/www-project-top-ten/ (access date: 01.09.2022).

82. Petrenko A. Confirming Configurations in EFSM Testing / A. Petrenko, S. Boroday, R. Groz // IEEE Trans. Software Eng. - Volume 30 (1). - 2004. - P. 29-42.

83. PHP (programming language). - [S. l.], 2022. - URL: https://secure. php.net/ (access date: 03.10.2022).

84. Prokopenko S. Locating a faulty component of an EFSM composition / S. Prokopenko // The Proceedings of ISP RAS. - Volume 26, Issue 6. - 2014. - P. 47-55.

85. RFC 1939 - POP3 Protocol. - [S. l.], 1996. - URL: http://www.rfc2.ru/ 1939.rfc (access date: 27.05.2022).

86. Shabaldina N. Solving parallel multi component automata equations / N. Shabaldina, N. Yevtushenko // Radioelectronics & Informatics Journal. - Volume 1 (40). - 2008. - P. 55-57.

87. Shirokova E. Checking Robustness of Web Services based on the Parallel Composition of Partial Timed Finite State Machines / E. Shirokova // Proceedings of IEEE East-West Desine & Test Symposium (EWDTS'2018). - Kazan. - 2018. - P. 256-261.

88. SQL Injection Cheat Sheet. - [S. l.], 2022. - URL: https://www.netsparker. com/blog/web-security/sql-injection-cheat-sheet/ (access date: 02.04.2022).

89. Stranger (Automata-Based Symbolic String Analysis Library). - [Santa Barbara], 2009. - URL: https://vlab.cs.ucsb.edu/stranger/ (access date: 03.10.2022).

90. Villa T. The Unknown Component Problem. Theory and Applications / T. Villa, N. Yevtushenko, R. K. Brayton, A. Mishchenko, A. Petrenko, A. Sangiovanni-Vincentelli // Berlin: Springer. - 2012. - 312 p.

91. Wang H. E. String Analysis via Automata Manipulation with Logic Circuit Representation / H. E. Wang, T. L. Tsai, C. H. Lin, F. Yu, J. Hong R. Jiang // Computer Aided Verification. - 2016. - P. 241-260.

92. World Wide Web Consortium, Extensible Markup Language. - [S. l.], 2008. - URL: http://www.w3.org/XML/ (access date: 09.11.2022).

93. World Wide Web Consortium, SOAP Version 1.2. - [S. l.], 2007. - URL: http://www.w3.org/TR/soap12-part0/ (access date: 02.11.2022).

94. World Wide Web Consortium, Web Service Choreography Interface. - [S. l.], 2002. - URL: http://www.w3.org/TR/wsci/ (access date: 10.10.2022).

95. World Wide Web Consortium, Web Services Activity. - [S. l.], 2011. -URL: http://www.w3.org/2002/ws/ (access date: 09.11.2022).

96. World Wide Web Consortium, Web Services Choreography Description Language. - [S. l.], 2005. - URL: http://www.w3.org/TR/ws-cdl-10/ (access date: 10.10.2022).

97. World Wide Web Consortium, Web Services Description Language. - [S. l.], 2007. - URL: http://www.w3.org/TR/wsdl/ (access date: 08.10.2022).

98. XMethods. - [S. l.], 2002. - URL: http://www.xmethods.net (access date: 23.03.2021).

99. XSS Filter Evasion Cheat Sheet. - [S. l.], 2022. - URL: https://www. owasp.org/index.php/XSS_Filter_Evasion_Cheat_Sheet (access date: 01.09.2022).

100. Yevtushenko N. Multi Component Digital Circuit Optimization by Solving FSM Equations / N. Yevtushenko, S. Zharikova, M. Vetrova // Euromicro Symposium on Digital System Design, IEEE Computer society. - 2003. - P. 62-68.

101. Yevtushenko N. Solution of Parallel Language Equations for Logic Synthesis / N. Yevtushenko, T. Villa, R. Brayton, A. Petrenko, A. Sangiovanni-Vincentelli // The Proceedings of the International Conference on Computer-Aided Design. - 2001. - P. 103-110.

102. Yu F. Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses / F. Yu, M. Alkhalaf, T. Bultan // Technical Report 2009-11, UCSB CS. - 2009.

103. Zhigulin M. FSM-based test derivation strategies for systems with timeouts / M. Zhigulin, N. Yevtushenko, S. Maag, A. Cavalli // Conference on Quality Software (QSIC'11) : proceedings of 11th International Conference. - Madrid, Spain, July 13-14. - IEEE Publisher. - 2011. - P. 141-149.

Приложение А

Акт об использовании результатов диссертационной работы в ООО «Томские

транспортные линии»

Общество с ограниченной ответственностью «Т Т Л» ИНН: 7017100944 КПП: 701701001

Почтовый адрес; 634021, г. Томск, ул. Шевченко,54

Телефон: [phone], Факс: [phone]____

АКТ ОБ ИСПОЛЬЗОВАНИИ

результатов кандидатской диссертационной работы Широковой Екатерины Владимировны

«УТВЕРЖДАЮ» ДиректошбОО «ТТЛ»

. ^ —"Ильичёв В.В.

¿л^/у 12 декабря .2022 г.

ш

/§Ь

Мы, нижеподписавшиеся, составили настоящий акт об использовании результатов диссертационной работы Широковой Екатерины Владимировны, посвященной применению автоматных композиций и уравнений для проверки безопасной работы и робастности компонентов веб-сервисов.

Краткое описание внедренных результатов работ:

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

- Предложенные алгоритмы проверки веб-сервисов на наличие уязвимостей к атакам на основе решения уравнений над полуавтоматами с таймаутами позволили также проверить ряд веб-сервисов, таких как сервис подачи заявок на грузоперевозки, сервис для расчета тарифа на перевозку, на наличие уязвимостей таких типов, как межсайтовый скриптинг, внедрение 8С>Ь-кода, и убедиться в их отсутствии.

Начальник отдела ИТ Инженер 1-ой категории

Бычков Е.П. Чистяков Р.С.

ВЕРНО

$ЕДУЩ'1Й ДОХУМЕНТОВЕД

-Андриенко й.в.

Приложение Б

Акт об использовании результатов диссертационной работы в ООО «Сибирский

дом «Кондитерский»

634059, г. Томск . проспект Мира, 33, тел. 62-95-19, 62-88-39

«УТВЕРЖДАЮ» Генеральный директор ООО «Сибирский Дбм «КОНДИТЕРСКИЙ»

- --УуГ Шабанов В.А.

25 октября 2022 г.

АКТ ИСПОЛЬЗОВАНИЯ результатов кандидатской диссертационной работы Широковой Екатерины Владимировны

Настоящим актом подтверждается использование результатов диссертационной работы Е.В. Широковой, посвященной проверке безопасного функционирования веб-сервисов на основе автоматных моделей.

Краткое описание использованных результатов работы:

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

В результате проведенной проверки веб-сервиса для продажи товаров была обнаружена уязвимость, а именно возможность внедрения БрЪ-кода. Обнаруженная уязвимость была устранена; после устранения данной уязвимости в веб-сервисе для продажи товаров уязвимостей типа межсайтовый скригттинг, внедрение 80Ь-кода обнаружено не было.

' > / Начальник отдела продаж Нижегородцев В.П.