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

• Type: Article in International Scientific Journal
• Date: 2022

Authors

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

Journal

Title: Journal of Logical and Algebraic Methods in Programming

Vol. 125

ISSN: 2352-2208

Publisher: Elsevier

Indexing

ISI Web of Knowledge - 4 Citations

Scopus - 4 Citations

Other information

Authenticus ID: 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.

Language: English

Type (Professor's evaluation): Scientific

No. of pages: 21