A Mandatory Integrity Control Model for the KasperskyOS Operating System

Existing models of mandatory integrity control in operating systems restrict accesses of active components of a system to passive ones and represent the accesses directly: subjects get read or write access to objects. Such a representation can be used in modeling of monolithic operating systems whose components that provide access to resources are part of the trusted computing base. However, the implementation of these components is extremely complex. Therefore, it is arduous to prove the absence of bugs (vulnerabilities) in them. In other words, proving such a model to be adequate to the real system is nontrivial and often left unsolved. This article presents a mandatory integrity control model for a microkernel operating system called KasperskyOS. Microkernel organization of the system allows us to minimize the trusted computing base to include only the microkernel and a limited number of other components. Parts of the system that provide resource access are generally considered untrusted. Even if some of them are erroneous, the operating system can still provide particular security guarantees. To prove that by means of a model, we introduce the notion of object drivers as intermediaries in operations on objects. We define the requirements that object drivers must satisfy. We also add the means for analysis of the consequences of violations of the requirements. We state and prove that the model either preserves integrity if all active components satisfy the requirements, or restricts the negative impact if some of the components are compromised. Correct implementation of the model guarantees that compromised components will not affect components with higher or incomparable integrity levels. We describe a policy specification language developed in accordance with the model. We provide an example of using it to describe a security policy that ensures a correct update of a system operated by KasperskyOS.

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.