Тестирование реализаций клиента протокола TLS

При разработке протоколов безопасности особую роль играют задачи обеспечения качества, надёжности и отказоустойчивости реализаций. Разработчики стандартов для таких протоколов ответственно подходят к разработке спецификаций и стараются предусмотреть множество возможных атак для того, чтобы минимизировать риск успешных атак на реализации. Поэтому для надежности реализаций очень важно соответствовать требованиям спецификации протокола, прежде всего в части обработки ошибок во входящих сообщениях или ошибки в последовательности сообщений, так как именно такие ситуации являются основным средством для осуществления атак на реализации протоколов.
Одним из основных инструментов для проверки соответствия реализации стандарту является тестирование. Данная статья продолжает серию работ авторов по автоматизации тестирования соответствия спецификациям протоколов безопаности интернета. В статье описаны результаты работы по созданию тестового набора для тестирования соответствия реализаций клиента протокола TLS спецификациям Интернета. В качестве базы для построения тестов мы использовали технологию UniTESK и программный пакет JavaTesK, реализующий эту технологию. Для построения атакующих воздействий на целевую реализацию использовался подход мутационного тестирования, при котором вместо корректных сообщений строятся их искаженные по определённым правилам копии. Были разработаны операторы мутации для некоторых основных типов данных, которые используются в формальной модели протокола. Подход был апробирован на ряде известных открытых реализаций клиентов протокола TLS. Этот подход доказал свою эффективность, поскольку обеспечил обнаружение отклонений от спецификации и других ошибок во всех выбранных реализациях клиента протокола.