Formal Verification of a Mandatory Integrity Control Model for the KasperskyOS Operating System
https://doi.org/10.15514/ISPRAS-2020-32(6)-3
Abstract
Models of mandatory integrity control in operating systems usually restrict accesses of active components of a system to passive ones and represent the accesses directly. This is suitable in case of monolithic operating systems whose components that provide access to resources are part of the trusted computing base. However, due to the sheer complexity of such components, it is extremely nontrivial to prove such a model to be adequate to the real system. KasperskyOS is a microkernel operating system that organizes access to resources via components that are not necessarily part of the trusted computing base. KasperskyOS implements a specifically developed mandatory integrity control model that takes such components into account. This paper formalizes the model and describes the process of automated proof of the model’s properties. For formalization, we use the Event-B language. We clarify parts specific to Event-B to make our presentation accessible to professionals familiar with discrete mathematics but not necessarily with Event-B. We reflect on the proof experience obtained in the Rodin platform.
About the Author
Vladimir Sergeevich BURENKOV
Kaspersky Lab
Russian Federation
PhD, research developer
Russian Federation
PhD, research developer
References
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 г. / Federal Service for Technical and Export Control. Announcement on Information Security Requirements Establishing Levels of Confidence in Information Protection Means and Information Technology Security Means. URL: https://fstec.ru/normotvorcheskaya/informatsionnye-i-analiticheskie-materialy/1812-informatsionnoe-soobshchenie-fstek-rossii-ot-29-marta-2019-g-n-240-24-1525, accessed 2020-04-16 (in Russian).
4. Буренков В.С., Кулагин Д.А. Модель мандатного контроля целостности в операционной системе 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.
5. Abrial, J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press. 2010, 612 p.
6. Event-B and the Rodin Platform. URL: http://www.event-b.org/, accessed 2020-04-16)
7. Kozachok A.V. TLA+ based access control model specification. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 5, 2018, pp. 147-162. DOI: 10.15514/ISPRAS-2018-30(5)-9.
8. Kim I., Kang M., Choi J., Zegzhda P. Formal Verification of Security Model Using SPR Tool. Computing and Informatics, vol. 25, no. 5, 2006, pp. 353-368.
9. Hu V., Kuhn D., Xie T., Hwang J. Model Checking for Verificaton of Mandatory Access Control Models and Properties. International Journal of Software Engineering and Knowledge Engineering, vol. 21, no. 1, 2011, pp. 103-127.
10. Zhang N., Ryan M., Guelev D. Evaluating Access Control Policies Through Model Checking. In Proc. of the International Conference on Information Security, 2005, pp. 446-460.
11. Devyanin P., Khoroshilov A., Kuliamin V., Petrenko A., Shchepetkov I. Using Refinement in Formal Development of OS Security Model. Lecture Notes in Computer Science, vol. 9609, 2015, pp. 107-115.
12. Devyanin P., Khoroshilov A., Kuliamin V., Petrenko A., Shchepetkov I. Formal Verification of OS Security Model with Alloy and Event-B. Lecture Notes in Computer Science, vol. 8477, 2014, pp. 209-313.
13. Девянин П.Н., Ефремов Д.В., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В.. Моделирование и верификация политик безопасности управления доступом в операционных системах. М., Горячая линия – Телеком, 2019, 214 стр. / Devyanin P.N., Efremov D.V., Kulyamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Modeling and verification of access control security policies in operating systems. M., Hotline – Telecom, 2019, 214 p. (in Russian),
14. Девянин П.Н., Кулямин В.В., Петренко А.К., Хорошилов А.В., Щепетков И.В. Интеграция мандатного и ролевого управления доступом и мандатного контроля целостности в верифицированной иерархической модели безопасности операционной системы. Труды Института системного программирования РАН, том 32, вып. 1, 2020, стр. 7-26 / Devyanin P.N., Kuliamin V.V., Petrenko A.K., Khoroshilov A.V., Shchepetkov I.V. Integrating RBAC, MIC, and MLS in Verified Hierarchical Security Model for Operating System. Trudy ISP RAN/Proc. ISP RAS, vol. 32, issue 1, 2020. pp. 7-26 (in Russian). DOI: 10.15514/ISPRAS–2020–32(1)–1.
15. Hussain S., Farid S., Alam M., Iqbal S., Ahmad S. Modeling of Access Control System in Event-B. The Nucleus, vol. 55, no. 2, 2018, pp. 74-84.
16. Romanovsky A., Thomas M. (Editors). Industrial Deployment of System Engineering Methods. Springer-Verlag, 2013. 274 pp.
17. 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.
Review
For citations:
BURENKOV V.S. Formal Verification of 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(6):31-48. (In Russ.) https://doi.org/10.15514/ISPRAS-2020-32(6)-3
Email this article 