IMDEA Software

IMDEA initiative

Home > Events > Software Seminar Series (S3)

Software Seminar Series (S3)

PAGE = software_seminar

Gaspard Anthoine

Thursday, April 3, 2025

11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)

Gaspard Anthoine, PhD Student, IMDEA Software Institute

Verification-efficient Homomorphic Signatures for Verifiable Computation over Data Streams

Abstract:

In this talk (which includes an extended introduction so that even non-cryptographers can follow along) we explore Homomorphic Signatures for NP (HSNP). HSNPs allow us to verify that a signed result is indeed the outcome of a specified (potentially complex) computation on signed inputs. This powerful notion was introduced by Fiore and Tucker at CCS 2022, where they combined zero-knowledge SNARKs (for succinct proof of correct computation) with linearly homomorphic signatures (LHS) to verify operations on streaming data. Although their approach was very flexible, the verification step of their LHS was quite costly. We address this limitation by introducing a new, more efficient LHS, significantly reducing the verification overhead. By retaining Fiore and Tucker’s modular design, our solution yields a streamlined HSNP, particularly advantageous for processing data that arrives in consecutive samples, such as sliding window statistics, histograms, and financial forecasts.


Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


David Balbás

Tuesday, March 18, 2025

11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)

David Balbás, PhD Student, IMDEA Software Institute

Unraveling end-to-end encryption: what, why, and how?

Abstract:

[No advanced knowledge of cryptography needed! Content suitable for a general audience].

End-to-end encryption (E2EE) stands as the gold standard for digital privacy. But how does this cryptographic shield truly work—and why does it matter for businesses and individuals alike?

We dive into the true meaning of E2EE, presenting why simple mechanisms to achieve authenticity and confidentiality do not suffice. We will borrow examples from cloud storage and secure messaging to understand how protocols can self-heal after breaches, ensuring past and future data stays locked even if current keys are leaked. Then, we will walk through the architecture of the Signal Protocol – the backbone of WhatsApp, Facebook Messenger, Signal, and others – whose ephemeral keys and resilience against device compromise set the benchmark for modern secure messaging. Finally, we will look at the additional challenges imposed by group conversations and how these can be addressed in practice.


Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Jorge Gallego

Tuesday, February 18, 2025

11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)

Jorge Gallego, PhD Student, IMDEA Software Institute

On the Existential Theory of the Reals Enriched with Integer Powers of a Computable Number

Abstract:

This paper investigates ER(r^Z), that is the extension of the existential theory of the reals by an additional unary predicate r^Z for the integer powers of a fixed computable real number r > 0. If all we have access to is a Turing machine computing r, it is not possible to decide whether an input formula from this theory satisfiable. However, we show an algorithm to decide this problem when:

  1. r is known to be transcendental, or
  2. r is a root of some given integer polynomial (that is, r is algebraic). In other words, knowing the algebraicity of r suffices to circumvent undecidability. Furthermore, we establish complexity results under the proviso that r enjoys what we call a polynomial root barrier. Using this notion, we show that the satisfiability problem of ER(r^Z) is
  3. in EXPSPACE if r is an algebraic number, and
  4. in 3EXP if r is a logarithm of an algebraic number, Euler’s e, or the number pi, among others. To establish our results, we first observe that the satisfiability problem of ER(r^Z) reduces in exponential time to the problem of solving quantifier-free instances of the theory of the reals where variables range over r^Z. We then prove that these instances have a small witness property: only finitely many integer powers of r must be considered to find whether a formula is satisfiable. Our complexity results are shown by relying on well-established machinery from Diophantine approximation and transcendental number theory, such as bounds for the transcendence measure of numbers. As a by-product of our results, we are able to remove the appeal to Schanuel’s conjecture from the proof of decidability of the entropic risk threshold problem for stochastic games with rational probabilities, rewards and threshold [Baier et al., MFCS'23]: when the base of the entropic risk is Euler’s e and the aversion factor is a fixed algebraic number, the problem is (unconditionally) in EXP.


Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Diego Castejón Molina

Wednesday, December 11, 2024

11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)

Diego Castejón Molina, PhD Student, IMDEA Software Institute

MixBuy: Contingent Payment in the Presence of Coin Mixers

Abstract:

With the increasing popularity of blockchains, cryptocurrencies are now accepted for the purchase of digital goods, such as e-books or gift cards. A contingent payment is a cryptographic protocol that models digital purchases, and it involves a buyer and a seller. The buyer owns crypto-coins, and the seller owns a digital product. Contingent payment ensures that the buyer and the seller can exchange coins and product securely. However, observers of the blockchain might learn which buyer purchased from which seller based on the information contained in the transaction. Is it possible to extend contingent payment so that the relationship between buyer and seller is hidden? In this talk, I will present how contingent payment works, as well as coin mixing, practical technique to hide the relationship between a sender and a receiver in a transaction regardless of the blockchain. Then, I will show that existing coin mixing schemes cannot be applied to contingent payment as they lead to devastating attacks. My presentation ends with MixBuy, the first protocol that hides the relationship between buyer and seller in a contingent payment, regardless of the blockchain. This talk is related to the paper: https://eprint.iacr.org/2024/953, which will be presented at The 25th Privacy Enhancing Technologies Symposium in 2025.


Time and place:
11:00am 302-Mountain View and Zoom3 (https://zoom.us/j/3911012202, password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain


Thaleia Doudali

Thursday, October 24, 2024

11:00am Lecture Hall and Zoom (https://zoom.us/j/3911012202 password:@s3)

Thaleia Doudali, Assistant Research Professor, IMDEA Software Institute

Building Computer Systems for Intelligent and Efficient Management of Resources and ML Applications

Abstract:

The massive scale and heterogeneity of current workloads and platforms, such as cloud applications and large machine learning models, break the effectiveness of conventional resource management approaches and create the need for new, custom-tailored systems solutions. The use of machine learning methods can enable robust management decisions, but comes with substantial overheads, practicality and interpretability concerns, therefore it is crucial to enable its practical use. In this talk, I will demonstrate data-driven insights and observations that enable the use of lightweight prediction models for forecasting resource usage and improving upon cloud resource efficiency. In addition, I will describe missed opportunities in the efficient serving of Large Language Model (LLM) inference. Finally, I will conclude with my research vision on the upcoming challenges and directions in system-level resource management.


Time and place:
11:00am Lecture Hall and Zoom (https://zoom.us/j/3911012202 password:@s3)
IMDEA Software Institute, Campus Montegancedo
28223-Pozuelo de Alarcón, Madrid, Spain