Hardware-Sicherheit auf neuem Niveau: Granite und die modulare Verifikation
Timing-Seitenkanäle gehören zu den hartnäckigsten Sicherheitsrisiken in der Mikroarchitektur. Während Entwickler an der funktionalen Korrektheit feilen, können Angreifer über die Zeit messen, wie lange Operationen dauern, und daraus Rückschlüsse auf geheime Daten ziehen. Das Team hinter Granite hat sich dieser Herausforderung gestellt und eine Methodik entwickelt, die Hardware und Software auf Timing-Sicherheit verifiziert—modular und mathematisch fundiert.
Das Problem: Unsichtbare Lecks
Moderne Prozessoren sind komplex. Sie führen Instruktionen spekulativ aus, verwalten Interrupts präzise und kommunizieren mit I/O-Systemen. Diese Merkmale sind funktional notwendig, erzeugen aber Timing-Variationen, die schweigend Geheimnisse preisgeben können. Ein kryptographischer Algorithmus mag mathematisch sicher sein, aber wenn seine Ausführungszeit von den eingegebenen Schlüsselbits abhängt, ist die praktische Sicherheit gefährdet.
Bisherige Verifikationsansätze haben dieses Problem nur partiell gelöst. Sie beschränkten sich oft auf ISA-Ebene (Instruction Set Architecture) oder auf einzelne Komponenten. Der Sprung zwischen abstrakten Sicherheitsmodellen und der tatsächlichen Wire-Level-Realisierung auf dem Chip blieb ein Vertrauenslücke—eine Lücke, die nur durch Vermutung gefüllt wurde, nicht durch Beweis.
Granite: Ein modularer Weg
Granite adressiert dieses Problem durch eine durchdachte Verifikationsstrategie. Die zentrale Idee ist leakage-aware refinement via determinism. Statt zu versprechen, dass die Hardware perfekt versteckt, was sie tut, definiert Granite präzise, welche Observables (messbare Effekte) zulässig sind—und beweist dann, dass der tatsächliche Prozessor diese Observables nicht überschreitet.
Die Spezifikation von Granite ist bewusst abstraktiv: Sie regelt nicht, wie viele Zyklen eine Instruktion braucht, nicht wann ein Interrupt auftritt und nicht die exakte Latenz von Subkomponenten wie Multiplizierer oder Memory. Stattdessen fokussiert Granite auf zwei Ebenen:
- Funktionale Korrektheit: Die Instruktionen berechnen das Richtige.
- Information-Flow-Abhängigkeiten: Welche öffentlichen Daten beeinflussen welche Aspekte der Ausführung?
Für geheime Daten, die nicht beeinflussen sollen, wird dies durch deterministische, aber unbekannte Funktionen modelliert. Diese Funktionen sind nicht vertrauenswürdig—nur die Tatsache, dass sie auf öffentlichen Daten arbeiten, ist garantiert.
Modulare Komposition
Ein Schlüsselmerkmal von Granite ist die Modularität. Subkomponenten wie ALUs oder Memory-Systeme werden gegen ihre eigenen Leakage-Specs verifiziert. Diese einzelnen Beweise komponieren sich dann zu einer Gesamtgarantie für den gesamten Chip. Das bedeutet: Ein Verifikationsingenieur kann einen Multiplizierer verifizieren, ohne den gesamten Prozessor verstehen zu müssen. Die formalen Beweise passen wie Bausteine zusammen.
Die Cicq-Verbindung
Das Besondere: Granite eliminiert die meisten Zwischenschichten aus der Trusted Computing Base (TCB). Das Team leitete seine Beweise in Rocq (ehemals Coq) ab, einem Theorem-Prover, der jeden Schritt überprüft. Durch eine zertifizierte statische Analyse erkennt das System, welche Software-Code cryptographic-constant-time einhält—das ist der Standard in der Kryptographie, bei dem Laufzeit und Speicherzugriff unabhängig vom Geheimnis sein müssen.
Das Ergebnis: Ein einzelner formaler Beweis, der von Hardware-Zyklen bis zur Softwareausführung reicht, ohne dass dazwischen vertraut werden muss. Selbst die ISA-Leakage-Verträge fallen aus der TCB weg—sie sind nur Annotationen, der Beweis prüft alles.
Was bedeutet das praktisch?
Für Entwickler kryptographischer Hardware bedeutet Granite konkret:
- Vollständiger Beweis der Timing-Sicherheit über alle Schichten hinweg
- Modulare Spezifikationen, die nicht die Details jeder Subkomponente festschreiben
- Composable Proofs, die wiederverwendbar sind
- Minimale TCB, da Beweise in Rocq überprüft sind
Es ist das erste Mal, dass eine Methodik diese Anforderungen erfüllt: modular, fundiert und mit direkter Verbindung zwischen ISA-Contracts und Cycle-by-Cycle Execution mit Wire-Level Observables.
Die Grenze des Machbaren
Granite ist kein Wundermittel. Es beweist, dass wenn ein Programm constant-time ist, dann läuft es auch timing-sicher auf der Hardware. Es prüft aber nicht selbstständig, ob Algorithmen constant-time sind—das ist Aufgabe der statischen Analyse. Und es skaliert auf komplexe Designs wie echte RISC-Prozessoren mit Pipelines, Spekulation und Interrupts.
Das ist nicht trivial. Timing-Seitenkanäle sind notorisch schwer zu beherrschen, weil so viele Faktoren zusammenspielen. Granite zeigt: Mit der richtigen Methodik und formalen Werkzeugen ist vollständige Verifikation möglich.
Fazit
Granite ist ein wichtiger Schritt für Hardware-Sicherheit. Es schließt eine kritische Lücke zwischen abstrakten Sicherheitsmodellen und echter Silizium-Implementierung. Für Projekte, die kryptographische Hardware verifizieren müssen oder wollen, bietet es einen praktischen, mathematisch fundierten Weg.
