Runtime Verification of Operating Systems Based on Abstract Models
Denis Valentinovich EFREMOV,
Viktoria Vladimirovna KOPACH,
Eugeny Valerievich KORNYKHIN,
Viktor Vyacheslavovich KULIAMIN,
Alexander Konstantinovich PETRENKO,
Alexey Vladimirovich KHOROSHILOV,
Ilya Viktorovich SHCHEPETKOV https://doi.org/10.15514/ISPRAS-2021-33(6)-2
Abstract
High complexity of a modern operating system (OS) requires to use complex models and high-level specification languages to describe even separated aspects of OS functionality, e.g., security functions. Use of such models in conformance verification of modeled OS needs to establish rather complex relation between elements of OS implementation and elements of the model. In this paper we present a method to establish and support such a relation, which can be effectively used in testing and runtime verification/monitoring of OS. The method described was used successfully in testing and monitoring of Linux OS core components on conformance to Event-B models.
Supporting agencies: This work was supported by the RFBR grant No. 20-01-00568.
About the Authors
Denis Valentinovich EFREMOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Researcher
Viktoria Vladimirovna KOPACH
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Researcher
Eugeny Valerievich KORNYKHIN
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Lomonosov Moscow State University
Russian Federation
Russian Federation
Ph.D. in Physics and Mathematics, Associate Professor of system programming departments at MSU and Senior Researcher at ISP RAS
Viktor Vyacheslavovich KULIAMIN
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Lomonosov Moscow State University, National Research University, Higher School of Economics
Russian Federation
Russian Federation
Ph.D. in Physics and Mathematics, leading researcher at ISP RAS, associate professor of system programming departments at MSU and the HSE
Alexander Konstantinovich PETRENKO
Ivannikov Institute for System Programming of the Russian Academy of Sciences, Lomonosov Moscow State University, National Research University, Higher School of Economics
Russian Federation
Russian Federation
Doctor of Physical and Mathematical Sciences, Professor, Head of the Department of ISP RAS, Professor of MSU and HSE
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 (MIPT)
Russian Federation
Russian Federation
Ph.D. in Physics and Mathematics, Leading Researcher, Director of the Linux OS Verification Center at ISP RAS, Associate Professor of System Programming Departments at MSU, HSE, and MIPT
Ilya Viktorovich SHCHEPETKOV
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Junior Researcher
References
1. J.-R. Abrial. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010, 612 p.
2. P.N. Devyanin, A.V. Khoroshilov et al. Using Refinement in Formal Development of OS Security Model. Lecture Notes in Computer Science, vol. 9609, 2016, pp. 107-115.
3. V. Kuliamin, A. Khoroshilov и D. Medveded. Formal Modeling of Multi-Level Security and Integrity Control Implemented with SELinux. In Proc. of the International Conference on Actual Problems of Systems and Software Engineering (APSSE), 2019, pp. 131-136.
4. А.К. Петренко, Д.В. Ефремов и др. Мониторинг и тестирование на основе многоуровневых спецификаций программ. Труды ИСП РАН, том 32, вып. 6, 2020 г., стр. 7-18 / A.K. Petrenko, D.V. Efremov et al. Monitoring and testing based on multi-level program specifications. Trudy ISP RAN/Proc. ISP RAS, vol. 32, issue 6, 2020, pp. 7-18 (in Russian). DOI: 10.15514/ISPRAS–2020–32(6)–1.
5. J.-R. Abrial, M. Butler et al. Rodin: an open toolset for modelling and reasoning in Event-B. International Journal on Software Tools for Technology Transfer, vol. 12, issue 6, 2010, pp. 447-466.
6. N. Wirth. Program Development by Stepwise Refinement. Communications of the ACM, vol. 14, issue 4, 1971, pp. 221-227.
7. M. Leuschel, M. Butler. ProB: A Model Checker for B. Lecture Notes in Computer Science, vol. 2805, 2003, pp. 855-874.
8. A. Khoroshilov, V. Kuliamin et al. A State-based Refinement Technique for Event-B. In Proc. of the Ivannikov Memorial Workshop (IVMEM), 2020, pp. 49-54.
9. G. Kroah-Hartman. LSM: Add all of the new security/* files for basic task control. URL: https://git.kernel.org/pub/scm/linux/kernel/git/tglx/history.git/commit?id=2b15fe6334aebd7d3340f8b826acb79b138afa74, accessed 15.01.2022.
10. J. Edge. Progress in security module stacking. URL: https://lwn.net/Articles/635771/, accessed 15.01.2022.
11. J. Edge. LSM stacking and the future. URL: https://lwn.net/Articles/804906/, accessed 15.01.2022.
12. Linux Integrity Subsystem. URL: http://linux-ima.sourceforge.net/, accessed 15.01.2022.
13. A. Edwards, T. Jaeger, X. Zhang. Runtime verification of authorization hook placement for the Linux security modules framework. In Proc. of the 9th ACM Conference on Computer and Communications Security, 2002, pp. 225-234.
14. T. Jaeger, A. Edwards, X. Zhang. Consistency analysis of authorization hook placement in the Linux security modules framework. ACM Transactions on Information and System Security (TISSEC), vol. 7, issue 2, 2004, pp. 175-205.
15. V.V. Rubanov, E. A. Shatokhin. Runtime verification of linux kernel modules based on call interception. In Proc. of the Fourth IEEE International Conference on Software Testing, Verification and Validation, 2011, pp. 180-189.
16. D.B. de Oliveira, T. Cucinotta, R.S. de Oliveira. Efficient formal verification for the Linux kernel. Lecture Notes in Computer Science, vol. 11724, 2019, pp. 315-332.
Review
For citations:
EFREMOV D.V., KOPACH V.V., KORNYKHIN E.V., KULIAMIN V.V., PETRENKO A.K., KHOROSHILOV A.V., SHCHEPETKOV I.V. Runtime Verification of Operating Systems Based on Abstract Models. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2021;33(6):15-26. (In Russ.) https://doi.org/10.15514/ISPRAS-2021-33(6)-2
Email this article 