Проблема неопределенности в анализе трасс на основе высокоуровневых моделей в контексте динамической верификации
https://doi.org/10.15514/ISPRAS-2024-36(4)-13
Аннотация
В данной статье обсуждается проблема применения метода динамической верификации к большим и сложным системам, в частности, операционным системам общего назначения. Современные практики и стандарты разработки критических систем требуют наличия формальной модели политики безопасности. Полнота и непротиворечивость формальных требований, указанных в модели политики безопасности, должна быть верифицирована с использованием формальных методов. Позже, когда будет разработана реализация системы, необходимо установить, что реализованные механизмы безопасности соответствуют указанным в модели требованиям. При использовании такого подхода удобно иметь единую модель, подходящую как для формальной верификации, так и для тестирования реализации. Для достижения этой цели необходимо, с одной стороны, выделить подмножество языковых конструкций модели, подходящих для обоих методов, а с другой, разработать специальные методики анализа трасс выполнения, позволяющие эффективно выполнять тысячи тестов. В статье приводится анализ языковых конструкций, позволяющих эффективное использование модели в рамках динамической верификации. Также в статье представлены методы оптимизации процесса динамической верификации систем. Предложенные методы были реализованы в прототипе инструмента анализа трасс и протестированы на модели системы контроля доступа для операционных систем на основе Linux.
Об авторе
Алексей Александрович КАРНОВ
Институт системного программирования РАН
Россия
Россия
Аспирант. Научные интересы: формальные спецификации, верификация и тестирование, статический и динамический анализ.
Список литературы
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).
Рецензия
Для цитирования:
КАРНОВ А.А. Проблема неопределенности в анализе трасс на основе высокоуровневых моделей в контексте динамической верификации. Труды Института системного программирования РАН. 2024;36(4):169-182. https://doi.org/10.15514/ISPRAS-2024-36(4)-13
For citation:
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
Послать статью по эл. почте 