A Fast and Verified Software Stack for Secure Function Evaluation
Tools
Tools
Tools
Almeida, José Bacelar, Barbosa, Manuel, Barthe, Gilles, Dupressoir, Francois, Grégoire, Benjamin, Laporte, Vincent and Pereira, Vitor (2017) A Fast and Verified Software Stack for Secure Function Evaluation In: The ACM Conference on Computer and Communications Security (CCS 2017), 30 Oct 03 Nov 2017, Dallas, USA.
|
Text
A Fast and Verified Software Stack for Secure Function Evaluation.pdf - Accepted version Manuscript Download (950kB) | Preview |
Official URL: https://doi.org/10.1145/3133956.3134017
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.
| Item Type: | Conference or Workshop Item (Conference Paper) | ||||||||||||||||||||||||
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Divisions : | Faculty of Engineering and Physical Sciences > Computing Science | ||||||||||||||||||||||||
| Authors : |
|
||||||||||||||||||||||||
| Date : | 3 November 2017 | ||||||||||||||||||||||||
| DOI : | 10.1145/3133956.3134017 | ||||||||||||||||||||||||
| Copyright Disclaimer : | © 2017 Association for Computing Machinery (ACM) | ||||||||||||||||||||||||
| Uncontrolled Keywords : | Secure Function Evaluation; Verified Implementation; Certified Compilation | ||||||||||||||||||||||||
| Related URLs : | |||||||||||||||||||||||||
| Depositing User : | Clive Harris | ||||||||||||||||||||||||
| Date Deposited : | 01 Sep 2017 12:57 | ||||||||||||||||||||||||
| Last Modified : | 16 Jan 2019 18:56 | ||||||||||||||||||||||||
| URI: | http://epubs.surrey.ac.uk/id/eprint/842130 |
Actions (login required)
 |
View Item |
Downloads
Downloads per month over past year