A Why3 proof of GMP algorithms
DOI:
https://doi.org/10.6092/issn.1972-5787/9730Keywords:
Program verification, arbitrary-precision integer arithmeticAbstract
Large-integer arithmetic algorithms are used in contexts where both their performance and their correctness are critical, such as cryptographic software. The fastest algorithms are complex enough that formally verifying them is desirable but challenging. We have formally verified a comprehensive arbitrary-precision integer arithmetic library that implements many state-of-the-art algorithms from the GMP library. The algorithms we have verified include addition, subtraction, Toom-Cook multiplication, division and square root. We use the Why3 platform to perform the proof semi-automatically. We obtain an efficient and formally verified C library of low-level functions on arbitrary-precision natural integers. This verification covers the functional correctness of the algorithms, as well as the memory safety and absence of arithmetic overflows of their C implementation. Using detailed pseudocode, we present the algorithms that we verified and outline their proofs.
References
Reynald Affeldt. On construction of a library of formally verified low-level arithmetic functions. Innovations in Systems and Software Engineering, 9(2):59–77, 2013.
Stefan Berghofer. Verification of dependable software using SPARK and Isabelle. In Jörg Brauer, Marco Roveri, and Hendrik Tews, editors, 6th International Workshop on Systems Software Verification, volume 24 of OpenAccess Series in Informatics (OASIcs), pages 15–31, Dagstuhl, Germany, 2012.
Yves Bertot, Nicolas Magaud, and Paul Zimmermann. A proof of GMP square root. Journal of Automated Reasoning, 29(3-4):225–252, 2002.
François Bobot, Jean-Christophe Filliâtre, Claude Marché, and Andrei Paskevich. Why3: Shepherd your herd of provers. In Boogie 2011: First International Workshop on Intermediate Verification Languages, pages 53–64, Wrocław, Poland, August 2011. https://hal.inria.fr/hal-00790310 .
Marco Bodrato and Alberto Zanoni. Integer and polynomial multiplication: Towards optimal Toom-Cook matrices. In 2007 International Symposium on Symbolic and Algebraic Computation, pages 17–24. ACM, 2007.
Martin Clochard. Preuves taillées en biseau. In vingt-huitièmes Journées Francophones des Langages Applicatifs (JFLA), Gourette, France, January 2017.
Stephen A. Cook. On the minimum computation time of functions. PhD thesis, 1966.
Marc Daumas and Guillaume Melquiond. Certification of bounds on expressions involving rounded operators. Transactions on Mathematical Software, 37(1):1–20, 2010.
Edsger Wybe Dijkstra. A discipline of programming, volume 1. Prentice-Hall Englewood Cliffs, 1976.
Jean-Christophe Filliâtre. One logic to use them all. In 24th International Conference on Automated Deduction (CADE-24), volume 7898 of Lecture Notes in Artificial Intelligence, pages 1–20, Lake Placid, USA, June 2013.
Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. A pragmatic type system for deductive verification. Research report, Université Paris Sud, 2016. https://hal.archives-ouvertes.fr/hal-01256434v3.
Jean-Christophe Filliâtre, Léon Gondelman, and Andrei Paskevich. The spirit of ghost code. Formal Methods in System Design, 48(3):152–174, 2016.
Jean-Christophe Filliâtre and Andrei Paskevich. Why3 — where programs meet provers. In Matthias Felleisen and Philippa Gardner, editors, 22nd European Symposium on Programming, volume 7792 of Lecture Notes in Computer Science, pages 125–128, Heidelberg, Germany, March 2013.
Sabine Fischer. Formal verification of a big integer library. In DATE Workshop on Dependable Software Systems, 2008.
Robert W Floyd. Assigning meanings to programs. In Program Verification, pages 65–81. Springer, 1993.
Léon Gondelman. A Pragmatic Type System for Deductive Software Verification.
PhD thesis, Université Paris-Saclay, December 2016.
Charles Antony Richard Hoare. An axiomatic basis for computer programming.
Communications of the ACM, 12(10):576–580, 1969.
Anatolii Karatsuba. Multiplication of multidigit numbers on automata. In Soviet
Physics Doklady, volume 7, pages 595–596, 1963.
Donald E. Knuth. The Art of Computer Programming, Volume 2 (3rd Ed.): Seminumerical Algorithms. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 1997.
Guillaume Melquiond and Raphaël Rieu-Helft. A Why3 framework for reflection proofs and its application to GMP’s algorithms. In Didier Galmiche, Stephan Schulz, and Roberto Sebastiani, editors, 9th International Joint Conference on Automated Reasoning, number 10900 in Lecture Notes in Computer Science, pages 178–193, Oxford, United Kingdom, July 2018.
Guillaume Melquiond and Raphaël Rieu-Helft. Formal verification of a state-of-the-art integer square root. In IEEE 26th Symposium on Computer Arithmetic (ARITH), Kyoto, Japan, June 2019.
Niels Moller and Torbjörn Granlund. Improved division by invariant integers. IEEE Transactions on Computers, 60:165–175, 2011.
Magnus O. Myreen and Gregorio Curello. Proof pearl: A verified bignum implementation in x86-64 machine code. In Georges Gonthier and Michael Norrish, editors, 3rd International Conference on Certified Programs and Proofs (CPP), volume 8307 of Lecture Notes in Computer Science, pages 66–81, Melbourne, Australia, December 2013.
Raphaël Rieu-Helft, Claude Marché, and Guillaume Melquiond. How to get an efficient yet verified arbitrary-precision integer library. In 9th Working Conference on Verified Software: Theories, Tools, and Experiments, volume 10712 of Lecture Notes in Computer Science, pages 84–101, Heidelberg, Germany, July 2017.
Norbert Schirmer. A verification environment for sequential imperative programs in Isabelle/HOL. In International Conference on Logic for Programming Artificial Intelligence and Reasoning, pages 398–414, 2005.
Marc Schoolderman. Verifying branch-free assembly code in Why3. In Working Conference on Verified Software: Theories, Tools, and Experiments, pages 66–83, 2017.
Andrei L Toom. The complexity of a scheme of functional elements realizing the multiplication of integers. In Soviet Mathematics Doklady, volume 3, pages 714–716, 1963.
Henry S. Warren. Hacker’s Delight. Addison-Wesley Professional, 2nd edition, 2012.
Jean Karim Zinzindohoué, Karthikeyan Bhargavan, Jonathan Protzenko, and Benjamin Beurdouche. HACL*: A verified modern cryptographic library. Cryptology ePrint Archive, Report 2017/536, 2017. https://eprint.iacr.org/2017/536
Downloads
Published
How to Cite
Issue
Section
License
Copyright (c) 2019 Raphael Rieu-Helft
Copyrights and publishing rights of all the texts on this journal belong to the respective authors without restrictions.
This journal is licensed under a Creative Commons Attribution 3.0 Unported License (full legal code).
See also our Open Access policy
