Cryptographic compilers free developers from having to implement cryptography on their own by turning high-level specifications of security goals into efficient implementations. Yet, trusting such tools is risky as they rely on complex mathematical machinery and claim security properties that are subtle and difficult to verify.
In this paper, we present ZKCrypt, an optimizing cryptographic compiler that achieves an unprecedented level of assurance without sacrificing practicality for a comprehensive class of cryptographic protocols, known as Zero-Knowledge Proofs of Knowledge. The pipeline of ZKCrypt tightly integrates purpose-built verified compilers and verifying compilers producing formal proofs in the CertiCrypt framework. By combining the guarantees delivered by each stage in the pipeline, ZKCrypt provides assurance that the implementation it outputs securely realizes the high-level proof goal given as input. We report on the main characteristics of ZKCrypt, highlight new definitions and concepts at its foundations, and illustrate its applicability through a representative example of an anonymous credential system.
Category / Keywords: implementation / zero-knowledge, cryptographic compiler, certifying compiler, formal verification Date: received 7 May 2012, last revised 29 Jun 2012 Contact author: santiago at microsoft com Available formats: PDF | BibTeX Citation Note: Added material on latest developments in the compiler. Version: 20120629:101510 (All versions of this report) Discussion forum: Show discussion | Start new discussion