Необходимо зарегистрироваться, чтобы получить доступ к полным текстам статей и выпусков журналов!
- Название статьи
- Применение TLA+ нотации для описания модели изолированной программной среды субъектов доступа и ее дальнейшей верификации
- Авторы
- Каннер Андрей Михайлович kanner@okbsapr.ru, программист группы программирования ПО для СЗИ отдела программирования СЗИ, ЗАО «ОКБ САПР», Москва, Россия
- В разделе
- ТЕХНИЧЕСКАЯ ЗАЩИТА ИНФОРМАЦИИ. УПРАВЛЕНИЕ ДОСТУПОМ
- Ключевые слова
- модель ИПСС / спецификация модели ИПСС / верификация модели ИПСС / темпоральная логика действий Лэмпорта / TLA+ / метод Model Checking
- Год
- 2021 номер журнала 3 Страницы 8 - 11
- Индекс УДК
- 004.056
- Код EDN
- Код DOI
- 10.52190/2073-2600_2021_3_8
- Тип статьи
- Научная статья
- Аннотация
- Рассматриваются недостатки верификации математических нотаций моделей безопасности. Предлагается использование темпоральной логики действий Лэмпорта для представления моделей безопасности на формальном языке, пригодном для верификации с применением инструментальных средств. Рассматривается модель изолированной программной среды субъектов доступа, приводится ее спецификация в TLA+ нотации, описываются достоинства верификации данной спецификации с использованием инструментальных средств.
- Полный текст статьи
- Для прочтения полного текста необходимо купить статью
- Список цитируемой литературы
-
Каннер А. М. Подход к верификации подсистемы управления доступом операционной системы Linux: мат. XXV Научно-практ. конф. "Комплексная защита информации" 15-17 сентября 2020 г. - М.: Медиа Группа "Авангард", 2020. С. 24-28.
Каннер А. М., Каннер Т. М. Моделирование и верификация подсистемы управления доступом средства защиты информации Аккорд-Х // Вопросы защиты информации. 2020. № 3. С. 6-10.
Kanner A. M. Correctness of Data Security Tools for Protection against Unauthorized Access and their Interaction in GNU/Linux // Global J. Pure and Applied Mathematics. 2016. V. 12. № 3. P. 2479-2501.
Щербаков А. Ю. Современная компьютерная безопасность. Теоретические основы. Практические аспекты. - М.: Книжный мир, 2009. - 352 с.
Щербаков А. Ю. Хрестоматия специалиста по современной информационной безопасности. Т. 1. - Saarbrucken: Palmarium Academic Publishing, 2016. - 272 с.
Kanner A. M., Kanner T. M. Verification of a Model of the Isolated Program Environment of Subjects Using the Lamports Temporal Logic of Actions: Proceedings of the VII International Conference "Engineering & Telecommunication", IEEE. 2020.
Kanner A. M., Kanner T. M. Special Features of TLA+ Temporal Logic of Actions for Verifying Access Control Policies: Proceedings of Ural Symposium on Biomedical Engineering, Radioelectronics and Information Technology, IEEE. 2021 (статья принята к публикации).
- Купить
- 500.00 руб
