A formal treatment of the role of verified compilers in secure computation

• Tipo: Artigo em Revista Científica Internacional
• Data: 2022

Autores

Almeida, JCB (Autor) Outra; Barbosa, M (Autor) FCUP; Barthe, G (Autor) Outra; Pacheco, H (Autor) FCUP; Pereira, V (Autor) Outra; Portela, B (Autor) FCUP

Revista

Título: Journal of Logical and Algebraic Methods in Programming

Vol. 125

ISSN: 2352-2208

Editora: Elsevier

Indexação

ISI Web of Knowledge - 4 Citações

Scopus - 4 Citações

Outras Informações

ID Authenticus: P-00V-V83

DOI: 10.1016/j.jlamp.2021.100736

Abstract (EN): 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.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 21