SPP 2253, Teilprojekt: HaSPro - Verifizierbare Hardwaresicherheit für Out-of-Order Prozessoren - Phase 2

HaSPro beschäftigt sich mit Transient Execution Side Channels (TES) wie Spectre und Meltdown, die nach wie vor erhebliche Sicherheitsrisiken für Computersysteme darstellen. Heutige Gegenmaßnahmen können lediglich einen Kompromiss zwischen Sicherheit und Rechenleistung erzielen. Das Projekt konzentriert sich auf Out-of-Order-Prozessoren (OoO) mit Speculation sowie auf die für Systemsicherheit essenziellen Trusted Execution Environments (TEEs). HaSPro Phase 1 nutzte Unique Program Execution Checking (UPEC) zur Sicherheitsanalyse gegen TES in Prozessoren. Ein zentrales Ziel bestand darin, UPEC für moderne Prozessorarchitekturen skalierbar zu machen. In Phase 1 wurde die Skalierbarkeit durch ein neues Konzept namens Mikroäquivalenz verbessert. Zudem wurden Seitenkanäle untersucht, die sogenanntes Constant Time Programming kompromittieren. Ein neu entwickeltes Verfahren namens UPEC-DIT kann Sicherheitsgarantien für Data Oblivious Computing berechnen. Im Hinblick auf TEEs konzentrierte sich Phase 1 auf die Identifizierung und Behebung von Schwachstellen in verbreiteten TEE-Designs wie Intel SGX und AMD SEV. Eine Reihe von Problemen wurden aufgedeckt, darunter Ciphertext-Lecks und datenabhängige Programmausführung. Es wurden Gegenmaßnahmen entwickelt, z.B. ein Attestierungsprotokoll für sicheres Speicherlayout sowie verbesserte Methoden bei der deterministischen Speicherverschlüsselung. Es wurden Werkzeuge entwickelt wie Microwalk-CI, das datenabhängiges Laufzeitverhalten in großen Codebasen identifiziert, und Cipherfix, das automatisch Speicherschreibvorgänge, die für Ciphertext-Seitenkanäle anfällig sind, identifiziert und absichert. HaSPro Phase 2 erforscht neue und hocheffiziente Gegenmaßnahmen gegen TES-Angriffe auf mehreren Ebenen: Hardware (HW), HW/SW-Schnittstelle und Software (SW). Es wird untersucht, wie sich HW-gestützte In-Process Isolation gegen verschiedene Spectre-Varianten einsetzen lässt und wie derartige Isolationsbarrieren bei automatisierter SW-Kompartierung genutzt werden können. Die Isolation sensibler Daten von potenziellen Spectre-Gadges kann z.B. durch Compiler-Unterstützung erfolgen. Auf der HW-Ebene werden geeignete Mikroarchitekturmaßnahmen für In-Process Isolation untersucht, wobei formale Methoden zur Berechnung von Sicherheitsgarantien zum Einsatz kommen. Zudem wird als Alternative zu SW-basierten Lösungen eine Secure-by-Construction-Designmethodik für HW-Architekturen für Secure Speculation untersucht. Ein weiteres Forschungsziel besteht in der Verbindung von Code-Kompartierung mit partiell probabilistischer TEE-Speicherverschlüsselung gegen Ciphertext-Seitenkanäle, als zusätzliche Kompromissmöglichkeit zwischen Kosten und Latenz. Alle entwickelten Schutzmechanismen werden auf ihre Wirksamkeit und ihren Overhead hin analysiert und mit bestehenden Verfahren verglichen. Die neuen Verfahren versprechen hocheffizienten Schutz gegen die verbleibende Angriffsfläche in modernen OoO-Prozessoren.