Une démarche pour l'assistance à l'utilisation des patrons de sécurité

摘要

The last decade has witnessed significant contributions in software engineering to design more secure systems and applications, e.g., in modeling and in validation. Software designers can now leverage specific patterns, called security patterns, to model more secure applications. But, despite the advantages offered by security patterns, these are rarely used in practice, because choosing and employing them is still a difficult and error-prone task. In this work, we propose an original approach to assist designers in using security patterns, i.e., for checking whether security patterns are correctly integrated into models and if vulnerabilities are yet exposed despite their use. This approach relies upon the analysis of the structural and behavioral properties of security patterns and on formal methods to check if these properties hold in the application model completed with patterns. We also provide a metric computation to assess the integration quality of patterns. Furthermore, we also check whether the vulnerabilities, which should be removed by the use of patterns, are not exposed in the model. We illustrate this approach on an example of Web application, the Moodle education platform.%Dans le but de concevoir des applications ne présentant pas de vulnérabilité, la sécurité doit être prise en compte dès les premières phases du cycle de vie du logiciel. Dans ce contexte, la communauté du Génie Logiciel a proposé la notion de patron de sécurité, qui représente une solution réutilisable pour modéliser des applications sûres. Néanmoins, le choix des patrons et leurs intégrations à un modèle existant restent des étapes difficiles, que le concepteur d'application soit expert ou non. Dans ce contexte, nous proposons une démarche d'assistance aux concepteurs focalisée premièrement sur l'intégration structurelle et comportementale de patrons de sécurité dans un modèle UML. Nous définissons et calculons des métriques de qualité d'intégration des patrons, qui permettent de guider le développeur dans son travail de modélisation. Dans une deuxième étape, cette démarche vise également à vérifier si les patrons de sécurité choisis et leurs contextualisations et intégrations dans le modèle évitent réellement l'apparition de vulnérabilités, qui sont supposées éliminées par l'utilisation de ces mêmes patrons. Cette démarche, fondée sur des propriétés en LTL et des méthodes formelles, est appliquée sur un cas d'utilisation d'application Web, la plateforme d'éducation "Moodle".