Comparison of methods for modeling access control in os and dbms in Event-B for the purpose of their verification with Rodin and ProB tools
The paper presents two methods of modeling interacting systems with developed access control mechanisms, such as OS and DBMS. These methods are the result of translating the description of the formal access control model of Astra Linux Special Edition OS (MROSL DP-model) from mathematical to formalized notation using the formal Event-B method, as well as its automatic verification using Rodin and ProB tools. The considered methods are based on the use of various options for constructing a hierarchy of specifications of the MROSL DP-model in the formalized notation using the technique “refinement”. We compare these methods showing their advantages and disadvantages. They consist in the complexity of writing specifications, the need to repeat proofs during the verification with the Rodin tool, the possibility of eliminating the effect of “combinatorial explosion” during the verification with the ProB tool. Based on the results of the comparison, it is concluded that considered methods can be useful in the development of other formal access control models and their verification using appropriate tools.
Keywords
formal access control model,
Event-B,
verification,
deductive verification,
Rodin,
model checking,
ProBAuthors
| Leonova Maria A. | LLC "RusBITech-Astra" | mleonova@astralinux.ru |
| Devyanin Petr N. | Academy of Cryptography of the Russian Federation; LLC "RusBITech-Astra" | pdevyanin@astralinux.ru |
Всего: 2
References
ГОСТ Р 59453.1-2021 «Защита информации. Формальная модель управления доступом. Ч. 1. Общие положения». М.: Стандартинформ, 2021. 16 с.
Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками: учеб. пособие для вузов. 3-е изд., перераб. и доп. М.: Горячая линия - Телеком, 2020. 352 с.
https://astralinux.ru/products/astra-linux-special-edition/- Операционная система специального назначения Astra Linux Special Edition. 2022.
Буренин П.В., Девянин П.Н., Лебеденко Е.В. и др. Безопасность операционной системы специального назначения Astra Linux Special Edition: учеб. пособие для вузов. 3-е изд., перераб. и доп. М.: Горячая линия - Телеком, 2019. 404 с.
Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
Девянин П.Н., Ефремов Д.В., Кулямин В.В. и др. Моделирование и верификация политик безопасности управления доступом в операционных системах. М.: Горячая линия - Телеком, 2019. 214 с.
Девянин П. Н., Леонова М. А. Применение подтипов и тотальных функций формального метода Event-B для описания и верификации МРОСЛ ДП-модели // Программная инженерия. 2020. Т. 11. №4. С. 230-241.
ГОСТ Р 59453.2-2021 «Защита информации. Формальная модель управления доступом. Ч.2. Рекомендации по верификация формальной модели управления доступом». М.: Стандартинформ, 2021. 12 с.
Abrial J.-R., Butler M., Hallerstede S., et al. Rodin: An open toolset for modelling and reasoning in Event-B // Intern. J. Software Tools for Technology Transfer. 2010. V. 12. No. 6. P. 447-466.
Девянин П. Н., Тележников В. Ю., Хорошилов А. В. Формирование методологии разработки безопасного системного программного обеспечения на примере операционных систем // Труды ИСП РАН. 2021. Т. 33. № 5. С. 25-40.
Leuschel M. and Butler M. ProB: an automated analysis toolset for the B method // Int. J. Softw. Tools Technol. Transf. 2008. No. 10(2). P. 185-203.
Девянин П. Н., Леонова М. А. Приёмы по доработке описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её автоматизированной верификации с применением инструментов Rodin и ProB // Прикладная дискретная математика. 2021. № 52. С. 83-96.
Abrial J.-R. and Hallerstede S. Refinement, decomposition, and instantiation of discrete models: Application to Event-B // Fundamenta Informaticae. 2007. V. 77. Iss. 1-2. P. 1-28.
