Team : APR
- Sorbonne Université - LIP6
Boîte courrier 169
Couloir 25-26, Étage 3, Bureau 303
4 place Jussieu
75252 PARIS CEDEX 05
Tel: +33 1 44 27 88 16, Matthieu.Journault (at) nulllip6.fr
Supervision : Antoine MINÉ
Precise and modular static analysis by abstract interpretation for the automatic proof of program soundness and contracts inference
Ensuring the scalability of static analyzers defined by abstract interpretation poses difficulties. A classical technique known to speed up analyses is the discovery and reuse of summaries for some of the sequences of statements of the source code. In this thesis we focus on a subset of C that does not allow recursion and define a modular analyzer, able to infer, prove and use (to improve the efficiency) such summaries.
Our modular analyzer is built on top of an existing C analyzer and is therefore able to handle unions, structures, arrays, memory allocations (static and dynamic), pointers, pointer arithmetic, pointer casts, function calls, string manipulations ... . String handling is provided by a new abstract domain defined in this thesis.
In this thesis we provide a lifting of classical numerical abstract domains to the representation of heterogeneous sets. This lifting can be used for relational domains and maintains only one numerical abstract state, in opposition to partitioning.
The last point of interest of this thesis is the definition of an abstract domain able to represent sets of trees with numerically labeled leaves. This abstraction is based on regular and tree regular languages and delegates the handling of numerical constraints to an underlying domain able to represent heterogeneous sets of environments.
As the thesis took place in the Mopsa project, we provide an overview of some of the results obtained by the Mopsa team during the thesis.
Defence : 11/21/2019 - 14h - Campus Jussieu, salle 24-34/201
Jury members :
Mme. BLAZY Sandrine (Professeur, IRISA) [rapporteur]
M. KING Andy (Professeur, University of Kent) [rapporteur]
M. CHAILLOUX Emmanuel (Professeur, Sorbonne Université)
M. LE GALL Tristan (Chercheur, CEA LIST)
M. SOTIN Pascal (Maître de Conférences, IRIT)
M. MINÉ Antoine (Professeur, Sorbonne Université)
- M. Jaume, M. Journault, M.‑J. Lesot, P. Manoury, I. Mounier : “Logique pour l’informatique”, (Ellipses), (ISBN: 9782340042612) (2020)
- M. Journault, P. Lafourcade, M. More, R. Poulain, L. Robert : “How to Teach the Undecidability of Malware Detection Problem and Halting Problem”, WISE13: The 13th World Conference on Information Security Education, Maribor, Slovenia (2020)
- M. Journault : “Precise and modular static analysis by abstract interpretation for the automatic proof of program soundness and contracts inference”, thesis, defence 11/21/2019, supervision Miné, Antoine (2019)
- M. Journault, A. Miné, A. Ouadjaout : “An abstract domain for trees with numeric relations”, ESOP 2019 - 28th European Symposium on Programming, vol. 11423, Lecture Notes in Computer Science, Prague, Czechia, pp. 724-751, (Springer) (2019)
- M. Journault, A. Miné, R. Monat, A. Ouadjaout : “Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer”, Verified Software. Theories, Tools, and Experiments, vol. 12031, Lecture Notes in Computer Science, New York, United States, pp. 1-18, (Springer) (2019)
- M. Journault, A. Miné, A. Ouadjaout : “Modular static analysis of string manipulations in C programs”, SAS 2018, Freiburg im Breisgau, Germany (2018)
- A. Miné, A. Ouadjaout, M. Journault : “Design of a Modular Platform for Static Analysis”, The Ninth Workshop on Tools for Automatic Program Analysis (TAPAS'18), Fribourg-en-Brisgau, Germany (2018)
- M. Journault, A. Miné : “Static Analysis by Abstract Interpretation of the Functional Correctness of Matrix Manipulating Programs”, Static Analysis, 23rd International Symposium, SAS 2016, Edinburgh, UK, September 8-10, 2016, Proceedings, vol. 9837, Lecture Notes in Computer Science, Edimbourg, United Kingdom, pp. 257-277, (Springer) (2016)