Testing the Astra Linux OS Security Subsystem Based on a Formal-ized Description of the Access Control Model

In Astra Linux operating system (OS), in addition to the traditional Discretionary Access Control, its PARSEC security subsystem implements Mandatory Access Control policies such as Mandatory Integrity Control (MIC) and Multilevel Security (MLS). Given the variety of entities (objects, files, directories, sockets, etc.) and subjects (processes) available in a given OS, these policies often have a complicated logic of functioning, which makes it difficult to test them using manual testing. This problem is especially aggravated in the context of the necessity to fulfill the Security Development Lifecycle in compliance with the requirements of the highest protection classes and trust levels established by the FSTEC of Russia regulatory documents. Besides, the MIC and MLS policies of this OS are based on the mandatory entity-role model of access and information flows security control in OS of Linux family (MROSL DP-model), described in the classical mathematical notation and in the formalized notation using the formal Event-B method. Therefore, the authors of this paper have developed and finalized the approach recommended by GOST R 59453.4-2025, taking into account the specifics of current releases of Astra Linux OS, which consists of tracing system calls and translating them into the language of the formal model in order to verify the compliance of the functioning access control policies with the model. The results of this work are described in this paper, which, firstly, outlines the results of the development and verification of the so-called lower-level representation of the MROSL DP-model (PARSEC-model) used for testing, performed in the Event-B and in essence represents a functional specification of access control-related system calls of the OS. Secondly, it describes a testing system that includes the Linux Kernel Module for tracing system calls, software for their translation into model traces, an animator of model traces using the ProB toolkit, and software for generating test results in the format of the Allure toolkit. Thirdly, the paper considers approach to using eBPF technology for parallelizing testing.

1. ГОСТ Р 56939-2024 «Защита информации. Разработка безопасного программного обеспечения. Общие требования». М.: Стандартинформ. 36 с. / GOST R 56939-2024 «Information protection. Secure Software Development. General requirements», 2024. (in Russian).

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

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

4. Выписка из Требований по безопасности информации, утвержденных приказом ФСТЭК России от 2 июня 2020 г. N 76. Доступно по ссылке: https://fstec.ru/dokumenty/vse-dokumenty/spetsialnye-normativnye-dokumenty/trebovaniya-po-bezopasnosti-informatsii-utverzhdeny-prikazom-fstek-rossii-ot-2-iyunya-2020-g-n-76, 05.06.2025 / Excerpts from Requirements for information security approved by FSTEK Russia order #76 of 2nd June 2020. Available at https://fstec.ru/dokumenty/vse-dokumenty/spetsialnye-normativnye-dokumenty/trebovaniya-po-bezopasnosti-informatsii-utverzhdeny-prikazom-fstek-rossii-ot-2-iyunya-2020-g-n-76, accessed 05.06.2025. (in Russian).

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

6. Девянин П.Н., Тележников В.Ю., Третьяков С.В. Основы безопасности операционной системы Astra Linux Special Edition. Управление доступом. Учебное пособие. М., Горячая линия – Телеком, 2022, 148 с. / Devyanin P.N., Telezhnikov V.Y., Tret’yakov S.V. Astra Linux Special Edition security basics. Access control. Hotline-Telecom, 2022, 148 p. (in Russian).

7. Bishop M. Computer Security: Art and Science, 2nd edition. Pearson Education Inc., 2018, 1440 p.

8. Abrial J.-R., Hallerstede S. Refinement, decomposition, and instantiation of discrete models: Application to Event-B // Fundamenta Informaticae, Volume 77, Issue 1-2, 2007, pp. 1-28.

9. Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010, 612 p.

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. ГОСТ Р 59453.4-2025 «Защита информации. Формальная модель управления доступом. Часть 4. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом». М.: Стандартинформ. 20 с. / GOST R 59453.4-2025 «Information protection. Formal model of access control. Part 4. Recommendations on verification of information protection tool implementing access control policies based on formalized descriptions of access control model», 2025 (in Russian).

12. Ефремов Д.В., Копач В.В., Корныхин Е.В., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы // Труды ИСП РАН, том 33, вып. 6, 2021, С. 15-26 / Efremov D.D., Kopach V.V., Kornykhin E.V., Kuliamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Runtime Verification of Operating Systems Based on Abstract Models. Trudy ISP RAN/Proc. ISP RAS, vol. 33, issue 6, 2021, pp. 15-26 (in Russian).

13. Петренко А.К., Девянин П.Н., Ефремов Д.В., Карнов А.А., Корныхин Е.В., Кулямин В.В., Хорошилов А.В. Методы динамической верификации промышленных средств защиты информации на основе формальных моделей управления доступом // Труды ИСП РАН, 2025, Т. 37, вып. 3, С. 277-290 / Petrenko A.K., Devyanin P.N., Efremov D.V., Karnov A.A., Kornykhin Е.V., Kuliamin V.V., Khoroshilov A.V. Methods of runtime verification of industrial information security tools based on formal access control models. Trudy ISP RAN/Proc. ISP RAS, vol. 37, issue 3, 2025. pp. 277-290 (in Russian)

