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

Механизм управления доступом является базовым для обеспечения безопасности системного программного обеспечения (ПО) такого, как операционная система (ОС) или система управления базами данных (СУБД). В качестве научной основы реализации такого механизма, а также в соответствии с требованиями нормативных документов отечественных регуляторов к сертифицированным средствам защиты информации должна разрабатываться соответствующая критериям ГОСТ Р 59453.1-2021 формальная модель управления доступом. Такой формальной моделью для сертифицированной по высшим классам защиты и уровням доверия ОС Astra Linux является мандатная сущностно-ролевая ДП-модель управления доступом и информационными потоками в ОС семейства Linux (МРОСЛ ДП-модель). С учетом внедрения в механизм управления доступом ОС Astra Linux новых элементов, с целью обеспечения более точного соответствия описания модели этому механизму, развитию научно обоснованных технологий и практик разработки и верификации формальных моделей МРОСЛ ДП-модель регулярно перерабатывается. В настоящее время завершена очередная такая переработка модели для двух уровней ее иерархического представления, соответствующих ролевому управлению доступом (представляющему традиционное для ОС семейства Linux дискреционное управление доступом) и мандатному контролю целостности, отражающая наиболее существенные изменения в ОС Astra Linux релиза 2023 года. В статье анализируются основные результаты этой переработки, в рамках которой: введены функции, задающие новые метки сущностей, изменены состав и описания де-юре правил преобразования состояний системы, административных и запрещающих ролей, скорректированы формулировки и заново доказаны несколько утверждений, а также внесены другие изменения в описание модели.

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