SPECUSYM: Speculative Symbolic Execution for Cache Timing Leak Detection
SPECUSYM: Speculative Symbolic Execution for Cache Timing Leak Detection
复制标题
DOI：
10.1145/3377811.3380428
复制
发表时间：
2019-11
期刊：
影响因子：
--
通讯作者：
Shengjian Guo;Yueqi Chen;Peng Li;Yueqiang Cheng;Huibo Wang;Meng Wu;Zhiqiang Zuo
中科院分区：
文献类型：
--
作者：
Shengjian Guo;Yueqi Chen;Peng Li;Yueqiang Cheng;Huibo Wang;Meng Wu;Zhiqiang Zuo
CPU缓存是现代处理器中有限但至关重要的存储组件，而缓存正时侧通道可能会通过物理可测量的定时差异无意间泄漏信息。投机性执行，必不可少的处理器优化以及这种差异的来源，可能会严重损害故意分支错误预测。尽管静态分析可以定性地验证投机执行下的无正时属性，但它无法产生认可，包括输入和推测流以诊断深度泄漏。这项工作提出了一种基于符号执行的新方法，用于精确检测推测执行引入的缓存正时泄漏。给定一个程序（在非规范执行中无泄漏），Specusym系统地探索了程序状态空间，在条件分支处模型投机行为，并积累了缓存副作用以及随后的路径探索。在动态执行期间，Specusym构造根据指定的缓存模型泄漏了内存访问的谓词，并进行基于约束的缓存行为分析以检查新的缓存行为。我们已经在Klee上实施了Specusym，并根据15个开源基准进行了评估。实验结果表明，在3种不同的缓存设置下，在6个程序中成功检测到的骨子孔从2个程序中成功检测到了误差，并在最近工作报告的2个程序中确定了误报。
CPU cache is a limited but crucial storage component in modern processors, whereas the cache timing side-channel may inadvertently leak information through the physically measurable timing variance. Speculative execution, an essential processor optimization, and a source of such variances, can cause severe detriment on deliberate branch mispredictions. Despite static analysis could qualitatively verify the timing-leakage-free property under speculative execution, it is incapable of producing endorsements including inputs and speculated flows to diagnose leaks in depth. This work proposes a new symbolic execution based method, Specusym, for precisely detecting cache timing leaks introduced by speculative execution. Given a program (leakage-free in non-speculative execution), SpecuSym systematically explores the program state space, models speculative behavior at conditional branches, and accumulates the cache side effects along with subsequent path explorations. During the dynamic execution, SpecuSym constructs leak predicates for memory visits according to the specified cache model and conducts a constraint-solving based cache behavior analysis to inspect the new cache behaviors. We have implemented SpecuSym atop KLEE and evaluated it against 15 open-source benchmarks. Experimental results show that SpecuSym successfully detected from 2 to 61 leaks in 6 programs under 3 different cache settings and identified false positives in 2 programs reported by recent work.