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 an Associate Professor at the Department of Computer Science in the Faculty of Science of the University of Porto (DCC-FCUP) and a researcher at HASLab/INESC TEC. My research interests lie in Cryptography and Information Security and its intersection with Program Verification.

I hold a Ph.D. in Electrical and Electronic Engineering from the Newcastle University, an M.Sc. from the same University, and a degree in Electrical and Computer Engineering from the Faculty of Engineering of the University of Porto. In the past I have been a visiting researcher at the University of Bristol, IT Porto and École Normale Supérieure. Between 2023 and 2025 I was a research fellow at the Max Planck Institute for Security and Privacy.

I have been working on the development of high-assurance cryptographic implementations for the last 20 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.

For information on my research, projects and publications, please see my page at HASLab.

For information on my teaching activities, please see my institutional page at FCUP.

Interest
Topics
Details

Details

  • Name

    Manuel Barbosa
  • Since

    01st November 2011
009
Publications

2025

Jazzline: Composable CryptoLine Functional Correctness Proofs for Jasmin Programs

Authors
Almeida, JB; Barbosa, M; Barthe, G; Blatter, L; Marinho Alves, GXD; Duarte, JD; Grégoire, B; Oliveira, T; Quaresma, M; Strub, PY; Tsai, MH; Wang, BY; Yang, BY;

Publication
CCS

Abstract

2025

CCS25 - Artifact for "Jazzline: Composable CryptoLine functional correctness proofs for Jasmin programs"

Authors
Almeida, JB; Barbosa, M; BARTHE, G; Blatter, L; Duarte, JD; Marinho Alves, GXD; Grégoire, B; Oliveira, T; Quaresma, M; Strub, PY; Tsai, MH; Wang, BY; Yang, BY;

Publication
Proceedings of the 2025 ACM SIGSAC Conference on Computer and Communications Security

Abstract
Jasmin is a programming language for high-speed and high-assurance cryptography. Correctness proofs of Jasmin programs are typically carried out deductively in EasyCrypt. This allows generality, modularity and composable reasoning, but does not scale well for low-level architecture-specific routines. CryptoLine offers a semi-automatic approach to formally verify algebraically-rich low-level cryptographic routines. CryptoLine proofs are self-contained: they are not integrated into higher-level formal verification developments. This paper shows how to soundly use CryptoLine to discharge subgoals in functional correctness proofs for complex Jasmin programs. We extend Jasmin with annotations and provide an automatic translation into a CryptoLine model, where most complex transformations are certified. We also formalize and implement the automatic extraction of the semantics of a CryptoLine proof to EasyCrypt. Our motivating use-case is the X-Wing hybrid KEM, for which we present the first formally verified implementation. © 2025 Copyright held by the owner/author(s).

2025

Formally Verified Correctness Bounds for Lattice-Based Cryptography

Authors
Barbosa, M; Kannwischer, MJ; Lim, TH; Schwabe, P; Strub, PY;

Publication
CCS

Abstract
Decryption errors play a crucial role in the security of KEMs based on Fujisaki-Okamoto because the concrete security guarantees provided by this transformation directly depend on the probability of such an event being bounded by a small real number. In this paper we present an approach to formally verify the claims of statistical probabilistic bounds for incorrect decryption in lattice-based KEM constructions. Our main motivating example is the PKE encryption scheme underlying ML-KEM. We formalize the statistical event that is used in the literature to heuristically approximate ML-KEM decryption errors and confirm that the upper bounds given in the literature for this event are correct. We consider FrodoKEM as an additional example, to demonstrate the wider applicability of the approach and the verification of a correctness bound without heuristic approximations. We also discuss other (non-approximate) approaches to bounding the probability of ML-KEM decryption. © 2025 Copyright held by the owner/author(s).

2025

Privacy and Security of FIDO2 Revisited

Authors
Barbosa, M; Boldyreva, A; Chen, S; Cheng, K; Esquível, L;

Publication
Proc. Priv. Enhancing Technol.

Abstract

2025

Tempo: ML-KEM to PAKE Compiler Resilient to Timing Attacks

Authors
Arriaga, A; Barbosa, M; Jarecki, S;

Publication
IACR Cryptol. ePrint Arch.

Abstract