NSF-DFG: SaTC: Leichte formale Ansätze für skalierbares Hardware-Fuzzing

• Antragsteller: Professor Dr.-Ing. Ahmad-Reza Sadeghi
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung seit 2024
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 538883423

Hardware-Designs werden zunehmend komplexer, um den steigenden Bedarf an maßgeschneiderter Hardware und höherer Leistung zu decken. Im Gegensatz zu Software-Schwachstellen, die gepatcht werden können, können die meisten Hardware-Schwachstellen nach der Herstellung nicht behoben werden, was zu Sicherheitslücken führt, die viele kritische Systeme gefährden und den Ruf der beteiligten Unternehmen beeinträchtigen. Daher ist es wesentlich, Schwachstellen vor der Herstellung zu erkennen. Bestehende formale Verifikations- und statische Analysetechniken erreichen zwar eine hohe Abdeckung, leiden jedoch in Bezug auf die Skalierbarkeit. Auf der anderen Seite skaliert Fuzzing im Vergleich zu diesen Techniken auf größere Hardware-Designs, kann jedoch nur tiefere Teile des Designs mit Anleitung erreichen. Diese Forschungsbemühung basiert auf der Hypothese, dass das Lenken von Fuzzing mithilfe von semantischen Rückmeldungen, die mithilfe formaler Verifikation und statischer Analyse generiert werden, auf eine skalierbarere Weise tiefe Hardware-Schwachstellen erkennen kann. Die vorgeschlagene Arbeit nutzt vier Forschungsschwerpunkte: (i) Formell unterstütztes Fuzzing: Formale Verifikation wird verwendet, um Anleitungen, z. B. Eingabewerte, zu generieren, die Fuzzing helfen, tiefe Zustände zu erreichen. Die Verzahnung von formaler Verifikation und Fuzzing wird durch das Erlernen von Kostenfunktionen für die Leistung von Fuzzing und formaler Verifikation mithilfe von maschinellem Lernen optimiert. (ii) Fuzzing unter Verwendung von Schwachstellenmustern: Die Formalisierung bekannter Schwachstellen in gut definierte Muster ermöglicht deren Erkennung mithilfe von mehrstufiger Analyse. Es wird eine Mustersprache entwickelt, um die Definition neuer Schwachstellen und Varianten bekannter Schwachstellen zu erleichtern. (iii) IFT-gesteuertes Fuzzing: Datenflüsse und Kontrollflüsse zwischen architektonischen und mikroarchitektonischen Registern werden identifiziert, um Fuzzing bei der Generierung von dynamischen Traces zur Erkennung von Spectre-ähnlichen Schwachstellen zu unterstützen. (iv) Automatische Fehlerinjektion: Aufbauend auf dem Erfolg von HACK@Events werden wir die Large Language Models (LLMs) und Code-Muster nutzen, um die automatische Fehlerinjektion und Fehlerübersetzung zwischen Designs zu automatisieren. Bei erfolgreicher Umsetzung wird die vorgeschlagene Forschung die Fähigkeiten bestehender Fuzzing- und formaler Verifikationsansätze erweitern, indem sie sie auf System-on-Chip und tiefe Hardware-Schwachstellen skalieren. Die Hauptverantwortlichen werden eine neue Generation der HACK@EVENT-Wettbewsserie organisieren, die durch die automatisierte Injektion und Übertragung von Fehlern auf neuere Plattformen unterstützt wird. Die Ergebnisse werden von den PIs in ihren Kursen zu Hardware-/Software-Verifikation und Hardware-Sicherheit und unterrepräsentierte Gruppen sowie bei HACK@EVENT auf Konferenzen im Hardware- und Sicherheitsbereich verbreitet.

• DFG-Verfahren: Sachbeihilfen
• Internationaler Bezug: USA
• Kooperationspartnerinnen / Kooperationspartner: Professor Jeyavijayan Rajendran; Professor Aakash Tyagi; Professorin Tuba Yavuz