Rigorous Analysis of Software Countermeasures against Cache Attacks
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 paper we devise novel techniques that provide support for bit-level and arithmetic reasoning about memory accesses in the presence of dynamic memory allocation. These techniques enable us to perform the first rigorous analysis of widely deployed software countermeasures against cache attacks on modular exponentiation, based on executable code.
Tue 20 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:50 - 12:30 | |||
10:50 25mTalk | Decomposition Instead of Self-Composition for Proving the Absence of Timing Channels PLDI Research Papers Timos Antonopoulos Yale University, Paul Gazzillo Yale University, Michael Hicks University of Maryland, College Park, Eric Koskinen Yale University, Tachio Terauchi JAIST, Shiyi Wei University of Maryland, College Park Media Attached | ||
11:15 25mTalk | Automatic Program Inversion using Symbolic Transducers PLDI Research Papers Media Attached | ||
11:40 25mTalk | Control-Flow Recovery from Partial Failure Reports PLDI Research Papers Peter Ohmann University of Wisconsin - Madison, Alexander L. Brooks University of Wisconsin, Madison, Loris D'Antoni University of Wisconsin–Madison, Ben Liblit University of Wisconsin–Madison Pre-print Media Attached | ||
12:05 25mTalk | Rigorous Analysis of Software Countermeasures against Cache Attacks PLDI Research Papers Media Attached | ||