Ensuring SFENCE Instruction Correctness: A Formal Verification Framework Based on Invariants

Several transient execution and micro-architectural data sampling attacks exploit race conditions and memory inconsistencies to leak security-critical information from microprocessors. The sfence instruction is commonly employed to create a memory barrier, preventing the reordering of store instructions by the compiler or the processor, and enhancing security. However, potential vulnerabilities, such as bugs and trojans in the hardware implementation of sfence could be exploited by attackers, undermining its defense mechanism. In this paper, a formal method based on invariants is provided to address the verification of sfence hardware implementation. Potential areas where hardware trojans can be designed to circumvent sfence are identified and, demonstrate that the proposed verification methodology will flag such trojans. The effectiveness of the approach is validated on the RSD, an open source RISC-V based superscalar out-of-order processor.