Инструменты для тестирования свойств безопасности

Первые инструменты основаны на модели Долева-Яо, конц 80-х начало 90-х : Interrogator NRL Protocol Analyzer Longley-Rigby В некоторые инструменты были включены техники индуктивного доказательства теорем, например, в NRL Protocol Analyzer, для того, чтобы показать, что размер рассматриваемого пространства достаточен для гарантирования безопасности. Дальнейшие работы: FDR - анализатора моделей универсального назначения - для обнаружения атаки посредника (man-in-the-middle) на протокол Нидхама-Шредера; анализаторов моделей Murφ и ASTRAL; инструментов для доказательства теорем - PVS и Isabelle; Усилия, которые были сделаны по применению анализаторов моделей универсального назначения для верификации протоколов защиты, таких как Murφ и FDR, привели к пониманию того, что анализаторы моделей универсального назначения слабо приспособлены к моделированию злоумышленника. Позднее были разработаны специализированные для протоколов анализаторы моделей Athena, BRUTUS. История разработки

Коммерческие инструменты для тестирования корпоративной безопасности информационных систем, брандмауэров и сетей: STAT Scanner; ISS Scanner; Cybercop. Альтернативой для тестирования безопасности распределенных систем является применение инструментов, в основе которых лежат формальные методы. Для тестирования свойств безопасности и мобильности применяются как специально разработанные для этих целей инструменты, так и существующие инструменты тестирования общего назначения. tiger team- имитирует действия хакеров для нападения на сеть предприятия Современные инструменты для тестирования

NRL Protocol Analyzer Назначение - инструмент для анализа свойств безопасности криптографических протоколов, который основан на формальных методах. Этот инструмент осуществляет автоматическую генерацию инвариантов с целью ограничить потенциально бесконечное пространство состояний. Снабжен языком темпоральной логики NPATRL (NRL Protocol Analyzer Temporal Requirements Language), позволяющим специфицировать требования к протоколу в терминах желательной или нежелательной последовательности событий. Принцип функционирования- полученное пространство исследуется на возможность проведения атак на протоколы и для доказательства безопасности протоколов, даже при потенциально неограниченном числе выполнений протокола или неограниченном числе атак злоумышленника. Протоколы в Анализаторе специфицируются как конечные автоматы, один из них моделирует злоумышленника, который согласно модели Долева-Яо способен читать, изменять или уничтожать записи в потоке информации, а также совершать криптографические операции и взаимодействовать с некоторыми законными пользователями системы. Пользователь Анализатора пытается определить, является ли протокол безопасным с помощью специфицирования небезопасного состояния. Например, можно запросить осуществить поиск состояния, в котором один и тот же ключ принят дважды принципалом (два события происходят), или состояние, в котором отвечающая сторона B принимает некий ключ для взаимодействия с инициатором A, в то время как A не инициировал этот протокол. Анализатор начинает движение из этого состояния и проходит в обратном направлении все маршруты в пространстве состояний, которые заканчиваются либо начальным состоянием, либо недостижимым состоянием. Назначение - для доказательства того, что никакая сторона не будет аутентифицирована некорректно, но не для того, чтобы доказать, что аутентификация завершается всегда. Обеспечивает средства для специфицирования и доказательства индуктивных лемм о недостижимости бесконечных классов состояний, что позволяет во многих случаях проводить исчерпывающее исследование пространства состояний. Особенности применения - анализатор не делает никаких предположений об ограничениях на число выполнений протокола, на количество принципалов, на число интерливинговых выполнений, или на количество применяемых криптографических функций. Все это приводит к бесконечности пространства состояний. Однако Анализатор Анализатор

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

Назначение - анализатор моделей, специально разработанный для протоколов защиты. Принцип функционирования - работает в обратном направлении, стартуя из неисправного состояния, и пытается выявить начальные условия, необходимые для достижения этого состояния. Как и в NRL Protocol Analyzer, состояния поддерживаются как можно более абстрактными. Описывается состояние - наиболее общая ошибка. Инструмент старается соединить это состояние с правой стороной правила. В случае NRL Protocol Analyzer - это правило переписывания, в случае Athena - это правило вывода. По мере продвижения поиска состояния конкретизируются в том смысле, что все больше переменных становятся связанными. Athena использует расширение модели пространства стрендов (strand space) в качестве модели вычислений. Достоинства - благодаря простоте и интуитивности этой модели инструмент Athena обладает неплохой эффективностью. Athena

