A detailed version of my CV can be found here.
Menlo Park, CA, USA - February 2021 - Ongoing
My role at SRI involves participating in various US government-funded projects, as well as participating in different proposal efforts. My research directions focus on the intersection of theoretical cryptography and formal methods, particularly research based on computer-aided cryptography, with focus on the development of machine-checked implementations of cryptographic software via code synthesis from mechanically verified cryptographic proofs in EasyCrypt.
Porto, Portugal - June 2020 - February 2021
I was responsible for a collaboration project between INESC TEC and SRI International with the goal of formally verify a zero-knowledge proof protocol based on the MPC-in-the-Head (MitH) construction. This project was carried out under the Securing Information for Encrypted Verification and Evaluation (SIEVE) program funded by the Defense Advanced Research Projects Agency (DARPA).
Porto, Portugal - July 2016 - April 2020
Developed my Ph.D. thesis “Integrated verification of cryptographic security proofs and implementations”, focusing on reducing the abstraction gap between cryptographic security proofs and real implementations.
Menlo Park, CA, United States - September 2018 - December 2018
The goal of this internship was the study and development of Multiparty Computation (MPC) techniques that could be applied to the particular case of Blockchain usage, and to provide formal proofs/implementation of the techniques explored.
Particularly, the work focused on the use of EasyCrypt to deliver formal proofs of proactive secret sharing and MPC primitives, as well developing a new EasyCrypt extraction tool that could be used to generate a verified implementations of such primitives.
Madrid, Spain - March 2016 - July 2016
Finished the development of a security proof and a verified implementation in OCaml of a concrete instantiation of Yao’s Secure Function Evaluation protocol using EasyCrypt.
Braga, Portugal - January 2015 - March 2016
Developed my master thesis “A deductive verification platform for cryptographic software”. The project consisted in developing a deductive verification platform for the CAO language, using the EasyCrypt toolset as a backend for the tool.
Started the development of a security proof and a verified implementation in OCaml of a concrete instantiation of Yao’s Secure Function Evaluation protocol using EasyCrypt, in cooperation with the Cryptography team at IMDEA Software, Madrid.
Covilhã, Portugal - January 2013 - July 2013
Developed my undergraduate project “Cloud Security: Homomorphic Encryption Schemes”, funded by Portugal Telecom - Inovação, under the PRICE (Privacy and Security Issues in Cloud Environment) project.
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
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
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
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
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
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
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
Talk at ACM Conference on Computer and Communications Security (CCS), Dallas, TX, USA, 2017, Dallas, TX, USA
Talk at ACM Conference on Computer and Communications Security (CCS) London, UK 2019, London, UK