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
Download Photo HD

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

002
Publications

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.

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; Proenca, J;

Publication
Proceedings of the ACM on Programming Languages

Abstract

2017

Towards new data management platforms for a DSO as market enabler – UPGRID Portugal demo

Authors
Alonso, A; Couto, R; Pacheco, H; Bessa, R; Gouveia, C; Seca, L; Moreira, J; Nunes, P; Matos, PG; Oliveira, A;

Publication
CIRED - Open Access Proceedings Journal

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

Supervised
thesis

2018

Conceção de uma plataforma genérica para as Utilities

Author
Xavier Passos Rodrigues

Institution
UM