Towards Trustworthy RISC-V Designs: Formal Verification of the MFENCE Instruction

Memory barriers play a crucial role in maintaining the consistency of shared data in parallel and multithreaded programming. The mfence instruction is a key component in addressing memory inconsistencies and preventing certain microarchitectural data sampling attacks. Specifically, mfence ensures the completion of certain memory operations in a specific order, preventing the reordering of memory operations across the barrier. Despite its significance, potential security vulnerabilities in the hardware implementation of mfence could be exploited by attackers, compromising its defense mechanism. This paper introduces a formal method for verifying the hardware implementation of mfence, 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 mfence. The efficacy of this approach is demonstrated using the RSD, an open-source RISC-V-based superscalar Out-of-Order processor.