Preview

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

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

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

https://doi.org/10.15514/ISPRAS-2020-32(6)-3

Полный текст:

Аннотация

Модели мандатного контроля целостности в операционных системах, как правило, накладывают ограничения на доступы активных компонент системы к пассивным и представляют эти доступы непосредственно. Такое представление можно использовать в случае операционных систем с монолитной архитектурой, где части системы, обеспечивающие доступ к ресурсам, входят в доверенную вычислительную базу. Однако доказательство отсутствия ошибок в таких компонентах и, следовательно, соответствия такой модели реальной системе является чрезвычайно трудной задачей. KasperskyOS – операционная система, основанная на микроядре и позволяющая организовать доступ к ресурсам с помощью компонентов, не обязательно входящих в доверенную вычислительную базу. Для KasperskyOS была разработана и реализована модель мандатного контроля целостности, учитывающая наличие таких компонентов и возможность их некорректного функционирования. В данной статье представлен процесс формализации этой модели и автоматизированного доказательства свойств, обеспечиваемых моделью. Описана разработка модели на языке Event-B и отражен опыт ее верификации с использованием платформы Rodin.

Об авторе

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


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

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.


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


БУРЕНКОВ В.С. Формальная верификация модели мандатного контроля целостности в операционной системе KasperskyOS. Труды Института системного программирования РАН. 2020;32(6):31-48. https://doi.org/10.15514/ISPRAS-2020-32(6)-3

For citation:


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

Просмотров: 103


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


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