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

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

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

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

безопасность, протоколы, тестирование, оценка устойчивости, Интернет, стандарты, формальные методы спецификации

1. 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