Аннотация:
В данной статье представлены результаты проекта по созданию тестового набора для тестирования соответствия реализаций протокола EAP и его методов спецификациям Интернета. В основе проекта лежит использование технологии UniTESK, позволяющей автоматизировать процесс верификации сетевых протоколов на основе их формальных моделей и расширения JavaTesK, реализующего эту технологию на языке программирования. Совместное использование методов мутационного тестирования позволяет протестировать устойчивость реализации протокола к искаженным сообщениям. Данный подход доказал свою эффективность, позволив обнаружить несколько критических уязвимостей и другие отклонения от спецификации в выбранных реализациях протокола.
Ключевые слова:тестирование, верификация, формальные методы, формальные спецификации, тестирование с использованием моделей, безопасность, аутентификация, контроль доступа, EAP, методы EAP, UniTESK, мутационное тестирование.
Полный текст:
PDF файл (497 kB)