Model Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification

Though modern microprocessors embed several hardware security mechanisms, aimed at guaranteeing confidentiality and integrity of sensible data, recently disclosed attacks such as Spectre and Meltdown witness weaknesses with potentially great impact on CPU security. Both vulnerabilities exploit speculative execution of modern high-performance micro-architectures, allowing the attacker to observe data leaked via a memory side channel, during speculated and mispredicted instructions. In this paper we present a methodology to formally verify, by means of a model checker, speculative vulnerabilities, such as the class of Spectre/Meltdown attacks, in microprocessors based on speculative execution. In detail, we discuss the problem of formally verifying confidentiality violations, since we deem it will help preventing new vulnerabilities of the same typology. We describe our methodology on a pipelined CPU inspired by the DLX RISC processor architecture. Due to scalability issues, and following related approaches in formal verification of correctness, our approach simplifies the model under verification by proper abstraction and reduction steps. The approach is based on flushing the pipeline, abstracting data and most of the speculative execution logic, keeping a subset of control data, plus speculated data state and tainting logic. Illegal propagation (data leakage) is encoded in terms of taint propagation, from a protected/invalid memory address to the address bus on a subsequent memory read, affecting the cache. We introduce the theoretical flow, relying on known theoretical results combined and exploited to prove soundness and completeness. Finally, using a state-of-the-art model checking tool, we present preliminary data on formal verification based on Bounded Model Checking, that to support our claims and highlight the feasibility of the approach.