Page Not Found
Page not found. Your pixels are in another canvas.
Sitemap
A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.
Pages
Page not in menu
This is a page not in th emain menu
Posts
Future Blog Post
Published:
This post will show up by default. To disable scheduling of future posts, edit config.yml and set future: false.
Blog Post number 4
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 3
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 2
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
Blog Post number 1
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
funding
ALICE: Automated-instrumentation of Legacy Insecure Cryptographic Executables
Principal Investigator of the Automated-instrumentation of Legacy Insecure Cryptographic Executables (ALICE) project.
EMPHASIZE: End-to-end Machinery for Proving Highly sensitive Application-oriented Statements In ZEro-knowledge
Co-Principal Investigator of the End-to-end Machinery for Proving Highly sensitive Application-oriented Statements In ZEro-knowledge (EMPHASIZE) project, part of the Securing Information for Encrypted Verification and Evaluation (SIEVE) DARPA program.
CHALO: Cognitive Health Assistant that Learns and Organizes
Leader of the Computer-Aided Cryptography for Health (CAC-H) task, part of the Cognitive Health Assistant that Learns and Organizes (CHALO) project, part of the Digital Health Security (DIGIHEALS) ARPA-H program.
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
Portfolio item number 1
Short description of portfolio item number 1
Portfolio item number 2
Short description of portfolio item number 2
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.
Machine-checked proof of security for AWS Key Management Service
EasyCrypt formalization of the AWS Key Management Service.
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.
EVOCrypt: EasyCrypt Verified OCaml Cryptographic library
EVOCrypt is a library that provides verified, high-assurance implementations of a series of cryptographic algorithms/protocols, including
- Commitment schemes
- MPC protocols
- Secret sharing schemes
- ZK protocols
Pathkit
The Pathkit toolset, that patches an ELF binary using one or more simple Python scripts.
Machine-checked security proof of Yao’s SFE protocol
EasyCrypt formalization and corresponding verified implementation of the Yao’s Secure Function Evaluation protocol.
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
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
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.