NSF-DFG: SaTC: Light-weight Formal Approaches for Scalable Hardware Fuzzing

• Applicant: Professor Dr.-Ing. Ahmad-Reza Sadeghi
• Subject Area: Security and Dependability, Operating-, Communication- and Distributed Systems ; Computer Architecture, Embedded and Massively Parallel Systems
• Term: since 2024
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 538883423

Hardware designs are becoming increasingly complex to meet the rising need for custom hardware and increased performance. However, unlike software vulnerabilities that can be patched, most hardware vulnerabilities cannot be fixed post-fabrication, resulting in security vulnerabilities that put many critical systems at risk and tarnish the reputation of the companies involved. Hence, it is essential to detect vulnerabilities pre-fabrication. Existing formal verification and static analysis techniques achieve high coverage, they suffer in terms of scalability. On the other hand, fuzzing scales to larger hardware designs compared to these techniques, yet can only reach deeper parts of the design with guidance. This proposal builds on the hypothesis that guiding fuzzing with semantic feedback generated using formal verification and static analysis can detect deep hardware vulnerabilities in a more scalable way. The proposed work leverages four research thrusts: (i) Formal Assisted Fuzzing: Formal verification will be utilized to generate guidance, e.g., input values, to help fuzzing reach deep states. Interleaving of formal verification and fuzzing will be optimized by learning cost functions for the performance of fuzzing and formal verification using Machine Learning. (ii) Vulnerability Pattern Guided Fuzzing: Formalizing known vulnerabilities into well-defined patterns will allow their detection using multi-level analysis. A pattern language will be developed to facilitate definitions of new vulnerabilities and the variants of known ones. (iii) IFT Guided Fuzzing: Data-flows and control-flows between architectural and microarchitectural registers will be identified to help fuzzing generate dynamic traces for detecting Spectre like vulnerabilities. (iv) Automated Bug Injection: Building on the success of HACK@Events, we will utilize the Large Language Models (LLMs) and code patterns to automate bug injection and bug translation across designs. If successful, the proposed research will advance the capabilities of existing fuzzing and formal verification approaches by scaling them to System-on-Chips (SOCs) and deep hardware vulnerabilities. PIs will organize a new generation of HACK@EVENT competition series that will be supported with automated injection and transfer of bugs to newer platforms. PIs will disseminate the results of the proposed research through their courses on Hardware/Software Verification and Hardware Security, through outreach events for K-12, undergraduate/graduate students, and underrepresented groups, and HACK@EVENT at the top conferences in the hardware and security domains.

• DFG Programme: Research Grants
• International Connection: USA
• Cooperation Partners: Professor Jeyavijayan Rajendran; Professor Aakash Tyagi; Professorin Tuba Yavuz