Model-checking for Secured Component Implementation.
Résumé
A security pattern is a reusable solution for a specific security issue. Based on an insecure model, and using a combination of security patterns, we can generate a model respecting some security requirements constituting a security policy. The resulting model needs to fulfill the security requirements without affecting the original functionalities and services. The security patterns need to be consistent with each
others, as well as the model, they also need to cover the whole security spectrum resulting in completeness. We can use model checking techniques in order to insure the correct functionality, as well as the consistency and completeness of the generated model. In this paper, we describe our approach to combine an architectural model with security patterns to generate a secure model. This model is later verified using model checking techniques to validate the properties of the model itself as well as the used patterns. Finally, using an experimental use case, we demonstrate the possible spatial complexity of our approach.