|
Эта публикация цитируется в 1 научной статье (всего в 1 статье)
Математические основы компьютерной безопасности
О приемах по доработке согласованного описания МРОСЛ ДП-модели для ОС и СУБД с целью его верификации инструментами Rodin и ProB
П. Н. Девянинab, М. А. Леоноваb a Академия криптографии Российской Федерации, г. Москва
b ООО «РусБИТех-Астра», г. Москва
Аннотация:
Рассматриваются приемы согласованного описания мандатной сущностно-ролевой ДП-модели управления доступом и информационными потоками в операционных системах семейства Linux (МРОСЛ ДП-модели) в математической и формализованной нотациях с целью обеспечения возможностей для, во-первых, её совместной верификации дедуктивным методом и методом проверки моделей (model checking) с применением инструментов Rodin и ProB соответственно, во-вторых, моделирования на формализованном языке метода Event-B взаимодействующих между собой систем с собственными развитыми механизмами управлениями доступом, таких, как ОС и СУБД, что необходимо для соответствия описанию модели в математической нотации.
Ключевые слова:
формальная модель управления доступом, верификация, Event-B, требования доверия, Astra Linux Special Edition.
Образец цитирования:
П. Н. Девянин, М. А. Леонова, “О приемах по доработке согласованного описания МРОСЛ ДП-модели для ОС и СУБД с целью его верификации инструментами Rodin и ProB”, ПДМ. Приложение, 2021, № 14, 126–132
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/pdma546 https://www.mathnet.ru/rus/pdma/y2021/i14/p126
|
Статистика просмотров: |
Страница аннотации: | 110 | PDF полного текста: | 29 | Список литературы: | 16 |
|