Назначение - анализ криптографических протоколов, специфицированных в CSP (Communicating sequential processes). Принцип функционирования - каждый агент, выполняющий протокол, моделируется с помощью процесса CSP, который находится либо в состоянии ожидания сообщения, либо посылает сообщение. Каналы используются для взаимодействия между процессами (т.е. между участниками протокола). Кроме того, каналы используются для моделирования злоумышленника и для поддержки трека важных событий в протоколе, таких как точки фиксации. Компилятор Casper позволяет автоматизировать конструирование злоумышленника. Злоумышленник истолковывается как параллельная композиция нескольких процессов, по одному на каждый факт или сообщение, из которых злоумышленник может получить какие- либо сведения о выполнении протокола. Каждый процесс имеет два состояния, в одном он знает сообщение, в другом - нет. Каждый из процессов может сгенерировать ряд событий. Casper создает спецификационный процесс для верификации, который затем используется инструментом FDR для проверки того, что протокол, выполняющийся параллельно со злоумышленником, является уточнением рассматриваемого спецификационного процесса. Под безопасным спецификационным процессом понимается такой процесс, в котором отсутствуют последовательности событий, соответствующие получению злоумышленником секретных сведений. FDR

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

Назначение - доказательства корректности протокола и теорем универсального назначения. правило Паульсона имеет форму: - если некая трасса содержит определенные события, тогда она может быть продолжена с помощью добавления определенного нового события в ее конец Принцип функционирования - Подобно моделям, используемым в Murφ и NRL Protocol Analyzer, протокол в Isabelle специфицируется с помощью набора правил, которые описывают поведение подлинных участников протокола. Эти правила описывают, при каких обстоятельствах агент создает и посылает сообщение. Murφ и NRL Protocol Analyzer используют эти правила для описания состояния, в которое переходит система, когда совершается некое действие или посылается сообщение. В противоположность этому, Паульсон использует эти правила для индуктивного определения множества возможных трасс. Каждое правило Паульсона имеет форму: - если некая трасса содержит определенные события, тогда она может быть продолжена с помощью добавления определенного нового события в ее конец-. Благодаря тому, что дается индуктивное определение для множества трасс в протоколе, доказательство корректности справедливо для произвольного числа протокольных сессий, а не только для модели с конечным числом состояний. Однако, как и в случае NRL Protocol Analyzer, этот инструмент не гарантирует завершения. К тому же не ясно, как осуществлять обратную связь на предмет получения информации о возможных ошибках в протоколе, для которого доказательство корректности не проходит. Особенности применения - метод проверки модели больше подходит для проектировщиков протоколов в целях их отладки. Недостаток - все инструменты, основанные на методе доказательства теорем, имеют общий недостаток, потому что требуют большого взаимодействия с пользователем и глубокого проникновения в суть проблемы при верификации протоколов. Isabelle

Назначение - для автоматизированного анализа протоколов, который в качестве формализма применяет теорию логику BAN. Принцип функционирования - с помощью подхода, названного авторами «генерация теории» (theory generation), инструмент позволяет автоматически закрыть разрывы, присущие логике BAN, между «идеализированным» и конкретным протоколами. Особенности применения - дает возможность доказывать положительные утверждения о протоколах, но не обеспечивает контр примеры. Кроме того, благодаря тому, что инструмент имеет дело с простыми логиками, обеспечивается такой же уровень автоматизации, которым обладают анализаторы моделей. Revere

BRUTUS Инструмент BRUTUS [Mar01] был разработан для верификации протоколов защиты, и по существу является анализатором моделей. BRUTUS позволяет моделировать и анализировать совместно несколько различных протоколов. При его разработке была сделана попытка выделить злоумышленника из модели и закодировать его как набор правил переписывания, которые можно применить к сообщениям во время выполнения протокола (или возможно во время выполнения иного протокола). От ограничения на количество применяемых правил переписывания разработчику не удалось избавиться, однако этот инструмент дает возможность не указывать заранее, о каких сообщениях модель должна сохранять информацию. BRUTUS имеет две компоненты. Одна компонента осуществляет исследование пространства состояний, другая является механизмом, вырабатывающим сообщения, что позволяет моделировать действия злоумышленника. Кроме того, BRUTUS снабжен темпоральной логикой знаний, с помощью которой можно описывать свойства безопасности. Эта логика позволяет специфицировать сведения о том, что не должен знать злоумышленник, и что другие участники должны или не должны знать. Для редукции пространства состояний устанавливается ряд симметрий, которые являются общими для всех моделей протоколов защиты. Кроме того, для сокращения исследуемого пространства состояний применяется метод редукции частичного порядка, суть которого в том. Что относительный порядок некоторых пар действий не существенен для корректного описания модели. Автор отмечает, что поскольку модели, с которыми работает инструмент, всегда являются абстрактными, корректность протокола доказать невозможно. Несмотря на это, инструмент очень полезен в качестве отладчика, и способен выявлять дефекты в протоколах.

