SymbFuzz: Symbolic Execution Guided Hardware Fuzzing

---

Review Form

Reviewer: The Guardian (Adversarial Skeptic)

Summary

The authors present SymbFuzz, a hybrid hardware fuzzing framework that combines the industry-standard Universal Verification Methodology (UVM) with symbolic execution. The proposed methodology aims to improve coverage and bug detection over existing hardware fuzzers by using an SMT solver to generate constraints that guide the fuzzer toward unexplored states, particularly when coverage stagnates. The framework is evaluated on several RISC-V processor cores, including a version of OpenTitan, where it reportedly finds 14 bugs, including one novel vulnerability, and achieves higher coverage than state-of-the-art fuzzers.

Strengths

1. Practical UVM Integration: The paper's most credible contribution is the direct integration of a fuzzer with the UVM framework. By generating constraints for the UVM sequencer, the approach bypasses the need for software surrogate models and could theoretically be integrated into existing commercial verification flows. This demonstrates sound engineering.

2. Assertion-Based Bug Detection: The use of security properties and assertions rather than relying solely on a golden reference model (GRM) is appropriate for security verification. As the authors correctly note (Section 5.2, page 11), many security flaws (e.g., side-channel leaks) do not manifest as functional incorrectness and would be missed by GRM-based differential testing.

Weaknesses

The paper's claims of superiority are built upon a methodology with significant underspecified components and an evaluation that lacks the necessary rigor to be conclusive.

1. Critically Underspecified Methodology: The core mechanisms are described at a high level but lack the technical depth required for reproducibility or to assess their robustness.

   • Checkpointing Mechanism: The authors claim to use a "lightweight snapshot mechanism that saves only the essential transaction history and architectural state" (Section 3, page 3). The definition of "essential" is entirely omitted. How is this state identified automatically and reliably? An incomplete state restoration could lead to divergent, non-deterministic behavior, invalidating any subsequent exploration from that checkpoint. This is a fundamental flaw that undermines the entire partial-reset premise.
   • Stagnation Heuristic: The invocation of the expensive symbolic execution engine is triggered when NoIncrement(Coverage) > Th (Algorithm 1, page 4). The parameter Th is set based on "pilot runs on smaller designs" (Section 5, page 7). This is an ad-hoc, non-generalizable heuristic. A core parameter of the system should not be based on empirical tuning without a formal justification for its transferability to new, more complex designs.
   • CFG Generation and Scalability: The entire approach hinges on a Control Flow Graph (CFG) generated by Pyverilog. The authors fail to address the well-known limitations of parsing tools like Pyverilog on complex, multi-file, industrial-grade SystemVerilog designs. More importantly, the proposed coverage metric—the Cartesian product of all conditional outcomes (Section 4.6, page 6)—is combinatorially explosive and computationally intractable for all but the simplest control structures. The proposed solution, to simply fuzz non-zero values, is a weak fallback that abandons the guided approach precisely when it is most needed.

2. Unconvincing and Potentially Misleading Evaluation: The experimental results are presented in a way that exaggerates impact while using weak baselines and questionable comparisons.

   • Weak Baseline Comparison: The claim of a "6.8× faster convergence" (Abstract, page 1) is made against "traditional UVM random testing." This is a meaningless comparison. Any guided fuzzer is expected to outperform pure random testing. The only valid baseline for a novel fuzzer is other state-of-the-art fuzzers, against which the claimed improvement is a much more modest 6-15% (Figure 4a, page 11).
   • Questionable "New Bug" Claim: The centerpiece result, Bug #01 (Table 1, page 8), is presented as a novel discovery in OpenTitan. However, the authors state this bug was in an IP generated by OpenTitan's reggen tool and "was not part of the HACK@DAC'24 competition" (Section 5.1, page 7). This implies the other fuzzers were not evaluated on the exact same design. Without confirmation that all tools were run on identical RTL, the comparison is invalid. It is possible SymbFuzz found this bug simply because it was the only tool run against the code containing it.
   • Unsupported Scalability Claims: The authors claim SymbFuzz "scales efficiently" (Section 5.5.2, page 12). The data in Table 3 suggests otherwise. The OpenTitan design (1.5M LoC) required 4x the latency and generated 3x the constraints of the next largest design (~200k LoC). This indicates a super-linear, and potentially exponential, increase in cost with design size, casting serious doubt on its applicability to next-generation multi-million gate SoCs.

3. Contradictory Performance Metrics: In Section 5.2 (page 11), the paper states SymbFuzz is "33% and 54% more efficient than DifuzzRTL and HWFP, respectively," yet also uses "4% more memory than DifuzzRTL." The term "efficient" is not defined. If it refers to CPU time, how can a more complex, SMT-solver-based approach be faster while using more memory? This lacks clarity and suggests a potential inconsistency in measurement or reporting.

Questions to Address In Rebuttal

The authors must address the following points directly and with specific evidence from their work:

1. Checkpointing Integrity: Provide a detailed, algorithmic description of how "essential" state is automatically identified for checkpointing. How do you formally guarantee that un-captured, non-architectural state (e.g., in pipeline registers, arbiters, or stateful peripherals) does not corrupt the design's behavior after a partial reset?

2. Stagnation Threshold Th: Justify the choice of Th. How sensitive are the final coverage results to this parameter? Provide data showing that the chosen Th is not simply over-fitted to the benchmark suite and can be expected to work on unseen designs.

3. Bug #01 Comparison: Please confirm the exact git commit hash of the OpenTitan repository used for all fuzzing comparisons. Were RFuzz, DifuzzRTL, and HWFP run on precisely the same version of the RTL that contained the reggen-generated bug (Bug #01)? If not, the claim of superior bug-finding ability for this case is unsubstantiated.

4. Computational Cost Breakdown: What percentage of the total execution time is spent in the SMT solver versus simulation? Provide this breakdown for the OpenTitan benchmark. This is critical for understanding the true cost of the symbolic execution component.

5. Scalability Projection: Given the data in Table 3, what is the projected latency and number of generated constraints for a design of 5 million LoC? How do you defend the claim of "efficient scaling" when the provided data suggests a steep increase in computational cost with design size?

---

Review Form

Reviewer: The Synthesizer (Contextual Analyst)

Summary

This paper presents SymbFuzz, a hybrid hardware fuzzing framework that integrates symbolic execution guidance into the industry-standard Universal Verification Methodology (UVM). The core idea is to leverage a traditional coverage-guided fuzzer for broad state-space exploration and, upon detecting stagnation, employ an SMT-based symbolic execution engine to generate new input constraints that steer the fuzzer toward uncovered paths.

The authors' primary contribution is not the invention of hybrid fuzzing itself, but its novel and pragmatic adaptation to the specific challenges and workflows of pre-silicon RTL verification. Key to their approach are: 1) a tight integration with UVM, where the solver generates UVM constraints directly for the testbench sequencer; 2) a Control Flow Graph (CFG) based model of the hardware state, focused on control registers; and 3) a checkpointing mechanism to avoid costly full resets during simulation. The framework is evaluated on several RISC-V processor cores, most notably a buggy version of the OpenTitan SoC, where it successfully identified all previously known bugs plus 14 new ones, including a vulnerability significant enough to be registered in the CWE database.

Strengths

1. Excellent Synthesis of Academic Concepts and Industrial Practice: The most significant strength of this work is its successful translation of the hybrid fuzzing paradigm, well-established in software security (e.g., Driller, QSYM), into the rigid and complex world of industrial hardware verification. The integration with UVM (Section 4.1, page 4) is the key insight. Instead of reinventing the entire test generation and simulation environment, the authors cleverly use symbolic execution as an "oracle" that feeds constraints back into the existing, trusted UVM machinery. This pragmatic approach dramatically lowers the barrier to adoption and makes the work immediately relevant to verification engineers.

2. Addressing a Core Problem in Hardware Verification: The paper sits squarely at the intersection of two critical challenges in modern SoC design: the scalability limits of formal verification and the shallowness of unguided, simulation-based methods like constrained-random testing. SymbFuzz offers a compelling "best of both worlds" solution, using the speed of simulation for general exploration and the analytical power of formal methods for targeted, deep exploration of hard-to-reach corner cases. The 6.8x faster convergence compared to traditional UVM random testing (Section 5.3, page 11) is a powerful testament to this approach's value.

