Formal model-driven security combining B-method and process algebra

Formal model-driven security combining B-method and process algebra

연구 분야: Safety

학회: Innovations in Systems and Software Engineering

The development of complex software systems as done today generates countless security vulnerabilities that are difficult to detect. In this context, several research works have adopted the Model Driven Security (MDS) approach, which investigates software models rather than implementations. Separation of concerns is a core technique in MDS; its intention is to master the complexity of the IS by distinguishing its functional concerns (data model and the associated business logic) from high-level ACIT properties (Availability, Confidentiality, Integrity, Traceability). However, a direct consequence of the separation of concerns principle is that functional and security models are often validated separately. Existing works in MDS are therefore stateless and they mostly validate security policies statically without taking into account the dynamic evolution of the IS. Hence, they do not address the impact of functional behavior on the security context of the system, which can be cause for several flaws, specially insider threats. In order to address this challenge, we propose Formal Model-Driven Security based on the B method and process algebra for both functional and security concerns. This paper is a review of our approach. It first presents the backbone of B4MSecure a MDE platform that we developed to assist our approach. Then it shows how dynamic analyses can be done based on this formal framework. In addition to the identification of insider threats it shows how testing can be done in order to verify the correctness of the IS.