Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/50515
Título: | A fast and verified software stack for secure function evaluation |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Barthe, Gilles Jacques Denis Dupressoir, François Grégoire, Benjamin Laporte, Vincent Pereira, Vitor |
Palavras-chave: | Secure function evaluation Certified compilation Verified implementation |
Data: | 30-Out-2017 |
Editora: | Association for Computing Machinery (ACM) |
Revista: | Proceedings of the ACM Conference on Computer and Communications Security |
Resumo(s): | 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/50515 |
ISBN: | 978-1-4503-4946-8/17/10 |
DOI: | 10.1145/3133956.3134017 |
ISSN: | 1543-7221 |
Versão da editora: | The original publication is available at https://dl.acm.org/citation.cfm?id=3134017 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
17CCSa.pdf | 927,8 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons