Извлечение опорных тестовых наборов из спецификаций криптопротоколов на предметно-ориентированном языке
https://doi.org/10.15514/ISPRAS-2023-35(6)-10
Аннотация
Работа посвящена описанию инструмента тестирования безопасности реализаций криптографических протоколов, работающего на основе спецификаций, написанных на декларативном интероперабельном встроенном предметно-ориентированном языке (emdedded [in Haskell] DSL). Рассмотрена задача формирования качественных опорных тестовых наборов для использования в тестировании безопасности реализаций протоколов. Предложен метод решения этой задачи в контексте представленного инструмента.
Ключевые слова
криптографические протоколы,
формальные спецификации криптографических протоколов,
тестирование криптографических протоколов,
тестирование на основе формальных спецификаций,
EDSL,
виртуальная машина SBSM/С2.
При поддержке: Исследование поддержано грантом Минобрнауки России № 075-15-2020-788.
Об авторе
Сергей Евгеньевич ПРОКОПЬЕВ
Институт системного программирования РАН,
АО «НПК «Криптонит»
Россия
Россия
Cтарший научный сотрудник отдела технологий программирования ИСП РАН, руководитель направления сетевых протоколов безопасности лаборатории сетевой и информационной безопасности АО НПК «Криптонит».
Список литературы
1. H. Kario. Tlsfuzzer. Available at: https://github.com/tomato42/tlsfuzzer, accessed 10.11.2023.
2. M. Ammann, L. Hirschi, S. Kremer. DY Fuzzing: Formal Dolev-Yao Models Meet Cryptographic Protocol Fuzz Testing. https://eprint.iacr.org/2023/057.
3. Пакулин Н.В., Шнитман В.З., Никешин А.В. Разработка тестового набора для верификации реализаций протокола безопасности TLS // Труды Института системного программирования РАН, том 23, 2012 г., стр. 387-404.
4. Kenneth L. McMillan and Lenore D. Zuck. 2019. Formal specification and testing of QUIC. In Proceedings of ACM Special Interest Group on Data Communication (SIGCOMM’19). ACM, New York, NY, USA, 14 pages.
5. ABZ – International Conference on Rigorous State Based Methods, Available at: https://abz-conf.org, accessed 10.11.2023.
6. Прокопьев С.Е. Формальный язык первичных спецификаций криптографических протоколов. Труды ИСП РАН. 2021;33(5):117-136. https://doi.org/10.15514/ISPRAS-2021-33(5)-7.
7. Prokopev, S. Cryptographic protocol conformance testing based on domain-specific state machine. J Comput Virol Hack Tech (2023). https://doi.org/10.1007/s11416-023-00474-1.
Рецензия
Для цитирования:
ПРОКОПЬЕВ С.Е. Извлечение опорных тестовых наборов из спецификаций криптопротоколов на предметно-ориентированном языке. Труды Института системного программирования РАН. 2023;35(6):167-178. https://doi.org/10.15514/ISPRAS-2023-35(6)-10
For citation:
PROKOPEV S.E. Extracting the Reference Test Suites from Cryptographic Protocol Specifications Written on a Domain-Specific Language. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2023;35(6):167-178. (In Russ.) https://doi.org/10.15514/ISPRAS-2023-35(6)-10
Послать статью по эл. почте 