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

Currently, I am a fourth year Ph.D. student under the MAPi doctoral programme, and a researcher at HASLab/INESC TEC, working for project SafeCloud and NanoSTIMA. I hold a M.Sc. thesis in Informatics Engineering from University of Minho.

My research interests are cryptography and information security, more specifically regarding secure multiparty computation protocols relying on trusted hardware. The goal of my Ph.D. project is to improve the implementation of high-assurance multiparty computation protocols, by bridging the gap between rigorous theoretical security models and efficient practical implementations. Relevant contributions in this context include the first provable security approach for formalizing security guarantees of Isolated Execution Environments (IEEs), and the first general approach to implementing MPC protocols using IEE-enabled systems.

Interest
Topics
Details

Details

  • Name

    Bernardo Luís Portela
  • Cluster

    Computer Science
  • Role

    Researcher
  • Since

    01st January 2014
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

A Practical Framework for Privacy-Preserving NoSQL Databases

Authors
Macedo, R; Paulo, J; Pontes, R; Portela, B; Oliveira, T; Matos, M; Oliveira, R;

Publication
36th IEEE Symposium on Reliable Distributed Systems, SRDS 2017, Hong Kong, Hong Kong, September 26-29, 2017

Abstract

2017

Secure Multiparty Computation from SGX

Authors
Bahmani, R; Barbosa, M; Brasser, F; Portela, B; Sadeghi, AR; Scerri, G; Warinschi, B;

Publication
Financial Cryptography and Data Security - 21st International Conference, FC 2017, Sliema, Malta, April 3-7, 2017, Revised Selected Papers

Abstract

2017

Secure Multiparty Computation from SGX

Authors
Bahmani, R; Barbosa, M; Brasser, F; Portela, B; Sadeghi, A; Scerri, G; Warinschi, B;

Publication
Financial Cryptography and Data Security - Lecture Notes in Computer Science

Abstract

2016

Foundations of Hardware-Based Attested Computation and Application to SGX

Authors
Barbosa, M; Portela, B; Scerri, G; Warinschi, B;

Publication
1ST IEEE EUROPEAN SYMPOSIUM ON SECURITY AND PRIVACY

Abstract
Exciting new capabilities of modern trusted hardware technologies allow for the execution of arbitrary code within environments completely isolated from the rest of the system and provide cryptographic mechanisms for securely reporting on these executions to remote parties. Rigorously proving security of protocols that rely on this type of hardware faces two obstacles. The first is to develop models appropriate for the induced trust assumptions (e.g., what is the correct notion of a party when the peer one wishes to communicate with is a specific instance of an an outsourced program). The second is to develop scalable analysis methods, as the inherent stateful nature of the platforms precludes the application of existing modular analysis techniques that require high degrees of independence between the components. We give the first steps in this direction by studying three cryptographic tools which have been commonly associated with this new generation of trusted hardware solutions. Specifically, we provide formal security definitions, generic constructions and security analysis for attested computation, key-exchange for attestation and secure outsourced computation. Our approach is incremental: each of the concepts relies on the previous ones according to an approach that is quasi-modular. For example we show how to build a secure outsourced computation scheme from an arbitrary attestation protocol combined together with a key-exchange and an encryption scheme.