ZHIOUA Zeineb

La personne a quitté EURECOM
  • ZHIOUA Zeineb

Thesis

Spécification et Vérification Formelles des Règles de Bonnes Pratiques pour la Certification des Programmes

LLes processus d'ingénierie logicielle ont connu une croissance exponentielle au cours des dernières années en termes de complexité de code et de taille d'équipe de développement travaillant sur le même projet. En conséquence, le développement de logiciels sécurisés est devenu une tâche de plus en plus difficile, du fait qu'elle nécessite tout d'abord d'établir les mécanismes de sécurité nécessaires pour éviter les failles et les erreurs pouvant être source de vulnérabilités.

Exécuter des tests ne permet pas de détecter les erreurs avant le lancement ou le déploiement du logiciel, en plus du fait qu'ils soient plus coûteux surtout s'ils doivent attendre la fin du développement pour être exécutés.

Adopter l'analyse statique du code et sa mise en place du côté des programmeurs seraient une décision judicieuse pour différentes raisons. Tout d'abord, l'analyse statique ne doit pas forcément attendre la fin du cycle de développement, et peut s'exécuter sur des morceaux de logiciel, ou même sur un produit qui n'est pas nécessairement complet ou fini.

Un autre avantage de l'application de l'analyse statique est qu'elle ne nécessite pas l'exécution ou la compilation du code, et peut être gérée par le développeur lorsque les activités de développement sont encore en cours. De plus, identifier et détecter avec précision la source de la violation peut être beaucoup plus rapide et plus précise.

L'utilisation d'outils d'analyse statique existants nécessite une expertise et une maîtrise des développeurs pour interpréter et appliquer les correctifs nécessaires pour remédier aux problèmes de sécurité détectés. Cependant, les développeurs ne devraient pas à la base être des experts en sécurité, et il serait donc nécessaire de leur fournir les directives et orientations nécessaires lors de l'utilisation d'outils d'analyse statique du code. En outre, ces outils sont plutôt centrés sur la détection de vulnérabilités et ne se concentrent pas sur la vérification des règles de bonnes pratiques de sécurité, étant que ces derniers sont présentés de manière informelle, ce qui rend leur interprétation et leur mise en oeuvre difficiles pour les développeurs.

L'objectif de cette thèse étant de réduire l'écart entre la présentation informelle des règles de programmation sécurisée et leur vérification automatique au niveau du code de point de vue du programmeur. Les règles de programmation sécurisée que nous considérons concernent les bonnes ainsi que les mauvaises pratiques de programmation.

L'intégration de la spécification formelle et la vérification automatique des règles de codage sécurisé dans les différentes phases du cycle de développement est un autre objectif essentiel de notre travail.

Nous expliquons comment ces règles pourraient être formalisées par des experts en sécurité, ensuite vérifiées formellement par les développeurs. Notre approche repose sur l'abstraction des actions dans un programme, et sur la combinaison de la vérification du modèle avec l'analyse de contrôle et de flux de données. Notre objectif est de formaliser l'ensemble des connaissances existantes dans les bonnes pratiques de sécurité à l'aide de formules dans le langage MCL, et de vérifier formellement la conformité des programmes avec ces règles de codage sécurisé, moyennant la vérification de modèle. Fournir un retour précis et clair au programmeur est un des objectifs de ce travail, et qui vise à fournir de l'aide au développeur pour lui expliquer succinctement la source de la violation, et éventuellement comment la corriger.

Ce travail de thèse a abouti à la conception d'une chaîne d'outils et à sa mise en oeuvre couvrant la vérification automatique et systématique de bout en bout de la conformité aux règles de codage sécurisé au niveau du code.