AutoFocus В работе [WJ02] описывается моделирование и тестирование систем, критических с точки зрения безопасности, с использованием инструмента AutoFocus. Этот инструмент представляет собой CASE-инструмент для графического специфицирования распределенных систем, который основан на формальном методе Focus [BS01]. AutoFocus обеспечивает симуляцию, генерацию кода, генерацию тестовых последовательностей и формальную верификацию моделируемых систем. Системы описываются в AutoFocus с использованием статического и динамического представлений, которые концептуально подобны аналогичным представлениям в UML-RT. Для моделирования систем, критических с точки зрения безопасности, в AutoFocus были добавлены некоторые аспекты описания свойств безопасности. Сценарии атак злоумышленника встраиваются в спецификацию системы, что стало возможным после добавления атрибутов безопасности в диаграммы SSD (System Structure Diagrams), которые подобны компонентным диаграммам UML и описывают структуру и интерфейс систем. Строится отображение, присваивающее атрибуты безопасности каждому компоненту системы и каналу, на основе которого AutoFocus автоматически производит соответствующие сценарии угроз. Поведение компоненты Intruder должно быть специфицировано с помощью диаграмм State Transition Diagrams или смоделировано в виде программы. Для моделирования транзакций, критических с точки зрения безопасности, вводятся типы данных для ключей, сообщений, и добавляются криптографические операции. Спецификация поведения моделируется с помощью конечных автоматов, которые в AutoFocus представляются в виде STD (State Transition Diagrams), т.е. STD - это пара (Состояния, Переходы). С переходом связывается набор входных локальных переменных и набор выражений на формальном языке Quest, которые могут содержать входные и компонентные переменные (пред- и постусловия). Кроме того, как и для SSD, каждому состоянию и переходу присваивается атрибут безопасности. Для прогонов тестовых сценариев AutoFocus использует трассы событий EETs (Extended Event Traces). В дополнение к сценарию угроз устанавливаются требования безопасности, которые формулируются в терминах предикатов первого порядка на последовательности выполнения. В качестве альтернативы могут быть использованы формулы темпоральной логики, т.к. их можно преобразовать в такие предикаты. Для облегчения описания требований безопасности AutoFocus был дополнен библиотекой шаблонов требований безопасности различного уровня абстракции. С помощью введенных расширений для систем, критически с точки зрения безопасности, инструмент AutoFocus позволяет автоматически генерировать тестовые последовательности из формальной модели безопасности, использовать мутации системной спецификации и сценарий атак. При тестировании конкретной реализации абстрактные тестовые последовательности подвергаются процессу конкретизации.

On-the-Fly Model-CheckerИнструмент OFMC (On-the-Fly Model-Checker) [BMV03], являющийся анализатором моделей для анализа протоколов защиты, комбинирует два метода. Первым является использование инертных (lazy) типов данных [Bas99] для простого способа построения эффективного оперативного анализатора моделей, работающего на бесконечном пространстве состояний. Второй состоит в применении символического метода для моделирования злоумышленника в модели Долева-Яо, чьи действия воспроизводятся оперативно в стиле управления по запросу (demand-driven way). Авторы формализовали применение символического метода для того, чтобы значительно сократить пространство состояний без исключения из рассмотрения каких-либо атак. Подход, названный авторами методом инертного злоумышленника, использует символическое представление с целью избежать явного перечисления возможных сообщений, которые злоумышленник может создавать. Сообщения злоумышленника представляются выражениями с переменными. Поддерживаются ограничения, описывающие, что должно быть сгенерировано и из каких знаний.

