Mikrochips finden als integrierte, miniaturisierte Rechnersysteme in vielen Bereichen Anwendung, beispielsweise in Smartphones, in Fahrzeugen, medizintechnischen Geräten oder der industriellen Fertigung. Sie sind zur technischen Grundlage unserer digitalisierten Gesellschaft geworden. Umso wichtiger ist es, dass sie vertrauenswürdig und sicher arbeiten – Grund für den Chiphersteller Intel, mit dem Hardware Security Academic Award bedeutende Fortschritte der weltweiten Sicherheitsforschung auszuzeichnen.
In diesem Jahr hat der Ansatz des Kaiserslauterer Forschungsteams um Prof. Dr. Wolfgang Kunz, Leiter des Lehrstuhls für Entwurf Informationstechnischer Systeme, die Intel-Jury überzeugt. Die Kaiserslauterer Forscher haben eine formale Rechenmethode entwickelt, die automatisch auf einem eigens entwickelten Software-Werkzeug abläuft. Damit lässt sich mathematisch beweisen, dass die Vertraulichkeitseigenschaften eines Mikrochips mit all seinen Komponenten wie gefordert erfüllt werden.
Die Juroren hoben insbesondere hervor, dass der vorgeschlagene Ansatz der erste seiner Art sei und großes Potenzial für die praktische Umsetzung besitze. Die Bewertung erfolgte anhand des Konferenzbeitrags „A Formal Approach to Confidentiality Verification in SoCs (System-on-Chips) at the Register Transfer Level“, welchen das Team letztes Jahr veröffentlichte.
Der TUK-Professor bewertet die Auszeichnung wie folgt: „Wir freuen uns sehr über diesen renommierten Preis. Das Thema der Cybersecurity ist ein global intensiv beforschtes Gebiet. Die Auszeichnung durch den weltweit führenden Chiphersteller Intel ermutigt unsere Arbeitsgruppe und bestätigt, dass unsere Ergebnisse international sehr positiv aufgenommen werden.“
Gemeinsam mit Kunz erhielten den Preis: Dipl.-Ing. Johannes Müller, M.Sc. Mohammad R. Fadiheh, Dipl.-Ing. Anna Lena Duque Antón, apl. Prof. Dr.-Ing. Dominik Stoffel – alle TUK – sowie Thomas Eisenbarth, Professor für IT-Sicherheit an der Universität zu Lübeck, ein Forschungspartner von Kunz.
Ausgezeichnete Methode
Die von Intel ausgezeichnete Verifikationsmethode ist eine Weiterentwicklung von UPEC (Unique Program Execution Checking) – einer Rechenmethode, die wie ein digitaler Spürhund funktioniert. Bereits 2019, kurz nachdem die Hardware-Schwachstellen Meltdown und Spectre bekannt wurden, konnten Kunz und seine Arbeitsgruppe mit UPEC derartige Seitenkanäle in Mikrochip-Prozessoren nachweisen. Um das Werkzeug zur Sicherheitsanalyse noch vielseitiger zu machen, haben die Forscher die Rechenmethode Schritt für Schritt weiterentwickelt.
Kunz erläutert: „Unser Ziel war es zunächst, nicht nur Seitenkanäle, sondern auch andere Designfehler aufzuspüren, die in einem Mikrochip-Entwurf stecken und die Vertraulichkeit verletzen können, und das für alle Module, aus denen ein solches Hardware-Ökosystem besteht – neben Prozessoren gehören dazu auch Bauteile wie Hardwarebeschleuniger, Kommunikationsschnittstellen, Sensoren und vieles mehr.“
Das neue Verfahren kommt bereits in der Entwurfsphase für Hardware zum Einsatz. „Dies eröffnet die besten Chancen, die Vertraulichkeitseigenschaften eines Mikrochips zu verifizieren“, weiß Müller, der die Fähigkeiten von UPEC im Rahmen seiner Doktorarbeit erweitert und skaliert hat.
Weitere Projekte in der Durchführung
Die Expertise von Kunz und seiner Arbeitsgruppe ist gefragt. So sind die TUK-Forschenden etwa am Projekt „Scale4Edge“ beteiligt, gefördert vom Bundesministerium für Bildung und Forschung (BMBF). Das Programm ist eingebettet in die Leitinitiative „Vertrauenswürdige Elektronik“ des BMBF. In diesem Rahmen entwickelt das Forschungsteam die UPEC-Verifikationsmethode für Mikrochip-Prozessoren mit dem Ziel einer späteren Vermarktung.
Gemeinsam mit Prof. Dr. Thomas Eisenbarth, Universität zu Lübeck, forscht Kunz zudem zur Sicherheit und Verlässlichkeit von sogenannten Out-of-Order-Prozessoren, die die Abarbeitung von Programmen durch spezielle Optimierung der zeitlichen Abläufe auf Hardwareebene beschleunigen. Das Projekt „HaSPro: Verifizierbare Hardwaresicherheit für Out-of-Order Prozessoren“ wird seit 2020 durch die Deutsche Forschungsgemeinschaft im Schwerpunkt „Nano Security“ gefördert.
