Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/66492
Título: | hnforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks |
Autor(es): | Almeida, José Bacelar Barbosa, Manuel Barthe, Gilles Pacheco, Hugo Pereira, Vitor Portela, Bernardo |
Palavras-chave: | Domain-specific-languages Multi-party-computation Privacy Secure-compilation Security Semantics Type-systems Verification |
Data: | 2018 |
Editora: | IEEE |
Revista: | Proceedings IEEE Computer Security Foundations Symposium |
Resumo(s): | 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 preprocessing that brings leakage to the acceptable range. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/66492 |
ISBN: | 9781538666807 |
DOI: | 10.1109/CSF.2018.00017 |
ISSN: | 1940-1434 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |