SpecVerilog: Adapting Information Flow Control for Secure Speculation
Drew Zagieboylo, Charles Sherk, Andrew C. Myers, G. Edward Suh · 2023
To address transient execution vulnerabilities, processor architects have proposed both defensive designs and formal descriptions of the security they provide. However, these designs are not typically formally proven to enforce the claimed guarantees; more importantly, there are few tools to automatically ensure that Register Transfer Level (RTL) descriptions are faithful to high-level designs.