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.
