Français Anglais
Accueil Annuaire Plan du site
Home > Research results > Dissertations & habilitations
Research results
Ph.D de

Group : Verification of Algorithms, Languages and Systems

Development and verification of arbitrary-precision integer arithmetic libraries

Starts on 01/10/2017
Advisor : MELQUIOND, Guillaume

Funding : Convention industrielle de formation par la recherche
Affiliation : Université Paris-Saclay
Laboratory : LRI - VALS & TrustInSoft

Defended on 03/11/2020, committee :
Rapporteurs :
- Karthikeyan Bhargavan, Directeur de recherche, Inria Paris
- Paul Zimmermann, Directeur de recherche, Inria Nancy

- 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

Research activities :

Abstract :
Arbitrary-precision integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic software or computer algebra systems. GMP is a very widely-used arbitrary-precision integer arithmetic library. It features state-of-the-art algorithms that are intricate enough that their formal verification is both justified and difficult. This thesis tackles the formal verification of the functional correctness of a large fragment of GMP using the Why3 deductive verification platform.

In order to make this verification possible, I have made several additions to Why3 that enable the verification of C programs. Why3 features a functional programming and specification language called WhyML. I have developed models of the memory management and datatypes of the C language, allowing me to reimplement GMP's algorithms in WhyML and formally verify them. I have also extended Why3's extraction mechanism so that WhyML programs can be compiled to idiomatic C code, where only OCaml used to be supported.

The compilation of my WhyML algorithms results in a verified C library called WhyMP. It implements many state-of-the-art algorithms from GMP, with almost all of the optimization tricks preserved. WhyMP is compatible with GMP and performance-competitive with the assembly-free version. It goes far beyond existing verified arbitrary-precision arithmetic libraries, and is arguably the most ambitious existing Why3 development in terms of size and proof effort.

In an attempt to increase the degree of automation of my proofs, I have also added to Why3 a framework for proofs by reflection. It enables Why3 users to easily write dedicated decision procedures that are formally verified programs and make full use of WhyML's imperative features. Using this new framework, I was able to replace hundreds of handwritten proof annotations in my GMP verification by automated proofs.