Research project conducted at IMDEA Software Institute under the supervision of Marco Guarnieri, focusing on automated synthesis of contracts that capture microarchitectural side-channel vulnerabilities in software systems.

Project Overview

Modern processors employ sophisticated optimizations that can inadvertently leak sensitive information through microarchitectural side channels. These leakages manifest through timing variations, cache behavior, and other observable microarchitectural states. This project develops automated techniques to synthesize formal contracts that precisely characterize these leakage patterns.