Linköping University: Students Alumni Trade and Industry/Society Internal Search
ahmre43_MEMCODE2017

Quantifying the Information Leak in Cache Attacks through Symbolic Execution

Sudipta Chattopadhyay
 
Moritz Beck
Ahmed Rezine
 
Andreas Zeller

15th ACM-IEEE International Conference on Formal Methods and Models for System Designn, MEMCODE 17

ABSTRACT
Cache timing attacks allow attackers to infer the properties of a secret execution by observing cache hits and misses. But how much information can actually leak through such attacks? For a given program, a cache model, and an input, our CHALICE framework leverages symbolic execution to compute the amount of information that can possibly leak through cache attacks. At the core of CHALICE is a novel approach to quantify information leak that can highlight critical cache side-channel leaks on arbitrary binary code. In our evaluation on real-world programs from OpenSSL and Linux GDK libraries, CHALICE effectively quantifies information leaks: For an AES-128 implementation on Linux, for instance, CHALICE finds that a cache attack can leak as much as 127 out of 128 bits of the encryption key.


[CBRZ17] Sudipta Chattopadhyay, Moritz Beck, Ahmed Rezine, Andreas Zeller, "Quantifying the Information Leak in Cache Attacks through Symbolic Execution", 15th ACM-IEEE International Conference on Formal Methods and Models for System Designn, MEMCODE 17
( ! ) perl script by Giovanni Squillero with modifications from Gert Jervan   (v3.1, p5.2, September-2002-)