Sound Leakage Contracts for Reliable Formal Verification

Modern processors weave a dense fabric of performance optimizations built over decades of research. These mechanisms often leave measurable footprints (e.g., cache state observable via timing) that have motivated high-impact exploits such as Spectre and render purely functional reasoning insufficient. Defenses and proofs of system security, therefore, must rest on sound, hardware-faithful leakage contracts to be trusted.

This docent lecture presents a principled workflow for building and stress-testing such contracts. We (i) formalize attacker-visible observations at the machine-code level; (ii) apply relational reasoning and symbolic execution to derive the weakest conditions for contract soundness; (iii) use constraint solving to synthesize targeted experiments; and (iv) run these microbenchmarks on real processors to check model–hardware agreement. The emphasis is on closing the loop between formal modeling, automated testing, and empirical measurement, yielding a methodology that can be adapted to analyze new channels, validate assumptions, and inform the design of robust countermeasures.