Skip to Main content Skip to Navigation
Journal articles

A Why3 proof of GMP algorithms

Raphaël Rieu-Helft 1, 2
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
Abstract : 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.
Complete list of metadata

Cited literature [30 references]  Display  Hide  Download

https://hal.inria.fr/hal-02477578
Contributor : Raphaël Rieu-Helft Connect in order to contact the contributor
Submitted on : Thursday, February 13, 2020 - 2:45:44 PM
Last modification on : Thursday, July 8, 2021 - 3:47:03 AM
Long-term archiving on: : Thursday, May 14, 2020 - 3:20:16 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Raphaël Rieu-Helft. A Why3 proof of GMP algorithms. Journal of Formalized Reasoning, ASDD-AlmaDL, 2019, ⟨10.6092/issn.1972-5787/9730⟩. ⟨hal-02477578⟩

Share

Metrics

Record views

118

Files downloads

444