Paper 2018/404

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, and Bernardo Portela

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 into multi-party protocols. We formalize protocol security using (distributed) probabilistic information-flow and prove that compilation is security-preserving: protocols do not leak more than 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 efficiently computable specification that fails to meet the allowed leakage upper-bound, and then apply a probabilistic pre-processing that brings the overall leakage to within the acceptable range.

Metadata
Available format(s)
PDF
Publication info
Published elsewhere. Major revision. 31st IEEE Computer Security Foundations Symposium
Keywords
Domain-specific languagesPrivacySecuritySemanticsType systemsVerificationMulti-party computationSecure compilation
Contact author(s)
vitor m pereira @ inesctec pt
History
2018-05-10: received
Short URL
https://ia.cr/2018/404
License
Creative Commons Attribution
CC BY

BibTeX

@misc{cryptoeprint:2018/404,
      author = {José Bacelar Almeida and Manuel Barbosa and Gilles Barthe and Hugo Pacheco and Vitor Pereira and Bernardo Portela},
      title = {Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks},
      howpublished = {Cryptology ePrint Archive, Paper 2018/404},
      year = {2018},
      note = {\url{https://eprint.iacr.org/2018/404}},
      url = {https://eprint.iacr.org/2018/404}
}
Note: In order to protect the privacy of readers, eprint.iacr.org does not use cookies or embedded third party content.