Adversarial symbolic execution for detecting concurrency-related cache timing leaks
Adversarial symbolic execution for detecting concurrency-related cache timing leaks
复制标题
DOI：
10.1145/3236024.3236028
复制
发表时间：
2018-07
期刊：
影响因子：
--
通讯作者：
Shengjian Guo;Meng Wu;Chao Wang
中科院分区：
文献类型：
--
作者：
Shengjian Guo;Meng Wu;Chao Wang
高速缓存是介于快CPU和慢存储器之间的高速存储器，其时序特性可能会泄露程序的敏感信息，从而允许对手进行侧信道攻击。现有的检测时序泄漏的方法要么完全忽略缓存，要么只关注程序本身产生的被动泄漏，而不考虑并发运行其他线程可能产生的泄漏。在这项工作中，我们表明，定时泄漏自由是不是一个组成的属性：一个程序，不泄漏时，单独运行时可能会成为泄漏时，与其他线程交织。因此，我们开发了一种新的方法，名为对抗符号执行，以检测这种泄漏。它系统地探讨了可行的程序路径和它们的交织，同时建模该高速缓存，并利用SMT求解器来决定是否有时序泄漏。我们已经在LLVM中实现了我们的方法，并在一组总共有14，455行C代码的真实世界密码上对其进行了评估。我们的实验证明了我们的方法的效率和它的有效性在检测侧通道泄漏。
The timing characteristics of cache, a high-speed storage between the fast CPU and the slow memory, may reveal sensitive information of a program, thus allowing an adversary to conduct side-channel attacks. Existing methods for detecting timing leaks either ignore cache all together or focus only on passive leaks generated by the program itself, without considering leaks that are made possible by concurrently running some other threads. In this work, we show that timing-leak-freedom is not a compositional property: a program that is not leaky when running alone may become leaky when interleaved with other threads. Thus, we develop a new method, named adversarial symbolic execution, to detect such leaks. It systematically explores both the feasible program paths and their interleavings while modeling the cache, and leverages an SMT solver to decide if there are timing leaks. We have implemented our method in LLVM and evaluated it on a set of real-world ciphers with 14,455 lines of C code in total. Our experiments demonstrate both the efficiency of our method and its effectiveness in detecting side-channel leaks.