HomeIssuesThe techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB

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 Matematika - Applied Discrete Mathematics. 2021. № 52. DOI: 10.17223/20710410/52/5

The paper presents techniques to specification access control model of OS Astra Linux Special Edition (the MROSL DP-model) in the formalized notation (formalized using the Event-B formal method), that are based on the use of several global types, separation of general total functions into specific total functions, reduction in the number of invariants and guard of events, which iterate over subsets of a certain set. The result of using these techniques was the simplification of automated deductive verification of formalized notation using the Rodin tool and adaptation of the model to verification by model checking formalized notation using the ProB tool. These techniques can be useful in development of the MROSL DP-model, and also in development of other access control models and verification using appropriate tools.
Download file
Counter downloads: 159
  • Title The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
  • Headline The techniques of formalization of OS Astra Linux Special Edition access control model using Event-B formal method for verification using Rodin and ProB
  • Publesher Tomask State UniversityTomsk State University
  • Issue Prikladnaya Diskretnaya Matematika - Applied Discrete Mathematics 52
  • Date:
  • DOI 10.17223/20710410/52/5
Keywords
access control model, deductive verification, Event-B, Rodin, model checking, ProB
Authors
References
https://astralinux.ru/products/astra-linux-special-edition/- Операционная система специального назначения Astra Linux Special Edition.
Буренин П. В., Девянин П. Н., Лебеденко Е. В. и др. Безопасность операционной системы специального назначения Astra Linux Special Edition: учеб. пособие для вузов / под ред. П. Н. Девянина. 3-е изд., перераб. и доп. М.: Горячая линия - Телеком, 2019. 404с.
https://fstec.ru/component/attachments/download/2832 - Информационное сообщение ФСТЭК России от 15.10.2020 № 240/24/4268.
Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками: учеб. пособие для вузов. 3-е изд., перераб. и доп. М.: Горячая линия - Телеком, 2020. 352 с.
Devyanin P. N., Khoroshilov A. V., Kuliamin V. V., et al. Integrating RBAC, MIC, and MLS in verified hierarchical security model for operating system // Program. Comput. Soft. 2020. V.46. P. 443-453.
Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
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.
Девянин П. Н., Ефремов Д. В., Кулямин В. В. и др. Моделирование и верификация политик безопасности управления доступом в операционных системах. М.: Горячая линия - Телеком, 2019. 214 с.
Девянин П. Н. Уровень запрещающих ролей иерархического представления МРОСЛ ДП-модели // Прикладная дискретная математика. 2018. №39. С. 58-71.
Девянин П. Н. Подходы к моделированию управления доступом в СУБД PostgreSQL в рамках МРОСЛ ДП-модели // Прикладная дискретная математика. Приложение. 2018. №11. С. 95-98.
Девянин П. Н. О результатах формирования иерархического представления МРОСЛ ДП-модели // Прикладная дискретная математика. Приложение. 2016. №9. С. 83-87.
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.
Девянин П. Н., Леонова М. А. Применение подтипов и тотальных функций формального метода Event-B для описания и верификации МРОСЛ ДП-модели // Программная инженерия. 2020. Т. 11. №4. С. 230-241.
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.
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 Matematika - Applied Discrete Mathematics. 2021. № 52. DOI: 10.17223/20710410/52/5
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 Matematika - Applied Discrete Mathematics. 2021. № 52. DOI: 10.17223/20710410/52/5
Download full-text version
Counter downloads: 155