FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks

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

Paper Information

Title:Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks
Authors:José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira and Bernardo Portela
Proceedings:CSF CSF Proceedings
Editors: Stephen Chong, Stephanie Delaune and Deepak Garg
Keywords:Domain-specific languages, Privacy, Security, Semantics, Type systems, Verification, Multi-party computation, Secure compilation
Abstract:

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.

Pages:15
Talk:Jul 10 11:30 (Session 54A: Secure computation)
Paper: