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
Sobre

Sobre

Sou um aluno de Doutoramento MAPi no meu quarto ano, e um investigador do HASLab/INESC TEC, de momento a trabalhar nos projetos SafeCloud e NanoSTIMA. Tenho um Mestrado em Engenharia Informática concluído na Universidade do Minho.

Os meus interesses para investigação são, principalmente, criptografia e segurança da informação. Mais especificamente, o tópico do meu trabalho é o desenvolvimento de protocolos de computação segura baseados em hardware confiável. O objetivo do meu projeto de doutoramento passa por melhorar o estado da arte em protocolos seguros altamente confiáveis, reduzindo a lacuna existente entre os modelos de segurança teóricos e as implementações práticas mais eficientes. As minhas contribuições de maior relevância no contexto deste trabalho incluem a primeira abordagem para formalizar garantias seguras oferecidas por ambientes de execução isolados, e a primeira implementação genérica de computação segura utilizando ambientes de execução isolados.

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Bernardo Luís Portela
  • Cargo

    Investigador Sénior
  • Desde

    01 janeiro 2014
003
Publicações

2023

General-Purpose Secure Conflict-free Replicated Data Types

Autores
Portela, B; Pacheco, H; Jorge, P; Pontes, R;

Publicação
2023 IEEE 36TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM, CSF

Abstract
Conflict-free Replicated Data Types (CRDTs) are a very popular class of distributed data structures that strike a compromise between strong and eventual consistency. Ensuring the protection of data stored within a CRDT, however, cannot be done trivially using standard encryption techniques, as secure CRDT protocols would require replica-side computation. This paper proposes an approach to lift general-purpose implementations of CRDTs to secure variants using secure multiparty computation (MPC). Each replica within the system is realized by a group of MPC parties that compute its functionality. Our results include: i) an extension of current formal models used for reasoning over the security of CRDT solutions to the MPC setting; ii) a MPC language and type system to enable the construction of secure versions of CRDTs and; iii) a proof of security that relates the security of CRDT constructions designed under said semantics to the underlying MPC library. We provide an open-source system implementation with an extensive evaluation, which compares different designs with their baseline throughput and latency.

2023

Soteria: Preserving Privacy in Distributed Machine Learning

Autores
Brito, C; Ferreira, P; Portela, B; Oliveira, R; Paulo, J;

Publicação
38TH ANNUAL ACM SYMPOSIUM ON APPLIED COMPUTING, SAC 2023

Abstract
We propose Soteria, a system for distributed privacy-preserving Machine Learning (ML) that leverages Trusted Execution Environments (e.g. Intel SGX) to run code in isolated containers (enclaves). Unlike previous work, where all ML-related computation is performed at trusted enclaves, we introduce a hybrid scheme, combining computation done inside and outside these enclaves. The conducted experimental evaluation validates that our approach reduces the runtime of ML algorithms by up to 41%, when compared to previous related work. Our protocol is accompanied by a security proof, as well as a discussion regarding resilience against a wide spectrum of ML attacks.

2023

Privacy-Preserving Machine Learning on Apache Spark

Autores
Brito, CV; Ferreira, PG; Portela, BL; Oliveira, RC; Paulo, JT;

Publicação
IEEE ACCESS

Abstract
The adoption of third-party machine learning (ML) cloud services is highly dependent on the security guarantees and the performance penalty they incur on workloads for model training and inference. This paper explores security/performance trade-offs for the distributed Apache Spark framework and its ML library. Concretely, we build upon a key insight: in specific deployment settings, one can reveal carefully chosen non-sensitive operations (e.g. statistical calculations). This allows us to considerably improve the performance of privacy-preserving solutions without exposing the protocol to pervasive ML attacks. In more detail, we propose Soteria, a system for distributed privacy-preserving ML that leverages Trusted Execution Environments (e.g. Intel SGX) to run computations over sensitive information in isolated containers (enclaves). Unlike previous work, where all ML-related computation is performed at trusted enclaves, we introduce a hybrid scheme, combining computation done inside and outside these enclaves. The experimental evaluation validates that our approach reduces the runtime of ML algorithms by up to 41% when compared to previous related work. Our protocol is accompanied by a security proof and a discussion regarding resilience against a wide spectrum of ML attacks.

2022

Boolean Searchable Symmetric Encryption With Filters on Trusted Hardware

Autores
Ferreira, B; Portela, B; Oliveira, T; Borges, G; Domingos, H; Leitao, J;

Publicação
IEEE TRANSACTIONS ON DEPENDABLE AND SECURE COMPUTING

Abstract
The prevalence and availability of cloud infrastructures has made them the de facto solution for storing and archiving data, both for organizations and individual users. Nonetheless, the cloud's wide spread adoption is still hindered by dependability and security concerns, particularly in applications with large data collections where efficient search and retrieval services are also major requirements. This leads to an increased tension between security, efficiency, and search expressiveness. In this article we tackle this tension by proposing BISEN, a new provably-secure boolean searchable symmetric encryption scheme that improves these three complementary dimensions by exploring the design space of isolation guarantees offered by novel commodity hardware such as Intel SGX, abstracted as Isolated Execution Environments (IEEs). BISEN is the first scheme to support multiple users and enable highly expressive and arbitrarily complex boolean queries, with minimal information leakage regarding performed queries and accessed data, and verifiability regarding fully malicious adversaries. Furthermore, BISEN extends the traditional SSE model to support filter functions on search results based on generic metadata created by the users. Experimental validation and comparison with the state of art shows that BISEN provides better performance with enriched search semantics and security properties.

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.

Teses
supervisionadas

2023

Privacy in Telecom Fraud Detection

Autor
Eduardo Carvalho Santos

Instituição
UP-FCUP

2023

Speculative Execution Resilient Cryptography

Autor
Rui Pedro Gomes Fernandes

Instituição
UP-FCUP

2023

Detection of Encrypted Malware Command and Control Traffic

Autor
Carlos António de Sousa Costa Novo

Instituição
UP-FCUP

2022

Detection of Encrypted Malware Command and Control Traffic

Autor
Carlos António de Sousa Costa Novo

Instituição
UP-FCUP

2022

An efficient Rust implementation of BFT for supporting Byzantine Tolerant Distributed Storage

Autor
Nuno Gonçalo Neto Martingo

Instituição
UP-FCUP