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 Vítor Parreira Pereira

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
CCS'17: PROCEEDINGS OF THE 2017 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY

Abstract
We present a high-assurance software stack for secure function evaluation (SFE). Our stack consists of three components: i.a verified compiler (CircGen) that translates C programs into Boolean circuits; ii. a verified implementation of Yao's SFE protocol based on garbled circuits and oblivious transfer; and iii. transparent application integration and communications via FRESCO, an open-source framework for secure multiparty computation (MPC). CircGen is a general purpose tool that builds on CompCert, a verified optimizing compiler for C. It can be used in arbitrary Boolean circuit-based cryptography deployments. The security of our SFE protocol implementation is formally verified using EasyCrypt, a tool-assisted framework for building high-confidence cryptographic proofs, and it leverages a new formalization of garbled circuits based on the framework of Bellare, Hoang, and Rogaway (CCS 2012). We conduct a practical evaluation of our approach, and conclude that it is competitive with state-of-the-art (unverified) approaches. Our work provides concrete evidence of the feasibility of building efficient, verified, implementations of higher-level cryptographic systems. All our development is publicly available.

2021

Machine-checked ZKP for NP-relations: Formally Verified Security Proofs and Implementations of MPC-in-the-Head

Authors
Bacelar Almeida, JC; Barbosa, M; Eldefrawy, K; Lengrand, SG; Pacheco, H; Pereira, V;

Publication
CoRR

Abstract

2018

hnforcing 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
IEEE 31ST COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF 2018)

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 preprocessing that brings leakage to the acceptable range.

2017

A Fast and Verified Software Stack for Secure Function Evaluation

Authors
Almeida, JB; Barbosa, M; Barthe, G; Dupressoir, F; Grégoire, B; Laporte, V; Pereira, V;

Publication
IACR Cryptology ePrint Archive

Abstract