Accéder directement au contenu Accéder directement à la navigation
Thèse

Validation formelle d'implantation de patrons de sécurité

Résumé : Les architectures de systèmes à logiciel posent des défis pour les experts de sécurité. nombreux travaux ont eu pour objectif d’élaborer des solutions théoriques, des guides méthodologiques et des recommandations, pour renforcer la sécurité et protéger ces systèmes.Une solution proposée est d’intégrer des patrons de sécurité comme solutions méthodologiques à adapter aux spécificités des architectures considérées. Une telle solution est considérée fiable si elle résout un problème de sécurité sans affecter les exigences du système.Une fois un modèle d’architecture implante les patrons de sécurisé, il est nécessaire de valider formellement ce nouveau modèle au regard des exigences attendues. Les techniques de model checking permettent cette validation en vérifiant, d’une part, que les propriétés des patrons de sécurité sont respectées et, d’autre part, que les propriétés du modèle initial sont préservées.Dans ce travail de thèse, nous étudions les méthodes et les concepts pour générer des modèles architecturaux respectant des exigences de sécurité spécifiques. Àpartir d’un modèle d’architecture logicielle, d’une politique de sécurité et d’une librairie des patrons de sécurité, nous souhaitons générer une architecture sécurisée. Chaque patron de sécurité est décrit par une description formelle de sa structure et de son comportement, ainsi qu’une description formelle des propriétés de sécurité associées à ce patron.Cette thèse rend compte des travaux sur l’exploitation de techniques de vérification formelle des propriétés, par model-checking. L’idée poursuivie est de pouvoir générer un modèle d’architecture qui implante des patrons de sécurité, et de vérifier que les propriétés de sécurité, comme les exigences de modèle, sont respectées dans l’architecture résultante.En perspective, les résultats de notre travail pourraient s'appliquer à définir une méthodologie pour une meilleure validation de la sécurité des systèmes industriels comme les SCADA.
Type de document :
Thèse
Liste complète des métadonnées

Littérature citée [73 références]  Voir  Masquer  Télécharger

https://tel.archives-ouvertes.fr/tel-02319224
Contributeur : Abes Star :  Contact
Soumis le : jeudi 17 octobre 2019 - 17:37:07
Dernière modification le : lundi 19 avril 2021 - 15:36:04

Fichier

2018_fadi_obeid_2.pdf
Version validée par le jury (STAR)

Identifiants

  • HAL Id : tel-02319224, version 1

Citation

Fadi Obeid. Validation formelle d'implantation de patrons de sécurité. Génie logiciel [cs.SE]. ENSTA Bretagne - École nationale supérieure de techniques avancées Bretagne, 2018. Français. ⟨NNT : 2018ENTA0002⟩. ⟨tel-02319224⟩

Partager

Métriques

Consultations de la notice

238

Téléchargements de fichiers

145