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
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

    Senior Researcher
  • Since

    01st November 2011
002
Publications

2022

A formal treatment of the role of verified compilers in secure computation

Authors
Almeida, JCB; Barbosa, M; Barthe, G; Pacheco, H; Pereira, V; Portela, B;

Publication
JOURNAL OF LOGICAL AND ALGEBRAIC METHODS IN PROGRAMMING

Abstract
Secure multiparty computation (SMC) allows for complex computations over encrypted data. Privacy concerns for cloud applications makes this a highly desired technology and recent performance improvements show that it is practical. To make SMC accessible to non-experts and empower its use in varied applications, many domain-specific compilers are being proposed. We review the role of these compilers and provide a formal treatment of the core steps that they perform to bridge the abstraction gap between high-level ideal specifications and efficient SMC protocols. Our abstract framework bridges this secure compilation problem across two dimensions: 1) language-based source- to target-level semantic and efficiency gaps, and 2) cryptographic ideal- to real-world security gaps. We link the former to the setting of certified compilation, paving the way to leverage long-run efforts such as CompCert in future SMC compilers. Security is framed in the standard cryptographic sense. Our results are supported by a machine-checked formalisation carried out in EasyCrypt. © 2021 Elsevier Inc.

2021

Experiences on teaching alloy with an automated assessment platform

Authors
Macedo, N; Cunha, A; Pereira, J; Carvalho, R; Silva, R; Paiva, ACR; Ramalho, MS; Silva, D;

Publication
SCIENCE OF COMPUTER PROGRAMMING

Abstract

2021

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

Authors
Almeida, JB; Barbosa, M; Correia, ML; Eldefrawy, K; Graham-Lengrand, S; Pacheco, H; Pereira, V;

Publication
CCS '21: PROCEEDINGS OF THE 2021 ACM SIGSAC CONFERENCE ON COMPUTER AND COMMUNICATIONS SECURITY

Abstract
MPC-in-the-Head (MitH) is a general framework that enables constructing efficient zero-knowledge (ZK) protocols for NP relations from secure multiparty computation (MPC) protocols. In this paper we present the first machine-checked implementations of MitH. We begin with an EasyCrypt formalization that preserves the modular structure of the original construction and can be instantiated with arbitrary MPC protocols, and secret sharing and commitment schemes satisfying standard notions of security. We then formalize various suitable components, which we use to obtain full-fledged ZK protocols for general relations. We compare two approaches for obtaining verified executable implementations. The first uses a fully automated extraction from EasyCrypt to OCaml. The second reduces the trusted computing base (TCB) and provides better performance by combining code extraction with formally verified manual low-level components implemented in the Jasmin language. We conclude with a discussion of the trade-off between the formal verification effort and the performance of resulting executables, and how our approach opens the way for fully verified implementations of state-of the-art optimized protocols based on MitH. © 2021 ACM.

2021

Rosy: An elegant language to teach the pure reactive nature of robot programming

Authors
Pacheco, H; Macedo, N;

Publication
International Journal of Robotic Computing

Abstract
Robotics is very appealing and is long recognized as a great way to teach programming, while drawing inspiring connections to other branches of engineering and science such as maths, physics or electronics. Although this symbiotic relationship between robotics and programming is perceived as largely beneficial, educational approaches often feel the need to hide the underlying complexity of the robotic system, but as a result fail to transmit the reactive essence of robot programming to the roboticists and programmers of the future. This paper presents Rosy, a novel language for teaching novice programmers through robotics. Its functional style is both familiar with a high-school algebra background and a materialization of the inherent reactive nature of robotic programming. Working at a higher-level of abstraction also teaches valuable design principles of decomposition of robotics software into collections of interacting controllers. Despite its simplicity, Rosy is completely valid Haskell code compatible with the ROS~ecosystem. We make a convincing case for our language by demonstrating how non-trivial applications can be expressed with ease and clarity, exposing its sound functional programming foundations, and developing a web-enabled robot programming environment.

2020

ROSY: An elegant language to teach the pure reactive nature of robot programming

Authors
Pacheco, H; Macedo, N;

Publication
Fourth IEEE International Conference on Robotic Computing, IRC 2020, Taichung, Taiwan, November 9-11, 2020

Abstract
Robotics is very appealing and is long recognized as a great way to teach programming, while drawing inspiring connections to other branches of engineering and science such as maths, physics or electronics. Although this symbiotic relationship between robotics and programming is perceived as largely beneficial, educational approaches often feel the need to hide the underlying complexity of the robotic system, but as a result fail to transmit the reactive essence of robot programming to the roboticists and programmers of the future. This paper presents ROSY, a novel language for teaching novice programmers through robotics. Its functional style is both familiar with a high-school algebra background and a materialization of the inherent reactive nature of robotic programming. Working at a higher-level of abstraction also teaches valuable design principles of decomposition of robotics software into collections of interacting controllers. Despite its simplicity, ROSY is completely valid Haskell code compatible with the ROS ecosystem. We make a convincing case for our language by demonstrating how non-trivial applications can be expressed with ease and clarity, exposing its sound functional programming foundations, and developing a web-enabled robot programming environment. © 2020 IEEE.

Supervised
thesis

2017

Infraestrutura de Big Data para manutenção ferroviária: um caso de estudo

Author
João Manuel Rodrigues Simões

Institution
UP-FEUP