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

Vitor is a PhD student under the MAP-i doctoral programme, developing his research at the Cryptography team of HASLab | INESC TEC.

He graduated in Computer Science at University of Beira Interior in 2013, where he started his contact with Cryptography, mainly in the field of Homomorphic Encryption.

In 2015, he completed his Master degree at University of Minho in Computer Science, where he specialised himself in Formal Methods in Software Engineering and in Cryptography. During the lecture year, he developed two cohesive projects: one in cooperation with Galois, where he explored post-quantum cryptographic algorithms in Cryptol, and one where he used a verification tool specific to the domain of Cryptography (EasyCrypt) to prove properties over probabilistic programs. 

His master thesis - "A deductive verification tool for cryptographic software" - focused on the construction of a deductive verification tool for the CAO language using the EasyCrypt toolset as a backend for the tool.

His research interests are focused in Cryptography and on how to apply Formal Methods in the verification of cryptographic primitives. In particular, he is interested in the verifiable security and in the provable security topics.

Interest
Topics
Details

Details

  • Name

    Vítor Parreira Pereira
  • Cluster

    Computer Science
  • Role

    Research Assistant
  • Since

    01st January 2015
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 Fast and Verified Software Stack for Secure Function Evaluation

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Gregoire, B; Laporte, V; Pereira, V;

Publication
Proceedings of the 2017 ACM SIGSAC Conference on Computer and Communications Security, CCS 2017, Dallas, TX, USA, October 30 - November 03, 2017

Abstract