Description
Date depot: 11 septembre 2019
Titre: Analyse statique par interprétation abstraite de langages dynamiques
Directeur de thèse:
Antoine MINE (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Non defini
Resumé:
Le but de la thèse est de développer de nouvelles analyses par interprétation abstraite pour les langages dynamiques.
L'interprétation abstraite est une théorie de l'approximation des sémantiques de programmes. Elle connaît une popularité croissante grâce à ses applications récentes à la conception d'outils effectifs de vérification utilisés dans l'industrie. Néanmoins, ces applications restent limitées à l'analyse de langages statiques, tels que C et Java. Les langages dynamiques, tels que JavaScript ou Python, ont une sémantique plus complexe et offrent peu d'information sur les exécutions possibles d'un programme à la compilation. Les points difficiles incluent: l'absence d'information de type statique, la possibilité d'ajouter des attributs dynamiquement aux objets, des constructions de contrôle complexes (comme les générateurs de Python ou bien les clôtures).
Le travail de thèse s'appuiera notamment sur l'analyse par interprétation abstraite de Python développée par l'équipe très récemment [NFM'18].
Le candidat explorera en particulier les directions de recherche suivantes: les analyse inter-procédurales modulaires afin de passer à l'échelle, l'inférence des appels aux bibliothèques C, la génération automatique des stubs, et l'analyse multi-langages pour les programmes mélangeant C et Python.
Le projet mêlera des aspects théoriques et fondamentaux dans le domaine de l'interprétation abstraite, ainsi que des aspects appliqués: l'implantation des solutions retenues et l'expérimentation dans le cadre d'analyses statiques de programmes réels. Les méthodes développées devront être bien définies formellement, ainsi que prouvées correctes en utilisant le cadre théorique de l'interprétation abstraite. Elles devront être motivées par l'analyse de cas d'étude réels, notamment dans le langage Python qui est au cœur du projet de l'équipe de recherche. Les méthodes feront l'objet d'une implantation logicielle au sein de la plateforme d'analyse statique MOPSA.
Les résultats de cette thèse devraient aboutir au développement d'analyseurs statiques sur de nouvelles classes de programmes et de langages, qui ne peuvent pas être actuellement traités par l'état de l'art. La thèse peut donc avoir un impact important sur l'amélioration de la sûreté de fonctionnement des logiciels.
Doctorant.e: Monat Raphael