Please use this identifier to cite or link to this item: http://repositorio.inesctec.pt/handle/123456789/10500
Title: Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Authors: Hugo Pereira Pacheco
Bernardo Luís Portela
Vítor Parreira Pereira
José Bacelar Almeida
Manuel Barbosa
Barthe,G
Issue Date: 2018
Abstract: We give a language-based security treatment of domain-specific languages and compilers for secure multi-party computation, a cryptographic paradigm that enables collaborative computation over encrypted data. Computations are specified in a core imperative language, as if they were intended to be executed by a trusted-third party, and formally verified against an information-flow policy modelling (an upper bound to) their leakage. This allows non-experts to assess the impact of performance-driven authorized disclosure of intermediate values. Specifications are then compiled to multi-party protocols. We formalize protocol security using (distributed) probabilistic information-flow and prove security-preserving compilation: Protocols only leak what is allowed by the source policy. The proof exploits a natural but previously missing correspondence between simulation-based cryptographic proofs and (composable) probabilistic non-interference. Finally, we extend our framework to justify leakage cancelling, a domain-specific optimization that allows to first write an efficient specification that fails to meet the allowed leakage upper-bound, and then apply a probabilistic pre-processing that brings leakage to the acceptable range. © 2018 IEEE.
URI: http://repositorio.inesctec.pt/handle/123456789/10500
http://dx.doi.org/10.1109/csf.2018.00017
metadata.dc.type: conferenceObject
Publication
Appears in Collections:HASLab - Articles in International Conferences

Files in This Item:
File Description SizeFormat 
P-00P-HTH.pdf629.63 kBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.