Разработка тестового набора для верификации реализаций протокола безопасности TLS

Статья посвящена разработке тестового набора для проверки соответствий реализаций узлов Интернет спецификациям протокола безопасности TLS. Для построения тестового набора использовалась технология автоматического тестирования UniTESK и программный пакет JavaTESK, реализующий эту технологию. Работа выполнялась в Институте системного программирования РАН в рамках проекта «Верификация реализаций расширяемых протоколов Интернета» при поддержке гранта РФФИ № 10-07-00145. В ходе ее выполнения были выделены требования к реализациям TLS, разработаны формальные спецификации и прототип тестового набора для верификации реализаций TLS. В статье кратко описаны метод формализации требований TLS, тестовый набор, а также результаты тестирования существующих реализаций сервера TLS. Эти результаты показывают, что предложенный в данной работе метод верификации позволяет эффективно автоматизировать тестирование таких сложных протоколов, как протоколы безопасности.

тестирование, верификация, формальные методы, формальные спецификации, MBT, тестирование с использованием моделей, модели программ, TLS, SSL, JavaTESK, UniTESK

1. IETF RFC 2246. Dierks, T. and C. Allen, "The TLS Protocol Version 1.0", January 1999.

2. IETF RFC 3268. Chown, P., "Advanced Encryption Standard (AES) Ciphersuites for Transport Layer Security (TLS)", June 2002.

3. IETF RFC 3546. Blake-Wilson, S., Nystrom, M., Hopwood, D., Mikkelsen, J., and T. Wright, "Transport Layer Security (TLS) Extensions", June 2003.

4. IETF RFC 4346. Dierks, T. and E. Rescorla, "The Transport Layer Security (TLS) Protocol Version 1.1", April 2006.

5. IETF RFC 4366. Blake-Wilson, S., Nystrom, M., Hopwood, D., Mikkelsen, J., and T. Wright, "Transport Layer Security (TLS) Extensions", April 2006.

6. IETF RFC 4507. Salowey, J., Zhou, H., Eronen, P., and H. Tschofenig, "Transport Layer Security (TLS) Session Resumption without Server-Side State", May 2006.

7. IETF RFC 4680. Santesson, S., "TLS Handshake Message for Supplemental Data", October 2006.

8. IETF RFC 4681. Santesson, S., Medvinsky, A., and J. Ball, "TLS User Mapping Extension", October 2006.

9. IETF RFC 5077. Salowey, J., Zhou, H., Eronen, P., and H. Tschofenig, "Transport Layer Security (TLS) Session Resumption without Server-Side State", January 2008.

10. IETF RFC 5246. Dierks, T. and E. Rescorla, "The Transport Layer Security (TLS) Protocol Version 1.2", August 2008.

11. IETF RFC 5746. E. Rescorla, M. Ray, S. Dispensa, N. Oskov. Transport Layer Security (TLS) Renegotiation Indication Extension. February 2010.

12. Bourdonov I., Kossatchev A., Kuliamin V., Petrenko A. UniTesK Test Suite Architecture // Proceedings of FME, LNCS 2391. Springer-Verlag, 2002. P. 77-88.

13. Bourdonov I.B., Demakov A.V., Jarov A.A., Kossatchev A.S., Kuliamin V.V., Petrenko A.K. and Zelenov S.V. Java Specification Extension for Automated Test Development // Proceedings of PSI’2001. Novosibirsk, Russia July 2-6 2001, LNCS 2244:301-307. Springer-Verlag, 2001.

14. Н.В. Пакулин. Формализация стандартов и тестовых наборов протоколов Интернета. Автореферат диссертации на соискание учёной степени кандидата физико-математических наук. Москва, 2006.

15. Н.В. Пакулин, А.В. Хорошилов "Разработка формальных моделей и тестирование соответствия для систем с асинхронными интерфейсами и телекоммуникационных протоколов", Журнал "Программирование" № 5, 2007 г., ISSN 0132-3474, с. 1-29.

16. А.В. Никешин, Н.В. Пакулин, В.З. Шнитман "Разработка тестового набора для верификации реализаций протокола безопасности IPsec v2", Труды Института системного программирования РАН, т. 18, 2010, стр. 151-182.

17. А.В. Никешин, Н.В. Пакулин, В.З. Шнитман "Верификация функций безопасности протокола IPsec v2", Журнал "Программирование" № 1, 2011, стр. 36-56.