ADV_SPM - формальные модели политики безопасности на практике
Автор: Хорошилов А.В., Щепетков И.В.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 3 т.29, 2017 года.
Бесплатный доступ
В статье рассматривается семейство требований доверия к безопасности ADV_SPM «Моделирование политики безопасности», которое определяется стандартом ГОСТ Р ИСО/МЭК 15408-3-2013 «Критерии оценки безопасности информационных технологий. Часть 3. Компоненты доверия к безопасности». Обсуждаются задачи, решаемые этим семейством, и вопросы, которые возникают при попытке интерпретировать его требования. На простом примере представляется подход к формализации политик безопасности при помощи языка формальных спецификаций Event-B и инструментов платформы Rodin.
Информационная безопасность, политики безопасности, формальные модели
Короткий адрес: https://sciup.org/14916440
IDR: 14916440 | DOI: 10.15514/ISPRAS-2017-29(3)-4
Список литературы ADV_SPM - формальные модели политики безопасности на практике
- ISO/IEC 15408-1:2012 Information technology -Security techniques -Evaluation criteria for IT security -Part 1: Introduction and general model.
- ISO/IEC 15408-2:2013 Information technology -Security techniques -Evaluation criteria for IT security -Part 2: Security functional requirements.
- ISO/IEC 15408-3:2013 Information technology -Security techniques -Evaluation criteria for IT security -Part 3: Security assurance requirements.
- 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
- 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
- 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
- Burenin P.V., Devyanin P.N., Lebedenko E.V., Proskurin V.G., Cibulya A.N. Security of the special purpose Astra Linux Special Edition operating system. Textbook for high schools. 2nd ed. Hot line -Telecom, Moscow , 2016. 312 p.
- Abrial J.-R. Modeling in Event-B: System and Software Engineering. Cambridge University Press, 2010.
- 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.
