| Branch prediction is an important performance optimization technique in modern processor design,greatly improving the execution efficiency of processor instruction pipelines.In recent years,security issues related to branch prediction mechanisms,represented by the Spectre vulnerability,have appeared frequently,indicating significant security risks in the design of modern processor branch predictors.However,the design of branch predictors is complex,and traditional testing and verification methods are inefficient and difficultto cover all vulnerabilities,making security verification based on formal methods a new research hotspot.This paper focuses on the formal verification of branch predictor security,and the main innovative points and achievements are summarized as follows:1.We propose a branch prediction security property definition based on information flow control theory--prediction non-interference:this means that when two users with different security levels share the same branch predictor,they cannot produce more additional information flow between them than sequential execution under the condition of predicted execution.A formal definition of this property is given.2.We describe branch prediction attacks as a combination of branch operations and establish a formal representation of branch prediction attacks.Based on this description,we model the design of Bimodal,Gshare,TAGE,BTB,RSB,and a general branch predictor,respectively,and explain the verification method for branch prediction security properties.3.We propose a processor hardware unit verification system using model checking technology,which has the advantages of adapting to multiple instruction set architectures,multiple hardware unit designs,and high verification efficiency.Based on this verification system,we verify multiple branch predictor models and discover a new attack that utilizes the leakage of branch history buffer to leak branch jump history information. |
PDF Full Text Request