IACR News item: 27 February 2023
Zhenkun Yang, Wen Wang, Jeremy Casas, Pasquale Cocchini, Jin Yang
ePrint Report
This paper presents a correct-by-construction method of designing an FHE model based on the automated program verifier Dafny. We model FHE operations from the ground up, including fundamentals like GCD, coprimality, Montgomery multiplications, and polynomial operations, etc., and higher level optimizations such as Residue Number System (RNS) and Number Theoretic Transform (NTT). The fully formally verified FHE model serves as a reference design for both software stack development and hardware design, and verification efforts. Open-sourcing our FHE Dafny model with modular arithmetic libraries to GitHub is in progress.
Additional news items may be found on the IACR news page.