B for Modeling Secure Information Systems The B4MSecure Platform

摘要

Several approaches dedicated to model access control policies (e.g. MDA-Security, SecureUML, UMLSec, etc.) have used the Model Driven Engineering paradigm in order to ensure a clear separation of business rules and constraints specific to a target technology. Their supporting techniques mainly focus on modeling and verification of security rules without taking into account the functional model of the application and its interaction with the security model. In order to take into account both models, we developed the B4MSecure platform. It is a Model Driven Engineering platform that allows to graphically model and formally reason on both functional and security models. It translates a UML class diagram associated to a SecureUML model into formal B specifications. The resulting B specifications follow the separation of concerns principles in order to be able to validate both models separately and then validate their interactions. This paper gives an overview of our platform.