Paper 2024/321

Formal Verification of Emulated Floating-Point Arithmetic in Falcon

Abstract

We show that there is a discrepancy between the emulated floating-point multiplication in the submission package of the digital signature Falcon and the claimed behavior. In particular, we show that some floating-point products with absolute values the smallest normal positive floating-point number are incorrectly zeroized. However, we show that the discrepancy doesn’t affect the complex fast Fourier transform in the signature generation of Falcon by modeling the floating-point addition, subtraction, and multiplication in CryptoLine. We later implement our own floating-point multiplications in Armv7-M assembly and Jasmin and prove their equivalence with our model, demonstrating the possibility of transferring the challenging verification task (verifying highly-optimized assembly) to the presumably more readable code base (Jasmin).

Note: In the previous versions of the paper, there was a mistake on the power-of-two exponents in the range of the intermediate floating-point numbers: the exponents should be further subtracted by 53. This was a human interpretation error, where the raw program logs were misread while writing the paper. There is no impact on other claims made in this paper.