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.

2018

Teaching how to program using automated assessment and functional glossy games (experience report)

Authors
Almeida, JB; Cunha, A; Macedo, N; Pacheco, H; Proenca, J;

Publication
Proceedings of the ACM on Programming Languages

Abstract

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.

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

Secure MultiParty Computation

Author
Daniel Casanova Faria Torres

Institution
UM