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

I am a post-doc at the Cryprography and Information Security group, HasLab, INESC/TEC, working with Manuel Barbosa. My main research interests are on areas related to Secure Multi-party Computation, Formal Methods, Functional Programming, Bidirectional Programming or Model Transformations.

Previously, I have been a post-doc at:

I completed my PhD on Bidirectional Data Transformation by Calculation at theUniversity of Minho with Alcino Cunha.

Find more here.

Interest
Topics
Details

Details

  • Name

    Hugo Pereira Pacheco
  • Cluster

    Computer Science
  • Role

    Researcher
  • Since

    01st November 2011
001
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.

2018

Teaching how to program using automated assessment and functional glossy games (experience report)

Authors
Almeida, JB; Cunha, A; Macedo, N; Pacheco, H; Proença, J;

Publication
Proceedings of the ACM on Programming Languages

Abstract

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

2016

A Tool-Chain for High-Assurance Cryptographic Software

Authors
Almeida, J; Barbosa, M; Pacheco, H; Pereira, V;

Publication
ERCIM NEWS

Abstract
Cryptography is an inherently interdisciplinary area and the development of high-quality cryptographic software is a time-consuming task drawing on skills from mathematics, computer science and electrical engineering, only achievable by highly skilled programmers. The challenge is to map high-level cryptographic specifications phrased using mathematical abstractions into efficient implementations at the level of C or assembly that can be deployed on a target computational platform, whilst adhering to the specification both in terms of correctness and security. The High Assurance Software Laboratory at INESC-TEC maintains a domain-specific toolchain for the specification, implementation and verification of cryptographic software centred on CAO, a cryptography analyses and operations-aware language.

2015

The essence of bidirectional programming

Authors
Fischer, S; Hu, Z; Pacheco, H;

Publication
Science China Information Sciences - Sci. China Inf. Sci.

Abstract