Synthesizing Microarchitectural Leakage Contracts from Counterexamples
IMDEA Software Institute
Modern processors keep secrets badly. Caches, branch predictors, and speculative execution all make code run faster by remembering and guessing — and those optimizations leave traces an attacker can measure. Spectre and its relatives showed that these microarchitectural side channels are not corner cases but a systemic gap between how we reason about programs and how hardware actually runs them.
This project develops techniques to close that gap automatically, by synthesizing leakage contracts from counterexamples.
Background: what is a leakage contract?
A leakage contract is a formal, hardware-level specification of exactly what a program is allowed to reveal through its execution on a given microarchitecture. It sits between software and hardware as a shared interface:
-
Software can be verified once against the contract — for example, to show a cryptographic routine is constant-time with respect to the contract.
-
Hardware is obligated to leak no more than the contract permits.
The catch is that writing these contracts by hand is hard and error-prone. A contract that is too permissive certifies insecure code as safe; one that is too strict rejects perfectly good programs. Getting them right requires anticipating every way a microarchitecture might leak — exactly the kind of reasoning humans are bad at.
The problem
We want contracts that are sound (they never under-approximate real leakage) yet precise (they don't forbid behavior the hardware never actually exposes), and we want to derive them without hand-crafting a model of every microarchitectural feature.
Approach: counterexample-guided synthesis
The core idea is to treat contract construction as a search refined by evidence. Rather than positing a contract up front, we learn one from concrete examples of leakage:
-
Start from a candidate contract (often the most permissive one).
-
Probe for a counterexample — a pair of executions that the candidate considers indistinguishable but that the microarchitecture actually separates (or vice versa).
-
Refine the contract to account for the counterexample.
-
Repeat until no further counterexamples can be found.
Each counterexample is a witness: a small, concrete piece of evidence that the current contract is wrong, and a hint about how to fix it. This makes the process instruction-centric — contracts are assembled from the leakage behavior of individual instructions, then composed.
Why this matters
-
Constant-time programming. Contracts give a precise target for what "constant-time" must mean on real hardware, not an idealized model.
-
Speculative execution defenses. Synthesized contracts can capture speculative leakage, helping verify Spectre mitigations rather than trusting them.
-
Reusable verification. Once a contract is established for a microarchitecture, every program can be checked against it independently.
Research outputs
This line of work has been shared at the Foundations of Computer Security workshop and, more recently, at the Microarchitecture Security Conference. The 2026 talk was presented by collaborator Elvira Moreno — it appears here as a project artifact rather than on my talks page, since I was not the presenter.
Collaborators
This research was conducted at the IMDEA Software Institute, in collaboration with Elvira Moreno, Tiziano Marinaro, Marco Patrignani, Roberto Guanciale, and Hamed Nemati.