Building a methodology for secure system software development on the example of operating systems
https://doi.org/10.15514/ISPRAS-2021-33(5)-2
Abstract
System software is a cornerstone of any software system, so building secure system software in accordance with requirements of certification authorities and state-of-the-art practices is an important scientific and technical problem. One of possible approaches to cope with the problem is to build a methodology for secure system software development including advanced scientific technologies and industry best practices. The paper presents current results achieved in building such methodology in the following directions. The first one is regulatory framework improvement including development of GOST R specifications defining requirements to formal models of access control policies and their formal verification. The second direction is design and verification of formal models of corresponding security functional requirements. The third direction is application of new and well established technologies of static and run-time analysis of systems software. The considered technologies include static analysis, fuzzing, functional and unit testing as well as testing the system software against formal models of its functional security requirements. The forth direction is development of methods for acquisition of results of all kinds of the analysis and for its analytical processing. All the directions are illustrated by practical examples of application of the methodology to development of Astra Linux operating system distribution that is certified according to the highest evaluation assurance levels.
About the Authors
Petr Nikolaevich DEVYANIN
RusBITech-Astra
Russian Federation
Russian Federation
Doctor of Technical Sciences, corresponding member of Russian Academy of Cryptography, professor, scientific director in RusBITech-Astra (Astra Linux)
Vladimir Iurevich TELEZHNIKOV
RusBITech-Astra
Russian Federation
Russian Federation
Ph.D in Technical Science, Head of Research Department
Alexey Vladimirovich KHOROSHILOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Lomonosov Moscow State University, National Research University Higher School of Economics, Moscow Institute of Physics and Technology (State University)
Russian Federation
Russian Federation
Leading Researcher, Ph.D. in Physics and Mathematics, Director of the Linux OS Verification Center at ISP RAS, Associate Professor of System Programming Departments at Moscow State University, the Higher School of Economics, and Moscow Institute of Physics and Technology
References
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.
Review
For citations:
DEVYANIN P.N., TELEZHNIKOV V.I., KHOROSHILOV A.V. Building a methodology for secure system software development on the example of operating systems. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(5):25-40. (In Russ.) https://doi.org/10.15514/ISPRAS-2021-33(5)-2
Email this article 