Formal-assisted Processor Fuzzing
Formal-assisted processor fuzzing is a hybrid verification methodology applied to hardware processor designs. It combines a coverage-guided hardware fuzzer with an underlying formal verification engine so that the formal component targets design regions that the fuzzer struggles to reach on its own, while the fuzzer handles the bulk of the input space exploration.
Motivation
Existing hardware fuzzers are effective at detecting security vulnerabilities in modern processors, but they do not fuzz the hard-to-reach design spaces well. Consequently, they cannot effectively exercise security-critical control- and data-flow logic, and may miss vulnerabilities in those regions.
Approach
A representative instantiation of formal-assisted processor fuzzing is the HyPFuzz hybrid fuzzer. HyPFuzz leverages formal verification tools to help fuzz the hard-to-reach parts of processors, and applies optimizations in time and space:
- A scheduling strategy prevents under- or over-utilization of the capabilities of the formal tools and the fuzzer, balancing how much effort each side contributes at any moment.
- Heuristic strategies select specific points in the design space for the formal tool to target, steering the formal component toward the most promising uncovered logic.
Evaluation
HyPFuzz was evaluated on five widely-used open-source processors. The reported results include:
- Detection of all vulnerabilities found by the most recent processor fuzzer at the time of publication.
- Discovery of three new vulnerabilities that were missed by previous extensive fuzzing and formal verification campaigns, leading to two new CVE entries.
- A coverage speedup of approximately 11.68× over the most recent processor fuzzer.
Relationship to Other Processor Fuzzers
Formal-assisted processor fuzzing sits alongside other processor-fuzzing paradigms:
- Traditional coverage-guided processor fuzzers such as DifuzzRTL and TheHuzz use code coverage and control-register coverage as feedback to guide mutation of randomly generated instruction seeds. These fuzzers generate seeds by randomly generating instructions and then mutate instructions in the current input; they are effective at broad coverage but tend to miss deep, hard-to-reach logic.
- Other hybrid hardware fuzzers such as PSOFuzz combine fuzzing with optimization algorithms (e.g., particle-swarm optimization) to improve coverage, and similarly inherit seed generation and mutation engines from traditional processor fuzzers such as TheHuzz.
A key limitation noted in the literature is that while the seed generators and mutation engines of hybrid fuzzers can identify valid instructions from the ISA, they lack well-defined feedback to determine a meaningful sequence of instructions that will lead to deep design regions.
Significance
By formally guiding fuzzing toward hard-to-reach design corners, formal-assisted processor fuzzing expands the effective coverage of processor security verification and has been shown to surface vulnerabilities missed by both prior fuzzing-only and prior formal-only efforts.