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

DOI10.1016/J.JLAMP.2021.100736MaRDI QIDQ2669248zbMATH OpenOpenAlexWikidataFDO

Authors José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira, Bernardo Portela

Publication date 9 March 2022

Published in Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlamp.2021.100736

zbMATH Keywords

certified compilationcomputer-aided cryptographyeasycryptformal verificationsecure compilationsecure multiparty computation

Mathematics Subject Classification ID

Computer science (68-XX)

Recommendations

• On compiling Boolean circuits optimized for secure multi-party computation
• Computationally sound abstraction and verification of secure multi-party computations
• Secure Multiparty Computation
• How to simulate it in Isabelle: towards formal proof for secure multi-party computation
• Efficient lookup-table protocol in secure multiparty computation

Cites work

• Advances in Cryptology - CRYPTO 2003
• Formal certification of a compiler back-end or: programming a compiler with a proof assistant
• How to share a secret
• Multiparty Computation from Somewhat Homomorphic Encryption
• Secure multiparty computation goes live

Cited in

(4)

• Yet another compiler for active security or: efficient MPC over arbitrary rings
• Certified compilation for cryptography: extended x86 instructions and constant-time verification
• A tribute to José Manuel Valença
• Compiling Information-Flow Security to Minimal Trusted Computing Bases

Describes a project that uses

Uses Software

• Sharemind
• HyCC
• JIFF
• Wysteria
• EasyUC

This page was built for publication: A formal treatment of the role of verified compilers in secure computation

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2669248)