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 - formal security policy models in practice
The paper examines the ADV_SPM "Security policy modelling" assurance family, which is part of the ADV "Development" assurance class and defined by the ISO/IEC 15408-3-2013 "Information technology - Security techniques - Evaluation criteria for IT security - Part 3: Security assurance components" standard. We discuss the objective set by this family, which is to provide additional assurance from the development of a formal security policy model of the target of evaluation security functionality and establishing a correspondence between the functional specification and this security policy model by means of a mathematical proof. We propose an approach to the formalization and verification of security policies using the Event-B modelling notation and the Rodin platform, whose rigour is used to obtain the desired security properties by means of formal machine-checkable proofs. The approach helps to identify and eliminate ambiguous, inconsistent, contradictory, or unenforceable security policy elements. We illustrate this approach with a simplified example of a FRU_PRS "Priority of service" model (defined in the second part of the standard) in which we provide a formal proof that the model contains no inconsistencies, and that an insecure state cannot be reached. We conclude that the approach is applicable for solving practical problems and it can be used to fulfil the requirements of the ADV_SPM assurance family.
Список литературы 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.
