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 multiplications in the submission package of Falcon and the claimed behavior. In particular, we show that floating-point products with absolute values the smallest normal positive floating-point number are incorrectly zeroized. However, we show that the discrepancy doesn’t effect the complex fast Fourier transform 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).
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- FalconFloating-point arithmeticFormal verificationCryptoLine
- Contact author(s)
- vincentvbh7 @ gmail com
- History
- 2024-04-19: revised
- 2024-02-24: received
- See all versions
- Short URL
- https://ia.cr/2024/321
- License
-
CC0
BibTeX
@misc{cryptoeprint:2024/321,
author = {Vincent Hwang},
title = {Formal Verification of Emulated Floating-Point Arithmetic in Falcon},
howpublished = {Cryptology ePrint Archive, Paper 2024/321},
year = {2024},
note = {\url{https://eprint.iacr.org/2024/321}},
url = {https://eprint.iacr.org/2024/321}
}
