Cookies Policy
We use cookies to improve our site and your experience. By continuing to browse our site you accept our cookie policy. Find out More
Close
  • 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
  • Cluster

    Computer Science
  • Role

    Senior Researcher
  • Since

    01st November 2011
001
Publications

2018

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks

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

Publication
Proceedings - IEEE Computer Security Foundations Symposium

Abstract
We give a language-based security treatment of domain-specific languages and compilers for secure multi-party computation, a cryptographic paradigm that enables collaborative computation over encrypted data. Computations are specified in a core imperative language, as if they were intended to be executed by a trusted-third party, and formally verified against an information-flow policy modelling (an upper bound to) their leakage. This allows non-experts to assess the impact of performance-driven authorized disclosure of intermediate values. Specifications are then compiled to multi-party protocols. We formalize protocol security using (distributed) probabilistic information-flow and prove security-preserving compilation: Protocols only leak what is allowed by the source policy. The proof exploits a natural but previously missing correspondence between simulation-based cryptographic proofs and (composable) probabilistic non-interference. Finally, we extend our framework to justify leakage cancelling, a domain-specific optimization that allows to first write an efficient specification that fails to meet the allowed leakage upper-bound, and then apply a probabilistic pre-processing that brings leakage to the acceptable range. © 2018 IEEE.

2017

Jasmin: High-Assurance and High-Speed Cryptography

Authors
Almeida, JB; Barbosa, M; Barthe, G; Blot, A; Grégoire, B; Laporte, V; Oliveira, T; Pacheco, H; Schmidt, B; Strub, PY;

Publication
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017

Abstract

2017

A Fast and Verified Software Stack for Secure Function Evaluation

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; Pereira, V;

Publication
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017

Abstract

2016

A Tool-Chain for High-Assurance Cryptographic Software

Authors
Almeida, J; Barbosa, M; Pacheco, H; Pereira, V;

Publication
ERCIM NEWS

Abstract
Cryptography is an inherently interdisciplinary area and the development of high-quality cryptographic software is a time-consuming task drawing on skills from mathematics, computer science and electrical engineering, only achievable by highly skilled programmers. The challenge is to map high-level cryptographic specifications phrased using mathematical abstractions into efficient implementations at the level of C or assembly that can be deployed on a target computational platform, whilst adhering to the specification both in terms of correctness and security. The High Assurance Software Laboratory at INESC-TEC maintains a domain-specific toolchain for the specification, implementation and verification of cryptographic software centred on CAO, a cryptography analyses and operations-aware language.

2016

Verifiable Side-Channel Security of Cryptographic Implementations: Constant-Time MEE-CBC

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F;

Publication
Fast Software Encryption - 23rd International Conference, FSE 2016, Bochum, Germany, March 20-23, 2016, Revised Selected Papers

Abstract
We provide further evidence that implementing software countermeasures against timing attacks is a non-trivial task and requires domain-specific software development processes: we report an implementation bug in the s2n library, recently released by AWS Labs. This bug (now fixed) allowed bypassing the balancing countermeasures against timing attacks deployed in the implementation of the MAC-then- Encode-then-CBC-Encrypt (MEE-CBC) component, creating a timing side-channel similar to that exploited by Lucky 13. Although such an attack could only be launched when the MEE-CBC component is used in isolation – Albrecht and Paterson recently confirmed in independent work that s2n’s second line of defence, once reinforced, provides adequate mitigation against current adversary capabilities – its existence serves as further evidence to the fact that conventional software validation processes are not effective in the study and validation of security properties. To solve this problem, we define a methodology for proving security of implementations in the presence of timing attackers: first, prove black-box security of an algorithmic description of a cryptographic construction; then, establish functional correctness of an implementation with respect to the algorithmic description; and finally, prove that the implementation is leakage secure. We present a proof-of-concept application of our methodology to MEE-CBC, bringing together three different formal verification tools to produce an assembly implementation of this construction that is verifiably secure against adversaries with access to some timing leakage. Our methodology subsumes previous work connecting provable security and side-channel analysis at the implementation level, and supports the verification of a much larger case study. Our case study itself provides the first provable security validation of complex timing countermeasures deployed, for example, in OpenSSL. © International Association for Cryptologic Research 2016.

Supervised
thesis

2017

Geração de descrições de computação para a cloud

Author

Institution
UM

2017

Computação Segura Sobre Sistemas de Dados em Ambientes Cloud

Author

Institution
UM

2016

Extending Conflict free Replicated DataTypes fault models

Author
Houssam Yactine

Institution
UM

2016

Análise de Segurança para Soluções de Software para a Cloud

Author
João Diogo Pereira da Rocha

Institution
UM

2015

Construção de uma ferramenta de verificação para software criptográfico

Author
Vítor Manuel Parreira Pereira

Institution
UM