Vitor Pereira

Vitor Pereira

Computer Scientist

Posts by Collection

funding

VeriWeird: Formal Verification of Weird Networks

Leader of the formal verification (FA2) research area of the VeriWeird project. VeriWeird’s key innovation is to develop a novel approach to the formalzation of hidden communication systems (HCS) that is based on the encoding of (HCS) properties in the simulation-based cryptgraphy proof paradigm.

portfolio

projects

ALICE: Automated-instrumentation of Legacy Insecure Cryptographic Executables

The key features of ALICE are: i. automatically detecting and extracting implementations of weak or broken cryptographic primitives from binaries without requiring source code or debugging symbols; ii. identifying the context and scope in which such primitives are used, and performing program analysis to determine the effects of replacing such implementations with more secure ones; and iii. replacing implementations of weak primitives with those of stronger or more secure ones.

CoCoCrypt: EasyCrypt code extraction tool

EasyCrypt to OCaml extraction tool, focused on the functional core of EasyCrypt. It takes as input an EasyCrypt script and produces a WhyML file that matches the EasyCrypt file (and appropriate dependencies). Finally, it is possible to obtain verified OCaml code by relying on Why3 own extraction mechanism.

Pathkit

The Pathkit toolset, that patches an ELF binary using one or more simple Python scripts.

ZKgen: an OCaml platform for zero knowledge computations

ZKgen is a ZK platform that aggregates multiple ZK protocols into a single solution, giving the user the flexibility to chose which ZK protocol best fit its application scenario. It supports the evaluation of ZK relations written in SIEVE IR format.

publications

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

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 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

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 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

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

talks

A Fast and Verified Software Stack for Secure Function

Published:

Abstract: We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i. a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao’s SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.

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

Published:

Abstract: Secure Multiparty Computation (MPC) enables a group of nn distrusting parties to jointly compute a function using private inputs. MPC guarantees correctness of computation and confidentiality of inputs if no more than a threshold tt of the parties are corrupted. Proactive MPC (PMPC) addresses the stronger threat model of a mobile adversary that controls a changing set of parties (but only up to tt at any instant), and may eventually corrupt all nn parties over a long time. This paper takes a first stab at developing high-assurance implementations of (P)MPC. We formalize in EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, several abstract and reusable variations of secret sharing and of (P)MPC protocols building on them. Using those, we prove a series of abstract theorems for the proactive setting. We implement and perform computer-checked security proofs of concrete instantiations of the required (abstract) protocols in EasyCrypt. We also develop a new tool-chain to extract high-assurance executable implementations of protocols formalized and verified in EasyCrypt. Our tool-chain uses Why as an intermediate tool, and enables us to extract executable code from our (P)MPC formalizations. We conduct an evaluation of the extracted executables by comparing their performance to performance of manually implemented versions using Python-based Charm framework for prototyping cryptographic schemes. We argue that the small overhead of our high-assurance executables is a reasonable price to pay for the increased confidence about their correctness and security.

teaching

Assistant Monitor - Informatics Lab

Undergraduate course, Universidade do Minho, 2015

Informatics Lab is an interdisciplinary course, where students practice what they learn in other courses, gaining also knowledge in useful mechanisms in Computer Science, such as the use of Unix shell or code documentation.

Assistant Lecturer - Funcional Programming

Undergraduate course, Faculdade de Ciências da Universidade do Porto, Departamento de Ciência de Computadores, 2018

Functional Programming course, offered by the Department of Computer Science at Universidade do Porto, teaches students the functional programming paradigm, using the Haskell language as support for the course activities.

Assistant Lecturer - Funcional Programming

Undergraduate course, Faculdade de Ciências da Universidade do Porto, Departamento de Ciência de Computadores, 2019

Functional Programming course, offered by the Department of Computer Science at Universidade do Porto, teaches students the functional programming paradigm, using the Haskell language as support for the course activities.