一句话：提出对抗性符号执行，建模缓存并探索并发交错，以SMT检测并发相关缓存时序泄漏。
缓存位于高速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.
DOI 原文 ·
@inproceedings{paperbot4568,
title = {Adversarial symbolic execution for detecting concurrency-related cache timing leaks},
author = {Shengjian Guo and Meng Wu and Chao Wang},
booktitle = {FSE},
year = {2018},
doi = {10.1145/3236024.3236028}
}