Применение моделей для тестирования протоколов безопасности Шнитман В. З. vzs@ispras.ruvzs@ispras.ru Никешин А. В. alexn@ispras.rualexn@ispras.ru Пакулин. - презентация

1 Применение моделей для тестирования протоколов безопасности Шнитман В. З. Никешин А. В. Пакулин Н. В. Институт системного программирования РАН

2 План презентации Введение Представление о протоколах безопасности Пример : TLS/SSL Задачи тестирования Автоматизация тестирования : модели Наш метод моделирования протоколов Один из результатов : тестовый набор для TLS/SSL Обсуждение. Направления дальнейших исследований 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 2

3 Протоколы безопасности Телекоммуникационные протоколы, использующие криптографические средства для обеспечения Конфиденциальности данных Целостности данных Аутентификации данных или субъектов IPsec, TLS/SSL, EAP, WPA, … 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 3

4 Несколько слов о безопасности Основные функции безопасности в телекоммуникациях : Конфиденциальность данных : предотвращение разглашения данных при передаче по сетям связи. Шифрование Целостность данных : предотвращение искажения данных при передаче ( модификация, удаление части данных, внедрение новых данных ) Контрольные суммы стойкими хэш - функциями Аутентификация данных : подтверждение идентичности отправителя данных Цифровая подпись 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 4

5 НЕСКОЛЬКО СЛОВ О TLS 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 5

6 Протокол TLS/SSL Пожалуй, наиболее часто используемый протокол безопасности ( эл. почта, HTTPS, web-API мобильных приложений ) Конфиденциальность, целостность, аутентификация Двухуровневый Прикладной уровень – handshake, уведомления, передача прикладных данных Уровень записей (records) – фрагментирование, шифрование, контрольные суммы 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 6

7 Защита данных 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 7 Прикладные данные Фрагментирование Сжатие Контрольная сумма Шифрование Отправка Прикладные данные сжимаются и шифруются в соответствии с текущим состоянием протокола записей TLS Прикладные данные рассматриваются как бинарные последовательности, их семантика или структура не учитываются TLS

8 Установление соединения TLS Клиент ClientHello Client Certificate ClientKeyExchange CertificateVerify ChangeCipherSpec Finished Сервер ServerHello Server Certificate ServerKeyExchange CertificateRequest SerververHelloDone ChangeCipherSpec Finished

9 ТЕСТИРОВАНИЕ СООТВЕТСТВИЯ 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 9

10 Задачи тестирования соответствия Тестирование соответствия – установление степени соответствия реализации стандарту ( протокола ) Зачем ? Основная гипотеза : любые две корректные реализации « договорятся » друг с другом Как ? См. следующие слайды 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 10

11 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 11/1 8 Общепринятая методология тестирования соответствия Тестовый набор состоит из формально заданных тестов, не привязанных к реализации. Цели тестирования (test purposes) описывают ситуации, подлежащие проверке. Цель тестирования реализуется в одном или нескольких тестах. Реализация считается соответствующей спецификации, если все цели тестирования успешно проверены. Тестовый набор Тесты TP

12 Понятие Test Case Абстрактный тестовый набор : набор формально заданных тестов, не привязанный к реализации. ISO 9646, TTCN Дальнейшее развитие TTCN2, TTCN3, UML Testing Profile Для протоколов Интернета : TAHI (Perl + C++), ETSI (TTCN3 + Java) Высокая трудоёмкость разработки тестового набора – тысячи тестов Вынесение вердиктов о корректности наблюдаемого поведения не опирается на модель протокола Нет строгой процедуры оценки полноты тестирования Test SystemSUT input alt reaction1 pass reaction2 inconc fail Тест (Test case) preambula postambula 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 12

13 Применение моделей для тестирования FSM Реализация EFSM FSM a b LTS SDL Estelle LOTOS passfail x z passfail u v Дерево обхода c Протоколы редко описываются FSM Сложные структуры сообщений / состояний : 16/32/64/128 битные поля, списки переменной длины, таблицы, таймеры, сложные функции Недетерминизм : случайные числа, недоопределённость стандартов, управление нагрузкой O(n 3 ) 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 13

14 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса Используемый подход к тестированию соответствия (1) Основан на технологии автоматизированного тестирования UniTESK Реализация Расширение языка Java Модель системы Модель теста Нотация S Контрактная спецификация Конечный автомат, заданный в неизбыточной форме 14

15 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса Предлагаемый подход к тестированию соответствия (2) Формальная спецификация Стандарт протокола (IETF RFC) Тестовый набор Формализация стандарта протокола Формальное задание тестов S 15

16 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса Формальные спецификации S Формальный интерфейс Элемент формального интерфейса 1.Сигнатура : In, Out 2.Контракт : pre, post 3.Выполнение : « эталонная реализация » 4.Набор разбиений пространства In S на конечное число классов эквивалентности 5.Машинно - читаемая нотация ( язык программирования ) Модель состояния системы. Множество допустимых состояний определяется инвариантом Inv. 16

17 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса Формализация стандартов Составление каталога требований и анализ требований Определение состава формального интерфейса S Формализация функциональных требований в пред - и постусловиях S 17

18 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса Неизбыточное задание автомата теста Неизбыточное задание автомата теста есть пятёрка E,s 0m, I, i,A S [ ]E]E = E S×S - отношение эквивалентности модельного состояния. S 0m - начальное модельное состояние А – конструктор конкретных тестовых воздействий I - алфавит обобщённых тестовых воздействий i – итератор обобщ. тестовых воздействий S 18

19 Тестирование соответствия модели Обходчик Автомат теста Определение текущего состояния Итератор обобщённых тестовых воздействий Конструктор конкретных тестовых воздействий 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 19

20 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса Разработка тестов Определение целей тестирования Разработка неизбыточных заданий автоматов тестов Реализация и отладка тестов S S S [ ]E]E = Формальная спецификация протокола Алфавит обобщённых тестовых воздействий Состояние автомата теста Итератор обобщ. и конструктор конкр. тестовых воздействий 20

21 ТЕСТИРОВАНИЕ TLS С ИСПОЛЬЗОВАНИЕ МОДЕЛЕЙ 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 21

22 Тестирование соответствия TLS Существуют коммерческие тестовые наборы Полнота неизвестна Разработаны вручную, test cases Тесты OpenSSL и GnuTLS не проверяют соответствие В основном тестируют внутреннее устройство Есть несколько сценариев для TLS 1 research проект по тестированию TLS On the Adequacy of Statecharts as a Source of Tests for Cryptographic ProtocolsK. R. Jayaram, Aditya P. Mathur, 2008 Небольшое покрытие спецификации 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 22

23 Результаты Проведен анализ стандарта TLS Извлечены 300 требований Разработана модель TLS 5 тыс. строк, Java Разработан тестовый набор для тестирования соответствия TLS Тестовые сценарии, 1 тыс. строк, Java Адаптер, 1 тыс. строк, Java Проведено тестирование ряда реализаций 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 23

24 Результаты (2) Почтовый сервер Postfix.2.9.3: OpenSSL 1.0.1c Не всегда отправляет уведомление о разрыве соединения Не всегда принимает уведомления Некорректно обрабатывает ошибки в ClientHello В отдельных ситуациях некорректно обрабатывает длины элементов сообщения Принимает сообщения черезмерной длины Некорректно обрабатывает дубликат ClientHello 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 24

25 Результаты (3) Java Runtime Environment 1.7.0_5 Игнорирует поле длины в сообщениях Handshake Не проверяет поля длин элементов Не осуществляет в ряде случаев проверку номера версии – нарушение критического требования Некорректные сообщения об ошибках 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 25

26 ОБСУЖДЕНИЕ 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 26

27 Результаты Получен новый результат : Разработана модель протокола TLS Разработан тестовый набор для проверки соответствия спецификации TLS Обнаружены отклонения от стандарта в распространенных реализациях В том числе нарушения критических требований 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 27

28 Планы развития Дальнейшее развитие тестового набора : Увеличение покрытия требований – рассмотрение большего количества аномальных ситуаций Добавление расширений TLS Упрощение генерации и анализа логов теста Бывает, генерируется до 2 Гб 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 28

29 Практика использования TLS Реализация openssl – стандарт де - факто Тщательная валидация в community Регулярное выявление уязвимостей 2009 год – нарушение целостности, переход TLS год – атака на алгоритм цифровой подписи ЭК, релиз 1.0.1c Apache, Mozilla, Google, сервера и клиенты, … Но … неадекватные сценарии использования Неадекватные настройки : Старые версии (SSL 3.0, TLS 1.0) Слабые алгоритмы (MD5, DES) Неадекватные сертификаты – просрочены, неверные имена, неверные права, самоподписные, … Отсутствие проверок аутентичности 40 из 100 популярных приложений Android не проверяют сертификат сервера Реализованы атаки man-in-the-middle для извлечения паролей, данных банковских карт и т. п. 15 ноября 2012 г. « Инфокоммуникационные технологии в научных исследованиях », Таруса 29