A formal treatment of the role of verified compilers in secure computation
| Autor: | Gilles Barthe, José B. Almeida, Hugo Pacheco, Vitor Pereira, Bernardo Portela, Manuel Barbosa |
|---|---|
| Rok vydání: | 2022 |
| Předmět: |
Ideal (set theory)
Logic business.industry Computer science 020207 software engineering Cloud computing Cryptography 02 engineering and technology Encryption computer.software_genre Theoretical Computer Science Computational Theory and Mathematics 020204 information systems 0202 electrical engineering electronic engineering information engineering Secure multi-party computation Leverage (statistics) Compiler Software engineering business computer Software Abstraction (linguistics) |
| Zdroj: | Journal of Logical and Algebraic Methods in Programming. 125:100736 |
| ISSN: | 2352-2208 |
| Popis: | Secure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed. We review the role of these compilers and provide a formal treatment of the core steps that they perform to bridge the abstraction gap between high-level ideal specifications and efficient SMC protocols. Our abstract framework bridges this secure compilation problem across two dimensions: 1) language-based source- to target-level semantic and efficiency gaps, and 2) cryptographic ideal- to real-world security gaps. We link the former to the setting of certified compilation, paving the way to leverage long-run efforts such as CompCert in future SMC compilers. Security is framed in the standard cryptographic sense. Our results are supported by a machine-checked formalisation carried out in EasyCrypt . |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect