Decentralized Finance (DeFi) leverages blockchain technology to provide financial services without intermediaries, relying on smart contracts to automate economic transactions. As of October 2025, DeFi protocols are estimated to manage over $100 billion in Total Value Locked, making them ideal targets for attacks. The complexity of DeFi protocols’ incentive mechanisms, combined with their entanglement in low-level implementation details, makes it challenging to precisely assess their structural and economic properties, analyse user strategies and attacks, and ensure that the code accurately reflects the intended functionalities. In this talk, we provide an overview of the different approaches used to study DeFi protocols - ranging from formal models to verification tools, as well as LLM-based methods - outline the main challenges, and discuss future directions.

I will present Zinc, a proof system that addresses the problem of high arithmetization costs in proof systems. Arithmetization is the step where one turns the computation/relation one wants to prove into a constraint that is in a suitable form for the proof system. In many natural applications this step is very costly, in the sense that the final constraints is easily of ‘size’ 16x or 32x than the original computation. Such applications include: hash computations, CPU instructions (arithmetic modulo 2^n and bitwise operations), lattice-based operations (as in, e.g. vFHE operations), legacy cryptography, machine learning, etc. Zinc (https://eprint.iacr.org/2025/316) is a proof system for constraints expressed over the integers. These, as we will see, allow to arithmetize many of the above operations cheaply. Additionally, for the same number of constraints, Zinc’s running time is similar to current state-of-the-art hash based proof system.I will also discuss our ongoing work towards a proof system where all the above operations are cheaply arithmetizable. During the talk I will focus especially on the problem of proving lattice-based operations, with a view of applying our techniques to vFHE

In this talk we present a variant of vertex cover on temporal graphs that has been recently introduced for timeline activities summarization in social networks. The problem has been proved to be NP-hard, even in restricted cases. We present algorithmic contributions for the problem. First, we present an approximation algorithm of factor O(T log n), on a temporal graph of T timestamps and n vertices. Then, we consider the restriction where at most one temporal edge is defined in each timestamp. For this restriction, which has been recently shown to be NP-hard, we present a 4(T-1) approximation algorithm and a parameterized algorithm when the parameter is the cost (called span) of the solution.Joint work with Riccardo Dondi

Modern systems face security challenges at every layer of the stack, from user authentication to machine learning and software execution. In this talk, we present three lines of research aimed at strengthening defenses. First, we discuss advances in password deception, including honeyword generation and breach detection frameworks that address practical weaknesses in existing approaches. Next, we examine the security of machine learning-based services, highlighting vulnerabilities such as membership inference, model inversion, and adversarial text generation, and analyzing why many attacks fail in realistic settings. Finally, we introduce VALIDATE, a novel framework for binary-level security assurance, designed to ensure that applications compiled with memory-safe programming languages (e.g., Rust) retain their protective checks and remain tamper-free before execution. Together, these perspectives underscore the need for holistic, multi-layered security that anticipates and disrupts adversaries at multiple points of attack.

Polymarket is a prediction market platform where users can speculate on future events by trading shares tied to specific outcomes, known as conditions. Each market on Polymarket is associated with a set of one or more such conditions. To ensure proper market resolution, the condition set must be exhaustive—collectively accounting for all possible outcomes—and mutually exclusive—only one condition may resolve as true. Thus, the collective prices (probabilities) of all related outcomes (whether in a condition or market) should be $1, representing a combined probability of 1 of any outcome. Despite this design, Polymarket exhibits cases where dependent assets are mispriced, allowing for purchasing (or selling) a certain outcome for less than (or more than) $1, guaranteeing profit. This phenomenon, known as arbitrage, could enable sophisticated participants to exploit such inconsistencies.

In this paper, we conduct an empirical arbitrage analysis on Polymarket data to answer three key questions: (Q1) What conditions give rise to arbitrage? (Q2) Does arbitrage actually occur on Polymarket?, and (Q3) Has anyone exploited these opportunities? A major challenge in analyzing arbitrage between related markets lies in the scalability of comparisons across a large number of markets and conditions, with a naive analysis requiring O(2n+m) comparisons. To overcome this, we employ a heuristic-driven reduction strategy based on timeliness, topical similarity, and combinatorial relationships, further validated by expert input.

Our study reveals two distinct forms of arbitrage on Polymarket: Market Rebalancing Arbitrage, which occurs within a single market or condition (intra-market), and Combinatorial Arbitrage, which spans across multiple markets (inter-market). We use on-chain historical order book data to analyze when these types of arbitrage opportunities have existed, and when they have been executed by users. We find a realized estimate of 40 million USD of profit extracted across both types of arbitrage during our measurement period.