On the Development of the Draft Standard GOST R “Information Protection. Formal Access Control Model. Part 3. Recommendations on Development”

Formal models of access control must be described in accordance with the requirements of FSTEC of Russia regulatory documents, in order to ensure trust in certified information security tools when they implement appropriate access control policies. The criterias that the description of each such model must meet were established in GOST R 59453.1-2021 “Information protection. Formal access control model. Part 1. General principles” to stimulate the development of formal access control models that are adequate to the operating conditions of modern information security tools. This standard also specifies additional criteria for cases where specific policies are implemented by information security tools: discretionary access control (DAC), mandatory access control (MAC), role-based access control (RBAC), or mandatory integrity control (MIC). A draft of the new standard GOST R “Information protection. Formal access control model. Part 3. Recommendations on development” was developed with the participation of the author to simplify the process of describing the formal model, which is scheduled for approval in 2024. This new standard is important for the development of regulatory and methodological support in this area. The standard will also be useful in developing a formal model for information security tools that are complex system software, such as an operating system (OS) or a database management system (DBMS). The article analyzes the results of the development of this draft standard, including the stages recommended in it for describing the formal model. Firstly, this is the stage of describing the states of the corresponding abstract automaton. Secondly, this is one of describing the rules for transition from states to states of an abstract automaton. Thirdly, this is the stage of formulating and implementing evidence of the fulfillment of safety conditions, the technologies and practical techniques used for this. In addition, the article provides examples of testing the recommendations set out in the draft standard when reworking the mandatory entity-role model of access and information flows security control in OS of Linux family (MROSL DP-model), which is used as the scientific basis for the implementation of the PARSEC security subsystem of certified according to the highest protection classes and trust levels of OS Astra Linux.

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

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

3. Девянин П.Н., Тележников В.Ю., Третьяков С.В. Основы безопасности операционной системы 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).

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

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

6. Trusted Computer System Evaluation Criteria / US Department Of Defense, 1985. CSC-STD-001-83.

7. ГОСТ Р ИСО/МЭК 15408-3-2013 «Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности». М.: Стандартинформ. 150 с. / GOST R ISO/IEC 15408-3-2013 «Information technology. Security techniques. Evaluation criteria for IT security. Part 3. Security assurance components», 2013 (in Russian).

8. Выписка из Требований по безопасности информации, утвержденных приказом ФСТЭК России от 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, 03.05.2024 / 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 03.05.2024. (in Russian).

9. Информационное сообщение ФСТЭК России от 10.02.2021 № 240/24/647. Доступно по ссылке: https://fstec.ru/dokumenty/vse-dokumenty/informatsionnye-i-analiticheskie-materialy/informatsionnoe-soobshchenie-fstek-rossii-ot-10-fevralya-2021-g-n-240-24-647, 03.05.2024 / Informational message of FSTEK Russia of 10th February 2021 #240/24/647. Available at: https://fstec.ru/dokumenty/vse-dokumenty/informatsionnye-i-analiticheskie-materialy/informatsionnoe-soobshchenie-fstek-rossii-ot-10-fevralya-2021-g-n-240-24-647, accessed 03.05.2024. (in Russian).

10. ГОСТ Р 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).

11. Девянин П.Н., Ефремов Д.В., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. Моделирование и верификация политик безопасности управления доступом в операционных системах. М.: Горячая линия – Телеком, 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).

12. Девянин П.Н., Леонова М.А. Приемы по доработке описания модели управления доступом ОССН 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).

13. Девянин П.Н., Хорошилов А.В., Тележников В.Ю. Формирование методологии разработки безопасного системного программного обеспечения на примере операционных систем. Труды ИСП РАН, том 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).

14. Девянин П.Н. Результаты переработки уровней ролевого управления доступом и мандатного контроля целостности формальной модели управления доступом ОС 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).