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.

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.

Cryptography plays a prominent role in today’s increasingly digital society. In fact, virtually all existing systems rely on cryptography at their core. Therefore, it is utterly important to build and analyze cryptographic protocols to secure real world systems. In this talk, I will share my vision for establishing secure and privacy-preserving blockchain applications through cryptographic protocols by showcasing examples of my work in the field. As an example, I will present our research on adaptor signatures, a novel cryptographic scheme that binds the creation of a digital signature to the knowledge of a cryptographic secret other than the signing key. In the realm of blockchain-based systems, the adaptor signatures scheme has become the building block for many blockchain applications proposed so far. Finally, I will conclude by highlighting my ongoing research efforts and future research directions.

Robust forecasts of future resource usage in cloud computing environments enable high efficiency in resource management solutions, such as autoscaling and overcommitment policies. Production-level systems use lightweight combinations of historical information to enable practical deployments. Recently, Machine Learning (ML) models, in particular Long Short Term Memory (LSTM) neural networks, have been proposed by various works, for their improved predictive capabilities. Following this trend, we train LSTM models and observe high levels of prediction accuracy, even on unseen data. Upon meticulous visual inspection of the results, we notice that although the predicted values seem highly accurate, they are nothing but versions of the original data shifted by one time step into the future. Yet, this clear shift seems to be enough to produce a robust forecast, because the values are highly correlated across time. We investigate time series data of various resource usage metrics (CPU, memory, network, disk I/O) across different cloud providers and levels, such as at the physical or virtual machine-level and at the application job-level. We observe that resource utilisation displays very small variations in consecutive time steps. This insight can enable very simple solutions, such as data shifts, to be used for cloud resource forecasting and deliver highly accurate predictions. This is the reason why we ask whether complex machine learning models are even necessary to use. We envision that practical resource management systems need to first identify the extent to which simple solutions can be effective, and resort to using machine learning to the extent that enables its practical use. This talk will be based on work that has been presented in the 14th edition of the annual ACM Symposium on Cloud Computing (SoCC ‘23).

In this talk, we address the problem of the (reactive) realizability of specifications of theories richer than Booleans, including arithmetic theories. Our approach transforms theory specifications into purely Boolean specifications by (1) substituting theory literals by Boolean variables, and (2) computing an additional Boolean requirement that captures the dependencies between the new variables imposed by the literals. The resulting specification can be passed to existing Boolean off-the-shelf realizability tools, and is realizable if and only if the original specification is realizable. The first contribution is a brute-force version of our method, which requires a number of SMT queries that is doubly exponential in the number of input literals. Then, we present a faster method that exploits a nested encoding of the search for the extra requirement and uses SAT solving for faster traversing the search space and uses SMT queries internally. Another contribution is a prototype in Z3-Python. Finally, we report an empirical evaluation using specifications inspired in real industrial cases. To the best of our knowledge, this is the first method that succeeds in non-Boolean LTL realizability.