Preview

Труды Института системного программирования РАН

Расширенный поиск

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

Аннотация

Статья посвящена разработке тестового набора для проверки соответствий реализаций узлов Интернет спецификациям нового протокола безопасности IPsec v2 [1-7]. Для построения тестового набора использовалась технология автоматического тестирования UniTESK [8] и программный пакет CTesK [9], реализующий эту технологию. Работа выполнялась в Институте системного программирования РАН в рамках проекта «Верификация функций безопасности протокола нового поколения IPsec v2» при поддержке гранта РФФИ № 07-07-00243. В ходе ее выполнения были выделены требования к реализациям IPsec v2, разработаны формальные спецификации и прототип тестового набора для верификации реализаций IPsec v2, в том числе реализаций протокола автоматического создания контекстов безопасности IKEv2. В статье описаны метод формализации требований IPsec v2, процесс создания тестового набора, а также результаты тестирования существующих реализаций. Эти результаты показывают, что предложенный в данной работе метод верификации позволяет эффективно автоматизировать тестирование таких сложных протоколов, как протоколы безопасности.

Об авторах

А. В. Никешин
ИСП РАН
Россия


Н. В. Пакулин
ИСП РАН
Россия


В. З. Шнитман
ИСП РАН
Россия


Список литературы

1. RFC4301 S. Kent, K. Seo. Security Architecture for the Internet Protocol December 2005

2. RFC4302 S. Kent. IP Authentication Header S. Kent December

3. RFC4303 S. Kent. IP Encapsulating Security Payload (ESP) December 2005

4. RFC4306 C. Kaufman, Ed. Internet Key Exchange (IKEv2) Protocol December 2005

5. RFC4307 J. Schiller. Cryptographic Algorithms for Use in the Internet Key Exchange Version 2 (IKEv2) December 2005

6. RFC4807 M. Baer, R. Charlet, W. Hardaker, R. Story, C. Wang. IPsec Security Policy Database Configuration MIB March 2007

7. RFC4868 S. Kelly, S. Frankel. Using HMAC-SHA-256, HMAC-SHA-384, and HMAC-SHA-512 with IPsec May 2007

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

9. CTesK 2.1: SeC Language Reference. М.: ИСП РАН, 2005. 167 с.

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

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

12. IETF RFC 2223. J. Postel, J. Reynolds. Instructions to RFC Authors. IETF, 1997. 20 с.

13. IETF BCP 14 | IETF RFC 2119. S. Bradner. Key words for use in RFCs to Indicate Requirement Levels. IETF, 1997. 3 с.

14. IETF RFC 1213. K. McCloghrie, M. T. Rose. Management Information Base for Network Management of TCP/IP-based internets: MIB-II. March 1991.

15. IETF RFC 2011 K. McCloghrie, Ed. SNMPv2 Management Information Base for the Internet Protocol using SMIv2. November 1996.

16. IETF RFC 1831. R. Srinivasan. RPC: Remote Procedure Call Protocol Specification Version 2, 1995.

17. IETF RFC 1832. R. Srinivasan, XDR: External Data Representation Standard, 1995.


Рецензия

Для цитирования:


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

For citation:


Nikeshin A.V., Pakulin N.V., Shnitman. V.Z. Conformance test suite for implementations of the security protocol suite IPsec v2. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2010;18. (In Russ.)



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)