Методы динамической верификации промышленных средств защиты информации на основе формальных моделей управления доступом.

В статье рассматриваются методы динамической верификации программных систем, представляющих собой средства защиты информации (СЗИ) или включающих такие средства в свой состав. Для обеспечения высокого уровня доверия и защищенности программных систем необходимо применять разные методы и технологии верификации, при этом важны не только потенциальная мощность метода, но возможность использовать его в реальных условиях промышленной разработки крупных и сложных программных систем. Строгость и точность верификации обеспечивают формальные методы, однако использование классических формальных методов диктует особые, крайне высокие требования к персоналу и влечёт за собой дополнительные трудозатраты. Статья предлагает технологию динамической верификации СЗИ, которая, с одной стороны, близка к техникам тестирования, поэтому проще для освоения инженерами-тестировщиками, и, с другой стороны, в качестве базы использует формальные модели управления доступом и спецификации внешних интерфейсов СЗИ, которые уже появляются у разработчиков ОС и СУБД, чья продукция должна соответствовать требованиям нового национального стандарта ГОСТ Р 59453.4-2025 «Защита информации. Формальная модель управления доступом. Часть 4. Рекомендации по верификации средства защиты информации, реализующего политики управления доступом, на основе формализованных описаний модели управления доступом». Данный стандарт также представлен в статье.

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.