Головная страница ИПМ Библиотеки, издания  •  Поиск публикаций  English 
Публикация

Материал конференции: "Научный сервис в сети Интернет: труды XXII Всероссийской научной конференции (21-25 сентября 2020 г., онлайн)"
Авторы: Никешин А.В., Шнитман В.З.
Верификация функций безопасности протокола TLS версии 1.3
Аннотация:
В данной работе представлен опыт верификации реализаций сервера криптографического протокола TLS версии 1.3. TLS является одним из наиболее востребованных криптографических протоколов, предназначенный для создания защищенных каналов передачи данных – одним из основных механизмов защиты информации в современных сетях. Протокол обеспечивает необходимую для своих задач функциональность: конфиденциальность передаваемых данных, целостность данных, аутентификацию сторон. В новой версии протокола TLS 1.3 была существенно переработана архитектура, устранив ряд недостатков предыдущих версий, выявленных как при разработке реализаций, так и в процессе их эксплуатации. В работе использовался новый тестовый набор для верификации реализаций протокола TLS 1.3 на соответствие спецификациям Интернет, разработанный на основе спецификации RFC8446 с использованием технологии UniTESK и методов мутационного тестирования. Для тестирования реализаций на соответствие формальным спецификациям применяется технология UniTESK, предоставляющая средства автоматизации тестирования на основе использования конечных автоматов. Состояния тестируемой системы задают состояния автомата, а тестовые воздействия – переходы этого автомата. При выполнении перехода заданное воздействие передается на тестируемую реализацию, после чего регистрируются реакции реализации и автоматически выносится вердикт о соответствии наблюдаемого поведения спецификации. Мутационные методы тестирования используются для обнаружения нестандартного поведения тестируемой системы (завершение из-за фатальной ошибки, 'подвисание', ошибки доступа к памяти) с помощью передачи некорректных данных, такие ситуации часто остаются за рамками требований спецификаций. В сообщения, сформированные на основе разработанной модели протокола, вносятся какие-либо изменения. Модель протокола позволяет вносить изменения в поток данных на любом этапе сетевого обмена, что позволяет тестовому сценарию проходить через все значимые состояния протокола и в каждом таком состоянии проводить тестирование реализации в соответствие с заданной программой. Представленный подход доказал свою эффективность в наших предыдущих проектах при тестировании сетевых протоколов, обеспечив обнаружение различных отклонений от спецификации и других ошибок.
Ключевые слова:
безопасность, TSL, TSLv1.3, протоколы, тестирование, оценка устойчивости, Интернет, стандарты, формальные методы спецификации
Язык публикации: русский,  страниц: 12 (с. 515-526)
Полный текст на русском языке: Сведения об авторах:
  • Никешин Алексей Вячеславович,  orcid.org/0000-0001-5781-9736,  ИСП РАН
  • Шнитман Виктор Зиновьевич,  orcid.org/0000-0002-1509-0972,  ИСП РАН