Publications

Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge

Published in ACM Conference on Computer and Communications Security (CCS) Copenhagen, Denmark 2023, 2023

Recommended citation: Samuel Dittmer, Karim Eldefrawy, Stéphane Graham-Lengrand, Steve Lu, Rafail Ostrovsky and Vitor Pereira. Boosting the Performance of High-Assurance Cryptography: Parallel Execution and Optimizing Memory Access in Formally-Verified Line-Point Zero-Knowledge. ACM Conference on Computer and Communications Security (CCS) Copenhagen, Denmark 2023

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

Published in Journal of Logical and Algebraic Methods in Programming Volume 125, 2022

Recommended citation: José Carlos Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira and Bernardo Portela. A formal treatment of the role of verified compilers in secure computation. Journal of Logical and Algebraic Methods in Programming Volume 125

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

Published in ACM Conference on Computer and Communications Security (CCS) Seoul, South Korea 2021, 2021

Recommended citation: José Bacelar Almeida, Manuel Barbosa, Manuel L Correia, Karim Eldefrawy, Stéphane Graham-Lengrand, Hugo Pacheco and Vitor Pereira, Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head. ACM Conference on Computer and Communications Security (CCS) Seoul, South Korea 2021

A High-Assurance Automatically Synthesized Evaluator for Machine-checked (Proactively) Secure Multi-party Computation Protocols

Published in ACM Conference on Computer and Communications Security (CCS) London, UK 2019, 2019

Recommended citation: Karim Eldefrawy and Vitor Pereira, A High-Assurance Automatically Synthesized Evaluator for Machine-checked (Proactively) Secure Multi-party Computation Protocols. ACM Conference on Computer and Communications Security (CCS) London, UK 2019

A Machine-Checked Proof of Security for AWS Key Management Service

Published in ACM Conference on Computer and Communications Security (CCS) London, UK 2019, 2019

Recommended citation: José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Matthew Campagna, Ernie Cohen, Benjamin Grégoire, Vitor Pereira, Bernardo Portela, Pierre-Yves Strub and Serdar Tasiran, A Machine-Checked Proof of Security for AWS Key Management Service. ACM Conference on Computer and Communications Security (CCS) London, UK 2019

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks

Published in IEEE Computer Security Foundations Symposium (CSF), Oxford, UK, 2018, 2018

Recommended citation: José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, Hugo Pacheco, Vitor Pereira and Bernardo Portela, Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks. In IEEE Computer Security Foundations Symposium (CSF), Oxford, UK, 2018

A Fast and Verified Software Stack for Secure Function Evaluation

Published in ACM Conference on Computer and Communications Security (CCS), Dallas, TX, USA, 2017, 2017

Recommended citation: José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Benjamin Grégoire, Vincent Laporte and Vitor Pereira, A Fast and Verified Software Stack for Secure Function Evaluation. In ACM Conference on Computer and Communications Security (CCS), Dallas, TX, USA, 2017