Der Prozessor wird oft als Herz des Computers bezeichnet, dabei ist er viel eher dessen Gehirn. Denn der Prozessor steuert und interpretiert Befehle, koordiniert Abläufe und sorgt dafür, dass von Nutzer:innen angeforderte Aufgaben an die entsprechenden Stellen weitergeleitet werden. Moderne Prozessoren tun das in enormer Geschwindigkeit und erledigen dabei viele Aufgaben parallel. Das schaffen sie unter anderem durch einen Trick, der ihnen hilft, die Prozessor-Ressourcen sinnvoll zu nutzen: die spekulative Ausführung. Xaver Fabian erklärt, was das bedeutet: „In Phasen, in denen der Prozessor nicht voll ausgelastet ist, versucht er mithilfe verschiedener Mechanismen vorauszusehen, welcher Programmschritt als nächstes folgen könnte. Er führt dann die dafür nötigen Berechnungen aus und speichert die Ergebnisse in einen Zwischenspeicher. Werden die Daten doch nicht gebraucht, verwirft er sie. Allerdings hat sich gezeigt, dass die verworfenen Daten eine Spur im Cache-Speicher hinterlassen und dort unter Umständen von Angreifer:innen ausgelesen werden können.“ Die erste Schwachstelle, die Angriffe dieser Art zulässt, ist 2018 unter dem Namen Spectre bekannt geworden und hat hohe Wellen geschlagen. Forschende finden seither regelmäßig neue Spectre-Varianten.
Methoden zum Schließen von Spectre-Lücken
Nachdem die ersten Spectre-Lücken bekannt wurden, wurden ad hoc Maßnahmen entwickelt, um sie zu schließen. Aber wer sagt eigentlich, dass diese Maßnahmen dann auch wirklich immer funktionieren? „Eine Möglichkeit, eine Sicherheitsgarantie dafür abgeben zu können, ist ein formales Modell zu entwickeln. Damit wird eine mathematische Analyse möglich und so können wir die Wirksamkeit der Maßnahmen auch belegen“, erklärt Fabian. Forschende erstellen solche Modelle mithilfe von logisch-mathematischen Methoden und speziellen formalen Sprachen. „Bislang haben sich viele Forschende dabei aber nur auf bestimmte Varianten von Spectre-Lücken und damit nur auf bestimmte Spekulationsmechanismen im Prozessor konzentriert und diese isoliert betrachtet. Ehrlich gesagt, weil auch so schon alles kompliziert genug ist. In Wahrheit laufen im Prozessor aber ja mehrere Spekulationsmechanismen gleichzeitig ab. Wir haben versucht, ein Modell zu schaffen, das es erlaubt diese Mechanismen zu kombinieren. Dahin zu kommen, war nicht einfach. Allein 200 Seiten mathematischer Beweisführung liegen irgendwo auf meinem Schreibtisch.“
Zunächst hat Fabian zwei bislang unbeachtete Spekulationsmechanismen in einer formalen Sprache ausgedrückt und sie somit der mathematischen Beweisführung zugänglich gemacht. Dann hat er diese sogenannten Semantiken mit einer bereits existierenden für einen anderen Mechanismus kombiniert. „Die Grundlage für meine Arbeit bietet die Vorarbeit von IMDEA-Forscher Dr. Marco Guarnieri und anderen. Zum einen habe ich eine von ihnen entwickelte Assembler-Sprache zur Formalisierung genutzt. Zum anderen konnte ich die beiden von mir neu entwickelten Semantiken direkt in das bereits bestehende Tool namens SPECTECTOR einbauen und so testen.“ Und seine Arbeit hat sich ausgezahlt.
Grundstein für zukünftige komplexe Analysen
Für eine umfangreiche Testung, wie robust Prozessoren gegen Spectre-Attacken sind, reicht SPECTECTOR dennoch nicht aus. „Das Modell ist noch ziemlich vereinfacht. Moderne Prozessoren sind sehr komplex und können ganz viel. Die Modellierungsansätze in der Forschung hängen da noch ziemlich hinterher.“ Seine Arbeit bildet aber den Grundstein für eine weitaus komplexere Analyse als sie bislang möglich war. „Wir machen hier absolute Grundlagenarbeit. Aber die braucht es auch. IT-Sicherheit wurde lange zu wenig Beachtung geschenkt. Aber ich habe den Eindruck, dass sich da in den vergangenen Jahren etwas verändert hat.“
Über seinen Distinguished Paper Award, mit dem herausragende Forschungsarbeiten ausgezeichnet werden, freut sich der gebürtige Schleswig-Holsteiner sehr. „Ich war ehrlich gesagt total überrascht. Es ist toll, dass meine Arbeit in der Community geschätzt wird.“
