Workshop on Foundations of Computer Security

June 29, 2013
Tulane University, New Orleans, Louisiana, USA

Affiliated with LICS'13 and CSF'13.

Home | Programme

Invited talk

Static Analysis of Cache Side Channels

Boris Köpf, IMDEA Software Institute

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

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.

Last modified on May 15, 2013.