Formal Verification of Early and Strict Serializing Instruction Enforcement
Kushal K. Ponugoti · 2024
Enforcing serializing instructions like lfence at earlier stages in the processor pipeline inhibits the issuance of subsequent instructions into the microarchitecture. This proactive measure prevents speculative execution by causing the processor to stall, thereby fortifying processors against transient execution attacks, including but not limited to Spectre and Load Value Injection. Consequently, the hardware implementation of lfence is a prime target for adversaries to introduce bugs and trojans to render this defense solution ineffective. This compromise in functionality exposes the processor to a range of vulnerabilities, posing a significant security risk. This paper introduces a generic invariant-based formal verification methodology to prove the correctness of lfence implementation, aiming to identify and address potential bugs and trojans. The methodology is designed to detect areas where trojans could be crafted to circumvent the protective features of lfence. The efficacy of this approach is demonstrated using the RSD, an open-source RISC-V-based superscalar Out-of-Order processor.