Validation formelle d’architecture logicielle basée sur des patrons de sécurité
Résumé
Les modèles de patrons de sécurité ont été proposés comme des solutions méthodologiques permettant de modéliser des mécanismes qui répondent à des problèmes de sécurité récurrents. Ceux-ci sont décrits dans la littérature et peuvent être exploités dans différents contextes de modélisation. Lors de leur intégration au sein d’un modèle d’architecture, ces modèles de patrons sont à adapter à ses spécificités. Une fois les modèles de patrons intégrés, il est nécessaire de valider formellement le résultat de cette intégration au regard des propriétés fonctionnelles de l’architecture initiale qui doivent être préservées, et au regard des propriétés formelles de sécurité associées aux patrons.
Dans notre travail, nous exploitons une technique de model-checking pour la vérification des propriétés. Nous cherchons à exploiter notre approche dans le cadre de la modélisation des architectures SCADA.