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
Interest
Topics
Details

Details

  • Name

    Tiago Filipe Oliveira
  • Cluster

    Computer Science
  • Role

    External Student
  • Since

    01st January 2014
004
Publications

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

2020

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

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

Publication
Progress in Cryptology - INDOCRYPT 2020 - 21st International Conference on Cryptology in India, Bangalore, India, December 13-16, 2020, Proceedings

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.

2019

Machine-Checked Proofs for Cryptographic Standards Indifferentiability of SPONGE and Secure High-Assurance Implementations of SHA-3

Authors
Almeida, JB; Baritel Ruet, C; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; Oliveira, T; Stoughton, A; Strub, PY;

Publication
PROCEEDINGS OF THE 2019 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY (CCS'19)

Abstract
We present a high-assurance and high-speed implementation of the SHA-3 hash function. Our implementation is written in the Jasmin programming language, and is formally verified for functional correctness, provable security and timing attack resistance in the EasyCrypt proof assistant. Our implementation is the first to achieve simultaneously the four desirable properties (efficiency, correctness, provable security, and side-channel protection) for a non-trivial cryptographic primitive. Concretely, our mechanized proofs show that: 1) the SHA-3 hash function is indifferentiable from a random oracle, and thus is resistant against collision, first and second preimage attacks; 2) the SHA-3 hash function is correctly implemented by a vectorized x86 implementation. Furthermore, the implementation is provably protected against timing attacks in an idealized model of timing leaks. The proofs include new EasyCrypt libraries of independent interest for programmable random oracles and modular indifferentiability proofs.