Cookies Policy
The website need some cookies and similar means to function. If you permit us, we will use those means to collect data on your visits for aggregated statistics to improve our service. Find out More
Accept Reject
  • Menu
Publications

Publications by Tiago Filipe Oliveira

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 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

2018

Are Deep Learning Methods Ready for Prime Time in Fingerprints Minutiae Extraction?

Authors
Rebelo, A; Oliveira, T; Correia, ME; Cardoso, JS;

Publication
Progress in Pattern Recognition, Image Analysis, Computer Vision, and Applications - Lecture Notes in Computer Science

Abstract

2019

BISEN: Efficient boolean searchable symmetric encryption with verifiability and minimal leakage

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

Publication
Proceedings of the IEEE Symposium on Reliable Distributed Systems

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, which current state of the art solutions try to balance through complex cryptographic protocols that tradeoff efficiency and expressiveness for near optimal security. In this paper 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 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, by exploiting trusted hardware and the IEE abstraction, BISEN reduces communication costs between the client and the cloud, boosting query execution performance. Experimental validation and comparison with the state of art shows that BISEN provides better performance with enriched search semantics and security properties. © 2019 IEEE.

2020

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

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

Publication
2020 IEEE Symposium on Security and Privacy, SP 2020, San Francisco, CA, USA, May 18-21, 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

Boolean Searchable Symmetric Encryption with Filters on Trusted Hardware

Authors
Ferreira, B; Portela, B; Oliveira, T; Borges, G; Domingos, HJ; Leitao, J;

Publication
IEEE Transactions on Dependable and Secure Computing

Abstract

  • 1
  • 2