As one of the fundamental optimizations in modern processors,
the \emph{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 {\sc SymO$_3$}, for exposing
cache timing leaks under the context of \emph{out-of-order}
execution. {\sc SymO$_3$} proposes new components that address
the modeling, reduction, and reasoning challenges of accommodating
program analysis to the software code \emph{out-of-order} analysis.
We implemented {\sc SymO$_3$} upon KLEE and conducted three
evaluations on it. Experimental results show that {\sc SymO$_3$}
successfully uncovers a set of cache timing leaks in five
real-world programs. Also, {\sc SymO$_3$} finds that, in general,
program transformation from compiler optimizations shrink the
surface to timing leaks. Furthermore, augmented with a speculative
execution modeling, {\sc SymO$_3$} identifies five more leaky
programs based on the compound analysis.