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.

Robotic systems are starting to revolutionize many applications, from transportation to health care, assisted by technological advancements, such as cloud computing, novel hardware design, and novel manufacturing techniques. However, several of the characteristics that make robots ideal for certain future applications such as autonomy, self-learning, knowledge sharing, can also raise concerns in the evolution of the technology from academic institutions to the public sphere. Blockchain, an emerging technology originated in the digital currency field, is starting to show great potential to make robotic operations more secure, autonomous, flexible, and even profitable. Therefore, bridging the gap between purely scientific domains and real-world applications. This talk seeks to move beyond the classical view of robotic systems to advance our understanding about the possibilities and limitations of combining state-of-the art robotic systems with blockchain technology.

The Linux kernel task scheduler is controls what task runs on what CPU and at what time, and hence is critical for all application performance. At the same time, because it has no precise information about application behavior, the Linux kernel task scheduler amounts to an immense collection of intertwined heuristics that are difficult to understand and evolve. We are investigating whether program verification, by forcing the declaration and checking of function specification can help understand the current state of the source code and protect its good properties over time. Still, program verification is widely considered to be difficult and time consuming. Furthermore, in the case of the Linux kernel, any verification effort is likely quickly out of date, given the rate of change in the code base.In this talk, we present a preliminary study of verification of one function of the Linux kernel task scheduler and the resistance of specifications to changes in the code over time.This investigation has revealed a bug in the source code and a possible missed optimization opportunity.Joint work with Keisuke Nishimura and Jean-Pierre Lozi.This work was presented at SAS 2024.

A labelled transition system is a directed graph whose edges are labelled with letters from a finite alphabet. The vertices of the digraph are the states of the system, and, for an input letter, the system nondeterministically choses an outgoing edge labelled by this letter and moves to the next state according to it. If there are no such outgoing edges, the system “dies”, that is, moves to an unsafe state. We consider the setting where we know the structure of a labelled transition system and the sequence of input letters, but we don’t know the current state of the system and the nondeterministic choices it makes. We study sequences of letters that guarantee entering the unsafe state regardless of the current state of the system and the choices it makes. Such sequences are called mortal. I will discuss the following questions: what is the computational complexity of deciding if a mortal sequence exists? for a given number of states, what is the maximum length of a shortest mortal sequence? The latter question can be interpreted as follows: what is the lower bound on the time that we need to spend observing a system before we know that it has entered the unsafe state? I will describe two equivalent ways of talking about such systems: via nondeterministic finite automata and via sets of nonnegative matrices. I will also explain our recent results with Stefan Kiefer (University of Oxford) about a subclass of labelled transition systems where many similar properties can be efficiently decided.