We consider circuit-based cloud-oriented cryptographic protocols for secure and verifiable computation over encrypted data. Our examples share as central component Yao's celebrated transformation of a boolean circuit into an equivalent garbled form that can be evaluated securely in an untrusted environment. We leverage the foundations of garbled circuits set forth by Bellare, Hoang, and Rogaway (CCS 2012, ASIACRYPT 2012) to build verified implementations of garbling schemes, a verified implementation of Yao's secure function evaluation protocol, and a verified (albeit partial) implementation of the verifiable computation protocol by Gennaro, Gentry, and Parno (CRYPTO 2010). The implementations are formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and critically rely on two novel features: a module and theory system that supports compositional reasoning, and a code extraction mechanism for generating implementations from formalizations.
Category / Keywords: implementation / Garbled Circuits, Secure Function Evaluation, Verifiable Computation, Verified Implementations, EasyCrypt Date: received 13 Jun 2014 Contact author: mbb at di uminho pt Available format(s): PDF | BibTeX Citation Version: 20140615:111829 (All versions of this report) Short URL: ia.cr/2014/456