Wie lassen sich Hardware-Ökosysteme und darin enthaltene sensible Daten gegen Hacker-Angriffe schützen? Wie können Sicherheitslücken entdeckt werden? Hier sind Lösungen aus der Sicherheitsforschung gefragt. Der Halbleiterhersteller Intel zeichnet mit dem Intel Hardware Security Academic Award innovative Forschungsergebnisse in diesem Bereich aus.
Das Gewinner-Projekt
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 hervor, dass der vorgeschlagene Ansatz der erste seiner Art sei und großes Potential für die praktische Umsetzung besitze.
Das Team
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.
Wie funktioniert das?
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.
Ausblick
Die TUK-Forschenden sind u.a. 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 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.
