Vérification Formelle Des Propriétés De Sécurité Des Logiciels

Résumé: Cette thèse présente une démarche de vérification formelle des propriétés de sécurité des logiciels. En effet, après étude des approches possibles : preuve formelle et model checking, nous avons identifié le model checking comme étant l'approche la plus adéquate pour notre problématique. Ainsi, la démarche proposée est fondée sur une combinaison de la technique de model checking et des mécanismes : d'annotation et d'abstraction basés sur l'interprétation abstraite. Pour procéder au model checking, nous avons commencé par exprimer les propriétés de sécurité (confidentialité, intégrité, disponibilité) dans une logique temporelle appropriée. Ensuite, nous avons spécifié les systèmes auxquels pouvait s'appliquer notre démarche à savoir : les systèmes dont l'évolution peut être assimilée à un programme impératif réduit aux structures de contrôle de base. Moyennant deux étapes : la première qui enrichit le code source par des informations relatives à la propriété à vérifier et la deuxième qui débarrasse le code source enrichi des informations superflues à la vérification de la propriété de sécurité, nous avons transformé le code source d'un programme impératif en un programme abstrait qui exhibe les instructions concernées par les propriétés à vérifier tout en faisant abstraction du reste. L'annotation aussi bien que l'abstraction ont été développées par interprétation abstraite autour d'une correspondance de Galois qui assure que le programme abstrait correspond au programme initial. Cette démarche a été illustrée par un exemple qui consiste en un gestionnaire de transactions bancaires simplifié.

Publié dans la revue: