MiRTL Attacks with Bugs Discovered by TransFuzz

TL;DR

EDA software like RTL simulators and synthesizers are prone to translation bugs: they might misinterpret some input hardware constructs, for example because of too aggressive optimizations. We introduce TransFuzz, a differential fuzzer that produces hardware designs to differentially fuzz EDA software, and discovered 25 CVEs and 20 translation bugs. We then build mistranslation (MiRTL) gadgets, which are primitives for leveraging translation bugs to stealthily inject hardware backdoors. The paper will be presented at USENIX Security 2025 and is already open-source here.

Motivation

When playing with previous hardware-related projects (CellIFT and Cascade), we noticed that when set outside of their comfort zone (basic handwritten Verilog), EDA software has bugs. For example CellIFT, by construction, does not have false negatives, but both synthesizers and simulators sometimes violate this property. This led us to explore these EDA software bugs as well as their security implications.

TransFuzz

We built TransFuzz to fuzz RTL simulators and synthesizers after a careful study of the characteristics of known translation bugs. TransFuzz is built around three major aspects:

  • TransFuzz generates hardware circuits as netlists of macrocells (reminiscent of CellIFT), which is the level at which EDA software typically performs optimizations.
  • TransFuzz explicitly generates deterministic hardware (reminiscent of Cascade), e.g., exempt from potential event reorderings that would affect the output.
  • TransFuzz performs differential fuzzing.

TransFuzz found translation bugs in all 4 tested open-source EDA applications: Icarus Verilog, CXXRTL, Verilator, and Yosys.

MiRTL attacks

Based on the translation bugs found in the EDA applications, we build mistranslation (MiRTL) gadgets. We define a MiRTL gadget as a construct that should output the constant logic value 0, but because of a given translation bug, it will produce the constant 1. The figure below shows some primitives that allow constructing MiRTL gadgets.

The threat model consists of a malicious contributor to the victim hardware description or to some EDA tool that will process this description (e.g., sv2v). The attacker intends to insert an arbitrary change in the target hardware design. As an example, we show that MiRTL gadgets can be used to inject arbitrary backdoors in a target hardware design by inserting a kernel data backdoor into (a local version of) the CVA6 RISC-V CPU, that is not detected by simulators or synthesizers because of the MiRTL gadgets.

Paper and code:

MiRTL will be presented at USENIX Security ‘25, and is readily open-source here! Bing generated the following logo for MiRTL:

Frequently Asked Questions

Are EDA applications now bug-free?
No, TransFuzz is not exhaustive. It does not guarantee to discover all translation bugs.

How do MiRTL gadgets relate to classical RTL trojans?
Classical RTL trojans typically hide using triggers that are extremely rare conditions in practice, but that are easy to enforce if known. MiRTL gadgets are orthogonal: they hide backdoors from white-box techniques, which are the most efficient to detect classical trojans. So a strong backdoor injection should combine classical hiding techniques (mostly effective at the end of the design & verification pipeline) with MiRTL gadgets (mostly effective at the start of the design & verification pipeline).

Acknowledgements

This work was supported in part by the Swiss State Secretariat for Education, Research and Innovation under contract number MB22.00057 (ERC-StG PROMISE).