Doctorat
Equipe : Vérification d'Algorithmes, Langages et Systèmes
Développement et vérification de bibliothèques d'arithmétique entière en précision arbitraire
Début le 01/10/2017
Direction : MELQUIOND, Guillaume
Ecole doctorale : ED STIC 580
Etablissement d'inscription : Université Paris-Saclay
Lieu de déroulement : LRI - VALS & TrustInSoft
Soutenue le 03/11/2020 devant le jury composé de :
Rapporteurs :
- Karthikeyan Bhargavan, Directeur de recherche, Inria Paris
- Paul Zimmermann, Directeur de recherche, Inria Nancy
Examinateur
- Patricia Bouyer, Directrice de recherche, CNRS
- Catherine Dubois, Professeure, ENSIIE
- Xavier Leroy, Professeur, Collège de France
- Micaela Mayero, Maître de conférences, Université Paris-Nord
Directeur de thèse
- Guillaume Melquiond, Chargé de recherche, Inria Saclay
Co-encadrant de thèse
- Pascal Cuoq, Directeur scientifique, TrustInSoft
Activités de recherche :
Résumé :
Les algorithmes d'arithmétique entière en précision arbitraire sont utilisés dans des contextes où leur correction et leurs performances sont critiques, comme les logiciels de cryptographie ou de calcul formel. GMP est une bibliothèque d'arithmétique entière en précision arbitraire très utilisée. Elle propose des algorithmes de pointe, suffisamment complexes pour qu'il soit à la fois justifié et difficile de les vérifier formellement. Cette thèse traite de la vérification formelle de la correction fonctionelle d'une partie significative de GMP à l'aide de la plateforme de vérification déductive Why3.
Afin de rendre cette preuve possible, j'ai fait plusieurs ajouts à Why3 qui permettent la vérification de programmes C. Why3 propose un langage fonctionnel de programmation et de spécification appelé WhyML. J'ai développé des modèles de la gestion de la mémoire et des types du langage C. Ceci m'a permis de réimplanter des algorithmes de GMP en WhyML et de les vérifier formellement. J'ai aussi étendu le mécanisme d'extraction de Why3. Les programmes WhyML peuvent maintenant être compilés vers du C idiomatique, alors que le seul langage cible était OCaml auparavant.
La compilation de mes programmes WhyML résulte en une bibliothèque C vérifiée appelée WhyMP. Elle implémente de nombreux algorithmes de pointe tirés de GMP en préservant presque toutes les astuces d'implémentation. WhyMP est compatible avec GMP, et est comparable à la version de GMP sans assembleur écrit à la main en termes de performances. Elle va bien au-delà des bibliothèques d'arithmétique en précision arbitraire vérifiées existantes. C'est sans doute le développement Why3 le plus ambitieux à ce jour en termes de longueur et d'effort de preuve.
Afin d'augmenter le degré d'automatisation de mes preuves, j'ai ajouté à Why3 un mécanisme de preuves par réflexion. Il permet aux utilisateurs de Why3 d'écrire des procédures de décision dédiées, formellement vérifiées et qui utilisent pleinement les fonctionnalités impératives de WhyML. À l'aide de ce mécanisme, j'ai pu remplacer des centaines d'annotations manuelles de ma preuve de GMP par des preuves automatiques.
