Enforcing Ideal-World Leakage Bounds in Real-World Secret Sharing MPC Frameworks
| Autor: | Vitor Pereira, Gilles Barthe, José B. Almeida, Bernardo Portela, Manuel Barbosa, Hugo Pacheco |
|---|---|
| Rok vydání: | 2018 |
| Předmět: |
021110 strategic
defence & security studies Theoretical computer science business.industry Computer science 0211 other engineering and technologies Probabilistic logic Cryptography 02 engineering and technology Mathematical proof computer.software_genre Encryption Secret sharing Imperative programming 0202 electrical engineering electronic engineering information engineering 020201 artificial intelligence & image processing Compiler business computer Protocol (object-oriented programming) |
| Zdroj: | CSF |
| Popis: | 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|