Материал конференции: "Научный сервис в сети Интернет: труды XXII Всероссийской научной конференции (21-25 сентября 2020 г., онлайн)"
Авторы:Никешин А.В., Шнитман В.З.
Верификация функций безопасности протокола TLS версии 1.3
Аннотация:
В данной работе представлен опыт верификации реализаций сервера криптографического протокола TLS версии 1.3. TLS является одним из наиболее востребованных криптографических протоколов, предназначенный для создания защищенных каналов передачи данных – одним из основных механизмов защиты информации в современных сетях. Протокол обеспечивает необходимую для своих задач функциональность: конфиденциальность передаваемых данных, целостность данных, аутентификацию сторон. В новой версии протокола TLS 1.3 была существенно переработана архитектура, устранив ряд недостатков предыдущих версий, выявленных как при разработке реализаций, так и в процессе их эксплуатации. В работе использовался новый тестовый набор для верификации реализаций протокола TLS 1.3 на соответствие спецификациям Интернет, разработанный на основе спецификации RFC8446 с использованием технологии UniTESK и методов мутационного тестирования. Для тестирования реализаций на соответствие формальным спецификациям применяется технология UniTESK, предоставляющая средства автоматизации тестирования на основе использования конечных автоматов. Состояния тестируемой системы задают состояния автомата, а тестовые воздействия – переходы этого автомата. При выполнении перехода заданное воздействие передается на тестируемую реализацию, после чего регистрируются реакции реализации и автоматически выносится вердикт о соответствии наблюдаемого поведения спецификации. Мутационные методы тестирования используются для обнаружения нестандартного поведения тестируемой системы (завершение из-за фатальной ошибки, 'подвисание', ошибки доступа к памяти) с помощью передачи некорректных данных, такие ситуации часто остаются за рамками требований спецификаций. В сообщения, сформированные на основе разработанной модели протокола, вносятся какие-либо изменения. Модель протокола позволяет вносить изменения в поток данных на любом этапе сетевого обмена, что позволяет тестовому сценарию проходить через все значимые состояния протокола и в каждом таком состоянии проводить тестирование реализации в соответствие с заданной программой. Представленный подход доказал свою эффективность в наших предыдущих проектах при тестировании сетевых протоколов, обеспечив обнаружение различных отклонений от спецификации и других ошибок.
