Interplay of Efficient Model Checking and Secure Processor Design: A Case Study on Secure Speculation

There is increasing use of model checking to verify the security of processors, including those with speculative execution. However, model checkers face scalability challenges and are limited in the scale of processors and specific security properties they can currently handle. This research shows how exploiting domain-specific information about the design of secure processors can be used to scale model checking and make it more efficient. Our key observation is that proofs of non-interference properties require both information-flow invariants and functionality-based invariants, while model checkers often spend substantial effort deriving functionality invariants that do not directly contribute to the final security proof. To address this problem, we introduce Uninterpreted Functions with History (HUF), a modular abstraction for sequential modules that preserves relevant information-flow properties while abstracting away security-irrelevant functionality. We further show that the same verification insight can guide hardware design: security mechanisms become significantly easier to verify when their security depends less on hard-toprove global functional correctness. We build a verification framework to automate the use of HUF abstractions in security verification. Practical demonstration of the verification methodology is conducted through case studies on BOOM processors for secure-speculation mitigations designed with the HUF-guided design guideline.