Supervision : Antoine MINÉ
Co-supervision : SOUMIER Vincent (Airbus)
Static analysis of program portability by abstract interpretation
Computer programs tend to be used much longer than expected at design time, and in a wider variety of environments. Adapting a software product for new usage may turn out to be difficult and costly. Ensuring the portability of programs is a major stake: it amounts to ensuring that their compilation and execution in a different environment will have small controlled impact on their semantics.
The goal of this thesis is to develop a novel class of static analyses by abstract interpretation, allowing to verify portability properties of low-level C programs, i.e. programs whose behaviors depend on the representation of computer memory.
Portability verification aims at proving the equivalence of two syntactically close versions of a program running in different environments. We first focus on the particular case of regression verification, which aims at proving the equivalence of two program versions running in the same environment. We propose a static analysis of software patches that is able to infer such equivalence properties, in particular in the context of low-level C programs such as those used in embedded software.
Then we develop an approach to portability analysis of C programs that is designed as an extension of patch analysis. We focus on two portability properties, related to the representation of the computer memory specified by the ABI: portability against different representations of scalars (endianness), and against different memory layouts (offsets of scalar fields in C structs).
We implemented a prototype static analyzer on top of the MOPSA platform, and experimented it on real-world open source and industrial software. It allows successful analyses of large, real-world avionics software up to one million lines of C.
Defence : 11/28/2022
Jury members :
YAHAV Eran (Technion, Israel) [Rapporteur]
CHANG Bor-Yuh Evan (University Colorado Boulder, USA) [Rapporteur]
MINÉ Antoine (Sorbonne Université/LIP6)
CHAILLOUX Emmanuel (Sorbonne Université/LIP6)
FERET Jérôme (INRIA/ENS-DI)
PUTOT Sylvie (École Polytechnique)
SOUMIER Vincent (Airbus)
- D. Delmas : “Static analysis of program portability by abstract interpretation”, thesis, defence 11/28/2022, supervision Miné, Antoine, co-supervision : Soumier, Vincent (Airbus) (2022)
- D. Delmas, A. Ouadjaout, A. Miné : “Static Analysis of Endian Portability by Abstract Interpretation”, 28th Static Analysis Symposium (SAS 2021), vol. 12913, Lecture Notes in Computer Science, Chicago, Illinois, United States, pp. 102-123, (Springer International Publishing) (2021)
- 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 - 3rd Workshop on Program Equivalence and Relational Reasoning, Prague, Czechia (2019)
- 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)