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 a lecturer 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.

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.

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

    Computer Science
  • Role

    Research Coordinator
  • Since

    01st November 2011
007
Publications

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. © 2021 Elsevier Inc.

2021

Secure Conflict-free Replicated Data Types

Authors
Barbosa, M; Ferreira, B; Marques, J; Portela, B; Preguica, N;

Publication
PROCEEDINGS OF THE 2021 INTERNATIONAL CONFERENCE ON DISTRIBUTED COMPUTING AND NETWORKING (ICDCN '21)

Abstract

2021

Provable Security Analysis of FIDO2

Authors
Barbosa, M; Boldyreva, A; Chen, S; Warinschi, B;

Publication
ADVANCES IN CRYPTOLOGY - CRYPTO 2021, PT III

Abstract
We carry out the first provable security analysis of the new FIDO2 protocols, the promising FIDO Alliance's proposal for a standard for passwordless user authentication. Our analysis covers the core components of FIDO2: the W3C's Web Authentication (WebAuthn) specification and the new Client-to-Authenticator Protocol (CTAP2). Our analysis is modular. For WebAuthn and CTAP2, in turn, we propose appropriate security models that aim to capture their intended security goals and use the models to analyze their security. First, our proof confirms the authentication security of WebAuthn. Then, we show CTAP2 can only be proved secure in a weak sense; meanwhile, we identify a series of its design flaws and provide suggestions for improvement. To withstand stronger yet realistic adversaries, we propose a generic protocol called sPACA and prove its strong security; with proper instantiations, sPACA is also more efficient than CTAP2. Finally, we analyze the overall security guarantees provided by FIDO2 and WebAuthn+sPACA based on the security of their components. We expect that our models and provable security results will help clarify the security guarantees of the FIDO2 protocols. In addition, we advocate the adoption of our sPACA protocol as a substitute for CTAP2 for both stronger security and better performance.

2021

Mechanized Proofs of Adversarial Complexity and Application to Universal Composability

Authors
Barbosa, M; Barthe, G; Gregoire, B; Koutsos, A; Strub, PY;

Publication
CCS '21: PROCEEDINGS OF THE 2021 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY

Abstract

2021

Machine-checked ZKP for NP relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

Authors
Almeida, JB; Barbosa, M; Correia, ML; Eldefrawy, K; Graham-Lengrand, S; Pacheco, H; Pereira, V;

Publication
CCS '21: PROCEEDINGS OF THE 2021 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY

Abstract
MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protocols, and secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first uses a fully automated extraction from EasyCrypt to OCaml. The second reduces the trusted computing base (TCB) and provides better performance by combining code extraction with formally verified manual low-level components implemented in the Jasmin language. We conclude with a discussion of the trade-off between the formal verification effort and the performance of resulting executables, and how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH. © 2021 ACM.

Supervised
thesis

2022

Formal Verification of Resource Usage

Author
Ana Carolina Ferreira da Silva

Institution
UP-FCUP

2022

High-speed and High-assurance Cryptographic Software

Author
Tiago Filipe Azevedo Oliveira

Institution
UP-FCUP

2022

Security in Conflict-free Replicated Data Types

Author
Diogo João Veiga de Sousa

Institution
UP-FCUP

2022

Security in Data Aggregation for Eventually Consistent Systems

Author
Pedro Miguel de Jesus Jorge

Institution
UP-FCUP

2022

High-Assurance, High-Speed Post-Quantum Cryptography in Safe Rust

Author
Leonardo Fernandes Moura

Institution
UP-FEUP