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).
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Published elsewhere. International Workshop on Security 2024
- Keywords
- FalconFloating-point arithmeticFormal verificationCryptoLine
- Contact author(s)
- vincentvbh7 @ gmail com
- History
- 2024-07-22: last of 4 revisions
- 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},
url = {https://eprint.iacr.org/2024/321}
}
