Förderperiode I

Task 1.1: Modellierung von Fehlerinjektion:

Gegenstand dieses Tasks ist die Modellierung von punktuellen Fehlerinjektionen mit bestimmter Auflösung (welche die Präzision des Angriffs beschreibt) sowie von Fehlerinjektionen durch Manipulation von Verzögerungsverhalten. Punktuelle Fehlerinjektionen sind in Angriffsmodellen verwendet worden. Dabei wird entweder eine hohe Auflösung („Kippen“ eines bestimmten Lei­tungswerts innerhalb der Schaltung bzw. eines Zustandsbits des Kryptosystems) oder eine ge­ringere Auflösung („Kippen“ einer zunächst unbekannten Untermenge von Bits innerhalb eines eingegrenzten Bereichs) unterstützt. Die Fehlerinjektion durch Manipulation von Verzögerungs­verhalten wird mittels physikalischen Messungen auf dem FPGA durchgeführt. Wie im Bericht über WP3 im Detail erläutert wird, wurden alle betrachteten Small-Scale-AES-Varianten als Schaltungen auf dem FPGA umgesetzt (in VHDL spezifiziert und mittels gängiger Synthese­software auf den Xilinx-FPGA-Baustein auf dem SAKURA-Board abgebildet) Für die Messun­gen wurde auf dem FPGA (vgl. WP3) ein Fehlerinjektor entwickelt und in das System integriert. Der Fehlerinjektor verschiebt kontrolliert das Zeitgebersignal (Clock), so dass statt der korrekten Werte die Zwischenergebnisse in die Register übernommen werden. Diese werden dann über die USB-Schnittstelle auf den Rechner übertragen und dort analysiert.

Task 1.2: Gemischte funktional-strukturelle Modelle:

Es wurden automatische Verfahren entwickelt, die auf Basis einer Beschreibung des Kryptosys­tems ein Fehlerangriffs-System aufstellen. Die Beschreibung kann dabei entweder als Schalt­kreis (strukturell) oder als Polynom (funktional) vorliegen, und das Fehlerangriffs-System ist dementsprechend entweder ein Schaltkreis, der mittels Tseitin-Transformation in eine Boole­sche Formel übertragen werden kann, oder ein Polynomsystem. Nach einer erfolgreichen Fehlerinjektion kann über das Fehlerangriffs-System der geheime Schlüssel aus dem korrekt und fehlerhaft verschlüsselten Text berechnet werden. Dieser Ablauf wurde in einer ersten Version umgesetzt und als Workshop-Beitrag veröffentlicht. Dazu wurde eine Umwandlung der Polynome in eine Boolesche Formel ent­wickelt, so dass funktionale und strukturelle Modelle kombiniert werden können. Diese Formel kann dann mit der aus dem Schaltkreis entwickelten Formel kombiniert werden. Dabei muss insbesondere auf die richtige Zuordnung der Variablen geachtet werden.

Ein Ziel des Projekts bestand in der Definition von Filterregeln, um in überspezifizierten SAT-Instanzen, die sowohl Klauseln aus dem funktionalen als auch aus dem strukturellen Modell beinhalten, eine Untermenge von besonders vielversprechenden Klauseln auszuwählen, die zu reduzierten Lösungszeiten führen. Die bislang gewonnenen Ergebnisse deuten darauf hin, dass die strukturellen Modelle oftmals in geringerer Zeit abgearbeitet werden als rein funktionale oder gemischt funktional-strukturelle Modelle. Dabei wurden auch einfache Filterre­geln auf der Basis der Klausellänge evaluiert.

Task 1.3: Adaptive Steuerung des Angriffs:

Die zentrale Aufgabe dieses Tasks ist die Abschätzung der Größe der Schlüssel-Kandidaten­menge, um zwischen der Fortsetzung der Berechnung, dem Übergang zur Brute-Force-Suche oder einer weiteren Fehlerinjektion zu entscheiden. Zu diesem Zwecke wurde der in Task T2.2 weiterentwickelte #SAT-Solver eingesetzt. Allerdings stellte sich hier heraus, dass bei der An­wendung auf die im Projekt erstellten Fehlerangriffs-Systeme die Anzahl der erfüllenden Bele­gungen der Formeln keinen Rückschluss auf die reale Kandidatenmenge zulässt. Durch den variablen Fehlerort kann es für den gleichen Schlüssel-Kandidaten verschiedene erfüllende Be­legungen für die Boolesche Formel geben. Der #SAT-Solver zählt alle diese erfüllenden Bele­gungen, und die Anzahl der erfüllenden Belegungen stellt nur eine (potentiell sehr ungenaue) Überabschätzung der Kardinalität der Schlüssel-Kandidatenmenge dar.

Task 2.1: Randbasen- und Gröbnerbasen-Verfahren:

Zuerst wurde eine Neu­implementation des Randbasis-Algorithmus (RBA) vorgenommen, und zwar sowohl als Proto­typ in der Toplevelsprache des Computeralgebrasystems ApCoCoA als auch als C++ Programm. Diese Implementation wurde sodann für Boolsche Polynome (also Polynome über dem Körper GF(2) modulo den Gleichungen x_i²-x_i=0) optimiert. Bereits die ersten Optimierungen lieferten einen sehr wesentlichen Performancegewinn für den Boolschen Fall. Der neue Algorithmus wurde auf verschiedene Gleichungssyste­me angewendet, die aus algebraischen Angriffen auf Versionen des Small Scale AES Krypto­systems stammen. Obwohl die Timings noch wesentlich langsamer waren als die des spezia­lisierten Pakets PolyBoRi des Sage-Computeralgebrasystems, zeigten sie doch eine vielversprechende Tendenz und boten weitere Verbesserungsmöglichkeiten. Ebenso wurden erste Möglichkeiten aufgezeigt, Zwischenergebnisse des Boolschen RBA in die Berechnungen des SAT-Solvers antom einzubringen und umgekehrt. Sodann wurden die Implementationen des RBA und des Boolschen RBA durch die Einführung einer signatur-basierten Version nochmals weiter verbessert. Durch diese Technik ist es möglich, die Abarbeitung vieler neuer Kandidatenpolynome für die Randba­sis zu vermeiden, indem Mehrfachberechnungen entdeckt werden, d.h. es wurden teilweise Analoga zu den in der Gröbner-Basis-Welt fundamentalen Buchbergerschen Kriterien für die Vermeidung unnötiger Reduktionen kritischer Paare gefunden. Die Timings des neuen Algorithmus angewandt auf Gleichungssysteme, die aus algebraischen Angriffen und Fehlerangriffen stammen, zeigen eine Beschleunigung mindestens um den Faktor sechs und für kleine und mittelgroße Beispiele stellen sie mit PolyBoRi vergleichbare Ergebnisse dar. Jedoch zeigt sich wie erwartet, dass die Lösungsmethode durch eine Umwandlung in ein Erfüllbarkeitsproblem und die Anwendung eines SAT-Solvers um ein bis zwei Größenord­nungen schneller ist. Erste Versuche ergeben aber auch, dass sich der SAT-Solver bei mittel­großen bis großen Beispielen, die aus algebraischen Fehlerangriffen stammen, durch die geschickte Auswahl und Einspeisung von Teilergebnissen des signaturbasierten Boolschen RBA noch weiter beschleunigen lässt.

Das Benchmarking sowohl der ApCoCoA-Prototypen als auch der optimierten C++-Implementa­tionen erfolgt mit einer Reihe von Beispielen, die aus algebraischen Angriffen und Fehlerangrif­fen auf Small-Scale AES, sowie aus algebraischen Fehlerangriffen auf den Lightweight Cipher LED64 stammen.

Task 2.2: SAT-Verfahren und inkrementelle Techniken:

Der Prototyp des #SAT-Solvers #antom wurde komplett überarbeitet und größten­teils neu entwickelt. Das Ergebnis ist der #SAT-Solver countAntom bzw. die hochparallele Vari­ante dCountAntom. Die wichtigsten Optimierungen für countAntom sind im Pre­processing, der Variablenordnung (welche ausführlich untersucht wurde) und dem Formel-Caching zu sehen. Für letzteres wurde mit Laissez-Faire Caching ein neues Caching Verfahren entwickelt, welches auch bei einem parallelen Lösungsvorgang ein korrektes Ergebnis garan­tiert. Mit dCountAntom wurde der Ansatz auf hochparallelen Cluster-Systemen mit bis zu 256 CPU- Kernen übertragen und dort erfolgreich eingesetzt.

Task 2.3: Enge Integration

Die Integration der Randbasen- und SAT-Solver wurde auf zwei Ebenen vorangetrieben. Auf der programmtechnischen Ebene wurde zum Zwecke der nebenläufigen Ausführung der beiden Solver und ihrer Kommunikation miteinander ein Shared-Memory Ansatz gewählt. Dies erlaubt eine sehr schnelle Kommunikation zwischen den Prozessen des Randbasen- und SAT-Solvers über einen gemeinsamen Speicherbereich.  Auf der konzeptuellen Ebene wurde die Transformation zwischen SAT-Klauseln, die vom SAT-Solver generiert werden, und Polynomsystemen, die durch den Randbasen-Solver erzeugt werden, umgesetzt. Die Konsistenz zwischen den beiden Systemen zu garantieren, hat sich als eine durchaus herausfordernde Anforderung herausgestellt, da bereits kleinste Änderungen etwa bei Variablenbenennungen sofort zu Abweichungen der beiden Solver und inkorrekten Lösungen führen. Um derartige Inkonsistenzen zu vermeiden, wurden Validierungsprogramme entwickelt, welche die Plausibilität der zwischen den Solvern ausgetauschten Klauseln bzw. Polynome überprüfen. Des Weiteren wurden hier die Verwaltung der kombinierten Klauselmen­ge und die Filterregel im Sinne des adaptiven Verfahrens aus Task T1.3 integriert.

Alle im Projekt betrachteten Schaltungen sind auf einem SAKURA-FPGA-Board umgesetzt und mit den polynomiellen Modellen abgegli­chen worden. Dabei waren recht komplexe technische Anpassungen vor allem im Bereich der USB-Anbindung zur Kommunikation zwischen dem Board und dem Steuerrechner, notwendig. Diese Schaltungen können unter Benchmarks heruntergeladen werden. Neben der FPGA-Abbildung wurde auch eine Synthese auf die Gatterebene mit gängigen kommerziellen Werkzeugen durchgeführt; die Ergebnisse sind ebenfalls auf der Benchmark-Webseite frei verfügbar.