About methods of developing consistent description of the mrosl dp-model for os and dbms for its verification with Rodin and ProB TOOLS
Access control mechanism performs one of the main functions to ensure the security of information security tools, such as OS or DBMS. Formal models of access control are developed to achieve confidence in correctness of this mechanism, to create conditions for the scientific justification of its compliance with the security requirements. The paper presents methods of consistent description of the MROSL DP-model in the language used in mathematics (mathematical notation) and in Event-B formal method (formalized notation). The first result of using these methods in refining the formalized notation was provision the possibility of its joint verification by deductive method and method of model checking using the Rodin and ProB tools. The second result was modeling using Event-B formal method of interacting systems with their own developed access control mechanisms, such as OS and DBMS, which is necessary to match the description of the model in mathematical notation. These methods are formed on expression of the properties of the original hierarchical description of the model in mathematical notation in a sequential refinement of the model levels based on the refinement technique of Rodin and on application of total functions instead of directly using axiom of mathematical induction.
Keywords
Astra Linux Special Edition,
verification,
assurance requirements,
formal model of access controlAuthors
| Devyanin P.N. | Academy of Cryptography of the Russian Federation; LLC "RusBitech-Astra" | pdevyanin@astralinux.ru |
| Leonova M.A. | LLC "RusBitech-Astra" | mleonova@astralinux.ru |
Всего: 2
References
Девянин П. Н., Леонова М. А. Приёмы по доработке описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения ее автоматизированной верификации с применением инструментов Rodin и ProB // Прикладная дискретная математика. 2021. №52. С. 83-96.
Девянин П. Н., Леонова М. А. Применение подтипов и тотальных функций формального метода Event-B для описания и верификации МРОСЛ ДП-модели // Программная инженерия. 2020. Т. 11. №4. С. 230-241.
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.
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.
Девянин П. Н., Ефремов Д. В., Кулямин В. В. и др. Моделирование и верификация политик безопасности управления доступом в операционных системах. М.: Горячая линия - Телеком, 2019. 214 с.
Буренин П. В., Девянин П. Н., Лебеденко Е. В. и др. Безопасность операционной системы специального назначения Astra Linux Special Edition: учеб. пособие для вузов / под ред. П. Н. Девянина. 3-е изд., перераб. и доп. М.: Горячая линия - Телеком, 2019. 404с.
Операционная система специального назначения Astra Linux Special Edition. https://astralinux.ru/products/astra-linux-special-edition/
ГОСТ Р 59453.2-2021 «Защита информации. Формальная модель управления доступом. Ч.2. Рекомендации по верификация формальной модели управления доступом». М.: Стандартинформ, 2021. 23 с.
ГОСТ Р 59453.1-2021 «Защита информации. Формальная модель управления доступом. Ч. 1. Общие положения». М.: Стандартинформ, 2021. 35 с.
Выписка из Требований по безопасности информации, утвержденных приказом ФСТЭК России № 76 от 02.06.2020. https://fstec.ru/tekhnicheskaya-zashchita-informatsii/dokumenty-po-sertifikatsii/120-normativnye-dokumenty/2126-vypiska-iz-trebovanij-po-bezopasnosti-informatsii-utverzhdennykh-prikazom-fstek-rossii-ot-2-iyunya-2020-g-n-76.
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.
Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
Девянин П. Н. Модели безопасности компьютерных систем. Управление доступом и информационными потоками: учеб. пособие для вузов. 3-е изд., перераб. и доп. М.: Горячая линия - Телеком, 2020. 352 с.
Bell D. E. and LaPadula L.J. Secure Computer Systems: Unified Exposition and Multics Interpretation. Bedford, Mass.: MITRE Corp., 1976.
Biba K. J. Integrity Considerations for Secure Computer Systems. Bedford, Mass.: MITRE Corp., 1975.
