ПРОГРАММИРОВАНИЕ, 2011, No 1, с. 36-56
ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 681.3.06
ВЕРИФИКАЦИЯ ФУНКЦИЙ БЕЗОПАСНОСТИ ПРОТОКОЛА
IPSEC V2
© 2011 г. А. В. Никешин, Н. В. Пакулин, В. З. Шнитман
Институт системного программирования РАН 109004 Москва, ул. Александра Солженицына, 25 E-mail: vzs@ispras.ru, npak@ispras.ru Поступила в редакцию 14.04.2010 г.
Статья посвящена разработке тестового набора для проверки соответствий реализаций узлов Интернет спецификациям нового протокола безопасности IPsec v2 [1-7]. Для построения тестового набора использовалась технология автоматического тестирования UniTESK [8] и программный пакет CTesK [9], реализующий эту технологию. Работа выполнялась в Институте системного программирования РАН в рамках проекта «Верификация функций безопасности протокола нового поколения IPsec v2» при поддержке гранта РФФИ 07-07-00243. В ходе ее выполнения были выделены требования к реализациям IPsec v2, разработаны формальные спецификации и прототип тестового набора для верификации реализаций IPsec v2, в том числе реализаций протокола автоматического создания контекстов безопасности IKEv2. В статье описаны метод формализации требований IPsec v2, процесс создания тестового набора, а также результаты тестирования существующих реализаций. Эти результаты показывают, что предложенный в данной работе метод верификации позволяет эффективно автоматизировать тестирование таких сложных протоколов, как протоколы безопасности.
1. ВВЕДЕНИЕ
Под семейством протоколов IPsec обычно понимается вся совокупность технических средств, обеспечивающих защиту передачи данных на уровне IP. В настоящее время эксплуатируются две несовместимые версии IPsec, которые обычно обозначаются как IPsec v1 и IPsec v2. В данной статье под IPsec мы будем понимать исключительно IPsec v2.
Семейство протоколов IPsec представляет собой инфраструктуру безопасности: спецификации IPsec v2 включают описание архитектуры обеспечения безопасности передачи данных в сетях IP, собственно протоколы защиты данных Authentication Header (AH) и Encapsulating Security Payload (ESP), протокол автоматического установления защищённого соединения Internet Key Exchange (IKEv2), а также криптографические алгоритмы аутентификации и шифрования [1-7].
Семейство IPsec предоставляет целую сово-
купность сервисов безопасности: контроль доступа, целостность в режиме без установления соединения (целостность дейтаграмм), аутентификацию источника данных, обнаружение и отклонение повторно воспроизводимых сообщений (вид частичной целостности последовательности сообщений), конфиденциальность данных и ограниченную конфиденциальность потоков трафика. Эти сервисы предоставляются на сетевом уровне и обеспечивают прозрачность для протоколов транспортного и верхнего уровней. IPsec предлагает единый стандартный метод защиты для всех протоколов, которые могут работать поверх IP (включая сам IP). Кроме того, IPsec v2 включает спецификацию минимальной функциональности межсетевых экранов, поскольку она является существенным аспектом организации контроля доступа на уровне IP.
Задачу тестирования соответствия можно условно разделить на две подзадачи: построение тестовых воздействий и оценка правильности
наблюдаемых результатов. К первой задаче примыкает проблема оценки полноты покрытия, -чем шире будет спектр тестовых воздействий, тем шире получится охват функций протокола при тестировании. Вторая задача заключается в вынесении вердикта о соответствии тестируемой системы спецификации протокола.
Разработанный метод верификации [10] основан на автоматизированном тестировании соответствия формальным спецификациям. Требования, представленные в тексте стандарта, изложены на английском языке и представляют собой неформальный текст, описывающий желаемое поведение системы на естественном языке. Для того, чтобы автоматизировано извлечь тесты для протокола, необходимо перевести его спецификацию в вид, пригодный для решений этой задачи. В разработанном подходе в этой роли выступают формальные спецификации, в которых требования задаются как логические выражения, записанные посредством математического формализма.
В основе подхода лежит представление протоколов как асинхронных автоматов, причем автомат задаётся неявно посредством контрактных спецификаций. А именно, формальное описание поведения протокола задаётся как контрактная спецификация: набор сообщений протокола рассматривается как некоторый формальный интерфейс между реализацией протокола и её окружением, поведение протокола описывается посредством пред- и постусловий. Такое задание протоколов позволяет описывать поведение сложных недетерминированных протоколов, таких как протоколы защиты передачи данных в сетях 1Р. Эти протоколы отличаются сложными структурами данных сообщений и состояния, недетерминированным поведением и неполными спецификациями - в спецификациях умышленно оставлены пробелы для облегчения реализации протоколов. Контрактные спецификации позволяют представлять требования к сложным протоколам в форме, пригодной для автоматизированного тестирования реализаций таких протоколов. Для протоколов, формальная спецификация которых задана в виде контрактной спецификации, разработан метод автоматизированного построения тестовых последовательностей с полностью автоматическим вынесением вердик-
тов о соответствии наблюдаемого поведения реализации её спецификации. В совокупности разработанные методы позволяют автоматизировать тестирование соответствия реализаций сложных сетевых протоколов их спецификациям.
В рамках предложенного метода тест представляет собой конечный автомат. С каждым переходом автомата сопоставлено определённое тестовое воздействие. При выполнении перехода это воздействие подаётся на тестируемую реализацию, регистрируются реакции реализации и автоматически выносится вердикт о соответствии наблюдаемого поведения спецификации. Обход автомата теста совершается автоматически во время тестирования, алгоритм обхода не зависит от протокола, тестируемой реализации или конкретного теста. Последовательность переходов определяет тестовую последовательность. В силу недетерминизма протоколов и различий в поддержке необязательных функций в реализациях конкретные тестовые последовательности, получаемые при прогоне тестов на разных реализациях, могут не совпадать друг с другом.
Предложенный подход к верификации функций безопасности включает два метода: метод формализации стандартов протоколов и метод формального задания тестовых наборов [11]. Метод формализации стандартов протоколов включает анализ спецификации протокола и извлечение требований, определение формального интерфейса протокола, формализацию функциональных требований к реализации протокола, задание критериев покрытия и разработку функции реконструкции состояния. Метод формализации тестовых последовательностей состоит из определения целей тестирования, разработки проекта автомата теста для конкретной цели тестирования, задания переходов автомата теста, задания функции определения состояния автомата теста по модельному состоянию контрактной спецификации протокола, проектирования настроечной информации автомата теста и разработки формата для представления опций, а также включает прогон тестового сценария и анализ результатов тестирования. Для описания автоматов тестов в данном методе используется специальный вид задания автоматов тестов, который называется тестовым сценарием.
2. ОБЗОР ПРОЦЕССА ФОРМАЛИЗАЦИИ СПЕЦИФИКАЦИИ IPSEC
2.1. Извлечение требований
Процесс формализации стандартов начинается с извлечения требований - утверждений, определяющих наблюдаемое поведение реализации протокола в зависимости от внутреннего состояния реализации и входных воздействий, оказываемых на неё окружением. Требования к протоколам Интернета изложены на английском языке в документах, называемых по историческим причинам «запросами комментариев» (Request for Comments, RFC).
Для построения формальной спецификации IPsec прежде всего необходимо из этих документов извлечь требования, регламентирующие поведение реализаций протоколов. Процесс извлечения требований связан с решением четырех задач: определение набора документов, регламентирующих протокол, идентификация функциональных требований в регламентирующих документах протокола, сведение требований в каталог и систематизация требований. Ниже этот процесс описан более подробно.
2.1.1. Определение набора документов, регламентирующих протокол
Регламентирующие документы IPsec разрабатываются Комитетом по стандартизации Интернета (Internet Engineering Task Force, IETF). Спецификации протоколов Интернета публикуются в формате IETF RFC [12] на английском языке. Анализ структуры документации начинается с изучения обзоров протоколов Интернета. Цель изучения - обнаружить связи между протоколами и составить список RFC для подробного изучения. В этот список должны быть занесены RFC, которые регламентируют сам протокол, его расширения и дополнения, а так же другие протоколы Интернета, с которыми протокол взаимодействует.
К настоящему моменту разработано более 50-ти документов, регламентирующих различные аспекты IPsec - применение криптографических алгоритмов, параметры настройки, базовые протоколы и т.д. К основным документам, регламентирующим IPsec v2 относятся спецификации [1-4].
2.1.2. Идентификация функциональных требований
Для обеспечения прослеживаемости требований, т.е для создания ссылок из разработанных формальных спецификаций в требования из регламентирующих документов, необходимо представить требования как уникальные именованные сущности. В данной работе эта задача решена составлением каталога требований.
Каталог требований - это список требований, налагаемых регламентирующими документами и общим контекстом предметной области. Каждое требование, извлечённое из документации, каталог привязывает к соответствующему месту в тексте. Одно такое требование обычно соответствует логически замкнутому фрагменту текста, выражающему одно ограничение на элемент функциональности или элемент данных. Каждое требование имеет уникаль
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.