Workshop on Foundations of Computer Security
With the recent progress in automation of quantitative information-flow analysis, the formal analysis of cache side channels becomes feasible. We demonstrate this by building CacheAudit, a versatile platform for the automatic, static analysis of cache side channels based on abstract interpretation. CacheAudit 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 foundations and architecture of
the CacheAudit platform, 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.