Paper 2023/281
Towards A Correct-by-Construction FHE Model
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.
Metadata
- Available format(s)
-
PDF
- Category
- Implementation
- Publication info
- Preprint.
- Keywords
- Fully Homomorphic EncryptionFormal VerificationCorrect by Construction
- Contact author(s)
-
zhenkun yang @ intel com
wen wang @ intel com - History
- 2023-02-27: revised
- 2023-02-24: received
- See all versions
- Short URL
- https://ia.cr/2023/281
- License
-
CC BY-NC-ND
BibTeX
@misc{cryptoeprint:2023/281,
author = {Zhenkun Yang and Wen Wang and Jeremy Casas and Pasquale Cocchini and Jin Yang},
title = {Towards A Correct-by-Construction FHE Model},
howpublished = {Cryptology ePrint Archive, Paper 2023/281},
year = {2023},
note = {\url{https://eprint.iacr.org/2023/281}},
url = {https://eprint.iacr.org/2023/281}
}
