Title
Exposing cache timing side-channel leaks through out-of-order symbolic execution
Abstract
As one of the fundamental optimizations in modern processors, the out-of-order execution boosts the pipeline throughput by executing independent instructions in parallel rather than in their program orders. However, due to the side effects introduced by such microarchitectural optimization to the CPU cache, secret-critical applications may suffer from timing side-channel leaks. This paper presents a symbolic execution-based technique, named SymO3, for exposing cache timing leaks under the context of out-of-order execution. SymO3 proposes new components that address the modeling, reduction, and reasoning challenges of accommodating program analysis to the software code out-of-order analysis. We implemented SymO3 upon KLEE and conducted three evaluations on it. Experimental results show that SymO3 successfully uncovers a set of cache timing leaks in five real-world programs. Also, SymO3 finds that, in general, program transformation from compiler optimizations shrink the surface to timing leaks. Furthermore, augmented with a speculative execution modeling, SymO3 identifies five more leaky programs based on the compound analysis.
Year
DOI
Venue
2020
10.1145/3428215
Proceedings of the ACM on Programming Languages
Keywords
DocType
Volume
Out-of-order execution,cache timing,side-channel leak,symbolic execution
Journal
4
Issue
ISSN
Citations 
OOPSLA
2475-1421
0
PageRank 
References 
Authors
0.34
0
8
Name
Order
Citations
PageRank
Guo Shengjian132.07
Yueqi Chen242.79
Jiyong Yu391.90
Meng Wu400.34
Zhiqiang Zuo5336.53
Peng Li600.34
Yueqiang Cheng716212.03
Huibo Wang892.89