Research Of Formalization Verification Method Of Processor Security Based On Model Checking

The security of processor microarchitecture is the foundation of computer system security.However,with the discovery of processor microarchitecture security vulnerabilities such as Spectre,Meltdown,and VoltJockey,the security of processor microarchitecture faces significant threats.Among them,microarchitectural data sampling vulnerabilities and cache timing side-channel attacks are two representative types of processor security vulnerabilities.Microarchitectural data sampling vulnerabilities steal the sensitive information from certain temporary buffers in the processor microarchitecture.Cache timing side-channel attacks exploit timing differences in cache operations caused by different cache states to steal secret information.Both of these vulnerabilities pose significant threats to processor security.This paper focuses on the formal verification methods for processor security,aiming to comprehensively verify the existence of these two types of security vulnerabilities in processors.The main innovations and achievements of this paper can be summarized as follows:For microarchitectural data sampling vulnerabilities,this paper proposes a generic security property through feature analysis and abstracts the modeling of processor microarchitecture components,ignoring states irrelevant to security properties and compressing the state space,and use method of model checking to verify this class of security properties.The verification results cover all attack paths of specific types of microarchitectural data sampling vulnerabilities and also evaluate Intel’s defense measures.For cache timing side-channel attacks,this paper defines side-channel security properties for single-level caches and verifies the RTL designs of SecVerilog and DAWG cache using model checking methods.The verification results show that both of these secure cache designs are vulnerable to side-channel attacks based on internal interference.Additionally,the paper proposes the definition of side-channel security properties for multi-level caches that support coherence protocols.The RTL designs of multi-level caches are also verified using model checking,revealing the existence of cache timing side-channel attacks.