Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
About

About

I am currently an Assistant Professor at the Department of Informatics at Universidade do Minho and researcher at HASLab/INESC TEC. I obtained my PhD degree in Computer Science from this university in 2003. My research interests lie in Cryptography  and Information Security and its intersection with Program Verification. 

I have been working on the development of high-assurance cryptographic implementations for the last 10 years, aiming to bridge the gap between theoretical security and real-world security. I am particularly interested in provable security and its interplay with the formal verification of cryptographic proofs and cryptographic software implementations. 

Interest
Topics
Details

Details

  • Name

    José Bacelar Almeida
  • Role

    Senior Researcher
  • Since

    01st November 2011
003
Publications

2023

Formally verifying Kyber Episode IV: Implementation correctness

Authors
Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Laporte, V; Léchenet, JC; Oliveira, T; Pacheco, H; Quaresma, M; Schwabe, P; Séré, A; Strub, PY;

Publication
IACR Trans. Cryptogr. Hardw. Embed. Syst.

Abstract
In this paper we present the first formally verified implementations of Kyber and, to the best of our knowledge, the first such implementations of any post-quantum cryptosystem. We give a (readable) formal specification of Kyber in the EasyCrypt proof assistant, which is syntactically very close to the pseudocode description of the scheme as given in the most recent version of the NIST submission. We present high-assurance open-source implementations of Kyber written in the Jasmin language, along with machine-checked proofs that they are functionally correct with respect to the EasyCrypt specification. We describe a number of improvements to the EasyCrypt and Jasmin frameworks that were needed for this implementation and verification effort, and we present detailed benchmarks of our implementations, showing that our code achieves performance close to existing hand-optimized implementations in C and assembly.

2023

Formally verifying Kyber Part I: Implementation Correctness

Authors
Almeida, JB; Barbosa, M; Barthe, G; Grégoire, B; Laporte, V; Léchenet, JC; Oliveira, T; Pacheco, H; Quaresma, M; Schwabe, P; Séré, A; Strub, PY;

Publication
IACR Cryptol. ePrint Arch.

Abstract

2023

Leakage-Free Probabilistic Jasmin Programs

Authors
Almeida, JB; Firsov, D; Oliveira, T; Unruh, D;

Publication
IACR Cryptol. ePrint Arch.

Abstract

2022

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

Authors
Almeida, JCB; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
Secure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed.We review the role of these compilers and provide a formal treatment of the core steps that they perform to bridge the abstraction gap between high-level ideal specifications and efficient SMC protocols. Our abstract framework bridges this secure compilation problem across two dimensions: 1) language-based source- to target-level semantic and efficiency gaps, and 2) cryptographic ideal- to real-world security gaps. We link the former to the setting of certified compilation, paving the way to leverage long-run efforts such as CompCert in future SMC compilers. Security is framed in the standard cryptographic sense. Our results are supported by a machine-checked formalisation carried out in EasyCrypt.

2022

Verified Password Generation from Password Composition Policies

Authors
Grilo, M; Campos, J; Ferreira, JF; Almeida, JB; Mendes, A;

Publication
INTEGRATED FORMAL METHODS, IFM 2022

Abstract
Password managers (PMs) are important tools that enable the use of stronger passwords, freeing users from the cognitive burden of remembering them. Despite this, there are still many users who do not fully trust PMs. In this paper, we focus on a feature that most PMs offer that might impact the user's trust, which is the process of generating a random password. We present three of the most commonly used algorithms and we propose a solution for a formally verified reference implementation of a password generation algorithm. We use EasyCrypt to specify and verify our reference implementation. In addition, we present a proof-of-concept prototype that extends Bitwarden to only generate compliant passwords, solving a frequent users' frustration with PMs. This demonstrates that our formally verified component can be integrated into an existing (and widely used) PM.

Supervised
thesis

2023

Extending Conflict Free Replicated Data Types Fault Models

Author
Houssam Ahmad Yactine

Institution
UM

2022

Implementação e verificação de código criptográfico com segurança pós-quântica

Author
Henrique José Carvalho Faria

Institution
UM

2022

Implementação Certificada da Componente Criptográfica do Gestor de Passwords KeePass

Author
Pedro Miguel Marques Freitas

Institution
UM

2022

Rastreabilidade e compromissos de segurança em veículos modernos

Author
Mariana Pereira Fernandes

Institution
UM

2022

PAdES Server Signer

Author
Francisco Fernando Vilela Araújo

Institution
UM