Direction de recherche : Antoine MINÉ

Co-encadrement : SOUMIER Vincent (Airbus)

Analyse statique de la portabilité des programmes par interprétation abstraite

Les logiciels tendent à être utilisés plus longtemps que prévu lors de leur conception, et dans une plus grande variété d'environnements. L'adaptation d'un logiciel à de nouvelles utilisations peut s'avérer difficile et coûteuse. Assurer la portabilité des programmes est un enjeu majeur : garantir que leur compilation et leur exécution dans un environnement différent a un effet maîtrisé sur leur sémantique.
Cette thèse vise au développement d'analyses statiques par interprétation abstraite pour vérifier de telles propriétés de portabilité sur des programmes C de bas niveau, c'est-à-dire dont le comportement dépend de la représentation de la mémoire.
Vérifier la portabilité consiste à prouver l'équivalence de deux versions syntaxiquement proches d'un programme, qui s'exécutent dans des environnements différents. Nous abordons d'abord le cas particulier de la vérification de non régression, qui vise à prouver l'équivalence de deux versions qui s'exécutent dans le même environnement. Nous proposons une analyse statique de patchs logiciels capable d'inférer de telles équivalences, notamment dans le contexte de programmes C de bas niveau comme ceux utilisés dans les systèmes embarqués.
Puis nous construisons une analyse portabilité comme une extension de l'analyse de patchs. Notre analyse infère deux propriétés liées à la représentation de la mémoire : la portabilité vis-à-vis d'un changement de représentation des scalaires (endianisme), et vis-à-vis d'une organisation différente de la mémoire (offsets des champs scalaires des structures C).
Nous avons implanté un analyseur statique prototype sur la plateforme MOPSA, et l'avons expérimenté sur des logiciels open source et industriels. Il analyse avec succès de grands logiciels avioniques (jusqu'à un million de lignes de C).

Publications 2015-2022

• 2022
  • D. Delmas : “Static analysis of program portability by abstract interpretation”, soutenance de thèse, soutenance 28/11/2022, direction de recherche Miné, Antoine, co-encadrement : Soumier, Vincent (Airbus) (2022)
• 2021
  • D. Delmas, A. Ouadjaout, A. Miné : “Static Analysis of Endian Portability by Abstract Interpretation”, 28^th Static Analysis Symposium (SAS 2021), vol. 12913, Lecture Notes in Computer Science, Chicago, Illinois, United States, pp. 102-123, (Springer International Publishing) (2021)
• 2019
  • D. Delmas, A. Miné : “Analysis of Software Patches Using Numerical Abstract Interpretation”, International Static Analysis Symposium, vol. 11822, Lecture Notes in Computer Science, Porto, Portugal, pp. 225-246, (Springer) (2019)
  • D. Delmas, A. Miné : “Analysis of Program Differences with Numerical Abstract Interpretation”, PERR 2019 - 3^rd Workshop on Program Equivalence and Relational Reasoning, Prague, Czechia (2019)
• 2015
  • A. Miné, D. Delmas : “Towards an industrial use of sound static analysis for the verification of concurrent embedded avionics software”, Embedded Software (EMSOFT), 2015 International Conference on, Amsterdam, Netherlands, pp. 65-74, (IEEE) (2015)