IACR News item: 15 June 2014
José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, Pie
ePrint Reportapproach to formally verifying implementations of higher-level cryptographic systems, directly in the computational model.
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.
Additional news items may be found on the IACR news page.