Cookies
O website necessita de alguns cookies e outros recursos semelhantes para funcionar. Caso o permita, o INESC TEC irá utilizar cookies para recolher dados sobre as suas visitas, contribuindo, assim, para estatísticas agregadas que permitem melhorar o nosso serviço. Ver mais
Aceitar Rejeitar
  • Menu
Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    José Bacelar Almeida
  • Cluster

    Informática
  • Cargo

    Investigador Sénior
  • Desde

    01 novembro 2011
003
Publicações

2022

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

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

Publicação
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

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

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

Publicação
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.

2020

The Last Mile: High-Assurance and High-Speed Cryptographic Implementations

Autores
Almeida, JB; Barbosa, M; Barthe, G; Gregoire, B; Koutsos, A; Laporte, V; Oliveira, T; Strub, PY;

Publicação
2020 IEEE SYMPOSIUM ON SECURITY AND PRIVACY (SP 2020)

Abstract
We develop a new approach for building cryptographic implementations. Our approach goes the last mile and delivers assembly code that is provably functionally correct, protected against side-channels, and as efficient as hand-written assembly. We illustrate our approach using ChaCha20-Poly1305, one of the two ciphersuites recommended in TLS 1.3, and deliver formally verified vectorized implementations which outperform the fastest non-verified code.We realize our approach by combining the Jasmin framework, which offers in a single language features of high-level and low-level programming, and the EasyCrypt proof assistant, which offers a versatile verification infrastructure that supports proofs of functional correctness and equivalence checking. Neither of these tools had been used for functional correctness before. Taken together, these infrastructures empower programmers to develop efficient and verified implementations by "game hopping", starting from reference implementations that are proved functionally correct against a specification, and gradually introducing program optimizations that are proved correct by equivalence checking.We also make several contributions of independent interest, including a new and extensible verified compiler for Jasmin, with a richer memory model and support for vectorized instructions, and a new embedding of Jasmin in EasyCrypt. © 2020 IEEE.

2020

Certified Compilation for Cryptography: Extended x86 Instructions and Constant-Time Verification

Autores
Almeida, JB; Barbosa, M; Barthe, G; Laporte, V; Oliveira, T;

Publicação
Progress in Cryptology - INDOCRYPT 2020 - 21st International Conference on Cryptology in India, Bangalore, India, December 13-16, 2020, Proceedings

Abstract

2019

Some Applications of the Formalization of the Pumping Lemma for Context-Free Languages

Autores
Ramos, MVM; Bacelar Almeida, JCB; Moreira, N; de Queiroz, RJGB;

Publicação
ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE

Abstract
Context-free languages are highly important in computer language processing technology as well as in formal language theory. The Pumping Lemma for Context-Free Languages states a property that is valid for all context-free languages, which makes it a tool for showing the existence of non-context-free languages. This paper presents a formalization, extending the previously formalized Lemma, of the fact that several well-known languages are not context-free. Moreover, we build on those results to construct a formal proof of the well-known property that context-free languages are not closed under intersection. All the formalization has been mechanized in the Coq proof assistant.

Teses
supervisionadas

2021

Gestão de Segurança de Informação para Sistemas de Confiança Seguros

Autor
Joana Fernandes Cunha

Instituição
UM

2021

Hungry Games: Development of a serious game for science communication about CRISPR

Autor
António Nunes da Cruz

Instituição
UP-FEUP

2021

Privacy and Security in Data Mining

Autor
Mafalda Guimarães Nunes

Instituição
UM

2021

Self-Sovereign Identity Decentralized Identifiers, Claims and Credentials using non Decentralized Ledger Technology

Autor
Ricardo Jorge Marques Peixoto

Instituição
UM

2021

Extending Conflict Free Replicated Data Types Fault Models

Autor
Houssam Ahmad Yactine

Instituição
UM