Preview

Труды Института системного программирования РАН

Расширенный поиск

Модель мандатного контроля целостности в операционной системе KasperskyOS

https://doi.org/10.15514/ISPRAS-2020-32(1)-2

Аннотация

Существующие модели мандатного контроля целостности в операционных системах накладывают ограничения на доступы активных компонент системы к пассивным и представляют эти доступы непосредственно. Такое представление можно использовать в случае операционных систем с монолитной архитектурой, где части системы, обеспечивающие доступ к ресурсам, входят в доверенную вычислительную базу. Однако эти части являются нетривиальными компонентами со сложной реализацией, в связи с чем доказательство отсутствия в них ошибок (уязвимостей) и, следовательно, соответствия модели реальной системе – чрезвычайно трудная задача, которая на практике, как правило, полностью не решается. В данной статье представлена модель мандатного контроля целостности для микроядерной операционной системы KasperskyOS. Базирование системы на микроядре предполагает минимизацию доверенной вычислительной базы. При таком подходе доступ к ресурсам предоставляется с помощью компонент, не входящих в доверенную вычислительную базу. Это создает предпосылки для гарантии соответствия системы определенным свойствам безопасности даже в случае некорректного функционирования этих компонент. В модели для представления частей системы, обеспечивающих доступ к ресурсам, введено понятие драйвера объектов, и операции получения доступа активных компонент (сущностей) к пассивным компонентам (объектам) выполняются посредством драйверов объектов. В статье определены требования, которым должны удовлетворять драйверы объектов и некоторые другие сущности. В модель также добавлены элементы, позволяющие провести ее анализ в случае нарушения данных требований. Сформулирована и доказана теорема о постоянном нахождении модели в целостном состоянии (об отсутствии в модели информационных потоков от менее целостных компонентов к более целостным либо несравнимым) в случае удовлетворения всеми сущностями сформулированных требований, а также об ограниченном характере распространения эффекта от нарушения целостности системы в случае наличия в системе компонентов, нарушающих требования. Корректная реализация модели гарантирует, что если компрометирована часть системы, уровень целостности компонентов которой ограничен некоторыми уровнями целостности, то это не приведет к компрометации части системы с более высокими или несравнимыми уровнями целостности. Описан язык спецификации политик мандатного контроля целостности, разработанный в соответствии с правилами модели, и приведен пример использования языка для задания политики безопасности системы, работающей под управлением KasperskyOS. Целью политики является обеспечение безопасности процесса обновления системы.

Об авторах

Владимир Сергеевич Буренков
АО «Лаборатория Касперского»
Россия
Rандидат технических наук, разработчик-исследователь


Дмитрий Александрович Кулагин
АО «Лаборатория Касперского»
Россия
Кандидат технических наук, ведущий разработчик


Список литературы

1. Jaeger T. Operating System Security. Morgan and Claypool Publishers, 2008, 220 p.

2. Landwehr C. Formal Models for Computer Security. ACM Computing Surveys, vol. 13, issue 3, 1981, pp. 247-278.

3. Федеральная служба по техническому и экспортному контролю. Информационное сообщение о требованиях по безопасности информации, устанавливающих уровни доверия к средствам технической защиты информации и средствам обеспечения безопасности информационных технологий от 29 марта 2019 г. / FSTEC Russia. Information message on information security requirements establishing levels of confidence in information security tools and information technology security tools dated March 29, 2019. Available at: https://fstec.ru/normotvorcheskaya/informatsionnye-i-analiticheskie-materialy/1812-informatsionnoe-soobshchenie-fstek-rossii-ot-29-marta-2019-g-n-240-24-1525 (in Russian), accessed 14.01.2020.

4. Young M. et al. The duality of memory and communication in the implementation of a multiprocessor operating system. In Proc. of the 11th Symposium on Operating Systems Principles, 1987, pp. 63-76.

5. Hohmuth M., Peter M., Härtig H., Shapiro J. Reducing TCB Size by Using Untrusted Components: Small Kernels versus Virtual-Machine Monitors. In Proc. of the 11th ACM SIGOPS European Workshop, 2004..

6. Biggs S., Lee D., Heiser G. The Jury Is. In Proc. of the 9th Asia-Pacific Workshop on Systems. 2018, Article No. 16.

