New Paper: Formal Verification of Emulated Floating-Point Arithmetic in Falcon

[Vincent Hwang]

Dear all,

I would like to share recent results on formally verifying the emulated floating-point arithmetic in Falcon. You can find the paper at https://eprint.iacr.org/2024/321.

Long story short: there is a discrepancy between the emulated floating-point multiplications in Falcon's C and Armv7-M assembly implementations and the claimed behavior. Fortunately, there is no impact to the complex FFT in the signature generation of Falcon via formal verification with CryptoLine. Furthermore, this paper also demonstrates equivalence proofs between emulations of floating-point addition, subtraction, and multiplication.

At the end of the paper, I also outlined some possible extensions. Hopefully, the community will figure out a clear path toward formally verifying (implementation correctness and equivalences) Falcon implementations in the future.

Thanks,

Vincent