| Title | A Fast and Verified Software Stack for Secure Function Evaluation |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Almeida, José Bacelar, Barbosa, Manuel, Barthe, Gilles, Dupressoir, François, Grégoire, Benjamin, Laporte, Vincent, Pereira, Vitor |
| Conference Name | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security |
| Publisher | ACM |
| Conference Location | New York, NY, USA |
| ISBN Number | 978-1-4503-4946-8 |
| Keywords | certified compilation, compiler security, composability, pubcrawl, Resiliency, secure function evaluation, verified implementation |
| 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. |
| URL | http://doi.acm.org/10.1145/3133956.3134017 |
| DOI | 10.1145/3133956.3134017 |
| Citation Key | almeida_fast_2017 |
A Fast and Verified Software Stack for Secure Function Evaluation