Cookies
Usamos cookies para melhorar nosso site e a sua experiência. Ao continuar a navegar no site, você aceita a nossa política de cookies. Ver mais
Aceitar Rejeitar
  • Menu
Sobre
Download foto HD

Sobre

Vitor é um estudante de Doutoramento sob o programa doutoral MAP-i, desenvolvendo a sua investigação no grupo de Criptografia do HASLab | INESC TEC.

Licenciou-se em Engenharia Informática na Universidade da Beira Interior em 2013, onde tomou pela primeira vez contacto com a Criptografia, nomeadamente na área de Criptografia Homomórfica.

Em 2015, completou o mestrado em Engenharia Informática na Universidade do Minho, onde se especializou em Métodos Formais em Engenharia de Software e em Criptografia. Durante o primeiro ano de mestrado, desenvolveu dois projetos integrados: um, em cooperação com a Galois, onde explorou algoritmos criptográficos pós-quânticos em Cryptol, e outro em que usou uma ferramenta de verificação especializada para a Criptogragia (EasyCrypt) para provar propriedades de programas probabilísticos.

A sua tese de mestrado - "A deductive verification tool for cryptographic software" - foca-se na construção de uma ferramenta de verificação dedutiva para a linguage CAO usando EasyCrypt como mecanismo de verificação.

A sua investigação foca-se na área da Criptografia e em como aplicar Métodos Formais na verificação de primitivas criptográficas. Em particular, os seus interesses passa pela área de "provable security".

Tópicos
de interesse
Detalhes

Detalhes

  • Nome

    Vítor Parreira Pereira
  • Cluster

    Informática
  • Desde

    01 janeiro 2015
Publicações

2018

Enforcing ideal-world leakage bounds in real-world secret sharing MPC frameworks

Autores
Almeida, JB; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B;

Publicação
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

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

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

Abstract