ГлавнаяАрхивПриёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB

Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB | Прикладная дискретная математика. 2021. № 52. DOI: 10.17223/20710410/52/5

Рассматриваются приёмы по доработке описания модели управления доступом отечественной защищённой операционной системы специального назначения Astra Linux Special Edition (МРОСЛ ДП-модели) в формализованной нотации (на формализованном языке метода Event-B), основанные на использовании нескольких глобальных типов, разделении общих тотальных функций на частные тотальные функции и сокращении числа инвариантов и охранных условий событий, предполагающих перебор подмножеств некоторого множества. Результатом их применения стало упрощение автоматизированной дедуктивной верификации модели с применением инструмента Rodin и её адаптация к верификации с использованием инструмента проверки моделей ProB. Данные приёмы могут быть полезны при разработке других моделей управления доступом и их верификации с применением соответствующих инструментов.
  • Title Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB
  • Headline Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB
  • Publesher Tomask State UniversityTomsk State University
  • Issue Прикладная дискретная математика 52
  • Date:
  • DOI 10.17223/20710410/52/5
Ключевые слова
модель управления доступом, дедуктивная верификация, Event-B, Rodin, метод проверки моделей, ProB
Авторы
Ссылки
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.
Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB | Прикладная дискретная математика. 2021. № 52. DOI: 10.17223/20710410/52/5
Приёмы описания модели управления доступом ОССН Astra Linux Special Edition на формализованном языке метода Event-B для обеспечения её верификации инструментами Rodin и ProB | Прикладная дискретная математика. 2021. № 52. DOI: 10.17223/20710410/52/5