Paper 2023/1322
Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge
Abstract
Despite the notable advances in the development of high-assurance, verified implementations of cryptographic protocols, such implementations typically face significant performance overheads, particularly due to the penalties induced by formal verification and automated extraction of executable code. In this paper, we address some core performance challenges facing computer-aided cryptography by presenting a formal treatment for accelerating such verified implementations based on multiple generic optimizations covering parallelism and memory access. We illustrate our techniques for addressing such performance bottlenecks using the Line-Point Zero-Knowledge (LPZK) protocol as a case study. Our starting point is a new verified implementation of LPZK that we formalize and synthesize using EasyCrypt; our first implementation is developed to reduce the proof effort and without considering the performance of the extracted executable code. We then show how such (automatically) extracted code can be optimized in three different ways to obtain a 3000x speedup and thus matching the performance of the manual implementation of LPZK. We obtain such performance gains by first modifying the algorithmic specifications, then by adopting a provably secure parallel execution model, and finally by optimizing the memory access structures. All optimizations are first formally verified inside EasyCrypt, and then executable code is automatically synthesized from each step of the formalization. For each optimization, we analyze performance gains resulting from it and also address challenges facing the computer-aided security proofs thereof, and challenges facing automated synthesis of executable code with such an optimization.
Note: Fixes soundness error
Metadata
- Available format(s)
-
PDF
- Category
- Cryptographic protocols
- Publication info
- Published elsewhere. Minor revision. ACM CCS 2023
- DOI
- 10.1145/3576915.3616583
- Keywords
- Zero-KnowledgeFormal VerificationParallelismVerified ImplementationVerified OptimizationsCode Synthesis
- Contact author(s)
-
samdittmer @ stealthsoftwareinc com
karim eldefrawy @ sri com
stephane graham-lengrand @ csl sri com
steve @ stealthsoftwareinc com
rafail @ cs ucla edu
vitor pereira @ sri com - History
- 2024-05-21: last of 4 revisions
- 2023-09-05: received
- See all versions
- Short URL
- https://ia.cr/2023/1322
- License
-
CC BY
BibTeX
@misc{cryptoeprint:2023/1322,
author = {Samuel Dittmer and Karim Eldefrawy and Stéphane Graham-Lengrand and Steve Lu and Rafail Ostrovsky and Vitor Pereira},
title = {Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge},
howpublished = {Cryptology {ePrint} Archive, Paper 2023/1322},
year = {2023},
doi = {10.1145/3576915.3616583},
url = {https://eprint.iacr.org/2023/1322}
}