Methods of Runtime Verification of Industrial Information Security Tools Based on Formal Access Control Models.

The paper discusses methods of runtime verification of software systems that are security protection mechanisms (PM) or include such mechanisms in their design. To ensure a high level of trust and security of software systems, it is necessary to use different verification methods and technologies. In this case, not only the potential power of the method is important, but also the possibility of using it in real conditions of industrial development of large and complex software systems. The rigor and accuracy of verification are ensured by formal methods; however, the use of classical formal methods dictates special, extremely high requirements for personnel and entails additional labor costs. The article proposes a technology for runtime verification of PM, which, on the one hand, is close to testing techniques, therefore it is easier for test engineers to master, and, on the other hand, uses formal access control models and specifications of external PM interfaces as a basis, which are already appearing among OS and DBMS developers, whose products must meet the requirements of the new national standard GOST R 59453.4-2025 "Information Security. Formal access control model. Part 4. Recommendations for verification of information security tools implementing access control policies based on formalized descriptions of the access control model. This standard is also presented in the article.

1. ГОСТ Р 59453.4-2025 «Защита информации. Формальная модель управления доступом. Часть 4. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом». М.: Стандартинформ, 2025. 20 с. / GOST R 59453.4-2025 «Information protection. 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», 2025 (in Russian).

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

3. ГОСТ Р 59453.2-2021 «Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификация формальной модели управления доступом». М.: Стандартинформ, 2021. 12 с./ GOST R 59453.2-2021 «Information protection. Formal access control model. Part 2. Recommendations on verification of formal access control model», 2021 (in Russian).

4. ГОСТ Р 59453.3-2025 «Защита информации. Формальная модель управления доступом. Часть 3. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом». М.: Стандартинформ, 2025. 20 с. / GOST R 59453.3-2025 «Information protection. Formal access control model. Part 3. Recommendations on development», 2025 (in Russian).

5. DO-178C - Software Considerations in Airborne Systems and Equipment Certification Software Considerations in Airborne Systems and Equipment Certification (RTCA DO178C), 2011 https://my.rtca.org/nc__store?search=do-178c

6. КТ-178С – Квалификационные требования. Часть 178 «Требования к программному обеспечению бортовой аппаратуры и систем при сертификации авиационной техники».

7. П.Н. Девянин, С.С. Жиляков, А.И. Смирнов. Тестирование подсистемы безопасности ОС Astra Linux на основе формализованного описания модели управления доступом, том 37, вып. 4, 2025. / Devyanin P.N., S.S. Zhiliakov, A.I. Smirnov. Testing the Astra Linux OS security subsystem based on a formalized description of the access control model. Trudy ISP RAN/Proc. ISP RAS, vol. 37, issue 4, 2025 (in Russian).

8. Операционная система специального назначения Astra Linux Special Edition. Доступно по ссылке: https://astra.ru/software-services/os/, 17.04.2025. / Astra Linux Special Edition operating system. Available at: https://astra.ru/software-services/os/, accessed 17.04.2025.

9. Abrial, Jean-Raymond. Modeling in Event-B: system and software engineering.- Cambridge University Press, 2010.

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

11. Девянин П.Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками. Учебное пособие для вузов. 3-е изд., перераб. и доп. М.: Горячая линия – Телеком, 2020. 352 с.: ил. / P.N. Devyanin. Security models of computer systems. Control for access and information flows. Hotline-Telecom, 2020, 352 p. (in Russian).

12. Michael Felderer, Philipp Zech, Ruth Breu, Matthias Büchler, Alexander Pretschner. Model-Based Security Testing: A Taxonomy and Systematic Classification.- Software Testing Verification and Reliability 00(2), July 2015:1-29, DOI:10.1002/stvr.1580.

13. Schieferdecker, Ina & Großmann, Jürgen & Schneider, Martin. (2012). Model-Based Security Testing. Electronic Proceedings in Theoretical Computer Science. A.K. Petrenko, H. Schlingloff (Eds.): Workshop on Model-Based Testing 2012 (MBT 2012), EPTCS 80, 2012, https://doi.org/10.4204/EPTCS.80

14. Krishnan, P., Pari-Salas, P. (2009). Model-Based Testing and the UML Testing Profile. In: Palsberg, J. (eds) Semantics and Algebraic Specification. Lecture Notes in Computer Science, vol 5700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04164-8_16/

15. Pierre-Alain Masson, Jacques Julliand, Jean-Chritophe Plessis, Eddie Jaffuel, Georges Debois. Automatic generation of model based tests for a class of security properties.- A-MOST '07: Proceedings of the 3rd international workshop on Advances in model-based testing, Pages 12-22, https://doi.org/10.1145/1291535.1291537

16. The B-Book: Assigning Programs to Meanings, Jean-Raymond Abrial, Cambridge University Press, 1996. ISBN 0-521-49619-5.

17. Tejeddine Mouelhi, Franck Fleurey, Benoit Baudry, Yves Le Traon. A Model-Based Framework for Security Policy Specification, Deployment and Testing.- K. Czarnecki et al. (Eds.): MoDELS 2008, LNCS 5301, pp. 537–552

18. OASIS eXtensible Access Control Markup Language (XACML) TC | OASIS. www.oasis-open.org.

19. Девянин П.Н., Ефремов Д.В., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. Моделирование и верификация политик безопасности управления доступом в операционных системах. М.: Горячая линия – Телеком, 2019. 214 с.: ил. / P.N. Devyanin, D.V. Efremov, V.V. Kuliamin, A.K. Petrenko, A.V. Khoroshilov. Modeling and verification of access control access policies in operating systems. Hotline-Telecom, 2019, 214 p. (in Russian).

20. L. Lamport. Specifying Systems, The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.

21. Козачок В.И., Козачок А.В., Кочетков Е.В. Многоуровневая модель политики безопасности управления доступом операционных систем семейства Windows.- Вопросы кибербезопасности, 2021, № 1(41), DOI: 10.21681/2311-3456-2021-1-41-56.

22. Event-B and the Rodin Platform, https://www.event-b.org/.

23. Е.В. Корныхин, Д.В. Ефремов, А.В. Карнов, А.К. Петренко. Инструмент АНИС - поддержка процессов верификации средств защиты информации на основе формальных моделей управления доступом.- Труды ИСП РАН, 2025, том 37, вып. 4.