Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы

В связи с высокой сложностью современных операционных систем (ОС) для спецификации даже отдельных аспектов их функциональности, как, например, функций безопасности, приходится использовать достаточно сложные модели на высокоуровневых языках. При этом задача верификации соответствия таким моделям серьезно усложняется из-за необходимости установления связей между реализацией операционной системы и моделью, представленными на сильно отличающихся языках. В данной работе мы представляем методику установления и поддержания таких связей, которую можно эффективно использовать при тестировании и мониторинге операционных систем. Описанная методика была успешно применена при тестировании и мониторинге компонентов ядра операционной системы Linux с использованием моделей на Event-B.

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.