Synthesizing Microarchitectural Leakage Contracts from Counterexamples

IMDEA Software Institute

Developing techniques to automatically synthesize contracts that capture microarchitectural side-channel vulnerabilities, with applications to secure software verification.

Modern processors employ complex microarchitectural optimizations — caches, branch predictors, speculative execution — that can leak sensitive information through timing side channels. Leakage contracts formally specify what information a program may leak through these channels.

This project focuses on:

• Automatic synthesis of leakage contracts from observed counterexamples

• Formal verification of software against synthesized contracts

• Application to constant-time programming and speculative execution defenses

• Integration with existing verification frameworks for cryptographic code