CPU caches introduce variations into the execution time of programs that can be exploited by adversaries to recover private information about users or cryptographic keys. Establishing the security of countermeasures against this threat often requires intricate reasoning about the interactions of program code, memory layout, and hardware architecture and has so far only been done for restricted cases.

In this talk, I will present novel techniques that provide support for bit-level and arithmetic reasoning about memory accesses in the presence of dynamic memory allocation. I will report on a case study which uses these techniques to perform the first rigorous analysis of widely deployed software countermeasures against cache attacks on modular exponentiation, based on executable code. The countermeasures are from different versions of libgcrypt and OpenSSL from the last 4 years, and our analysis measures their vulnerability to a hierarchy of attacks.