Генерация кода исполняемой модели Event-B на языке Python

Данное исследование проводится в контексте динамической верификации средств защиты информации на основе формальной модели. Процесс верификации можно разбить на два этапа: формальная верификация модели и тестирование реализации с использованием верифицированной модели. Так как многие модели создаются с расчетом на формальную верификацию, для проведения первого этапа уже существуют готовые решения. При этом для тестирования реализации необходимо воспроизвести поведение модели, что является сложной задачей, особенно если рассматривать промышленное применение такого подхода. В статье предлагается возможная методика воспроизведения поведения модели при помощи сгенерированного на основе модели программного кода. Предлагаемая методика нацелена, с одной стороны, на получение эффективного по времени процесса воспроизведения поведения модели, а с другой, на увеличение читаемости программного кода и на визуальное соответствие между кодом и текстом исходной модели. Прозрачность процесса является важным качеством при работе с ответственными системами, а его простота дает возможность для широкого применения технологии на практике.

1. ГОСТ Р 59453.1. Защита информации. Формальная модель управления доступом. Часть 1. Общие положения: описание стандарта и тендеры. – Введен 2021-06-01 – Москва: Стандартинформ, 2021. / State Std. GOST R 59453.1. Information protection. Formal access control model. Part 1. General principles. Moscow, 2021 (in Russian).

2. ГОСТ Р 59453.2. Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификации формальной модели управления доступом. – Введен 2021-06-01 – Москва: Стандартинформ, 2021. / State Std. GOST R 59453.1. Information protection. Recommendations on verification of formal access control model. Part 2. General principles. Moscow, 2021 (in Russian).

3. ГОСТ Р 59453.3. Защита информации. Формальная модель управления доступом. Часть 3. Рекомендации по разработке. – Введен 2025-03-31 – Москва: Стандартинформ, 2025. / State Std. GOST R 59453.3. Information protection. Recommendations on verification of formal access control model. Part 3. Recommendations on development. Moscow, 2025 (in Russian).

4. ГОСТ Р 59453.4. Защита информации. Формальная модель управления доступом. Часть 4. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом. – Введен 2025-03-31 – Москва: Стандартинформ, 2025. / State Std. GOST R 59453.4. Information protection. Recommendations on verification of formal access control model. Part 4. Recommendations for verification of information security features that implement access control policies based on formal descriptions of the access control model. Moscow, 2025 (in Russian).

5. Abrial J.-R., Butler M., Hallerstede S., Hoang T., Mehta F., Voisin L. Rodin: an open toolset for modelling and reasoning in Event-B. The International Journal on Software Tools for Technology Transfer, vol. 12. Springer, 2010, pp. 447–466. DOI: 10.1007/s10009-010-0145-y.

6. Девянин П.Н., Ефремов Д.В., Кулямин В.В., Петренко А.К., Хорошилов А.В.,

7. Щепетков И.В. Моделирование и верификация политик безопасности управления доступом в операционных системах. Горячая линия – Телеком, Москва, Россия, 2019. / Devyanin P.N., Efremov D.V., Kulyamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Modeling and verification of access control security policies in operating systems. Moscow, Russia: Hotline-Telecom, 2019 (in Russian).

8. Ефремов Д.В., Копач В.В., Корныхин Е.В., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы. Труды ИСП РАН, 2021, том 33, вып. 6, стр. 15–26. DOI: 10.15514/ISPRAS-2021-33(6)-2. / Efremov D.V., Kopach V.V., Kornykhin E.V.,

9. Kulyamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Runtime verification of operating systems based on abstract models. Proceedings of ISP RAS, 2021, vol. 33, no. 6, pp. 15–26 (in Russian). DOI: 10.15514/ISPRAS-2021-33(6)-2.

10. Девянин П.Н., Леонова М.А. Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB. ПДМ, 2021, № 52, стр. 83–96. DOI: 10.17223/20710410/52/5. / Devyanin P.N., Leonova M.A. The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB. Prikladnaya Diskretnaya Matematica, 2021, no. 52, pp. 83–96, (in Russian). DOI: 10.17223/20710410/52/5.

