ADV_SPM - Формальные модели политики безопасности на практике
https://doi.org/10.15514/ISPRAS-2017-29(3)-4
Аннотация
В статье рассматривается семейство требований доверия к безопасности ADV_SPM «Моделирование политики безопасности», которое определяется стандартом ГОСТ Р ИСО/МЭК 15408-3-2013 «Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности». Обсуждаются задачи, решаемые этим семейством, и вопросы, которые возникают при попытке интерпретировать его требования. На простом примере представляется подход к формализации политик безопасности при помощи языка формальных спецификаций Event-B и инструментов платформы Rodin.
Об авторах
А. В. Хорошилов
ИСП РАН; ВМК МГУ; Московский физико-технический институт; НИУ ВШЭ
Россия
Россия
И. В. Щепетков
ИСП РАН
Россия
Россия
Список литературы
1. ГОСТ Р ИСО/МЭК 15408-1-2012 Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 1. Введение и общая модель.
2. ГОСТ Р ИСО/МЭК 15408-2-2013 Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 2. Функциональные компоненты безопасности.
3. ГОСТ Р ИСО/МЭК 15408-3-2013 Информационная технология. Методы и средства обеспечения безопасности. Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности
4. Huynh, N., Frappier, M., Mammar, A., Laleau, R., Desharnais, J.: Validating the RBAC ANSI 2012 standard using B. In: Abstract State Machines, Alloy, B, TLA, VDM, and Z. (2014) 255–270
5. Devyanin P.N., Khoroshilov A.V., Kuliamin V.V., Petrenko A.K., Shchepetkov I.V. Formal Verification of OS Security Model with Alloy and Event-B. In A. Yamine and K.-D. Schewe, eds. Abstract State Machines, Alloy, B, TLA, VDM, and Z, LNCS 8477:309-313, Proceedings of ABZ-2014, Toulouse, France, June 2-6, 2014, pp. 309-313. DOI: 10.1007/978-3-662-43652-3_30.
6. Devyanin P.N., Khoroshilov A.V., Kuliamin V.V., Petrenko A.K., Shchepetkov I.V. Comparison of Specification Decomposition Methods in Event-B. Programming and Computer Software, 2016, Vol. 42, No. 4, pp. 198–205. DOI: 10.1134/S0361768816040022.
7. Буренин П.В., Девянин П.Н., Лебеденко Е.В., Проскурин В.Г., Цибуля А.Н. Безопасность операционной системы специального назначения Astra Linux Special Edition. Учебное пособие для вузов. 2-е изд. М.: Горячая линия — Телеком, 2016, 312 с.
8. Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
9. Abrial J.-R., Butler M., Hallerstede S., Hoang T. S., Mehta F., Voisin L. Rodin: An Open Toolset for Modelling and Reasoning in Event-B. International Journal on Software Tools for Technology Transfer, 12(6), рр. 447-466, 2010.
Рецензия
Для цитирования:
Хорошилов А.В., Щепетков И.В. ADV_SPM - Формальные модели политики безопасности на практике. Труды Института системного программирования РАН. 2017;29(3):43-56. https://doi.org/10.15514/ISPRAS-2017-29(3)-4
For citation:
Khoroshilov A.V., Shchepetkov I.V. ADV_SPM - Formal security policy models in practice. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2017;29(3):43-56. (In Russ.) https://doi.org/10.15514/ISPRAS-2017-29(3)-4
Послать статью по эл. почте 