Paper 2014/456

Verified Implementations for Secure and Verifiable Computation

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Guillaume Davy, François Dupressoir, Benjamin Grégoire, and Pierre-Yves Strub


Formal verification of the security of software systems is gradually moving from the traditional focus on idealized models, to the more ambitious goal of producing verified implementations. This trend is also present in recent work targeting the verification of cryptographic software, but the reach of existing tools has so far been limited to cryptographic primitives, such as RSA-OAEP encryption, or standalone protocols, such as SSH. This paper presents a scalable approach 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.

Available format(s)
Publication info
Preprint. MINOR revision.
Garbled CircuitsSecure Function EvaluationVerifiable ComputationVerified ImplementationsEasyCrypt
Contact author(s)
mbb @ di uminho pt
2014-06-15: received
Short URL
Creative Commons Attribution


      author = {José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and Guillaume Davy and François Dupressoir and Benjamin Grégoire and Pierre-Yves Strub},
      title = {Verified Implementations for Secure and Verifiable Computation},
      howpublished = {Cryptology ePrint Archive, Paper 2014/456},
      year = {2014},
      note = {\url{}},
      url = {}
Note: In order to protect the privacy of readers, does not use cookies or embedded third party content.