Формирование методологии разработки безопасного системного программного обеспечения на примере операционных систем

Разработка безопасного системного программного обеспечения (ПО), на основе которого строятся сертифицированные средства защиты информации, достижение доверия к нему согласно требованиями нормативных документов отечественных регуляторов – крупная научно-техническая проблема. Возможным путем ее решения является формирование соответствующей методологии, которая должна включить передовые научные результаты в области информационной безопасности и системного программирования и отразить лучшие практики разработки такого ПО. В статье рассматриваются текущие результаты формирования этой методологии, которое осуществляется по следующим направлениям. Во-первых, это деятельность по развитию нормативной базы в области разработки и обеспечения доверия к безопасному системному ПО, включая создание профильных национальных стандартов. Во-вторых, разработка и верификация формальных моделей управления доступом, как основы механизмов защиты, входящих в состав системного ПО и составляющих его поверхность атаки. В-третьих, методы и технологии статического и динамического анализа программного кода системного ПО с учётом его специфики. В-четвертых, способы сбора и аналитической обработки данных, получаемых в ходе анализа программного кода системного ПО. Все направления формирования методологии иллюстрируются примерами ее практического применения и апробации при разработке ОС семейства Linux, в особенности сертифицированной по высшим классам защиты и уровням доверия операционной системы специального назначения Astra Linux Special Edition.

1. ГОСТ Р 56939-2016. Защита информации. Разработка безопасного программного обеспечения. Общие требования. / GOST R 56939-2016. Information protection. Secure Software Development. General requirements. Federal Agency for Technical Regulation and Metrology, 2016 (in Russian).

2. Выписка из Требований по безопасности информации, утвержденных приказом ФСТЭК России от 2 июня 2020 г. N 76 / Excerpts from Requirements for information security approved by FSTEK Russia order #76 of 2nd June 2020. Available at: https://fstec.ru/tekhnicheskaya-zashchita-informatsii/dokumenty-po-sertifikatsii/120-normativnye-dokumenty/2126-vypiska-iz-trebovanij-po-bezopasnosti-informatsii-utverzhdennykh-prikazom-fstek-rossii-ot-2-iyunya-2020-g-n-76, accessed 14.11.2021 (in Russian).

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

4. Bishop M. Computer Security: art and science. Addison-Wesley Professional, 2002. 1084 p.

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

6. Девянин П.Н., Ефремов Д.В. и др. Моделирование и верификация политик безопасности управления доступом в операционных системах. М., Горячая линия – Телеком, 2019 г., 214 стр. / P.N. Devyanin, D.V. Efremov et al. Modeling and verification of access control access policies in operating systems. Hotline-Telecom, 2019, 214 p. (in Russian).

7. Microsoft Security Development Lifecycle. Available at: https://www.microsoft.com/en-us/securityengineering/sdl, accessed 14.11.2021.

8. Операционная система специального назначения Astra Linux Special Edition / Astra Linux Special Edition operating system. Available at: https://astralinux.ru/products/astra-linux-special-edition, accessed 14.11.2021.

9. П.В. Буренин, П.Н. Девянин и др. Безопасность операционной системы специального назначения Astra Linux Special Edition. Учебное пособие для вузов. М., Горячая линия – Телеком, 2019 г., 404 стр. / P.V. Burenin, P.N. Devyanin et al. Information security with Astra Linux Special Edition. Hotline-Telecom, 2019, 404 p. (in Russian).

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

11. ГОСТ Р 59453.2-2021. Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификация формальной модели управления доступом / GOST R-59453.2-2021 «Information protection. Formal access control model. Part 2. Recommendations on verification of formal access control model» (in Russian).

12. Документы по сертификации средств защиты информации и аттестации объектов информатизации по требованиям безопасности информации / Documents for certification of information security software and attestation of information systems according to information security requirements. Available at: http://fstec.ru/tekhnicheskaya-zashchita-informatsii/dokumenty-po-sertifikatsii/120-normativnye-dokumenty, accessed 14.11.2021 (in Russian).

13. Информационное сообщение ФСТЭК России от 29.03.2019 № 240/24/1525 / Informational message of FSTEK Russia 29th March 2021 #240/24/1525. Available at: https://fstec.ru/component/attachments/download/2286, accessed 14.11.2021 (in Russian).

14. Буренков В.С., Кулагин Д.А. Модель мандатного контроля целостности в операционной системе KasperskyOS. Труды ИСП РАН, том 32, вып. 1, 2020 г, стр. 27-56 / Burenkov V.S., Kulagin D.A. A Mandatory Integrity Control Model for the KasperskyOS Operating System. Trudy ISP RAN/Proc. ISP RAS, vol. 32, issue 1, 2020. pp. 27-56 (in Russian). DOI: 10.15514/ISPRAS-2020-32(1)-2.

15. 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, no. 6. 2010, pp. 447-466.

16. Девянин П.Н., Леонова М.А. Приёмы по доработке описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её автоматизированной верификации с применением инструментов Rodin и ProB. Прикладная дискретная математика, no. 52, 2021 г., стр. 83-96 / Devyanin P.N., Leonova M.A. The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB. Applied discrete mathematics, no. 52, 2021, pp. 83–96 (In Russian).

17. Kirchner F., Kosmatov N. et al. Frama-C: a software analysis perspective. Formal Aspects of Computing, vol. 27, issue 3, 2015, pp. 573-609.

18. Cppcheck. A tool for static C/C++ code analysis. Available at: http://cppcheck.sourceforge.net, accessed 14.11.2021.

19. Clang Static Analyzer. Available at: https://clang-analyzer.llvm.org/, accessed 14.11.2021.

20. Статический анализатор Svace. URL: http://www.ispras.ru/technologies/svace / SVACE static analyzer. Available at: https://www.ispras.ru/en/technologies/svace/, accessed 14.11.2021.

21. Syzkaller project. Available at: https://github.com/google/syzkaller, accessed 14.11.2021.

22. American Fuzzy Loop. Available at: https://github.com/google/AFL, accessed 14.11.2021.

23. Комплекс динамического анализа программ Crusher. URL: https://www.ispras.ru/technologies/crusher / ISP Crusher: a dynamic analysis toolset. Available at: https://www.ispras.ru/en/technologies/crusher/, accessed 14.11.2021.