3. Strong and Convincing Empirical Validation: The results presented are impressive and serve as strong evidence for the framework's efficacy. Finding a large number of new bugs is a good outcome, but discovering a previously unknown, CWE-worthy vulnerability in a well-scrutinized open-source design like OpenTitan (Bug #01, Table 1, page 8) elevates the work significantly. It proves that the technique is not merely finding trivial bugs but is capable of uncovering subtle and impactful security flaws that other methods have missed.

4. Thoughtful Hardware-Specific Design Choices: The authors demonstrate a clear understanding of the hardware verification domain. The development of a checkpoint and partial-reset mechanism (Section 4.5, page 5) directly addresses a major performance bottleneck in hardware simulation (lengthy reset and initialization sequences). This shows the work is not a simple port of a software technique but a carefully engineered solution tailored to its target domain.

Weaknesses

1. Understated Connection to the Broader Hybrid Fuzzing Lineage: While the work is novel in the hardware context, it would be strengthened by more explicitly positioning itself as the hardware counterpart to the rich history of hybrid fuzzers in the software domain. Acknowledging this intellectual lineage would allow the authors to better highlight the non-trivial contributions required for this adaptation—such as modeling hardware state, handling concurrency implicitly through the simulator, and the aforementioned UVM integration, which have no direct software equivalents.

2. Limited Discussion on the Scalability of the Static Analysis Phase: The paper demonstrates scalability on cores up to ~200k LoC (Table 3, page 12). However, modern SoCs are orders of magnitude larger. The framework relies on an initial static analysis phase to generate the CFG and dependency equations. It would be beneficial to include a discussion on how this analysis phase scales with design size and complexity. For instance, what are the computational and memory bottlenecks—CFG generation, dependency analysis, or the SMT solving itself—when faced with a multi-million gate design composed of numerous interacting IPs?

3. Implicit Manual Effort in Property Definition: The bug detection mechanism relies on a predefined set of security properties written as SystemVerilog assertions (e.g., Listing 5, 7, 9). While effective, the paper does not discuss the effort required to create these properties. For the framework to be truly scalable across new and varied designs, the effort of property specification is a critical factor. A brief discussion on whether these properties are highly generic or require significant design-specific expertise to write would add important context.

Questions to Address In Rebuttal

1. The core concept of using a solver to overcome fuzzer roadblocks is central to hybrid fuzzers in software. Could you elaborate on the most significant unexpected challenges you faced when translating this paradigm from the software domain (sequential programs, single address space) to the hardware RTL/UVM domain (massive concurrency, complex state, cycle-accurate simulation)?

2. Regarding scalability, your results on cores like CVA6 are promising. If you were to apply SymbFuzz to a full commercial SoC with dozens of IPs, what part of your toolchain—CFG generation, dependency equation solving, or runtime coverage tracking—do you anticipate would become the primary performance bottleneck?

3. Your bug-finding capability is impressive and hinges on security properties. For a verification team adopting SymbFuzz for a completely new IP, what is the expected workflow for developing the necessary properties? Are the properties you used for OpenTitan generalizable (e.g., patterns for information leakage), or do they require deep, IP-specific expert knowledge to formulate?

---

Review Form

Reviewer: The Innovator (Novelty Specialist)

Summary

This paper presents SymbFuzz, a hybrid hardware fuzzing framework that uses symbolic execution to guide test generation towards uncovered states. The authors' central claim to novelty rests on being the first such framework to be implemented on and deeply integrated with the industry-standard Universal Verification Methodology (UVM). The proposed system builds a Control Flow Graph (CFG) from the RTL, identifies checkpoints at high-fanout nodes, and when coverage stagnates, uses an SMT solver on dependency equations to generate new input constraints for the UVM sequencer. This allows the fuzzer to escape local coverage maxima and explore hard-to-reach states.

