A Why3 proof of GMP algorithms

Raphaël Rieu-Helft (1, 2)

1 TIS - TrustInSoft
2 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations

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.

Keywords: Program verification; Arbitrary-precision integer arithmetic

Domains: Computer Arithmetic; Logic in Computer Science [cs.LO]

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