7. Herder J. N., Bos H., Gras B., Homburg P., Tanenbaum A. S. Construction of a Highly Dependable Operating System. In Proc. of the Sixth European Dependable Computing Conference, 2006, pp. 3-12.

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

9. Biba K. Integrity Considerations for Secure Computer Systems. Technical report MTR-3153, The MITRE Corporation, 1977.

10. Lipner S. Non-Discretionary Controls for Commercial Applications. In Proc. of the 1982 IEEE Symposium on Security and Privacy, 1982. pp. 2-10.

11. Clark D., Wilson D. A Comparison of Commercial and Military Computer Security Policies. In Proceedings of the 1987 IEEE Symposium on Security and Privacy, 1987, pp. 184-195.

12. Lee, T. Using Mandatory Integrity to Enforce “Commercial” Security. In Proc. of the 1988 IEEE Symposium on Security and Privacy, 1988, pp. 140-146.

13. Brewer D., Nash M. The Chinese Wall Security Policy. In Proc. of the 1989 IEEE Symposium on Security and Privacy, 1989, pp. 206-214.

14. Liu Z., Wang T., Li W. An Integrity Control Model for Operating System. In Proc. of the 2009 International Conference on Management and Service Science, 2009, pp. 1-4.

15. Bell D., LaPadula L. Secure Computer System: Unified Exposition and Multics Interpretation. Technical Report MTR-2997 Rev. 1, The MITRE Corporation, 1976.

16. Li N., Mao Z., Chen H. Usable Mandatory Integrity Protection for Operating Systems. In Proc. of the 2007 IEEE Symposium on Security and Privacy, 2007, pp. 164-178.

17. Zhai E. et al. SecGuard: Secure and Practical Integrity Protection Model for Operating Systems. In Proc.of the 13th Asia-Pacific Web Conference, 2011, pp. 370-375.

18. Devyanin P. et al. Using Refinement in Formal Development of OS Security Model. Lecture Notes in Computer Science, vol. 9609. 2015, pp. 107-115.

19. Devyanin P. et al. Formal Verification of OS Security Model with Alloy and Event-B. Lecture Notes in Computer Science, vol. 8477, 2014, pp. 309-313.

20. П.Н. Девянин и др. Моделирование и верификация политик безопасности управления доступом в операционных системах. Горячая линия–Телеком, 2019б 214 стр. / P.N. Devyanin, D.V. Efremov, V.V. Kulyamin, A.K. Petrenko, A.V. Khoroshilov, I.V. Shchepetkov. Modeling and verification of access control security policies in operating systems. Hotline – Telecom, 2019, 214 p.

21. Yosifovich P., Russinovich M., Solomon D., Ionescu A. Windows Internals, Part 1: System architecture, processes, threads, memory management, and more (7th Edition). Microsoft Press. 2017. 800 p.

22. Rushby J. Design and Verification of Secure Systems. In Proc. of the 8th ACM Symposium on Operating Systems Principles, 1981, pp. 12-21.

23. Alves-Foss J., Oman P., Taylor C. The MILS Architecture for High-Assurance Embedded Systems. International Journal of Embedded Systems, vol. 2, no. 3/4, 2006, pp. 239-247.

24. Spencer R., Smalley S., Loscocco P., Hibler M., Andersen D., Lepreau J. The Flask Security Architecture: System Support for Diverse Security Policies. In Proc. of the 8th USENIX Security Symposium, 1999.

25. Baier C., Katoen J.-P. Principles of Model Checking. The MIT Press. 2008. 975 pp.

26. Bishop M., Snyder L. The Transfer of Information and Authority in a Protection System. In Proc. of the 7th ACM symposium on Operating systems principles, 1979, pp. 45-54.

27. Bishop M. Conspiracy and Information Flow in the Take-Grant Protection Model. Journal of Computer Security, vol. 4, no. 4, 1996, pp. 331-359.


Рецензия

Для цитирования:


Буренков В.С., Кулагин Д.А. Модель мандатного контроля целостности в операционной системе KasperskyOS. Труды Института системного программирования РАН. 2020;32(1):27-56. https://doi.org/10.15514/ISPRAS-2020-32(1)-2

For citation:


Burenkov V.S., Kulagin D.A. A Mandatory Integrity Control Model for the KasperskyOS Operating System. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2020;32(1):27-56. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(1)-2



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)