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