Тестирование подсистемы безопасности ОС Astra Linux на основе формализованного описания модели управления доступом

В операционной системе (ОС) Astra Linux кроме традиционного для большинства ОС дискреционного управления доступом ее подсистемой безопасности PARSEC реализуются механизмы мандатного контроля целостности (МКЦ) и мандатного управления доступом (МРД). С учетом многообразия имеющихся в данной ОС сущностей (объектов доступа, файлов, каталогов, сокетов и др.) и субъектов (процессов) эти механизмы имеют сложную логику функционирования, затрудняющую их тестирование с использованием вручную подготовленных тестов. Влияет на проблему необходимость выполнения процессов разработки безопасного программного обеспечения (ПО) для соответствия ОС Astra Linux требованиям высших классов защиты и уровней доверия. Вместе с тем в основе механизмов МКЦ и МРД этой ОС используется мандатная сущностно-ролевая ДП-модель управления доступом и информационными потоками в ОС семейства Linux (МРОСЛ ДП-модель), описанная в классической математической нотации и в формализованной нотации на языке формального метода Event-B. Авторами развивается рекомендованный ГОСТ Р 59453.4-2025 подход к тестированию механизмов управления доступом на основе сбора трасс системных вызовов ОС и их перевода на язык формальной модели с целью проверки соответствия ей логики функционирования механизма управления доступом ОС. Результатам этой работы посвящена настоящая статья, в которой, во-первых, изложены итоги разработки и верификации используемого для тестирования нижнеуровневого представления МРОСЛ ДП-модели (PARSEC-модели), выполненного на языке формального метода Event-B и представляющего функциональную спецификацию связанных с управлением доступом системных вызовов ОС. Во-вторых, описывается система тестирования, включающая модуль ядра ОС для сбора трасс системных вызовов, ПО для их преобразования в модельные трассы, аниматор модельных трасс, выполненный с применением инструментального средства ProB, и ПО для формирования результатов тестирования в формате инструментального средства Allure. В-третьих, в статье рассматривается подход к использованию для распараллеливания тестирования технологии eBPF.

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.