Uncertainty Problem in High-Level Model-Based Trace Analysis as Part of Runtime Verification
https://doi.org/10.15514/ISPRAS-2024-36(4)-13
Abstract
The article discusses the problem of applying runtime verification to large and complex systems such as general-purpose operating systems. When verifying the security mechanisms of operating systems, modern practices and standards require a formal security policy model (SPM). The SPM must be verified using formal model methods, and it must also be used to verify the completeness and consistency of the operating system’s security mechanisms by confirming compliance with the formal requirements of the SPM. In this case, it is convenient to have a single model suitable for both formal verification and implementation testing. For practical application, it is necessary, on the one hand, to select a subset of model language constructs suitable for both acts, and on the other hand, to develop special techniques for analyzing execution traces that allow to effectively perform thousands of test cases. The article addresses both of these issues. We present an analysis of language constructs that allow us to use the model for both verification and execution trace analysis. We also offer techniques that have been developed to optimize the runtime verification of Linux-based systems. We also implemented the proposed methods in the trace analysis tool prototype.
About the Author
Aleksei Aleksandrovich KARNOV
Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Russian Federation
Postgraduate student. Research interests: formal specifications, verification and testing, static and dynamic analysis.
References
1. Bartocci E., Falcone Y., Fracalanza A., Reger G. Introduction to runtime verification. In Bartocci E., Falcone Y. (editors) Lectures on Runtime Verification. Lecture Notes in Computer Science, vol. 10457, Springer, 2018. pp. 1–33. DOI: 10.1007/978-3-319-75632-5_1.
2. Reger G., Havelund K. What Is a Trace? A Runtime Verification Perspective. In Margaria T., Steffen B. (editors) Leveraging Applications of Formal Methods, Verification and Validation: Discussion, Dissemination, Applications. Lecture Notes in Computer Science, vol. 9953, Springer, 2016. DOI: 10.1007/978-3-319-47169-3_25.
3. ГОСТ Р 59453.1. Защита информации. Формальная модель управления доступом. Часть 1. Общие положения: описание стандарта и тендеры. – Введен 2021-06-01 – Москва: Стандартинформ, 2021. / State Std. GOST R 59453.1. Information protection. Formal access control model. Part 1. General principles. Moscow, 2021 (in Russian).
4. ГОСТ Р 59453.2. Защита информации. Формальная модель управления доступом. Часть 2. Рекомендации по верификации формальной модели управления доступом. – Введен 2021-06-01 – Москва: Стандартинформ, 2021. / State Std. GOST R 59453.1. Information protection. Recommendations on verification of formal access control model. Part 2. General principles. Moscow, 2021 (in Russian).
5. Девянин П. Н., Ефремов Д. В., Кулямин В. В., Петренко А. К., Хорошилов А. В.,
6. Щепетков И. В. Моделирование и верификация политик безопасности управления доступом в операционных системах. Горячая линия – Телеком, Москва, Россия, 2019. / 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. Moscow, Russia: Hotline-Telecom, 2019 (in Russian).
7. Ефремов Д. В., Копач В. В., Корныхин Е. В., Кулямин В. В. , Петренко А. К., Хорошилов А. В., Щепетков И. В. Мониторинг и тестирование модулей операционных систем на основе абстрактных моделей поведения системы. Труды ИСП РАН, 2021, том 33, вып. 6, стр. 15–26. DOI: 10.15514/ISPRAS-2021-33(6)-2. / Efremov D. V., Kopach V. V., Kornykhin E. V.,
8. Kulyamin V. V., Petrenko A.K., Khoroshilov A. V., Shchepetkov I. V. Runtime verification of operating systems based on abstract models. Proceedings of ISP RAS, 2021, vol. 33, no. 6, pp. 15–26 (in Russian). DOI: 10.15514/ISPRAS-2021-33(6)-2.
9. Девянин П. Н., Леонова М. А. Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB. ПДМ, 2021, № 52, стр. 83–96. DOI: 10.17223/20710410/52/5. / Devyanin P. N., Leonova M. A. The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB. Prikladnaya Diskretnaya Matematica, 2021, no. 52, pp. 83–96, (in Russian). DOI: 10.17223/20710410/52/5.
10. Abrial J.-R., Butler M., Hallerstede S., Hoang T., Mehta F., Voisin L. Rodin: an open toolset for modelling and reasoning in Event-B. The International Journal on Software Tools for Technology Transfer, vol. 12. Springer, 2010, pp. 447–466. DOI: 10.1007/s10009-010-0145-y.
11. Leuschel M., Butler M. ProB: an automated analysis toolset for the B method. The International Journal on Software Tools for Technology Transfer, vol. 10, Springer, 2008, pp. 185–203.
12. DOI: 10.1007/s10009-007-0063-9.
13. Déharbe D. Integration of SMT-solvers in B and Event-B development environments. Science of Computer Programming, vol. 78, 2013, pp. 310– 326. DOI: 10.1016/j.scico.2011.03.007.
14. Schmidt J., Leuschel M. SMT solving for the validation of B and Event-B models. The International Journal on Software Tools for Technology Transfer, vol. 24, Springer, 2022, pp. 1043–1077.
15. DOI: 10.1007/s10009-022-00682-y.
16. Brauer E. Second-order logic and the power set. Journal of Philosophical Logic, vol. 47, 2018, pp. 123–142. DOI: 10.1007/s10992-016-9422-x.
17. Fürst A., Hoang T., Basin D., Desai K., Sato N., Miyazaki K. Code generation for Event-B. Presented at the Integrated Formal Methods 2014, Bertinoro, Italy, 09 2014.
18. Wright S., Automatic generation of C from Event-B. Presented at the Workshop on Integration of Model-based Formal Methods and Tools, Bangkok, Thailand, 02 2009.
19. Yang F., Jacquot J.-P., Souquières J. JeB: Safe simulation of Event-B models. Presented at the The 20th Asia-Pacific Software Engineering Conference, Bangkok, Thailand, 12 2013.
20. DOI: 10.1109/APSEC.2013.83
21. Cataño N., Rivera V., EventB2Java: A code generator for Event-B. In Rayadurgam, S., Tkachuk, O. (editors) NASA Formal Methods. Lecture Notes in Computer Science, vol. 9690, Springer, 2016.
22. DOI: 10.1007/978-3-319-40648-0_13.
23. Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками. Горячая линия – Телеком, Москва, Россия, 2013. / Devyanin P. N. Security models of computer systems. Control for access and information flows. Moscow, Russia: Hotline-Telecom, 2013, (in Russian).
Review
For citations:
KARNOV A.A. Uncertainty Problem in High-Level Model-Based Trace Analysis as Part of Runtime Verification. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2024;36(4):169-182. (In Russ.) https://doi.org/10.15514/ISPRAS-2024-36(4)-13
Email this article 