Colloquia and Seminars

Modern CPUs rely on largely undocumented performance mechanisms - including speculative execution, branch prediction, prefetching, and store-load reordering - that have repeatedly introduced unintended security vulnerabilities.

Spectre and Meltdown demonstrated that speculative execution combined with microarchitectural side channels can leak across security boundaries, and despite extensive mitigations, new leaks continue to emerge.

Arm CPUs, which power the vast majority of smartphones and are increasingly prevalent in laptops, HPC systems, and datacenters, have received substantially less scrutiny than x86-64, yet are vulnerable to Spectre-class attacks and Arm-specific attacks such as TikTag and PACMAN.

A recurring pattern underlies many of these leaks: instructions impose preconditions on their operands - for example, a matching MTE tag or valid pointer signature - and violating these preconditions can cause faults or other attacker-observable microarchitectural effects. We port Revizor, a black-box fuzzer based on model-based relational testing, to AArch64, add headless fuzzing of remote CPUs, and extend it to Arm-specific features including MTE and PAuth. We further introduce a novel methodology for systematically fuzzing how instructions handle operands that violate their preconditions, enabling us to uncover a previously unknown leak arising from CPU canonicality and alignment checks on loads, stores, and indirect branches.

We demonstrate the leak on the Neoverse N3 and Google Tensor G3, spanning server-class and mobile Arm CPUs, and show that it crosses both privilege (EL0–EL2) and virtualization (attacker-VM to victim-host) boundaries. Finally, we weaponize the leak with two distinct ROP chains, built from musl and OpenSSL, achieving arbitrary reads from a victim process's address space and, in the OpenSSL case, recovering a complete RSA-2048 private key.

Quantitative finite-state systems, such as quantitative automata and graph games, are typically time-symmetric. We investigate the consequences of introducing geometric decay into these systems, through the lenses of discounted-sum automata (NDAs) and Robin Hood bidding games.

NDAs are nondeterministic finite automata equipped with transition weights, where the value of a run is the discounted sum of its weights, and the value of a word is the minimum value over all its accepting runs. The determinization problem asks whether, given an NDA, there exists a deterministic discounted-sum automaton (DDA) that assigns the exact same value to every word. We prove that the determinization problem for NDAs with integral discounting factors is decidable. Specifically, we provide an EXPSPACE algorithm to decide determinizability alongside an explicit construction for the equivalent DDA, and we establish a PSPACE-hardness lower bound for the problem.

As for graph games, we focus on Bidding Games, where players are allocated monetary budgets and bid in auctions to determine movement along the graph. We enrich this model with a wealth-redistribution phase before each turn, which discounts the difference between the players’ budgets. For reachability objectives, we prove the existence of a threshold function - the exact initial budget required for the reachability player to guarantee a win.

We place the associated computational problem in NP. We also reveal that, unlike traditional models, a Robin Hood game may become undetermined exactly at the threshold. For Büchi objectives, we provide a computable candidate for a threshold.

A well-known application of the celebrated color-coding technique is fast detection of paths in a distributed setting with limited bandwidth, by propagating a signal along colorful paths [Even et al., DISC 2017]. However, since vertices of the same color are indistinguishable by this procedure, it cannot detect induced paths, as they appear the same as cycles.

We present a distributed local-counting technique that allows us to design fast algorithms for detecting induced paths, improving upon the state of the art in several aspects (time complexity, detection variant, and more).

The following observation illustrates our key technical ingredient: For each edge, count the number of signals, over all permutations of the random coloring, that terminate at that edge. An induced path contributes one to that count, while a cycle contributes two. Refining and generalizing this idea lets us distinguish induced 4-paths from other 4-vertex subgraphs in constant time and yields fast algorithms for detecting paths of lengths 5 and 6.

Many program‑safety verification tasks reduce to deciding the satisfiability of Constrained Horn Clauses (CHCs). When a program depends on bit‑level behavior such as bitwise logic, shifts, or overflow‑sensitive arithmetic, encoding its CHCs over the theory of fixed‑size bit‑vectors is exact but scales poorly, whereas encoding them over integer arithmetic is far more tractable but requires an expensive modeling of the bit‑level operations that can cancel out the gain. We present the first implementation of a theory‑modular framework, designed by our advisors, that avoids committing to either theory. It partitions a set of bit‑vector CHCs into a bit‑vector fragment and an integer fragment linked by interface constraints, and a backward‑reasoning algorithm discharges the two with separate, theory‑specific solvers, crossing between them and iteratively strengthening the interface to avoid re‑deriving already‑refuted reasoning. We further present a proof‑of‑concept abstraction‑refinement extension that abstracts bit‑manipulating subexpressions during translation and refines them on demand, lightening the load on the bit‑vector solver.

My research focuses on knowledge and dynamics of language models - spanning their fine-tuning efficiency, training dynamics, and mergeability. I will begin by introducing Fast Forward, a simple optimization strategy that significantly accelerates large segments of low-rank training to save computational costs. Next, I will explore the training dynamics of large language models, revealing the fundamental disconnect between how internal parametric knowledge and external knowledge are acquired and forgotten over trainin.. We will then transition to the biological domain to examine the training dynamics of protein language models. Finally, I will conclude by exploring the underlying causes of model mergeability, demonstrating how a base model's prior knowledge influences the success of merging multiple fine-tuned models into a single multitask model. Together, these works provide deeper insights into the mechanics of model knowledge and learning and offer practical methods for more efficient and robust AI development.

Free recall is a standard memory task in which a subject is presented with a sequence of items and, after presentation, asked to retrieve as many as possible in any order. Understanding free recall is not only a question of retrieval capacity, but also of retrieval structure: recalled items appear in clusters, transitions are highly non-random, and retrieval depends strongly on temporal position. We introduce the Tree of Memory (TOM), a computational model in which memory is represented by a hierarchical episodic data structure (episodic tree) augmented with a sparse semantic graph. Experience is organized across multiple temporal scales in different levels of the hierarchy, and recall is modeled as a probabilistic search process over this representation. Specifically, retrieval proceeds through a stochastic depth-first traversal of the episodic tree, interleaved with local exploration of semantic edges whenever an item is reached.

We characterize distinct asymptotic recall regimes and show that the expected number of retrieved items grows logarithmically or as a sublinear power law, depending on how the probability of traversing deeper levels of the memory hierarchy scales with list length. We also study how the same memory representation supports different retrieval algorithms. This allows us to ask how changes in search strategy and auxiliary structure affect recall efficiency. One variant introduces additional semantic links that guide retrieval through a learned sequence, yielding linear recall in list length with high probability. Another uses a small set of pointers to recently formed subtrees, enabling efficient retrieval of entire temporal chunks. These variants highlight explicit trade-offs between recall performance, representation complexity, scalability, and auxiliary memory. Simulations further show that TOM reproduces canonical empirical signatures of free recall. Together, these results suggest that hierarchical representations and probabilistic graph search provide a compact computational framework for understanding both spontaneous and strategy-driven memory retrieval.