Spider Spider [LGL03] представляет собой интегрированную среду для проверки модели протоколов защиты. В Spider протоколы описываются в терминах алгебры процессов (а именно, spy-исчисления). Взаимодействующие процессы с конечным поведением представляются некоей параллельной композицией. Каждый процесс представляет экземпляр отдельной роли в протоколе. Злоумышленник в стиле Dolev-Yao неявно определяется семантикой исчисления, поскольку среда контролирует все события, касающиеся взаимодействия. Свойства безопасности записываются в виде формул темпоральной логики линейного времени. Более конкретно, spy-исчисление имеет семантику, основанную на системах размеченных переходов (LTSs), где трассы являются темпоральной моделью, на которой определяются отношения выполнимости формул темпоральной логики. Алгоритм проверки модели осуществляет поиск в глубину, который проверяет выполнимость формулы на всех трассах, сгенерированных оперативно из типизированной версии исчисления. На этом этапе использованию типов придается окончательный вид для того, чтобы получить конечно-автоматные модели, где число сообщений, исходящих от злоумышленника, конечно. Во время выполнения получаются типизированные версии описания протокола с помощью придания каждой переменной типа из набора базовых типов. Инструмент обладает ощутимой гибкостью, поскольку среда моделирования является абстрактной, и протокол специфицируется один раз для всех случаев, т.к. не типизированное выражение в spy-исчислении допускает семантику бесконечного пространства состояний. После создания такой спецификации из нее полу- автоматизированным способом могут быть получены различные типизированные версии с семантикой конечного пространства состояний с помощью наложения ограничений на типы. Кроме того, использование логики дает возможность не фиксировать заранее класс исследуемых свойств.

CoSeC CoSeC (Compositional Security Checker) [FG97] является инструментом для автоматической верификации некоторых композиционных свойств информационных потоков, который основан на формальной семантике. Спецификация, поступающая на вход CoSeC, пишется на языке Security Process Algebra, который был разработан на основе алгебры процессов и служит для спецификации параллельных систем, где действия принадлежат двум различным уровням конфиденциальности. Свойства, которые можно верифицировать с помощью CoSeC, выводятся из свойства невлияния (Non Interference) [GM82].

TAF-SFT Инструмент TAF-SFT [CB04] предназначен для автоматизированного тестирования функций безопасности. Основополагающей рамочной концепцией служит TAF (Test Automation Framework) [Saf00], которая автоматизирует процесс тестирования системы. Процесс тестирования включает разработку функциональной модели, анализ модели, автоматизированную генерацию тестового кода, автоматизированное выполнение тестов и анализ результатов. Для написания спецификаций используется формальный язык SCR (Software Cost Reduction) [HKLB98]. На основе результирующей поведенческой спецификационной модели TAF-SFT генерирует тестовые векторы. Затем поведенческая модель и тестовые векторы комбинируются со спецификациями интерфейсов продукта для того, чтобы автоматически сгенерировать тестовые драйверы (код выполнения тестов). Тестовый код выполняется над тестируемым продуктом, результаты прогона тестов сравниваются с ожидаемыми результатами, после чего создается тестовый отчет. Качество системы генерации тестов основано на том, насколько хорошо сгенерированные тесты удовлетворяют выбранному критерию покрытия. Для инструмента TAF-SFT в качестве критерия покрытия был выбран критерий покрытия модели, т.е. генератор тестовых векторов будет генерировать, по крайней мере, один тестовый вектор для каждого маршрута модели. Хотя в статье описывается применение этого инструмента к тестированию безопасности коммерческой СУБД, а именно к тестированию функций контроля доступа, авторы утверждают, что TAF-SFT может применяться к тестированию любых функций безопасности, которые могут быть смоделированы на основе опубликованных интерфейсов продукта. Инструмент TAF-SFT применялся для моделирования и генерации тестов также и для таких функций безопасности, как генерация аудита, управление безопасностью, идентификация и аутентификация, управление сеансами. Основным недостатком этого инструмента является то, что от разработчика модели требуется детальное знание семантики функций безопасности. Кроме того, возникает сложность отображения информации, если тестируемый продукт имеет сложные интерфейсы.

MAST Инструмент MAST (Mobile Agent-based Security Tool) [CCS03] предназначен для автоматизированной поддержки безопасности всех систем в отдельном домене или во всей сети. Инструмент проверяет, произведены ли все вышедшие обновления систем в сети, а также выявляет ошибки в конфигурациях систем, которые могут привести к их уязвимостям. Инструмент MAST интегрирует две ключевые технологии - систему мобильных агентов NOMADS [SBB00] и инструменты для концептуальных отображений CmapTools [CFN03]. Концептуальные отображения Новака [Novak] представляют собой графическое представление концепций и их взаимосвязей, которое дает строгое и сжатое описание конкретной области знания. Инструменты CmapTools дают возможность работать с концептуальными отображениями в оперативном режиме. С их помощью можно создавать хранилища концептуальных отображений (которые называются моделями знаний) и разделять их в среде Интернет. Система мобильных агентов NOMADS, основанная на Java- агентах, дает высокую степень мобильности агентов в распределенной сети и обеспечивает защиту системы от различных форм атак.