Paper 2017/821

A Fast and Verified Software Stack for Secure Function Evaluation

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte, and Vitor Pereira

Abstract

We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.

Metadata
Available format(s)
PDF
Category
Implementation
Publication info
Published elsewhere. ACM Conference on Computer and Communication Security
Keywords
high-assuranceMPC
Contact author(s)
fdupress @ gmail com
History
2017-08-31: received
Short URL
https://ia.cr/2017/821
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2017/821,
      author = {José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and François Dupressoir and Benjamin Grégoire and Vincent Laporte and Vitor Pereira},
      title = {A Fast and Verified Software Stack for Secure Function Evaluation},
      howpublished = {Cryptology ePrint Archive, Paper 2017/821},
      year = {2017},
      note = {\url{https://eprint.iacr.org/2017/821}},
      url = {https://eprint.iacr.org/2017/821}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.