30-Mar-2017: XIX scientific conference "RusCrypto'2017" took place in Moscow

XIX scientific conference "RusCrypto'2017" has taken place in Moscow region on March, 21-24 at "Sunny Park Hotel & SPA" dedicated to information security and privacy.

At the section "Analysis, modeling and program transformation technologies for creating secure software" Alexey Khoroshilov presented a talk ADV_SPM — Formal security policy models in practice, discussing the ADV_SPM "Security policy modeling" assurance family, which is a 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.

While historical roots of the term "security policy" are in access control policies and security policy models have appeared as access control models, ADV_SPM considers "security policy" wider, as a set of related functional security requirements. That is why for illustration we have taken a simplified example of security policy defining a FRU_PRS "Priority of service" model (defined in ISO/IEC 15408-2). We have demonstrated an approach to the formalization and verification of security policies using the Event-B modeling notation and the Rodin platform, whose rigour is used to obtain the desired security properties by means of formal machine-checkable proofs.