Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/50515
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Almeida, José Bacelar | por |
dc.contributor.author | Barbosa, Manuel | por |
dc.contributor.author | Barthe, Gilles Jacques Denis | por |
dc.contributor.author | Dupressoir, François | por |
dc.contributor.author | Grégoire, Benjamin | por |
dc.contributor.author | Laporte, Vincent | por |
dc.contributor.author | Pereira, Vitor | por |
dc.date.accessioned | 2018-02-15T12:09:46Z | - |
dc.date.available | 2018-02-15T12:09:46Z | - |
dc.date.issued | 2017-10-30 | - |
dc.identifier.isbn | 978-1-4503-4946-8/17/10 | - |
dc.identifier.issn | 1543-7221 | por |
dc.identifier.uri | https://hdl.handle.net/1822/50515 | - |
dc.description.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. | por |
dc.description.sponsorship | POCI-01-0145-FEDER-006961, FCT-PD/BD/113967/2015 | por |
dc.language.iso | eng | por |
dc.publisher | Association for Computing Machinery (ACM) | por |
dc.relation | info:eu-repo/grantAgreement/FCT/5876/147326/PT | por |
dc.rights | openAccess | por |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | por |
dc.subject | Secure function evaluation | por |
dc.subject | Certified compilation | por |
dc.subject | Verified implementation | por |
dc.title | A fast and verified software stack for secure function evaluation | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | The original publication is available at https://dl.acm.org/citation.cfm?id=3134017 | por |
oaire.citationStartPage | 1989 | por |
oaire.citationEndPage | 2006 | por |
oaire.citationConferencePlace | Austin, TX, USA | por |
oaire.citationVolume | Part F131467 | por |
dc.identifier.doi | 10.1145/3133956.3134017 | por |
dc.subject.fos | Ciências Naturais::Ciências da Computação e da Informação | por |
dc.description.publicationversion | info:eu-repo/semantics/publishedVersion | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Proceedings of the ACM Conference on Computer and Communications Security | por |
sdum.conferencePublication | Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security | por |
sdum.bookTitle | CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY | por |
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