Сборники трудов ИСП РАН


Разработка тестового набора для верификации реализаций протокола безопасности TLS.

А.В. Никешин, Н.В. Пакулин, В.З. Шнитман.

Аннотация

Статья посвящена разработке тестового набора для проверки соответствий реализаций узлов Интернет спецификациям протокола безопасности TLS. Для построения тестового набора использовалась технология автоматического тестирования UniTESK и программный пакет JavaTESK, реализующий эту технологию.

Работа выполнялась в Институте системного программирования РАН в рамках проекта «Верификация реализаций расширяемых протоколов Интернета» при поддержке гранта РФФИ № 10-07-00145. В ходе ее выполнения были выделены требования к реализациям TLS, разработаны формальные спецификации и прототип тестового набора для верификации реализаций TLS. В статье кратко описаны метод формализации требований TLS, тестовый набор, а также результаты тестирования существующих реализаций сервера TLS. Эти результаты показывают, что предложенный в данной работе метод верификации позволяет эффективно автоматизировать тестирование таких сложных протоколов, как протоколы безопасности.

Ключевые слова

тестирование, верификация, формальные методы, формальные спецификации, MBT, тестирование с использованием моделей, модели программ, TLS, SSL, JavaTESK, UniTESK

Издание

Труды Института системного программирования РАН, том 23, 2012, стр. 387-404.

ISSN 2220-6426 (Online), ISSN 2079-8156 (Print).

DOI: 10.15514/ISPRAS-2012-23-22

Полный текст статьи в формате pdf Вернуться к содержанию тома