Modeling, Derivation, and Automated Analysis of Branch Predictor Security Vulnerabilities.

With the intensification of microarchitectural side-channel attacks targeting branch predictors, the security boundary of computer systems and users' security-critical data are under serious threat. Since the root cause of these attacks is the neglect of security issues in the microarchitecture design of branch predictors, an analysis framework that can exhaustively and automatically explore these concerns in the design phase is imminent. In this paper, we propose a comprehensive and automated evaluation framework for inspecting the security guarantees of branch predictors at the microarchitecture design stage. Our technique involves a three-step modeling approach that abstractly characterizes 19 branch predictor states and 53 operations that could affect these states. Subsequently, we develop a symbolic execution-based framework to investigate all three-step combinations and derive 156 valid attack patterns against branch predictors, including 89 novel attacks never considered in the previous work. Finally, we apply our framework to 8 secure branch predictor designs and four typical hardware-based countermeasures against speculative execution attacks to evaluate their security capabilities. The result demonstrates that these security branch predictors provide efficient security guarantees and outperform those hardware-based alleviations against speculative execution attacks, indicating that the security branch predictors are promising in mitigating branch predictor security vulnerabilities.