Опыт верификации реализаций протокола TLS 1.3

Main Article Content

Алексей Вячеславович Никешин
Виктор Зиновьевич Шнитман

Аннотация

Представлен опыт верификации реализаций сервера криптографического протокола TLS версии 1.3. TLS – широко распространенный криптографический протокол, предназначенный для создания защищенных каналов передачи данных и обеспечивающий необходимую для этого функциональность: конфиденциальность передаваемых данных, целостность данных, аутентификацию сторон. Новая версия протокола TLS 1.3 была представлена в августе 2018 года и имеет ряд существенных отличий по сравнению с предыдущей версией 1.2. Ряд разработчиков протокола TLS уже включил поддержку последней версии в свои реализации. Данные обстоятельства делают актуальным проведение исследований в области верификации и безопасности реализаций новой версии протокола TLS. В работе использован новый тестовый набор для верификации реализаций протокола TLS 1.3 на соответствие спецификациям интернета, разработанный на основе спецификации RFC 8446 с использованием технологии UniTESK и методов мутационного тестирования. Текущая работа является частью проекта верификации протокола TLS 1.3 и охватывает часть дополнительной функциональности и необязательных расширений протокола.


Для тестирования реализаций на соответствие формальным спецификациям применена технология UniTESK, предоставляющая средства автоматизации тестирования на основе использования конечных автоматов. Состояния тестируемой системы задают состояния автомата, а тестовые воздействия – переходы этого автомата. При выполнении перехода заданное воздействие передается на тестируемую реализацию, после чего регистрируются реакции реализации и автоматически выносится вердикт о соответствии наблюдаемого поведения спецификации. Мутационные методы тестирования используются для обнаружения нестандартного поведения тестируемой системы с помощью передачи некорректных данных. В поток обмена протокола, создаваемый в соответствии со спецификацией, вносятся некоторые изменения: либо изменяются значения полей сообщений, сформированных на основе разработанной модели протокола, либо изменяется порядок сообщений в потоке обмена. Модель протокола позволяет вносить изменения в поток данных на любом этапе сетевого обмена, что позволяет тестовому сценарию проходить через все значимые состояния протокола и в каждом таком состоянии проводить тестирование реализации в соответствии с заданной программой. На данный момент было обнаружено несколько отклонений реализаций от спецификации.


Представленный подход доказал свою эффективность в нескольких наших проектах при тестировании сетевых протоколов, обеспечив обнаружение различных отклонений от спецификации и других ошибок.

Article Details

Библиографические ссылки

Dierks T., Rescorla E. The Transport Layer Security (TLS) Protocol Version 1.2. August 2008. IETF RFC 5246. URL: https://tools.ietf.org/html/rfc5246
2. Rescorla E. The Transport Layer Security (TLS) Protocol Version 1.3. August 2018. IETF RFC 8446. URL: https://tools.ietf.org/html/rfc8446
3. Eastlake D. Transport Layer Security (TLS) Extensions: Extension Definitions. January 2011. IETF RFC 6066. URL: https://tools.ietf.org/html/rfc6066
4. Thomson M. Record Size Limit Extension for TLS. August 2018. IETF RFC 8449. URL: https://tools.ietf.org/html/rfc8449
5. Bourdonov I., Kossatchev A., Kuliamin V., and Petrenko A. UniTesK Test Suite Architecture // Proceedings of FME 2002. LNCS 2391. P. 77–88, Springer-Verlag, 2002.
6. Java Development Kit 14.0.1 GA. URL: https://jdk.java.net/14/
7. OpenSSL Project. URL: https://www.openssl.org/
8. JavaTESK. URL: http://www.unitesk.ru/content/category/5/25/60/
9. Никешин А.В., Пакулин Н.В., Шнитман В.З. Разработка тестового набора для верификации реализаций протокола безопасности TLS // Труды ИСП РАН. 2012. Т. 23. С. 387–404.
10. Никешин А.В., Пакулин Н.В., Шнитман В.З. Тестирование реализаций клиента протокола TLS // Труды ИСП РАН. 2015.Т. 27, вып. 2. С. 145–160.
11. Никешин А.В., Шнитман В.З. Тестирование соответствия реализаций протокола EAP и его методов спецификациям Интернета // Труды ИСП РАН. 2018. Т. 30, вып. 6. С. 89–104. URL: https://doi.org/10.15514/ISPRAS-2018-30(6)-5