[Resource Topic] 2023/281: Towards A Correct-by-Construction FHE Model

Welcome to the resource topic for 2023/281

Towards A Correct-by-Construction FHE Model

Authors: Zhenkun Yang, Wen Wang, Jeremy Casas, Pasquale Cocchini, Jin Yang


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.

ePrint: https://eprint.iacr.org/2023/281

See all topics related to this paper.

Feel free to post resources that are related to this paper below.

Example resources include: implementations, explanation materials, talks, slides, links to previous discussions on other websites.

For more information, see the rules for Resource Topics .