11. Карнов А.А. Проблема неопределенности в анализе трасс на основе высокоуровневых моделей в контексте динамической верификации. Труды ИСП РАН, 2024, том 36, вып. 4, стр. 169–182. DOI: 10.15514/ISPRAS-2024-36(4)-13 / Karnov A.A. Uncertainty Problem in High-Level Model-Based Trace Analysis as Part of Runtime Verification. Proceedings of the ISP RAS, 2024, vol. 36, no. 4, pp. 169–182. (In Russian). DOI: 10.15514/ISPRAS-2024-36(4)-13

12. J.-R. Abrial, The Event-B Modelling Notation, Available at: https://wiki.event-b.org/index.php/Event-B_Modelling_Language

13. Metayer C., Voisin L., The Event-B Mathematical Language, Available at: https://wiki.event-b.org/index.php/Event-B_Mathematical_Language

14. Abrial J.-R., Hallerstede S., Refinement, Decomposition, and Instantiation of Discrete Models: Application to Event-B. In Fundamenta Informaticae, 2007, vol. 77, pp. 1–28. DOI: 10.5555/2366448.2366450.

15. Börger E., ASM Refinement Method. In Formal Aspects of Computing, vol. 15, pp. 237–257, Springer-Verlag, 2003. DOI: 10.1007/s00165-003-0012-7

16. Efremov D., Shchepetkov I., Runtime verification of Linux kernel security module. In International Symposium on Formal Methods, 2019, pp. 185–199. Available at: https://arxiv.org/pdf/2001.01442

17. Bartocci E., Falcone Y., Fracalanza A., Reger G. Introduction to runtime verification. In Bartocci E., Falcone Y. (editors) Lectures on Runtime Verification. Lecture Notes in Computer Science, vol. 10457, Springer, 2018. pp. 1–33. DOI: 10.1007/978-3-319-75632-5_1.

18. Leuschel M., Butler M. ProB: an automated analysis toolset for the B method. The International Journal on Software Tools for Technology Transfer, vol. 10, Springer, 2008, pp. 185–203.

19. DOI: 10.1007/s10009-007-0063-9.

20. Servat, T., BRAMA: A New Graphic Animation Tool for B Models. In Julliand, J., Kouchnarenko, O. (edsitors) Formal Specification and Development in B. Lecture Notes in Computer Science, vol. 4355. Springer, 2007. DOI: 10.1007/11955757_28

21. AnimB. Available at: https://wiki.event-b.org/index.php/AnimB

22. Code generation activity. Available at: https://wiki.event-b.org/index.php/Code_Generation_Activity

23. Wright S., Automatic generation of C from Event-B. Presented at the Workshop on Integration of Model-based Formal Methods and Tools, Bangkok, Thailand, 02 2009.

24. Cataño N., Rivera V., EventB2Java: A code generator for Event-B. In Rayadurgam, S., Tkachuk, O. (editors) NASA Formal Methods. Lecture Notes in Computer Science, vol. 9690, Springer, 2016.

25. DOI: 10.1007/978-3-319-40648-0_13.

26. A Concise Summary of the Event-B mathematical toolkit. Available at: https://wiki.event-b.org/images/EventB-Summary.pdf

27. Петренко А.К., Девянин П.Н., Ефремов Д.В., Карнов А.А., Корныхин Е.В., Кулямин В.В., Хорошилов А.В., Динамическая верификация промышленных средств защиты информации на основе формальных моделей управления доступом. Труды ИСП РАН, 2025, том 37, вып. 3, стр. 275–288. DOI: 10.15514/ISPRAS-2025-37(3)-19 / Petrenko A.K., Devyanin P.N., Efremov D.V., Karnov A.A., Kornykhin E.V., Kulyamin V.V., Khoroshilov A.V., Dynamic verification of industrial information security tools based on formal access control models. Proceedings of the ISP RAS, 2025, vol. 37, issue 3, pp. 275–288. DOI: 10.15514/ISPRAS-2025-37(3)-19