While the fundamental concept of symbolic-execution-guided fuzzing is well-established in the software domain, this paper's primary novel contribution lies in the architectural adaptation and practical implementation of this concept within a commercial-grade hardware verification environment. The specific mechanisms for state restoration (via input-sequence replay) and closed-loop guidance (via UVM sequencer constraints) are presented as novel solutions tailored for the hardware verification domain.

Strengths

1. Novelty in Integration and Practicality: The most significant and undeniable novel contribution is the integration of a hybrid fuzzer into the UVM framework (Section 4.1, page 4). Prior academic hardware fuzzers (e.g., RFuzz, DifuzzRTL, HWFP) are typically standalone tools built on simulators like Verilator. By architecting their solution around UVM components (sequencer, driver, monitor), the authors present a genuinely new pathway for transitioning advanced fuzzing research into industrial practice. This is not merely a reimplementation; it requires a novel design to bridge the gap between symbolic constraint solving and UVM's transaction-based stimulus generation.

2. Domain-Specific State Management Mechanism: The checkpointing mechanism (Section 4.5, page 5) is a novel implementation of state-saving for RTL simulation. It eschews heavyweight, full-state snapshots (common in software via fork-servers) in favor of a lightweight approach: saving the input vector sequence that leads to a checkpoint and re-simulating from reset to restore that state. While re-simulation is not a new idea, its systematic application based on CFG analysis to accelerate path exploration in hardware fuzzing is a novel refinement.

3. Generality over Prior Hybrid Hardware Fuzzers: The paper effectively distinguishes its approach from the closest prior art, HypFuzz [15]. By operating directly on RTL inputs rather than ISA-level binaries, SymbFuzz offers a more general solution applicable to any hardware IP, not just processor cores. This extension of scope is a meaningful "delta" and represents a novel advancement in the applicability of hybrid fuzzing for hardware.

Weaknesses

1. The Core Algorithm is Not Fundamentally New: The central weakness from a novelty perspective is that the underlying algorithm—using symbolic execution to solve path constraints when random mutation gets stuck—is the canonical definition of hybrid or concolic fuzzing. This technique has a long and storied history in software verification, with seminal works like Driller [54], SAGE, and KLEE [12] establishing the paradigm over a decade ago. The paper should more explicitly frame its contribution as a novel adaptation and engineering of this known paradigm to a new domain, rather than implying the hybrid loop itself is a new invention.

2. Incremental Advancement in Guidance: While the implementation is novel, the guidance strategy itself is a straightforward application of symbolic execution. The process of identifying an uncovered branch, tracing its path condition backward, and solving for inputs is conceptually identical to existing work. The novelty is in the plumbing (getting constraints into UVM), not in the guidance logic itself.

3. Overstated Novelty of CFG-based Coverage: The use of a CFG to model hardware states and track coverage is a logical step, but not a profound conceptual leap. Static analysis to extract state machines or flow graphs from RTL is a standard technique in formal verification and synthesis tools. While its application to guide a fuzzer is appropriate, it doesn't represent a fundamentally new analysis technique.

Questions to Address In Rebuttal

1. The core concept of hybrid fuzzing is well-established in software. Beyond the significant challenge of UVM integration, what were the fundamental hardware-specific challenges (e.g., dealing with 4-state logic, timing semantics, complex clocking domains) that required a genuinely novel algorithmic solution, rather than a direct porting of software-based concolic execution principles?

2. The paper effectively differentiates itself from HypFuzz [15] on implementation (RTL vs. ISA) and oracle (assertions vs. differential). Could the authors elaborate on the conceptual novelty of their guidance mechanism compared to HypFuzz? Does HypFuzz's "formal-assisted" search employ a similar symbolic constraint-solving loop, and if so, what is the key conceptual—not just implementation—difference in how SymbFuzz performs its guided search?

3. The dependency equation generation (Section 4.4.2, page 5) appears critical to the guidance mechanism. The paper presents a toy example. How does this analysis scale to large, industrial designs where a single output may depend on thousands of internal registers and inputs over many cycles? Is the novelty of the approach constrained by the scalability of this preliminary analysis, and is the analysis itself novel compared to techniques used in, for example, information flow tracking (IFT) static analysis?