Side-channel attacks recover secret inputs to programs from physical characteristics of computations, such as execution time or power consumption. CPU caches are a particularly rich source of side channels because their behavior heavily impacts execution time and can be monitored in various ways.

CacheAudit is a novel platform that enables the automatic, static analysis of such cache side channels; it takes as input a program binary and a cache configuration, and it derives formal, quantitative security guarantees for a comprehensive set of side-channel adversaries, namely those based on observing cache states, traces of hits and misses, and execution times.

In this talk I will present the theoretical foundations and the architecture of CacheAudit, and the results we obtain when analyzing library implementations of symmetric cryptosystems such as AES or Salsa. I will conclude with an outlook on how CacheAudit can be used for engineering certified proofs of security of leakage-resilient cryptosystems on platforms with concurrency and caches.