Collaborative Research: NSF-DFG: SaTC: CORE: Small: VeriFuzz: Light-weight Formal Approaches for Scalable Hardware Fuzzing

Modern embedded systems rely on hardware as the root of trust and are utilized across industries such as healthcare, transportation, and communication. However, the increase in use and complexity of these systems has led to a rise in security-critical hardware vulnerabilities that can be exploited by cross-layer attacks, disrupting traditional threat models that assume either hardware-only or software-only adversaries.

These attacks do not only threaten the reputation of companies and cause monetary damage, but the attacks also undermine the safety, security, and resilience of critical infrastructure in the nation and society at large. Existing hardware validation and verification techniques neither scale to large designs nor achieve sufficient coverage. This project aims to improve scalability and effectiveness of hardware security verification.

The results are disseminated through organizing a new generation of Hack@EVENT hardware security competitions and outreach activities at venues such as Grace Hopper Celebration of Computing. The team uses the developed techniques to empower validation and verification efforts both in educational and industrial contexts.

Fuzzing, an automated input generation technique, has recently been adapted to hardware security validation. Although fuzzing achieves better scalability compared to traditional validation techniques, existing hardware fuzzing approaches do not achieve sufficient design coverage to provide high assurance. The team develops novel fuzzing techniques through the orchestration of formal verification, symbolic execution, and static analysis in providing guidance for effective input state space exploration.

The team also models the patterns of various hardware vulnerability types such as information leakage, denial of service, and micro-architectural vulnerabilities to support fuzzing without relying on golden models or property specifications. This project further automates hardware bug injection. The team leverages their experience in organizing and participating in hardware security competitions and integrating large language model with fuzzing to facilitate bug injection.

This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.