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

The access control mechanism is the basis for ensuring the security of system software (OS or DBMS). In accordance with the requirements of regulatory documents of domestic regulators for certified information security tools, as a scientific basis for the implementation of such a mechanism, a formal access control model that meets the GOST R 59453.1-2021 criteria should be developed. Such a formal model for the Astra Linux operating system certified for the highest protection classes and assurance levels is the mandatory entity-role model of access and information flows security control in OS of Linux family (MROSL DP-model). Taking into account the introduction of new elements into the access control mechanism of the Astra Linux and in order to ensure a more accurate correspondence of the model description to this mechanism, the development of scientifically based technologies and practices for the development and verification of formal models, the MROSL DP-model is regularly revised. Another such revision of the model now has been completed for two levels of its hierarchical representation, corresponding to role-based access control (representing discretionary access control, traditional for the OS of Linux family) and mandatory integrity control, reflecting the most significant changes in the Astra Linux release 2023. The article analyzes the main results of this revision, within which: functions that define new entity labels are introduced, the composition and descriptions of the de-jure rules for transforming system states, administrative and negative roles are changed, the wording is corrected and several statements are re-proved, and other changes are made in the model description.

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

3. Информационное сообщение ФСТЭК России от 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, 07.12.2023 / 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 07.12.2023. (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. ГОСТ Р 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).

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

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

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

10. Abrial J.-R., Butler M., Hallerstede S. et al. Rodin: An open toolset for modelling and reasoning in Event-B // International Journal on Software Tools for Technology Transfer. 2010. Vol. 12, no. 6, pp. 447-466.

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

12. 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.

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