14. Девянин П.Н., Хорошилов А.В., Тележников В.Ю. Формирование методологии разработки безопасного системного программного обеспечения на примере операционных систем // Труды ИСП РАН, том 33, вып. 5, 2021, С. 25-40 / Devyanin P.N., Telezhnikov V.Y., Khoroshilov V.V. Building a methodology for secure system software development on the example of operating systems. Trudy ISP RAN/Proc. ISP RAS, vol. 33, issue 5, 2021, pp. 25-40 (in Russian).

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

16. Девянин П.Н. О разработке проекта национального стандарта ГОСТ Р «Защита информации. Формальная модель управления доступом. Часть 3. Рекомендации по разработке» // Труды ИСП РАН, том 36, вып. 3, 2024, С. 63-82 / Devyanin P.N. On the development of the draft standard GOST R “Information protection. Formal access control model. Trudy ISP RAN/Proc. ISP RAS, vol. 36, issue 3, 2024, pp. 63-82 (in Russian).

17. Девянин П.Н. Результаты переработки уровней ролевого управления доступом и мандатного контроля целостности формальной модели управления доступом ОС Astra Linux // Труды ИСП РАН, том 35, вып. 5, 2023, С. 7-22 / Devyanin P.N. The Results of Reworking the Levels of Role-Based Access Control and Mandatory Integrity Control of the Formal Model of Access Control in Astra Linux. Trudy ISP RAN/Proc. ISP RAS, vol. 35, issue 5, 2023, pp. 7-22 (in Russian).

18. ГОСТ Р 59453.2-2021 «Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификация формальной модели управления доступом». М.: Стандартинформ. 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).

19. Abrial J.-R., Butler M. et al. Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, vol. 12, issue 6, 2010, pp. 447-466.

20. Leuschel M., Butler M. ProB: A Model Checker for B. Lecture Notes in Computer Science, vol. 2805, 2003, pp. 855-874.

21. Ковалев М.Г. Трассировка сетевых пакетов в ядре Linux с использованием eBPF // Труды ИСП РАН, том 32, вып. 3, 2020, С. 71-78 (на английском языке) / Kovalev M.G. Tracing Network Packets in the Linux Kernel using eBPF. Trudy ISP RAN/Proc.ISP RAS, vol. 32, issue 3, 2020. pp. 71-78.

22. Gregg B. BPF Performance Tools. Addison-Wesley Professional, 2019, 880 p.

23. Tetragon. Overview. Available at https://tetragon.io/docs/overview/, accessed 05.06.2025.

24. The Falco Project. Developer Guide. Available at https://falco.org/docs/developer-guide/, accessed 05.06.2025.

25. Aqua Security. Aqua Tracee. Available at https://www.aquasec.com/products/tracee/, accessed 05.06.2025.

26. Wright C., Cowan C., Smalley S., Morris J., Kroah-Hartman G. Linux Security Modules: General Security Support for the Linux Kernel. Proc. of the 11-th USENIX Security Symposium, pp. 17–31, 2002.

27. Девянин П.Н., Старостин А.А., Панов Д.С., Усачев С.В. Проектирование и развитие механизма мандатного контроля целостности в операционной системе Astra Linux // Труды ИСП РАН, том 37, вып. 2, 2025, С. 61-78 / Devyanin P.N., Starostin A.A., Panov D.S., Usachev S.V. Design and Development of a Mandatory Integrity Control Mechanism in the Astra Linux Operating System. Trudy ISP RAN/Proc. ISP RAS, vol. 37, issue 2, 2025, pp. 61–78 (in Russian).

28. D. Efremov and I. Shchepetkov. Runtime Verification of Linux Kernel Security Module. Proc. Of International Workshop on Formal Methods, LNCS 12233:185-199, Springer, 2020.

29. Allure Report Documentation. Available at https://allurereport.org/docs/, accessed 05.06.2025.

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

31. pytest: helps you write better programs. Available at https://docs.pytest.org/en/stable/, accessed 05.06.2025.

32. bpf-helpers(7) – Linux manual pages. Available at https://man7.org/linux/man-pages/man7/bpf-helpers.7.html, accessed 05.06.2025.

33. BPF CO-RE, eBPF Docs. Available at https://docs.ebpf.io/concepts/core/, accessed: 05.06.2025.

34. Linux 6.0 Adding Run-Time Verification For Running On Safety Critical Systems. Available at https://www.phoronix.com/news/Linux-6.0-Runtime-Verification, accessed 05.06.2025.