Welcome to the resource topic for 2023/281
Title:
Towards A Correct-by-Construction FHE Model
Authors: Zhenkun Yang, Wen Wang, Jeremy Casas, Pasquale Cocchini, Jin Yang
Abstract: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 .