University of Surrey

Test tubes in the lab Research in the ATI Dance Research

A Fast and Verified Software Stack for Secure Function Evaluation

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.

[img] Text
A Fast and Verified Software Stack for Secure Function Evaluation.pdf - Accepted version Manuscript
Restricted to Repository staff only until 3 November 2017.

Download (950kB)

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 :
NameEmailORCID
Almeida, José BacelarUNSPECIFIEDUNSPECIFIED
Barbosa, ManuelUNSPECIFIEDUNSPECIFIED
Barthe, GillesUNSPECIFIEDUNSPECIFIED
Dupressoir, Francoisf.dupressoir@surrey.ac.ukUNSPECIFIED
Grégoire, BenjaminUNSPECIFIEDUNSPECIFIED
Laporte, VincentUNSPECIFIEDUNSPECIFIED
Pereira, VitorUNSPECIFIEDUNSPECIFIED
Date : 3 November 2017
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 : 01 Sep 2017 12:57
URI: http://epubs.surrey.ac.uk/id/eprint/842130

Actions (login required)

View Item View Item

Downloads

Downloads per month over past year


Information about this web site

© The University of Surrey, Guildford, Surrey, GU2 7XH, United Kingdom.
+44 (0)1483 300800