Computergestützte Verifikation physikalischer Sicherheitseigenschaften

• Antragsteller: Dr.-Ing. Pascal Sasdrich
• Fachliche Zuordnung: Sicherheit und Verlässlichkeit, Betriebs-, Kommunikations- und verteilte Systeme ; Rechnerarchitektur, eingebettete und massiv parallele Systeme
• Förderung: Förderung seit 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 510964147

Der Schutz sicherheitskritischer Implementierungen gegen physikalische Angriffe, z. B. Side-Channel Analysis (SCA) oder Fault Injection Analysis (FIA), ist eine arbeitsintensive, anspruchsvolle und fehleranfällige Aufgabe aufgrund der starken Abhängigkeit von menschlichen Faktoren. Folglich kann die computergestützte Sicherheitsverifikation physikalisch geschützter Implementierungen den Entwicklern dabei helfen, die Auswirkungen menschlicher Faktoren zu verringern und die Asymmetrie des Aufwands abzuschwächen, d. h. während für den Nachweis der Unsicherheit nur ein einziges Gegenbeispiel erforderlich ist, muss bei Sicherheitsbeweisen die Gewissheit bestehen, dass es keine Gegenbeispiele gibt. Mit leistungsfähigen computergestützten Verifikationswerkzeugen werden die Robustheit und Qualität künftiger Entwürfe (im Hinblick auf die physikalische Sicherheit) erhöht und die sicherheitsorientierten Hardwareentwicklungszyklen verkürzt und gestrafft. Das vorliegende Vorhaben wird dazu die theoretischen Grundlagen und Modellierungsverfahren im Hinblick auf physikalische Angreifer verbessern. Neben der praktischen Umsetzung von Modellen und Verifikationsroutinen werden fortgeschrittene computergestützte Sicherheitsverifikationswerkzeuge entwickelt und untersucht. Das Arbeitsprogramm dieses Projektes ist daher besonders an der Schnittstelle zwischen Theorie und Praxis angesiedelt, um die Forschungsherausforderungen in abgestimmter Weise aus beiden Perspektiven zu untersuchen. Durch Fortschritte bei den Sicherheitsdefinitionen und Angreifermodellen, die den Anwendungsbereich und die Perspektive der Sicherheitsverifikation weiter vorantreiben, wird die zunehmende Komplexität der fortgeschrittenen Modelle und Definitionen durch Abstraktion und Untersuchung fortgeschrittener Verifikationsmethoden reduziert. Die praktische Umsetzung hilft dann bei der Validierung, Bewertung und Anwendung der Modelle und Definitionen zur Entwicklung sicherer Schaltungen und Systeme. Schließlich ermöglicht die tiefe Integration effizienter Algorithmen, Datenstrukturen und Verifikationsstrategien in bestehende Electronic Design Automation (EDA) erstmals sicherheitsorientierte Entwicklungswerkzeuge und ebnet den Weg für weitere Forschung, z. B. zur sicherheitsbewussten Synthese und Optimierung. Genauer gesagt implementiert die derzeitige computergestützte Sicherheitsverifikation von physikalischen Sicherheitseigenschaften meist nur rudimentäre Werkzeuge, konzentriert sich auf Proof-of-Concept-Implementierungen und erlaubt nur die Verifikation von Kleinstschaltungen. Mit Hilfe der Projektergebnisse wird daher die nächste Generation computergestützter Sicherheitsverifikationswerkzeuge in moderne sicherheitsorientierte EDA-Flows integriert werden und erstmals eine umfassende Sicherheitsverifikation ermöglichen, z. B. für vollständige Implementierungen symmetrischer Kryptographie, fortschrittliche Post-Quantum Cryptography (PQC)-Beschleuniger oder komplexe RISC-V-Prozessorarchitekturen.

• DFG-Verfahren: Emmy Noether-Nachwuchsgruppen