💻 computer science

Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

Diese Arbeit liefert formale Beweise in Lean 4, dass frische Maskierung in Pipelines von NTT-Stufen für PQC-Hardware (ML-KEM/ML-DSA) über $\mathbb{Z}_q$ eine kompositionssichere, kontextunabhängige Uniformität garantiert und damit die strukturelle Unsicherheit des Adams-Bridge-Beschleunigers erklärt.

Ursprüngliche Autoren: Ray Iskander, Khaled Kirah

Veröffentlicht 2026-04-23

📖 4 Min. Lesezeit☕ Kaffeepausen-Lektüre

CC BY 4.0

Ursprüngliche Autoren: Ray Iskander, Khaled Kirah

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

🛡️ Der unsichtbare Schutzschild: Wie man geheime Zahlen in Computer-Chips sicher macht

Stellen Sie sich vor, Sie bauen einen hochmodernen Tresor (einen Computer-Chip), der die Geheimnisse der Zukunft bewahren soll – sogenannte Post-Quanten-Kryptografie. Diese Geheimnisse sind extrem wichtig, denn sie schützen alles von Bankkonten bis zu Staatsgeheimnissen vor zukünftigen Supercomputern.

Das Problem: Wenn dieser Tresor arbeitet, "leckt" er manchmal winzige Informationen aus (z. B. durch den Stromverbrauch). Ein Hacker könnte diese winzigen Lecks sammeln und das Geheimnis erraten.

Um das zu verhindern, nutzen Ingenieure eine Technik namens Maskierung. Das ist wie das Mischen von echten Geheimnissen mit viel "Rauschen" oder falschen Spuren.

🧩 Das Puzzle: Die "NTT"-Maschine

Der Herzschlag dieser neuen Tresore ist eine spezielle Rechenmaschine namens NTT (Number Theoretic Transform). Man kann sich das wie eine riesige Fließbandanlage vorstellen, auf der Zahlen von einem Band zum nächsten wandern.

Jede Station auf diesem Band ist ein kleiner "Butterfly"-Prozessor (ein Fachbegriff für eine bestimmte Art von Rechenoperation).

Die alte Idee: Ingenieure dachten: "Wenn jede einzelne Station auf dem Fließband sicher ist (weil sie maskiert ist), dann ist das ganze Band sicher."
Die Realität: Das war ein gefährlicher Irrtum. Es gibt eine Lücke in der Logik, die bisher niemand mathematisch bewiesen hatte.

🚨 Die Falle: Der "Punkt-für-Punkt"-Trick

Stellen Sie sich vor, Sie wollen prüfen, ob eine Station sicher ist. Ein Ingenieur schaut sich an: "Wenn ich das Geheimnis ändere, aber die Masken (das Rauschen) gleich lasse, ändert sich dann der Ausgangswert?"

Das Ergebnis: Ja! Der Wert ändert sich.
Die falsche Schlussfolgerung: Der Ingenieur denkt: "Aha! Das ist unsicher!" und wirft den Entwurf weg.
Die Wahrheit: Das ist eine Falle. Bei dieser speziellen Rechenart (dem "Butterfly") ist es normal, dass sich der Wert ändert, wenn man das Geheimnis ändert. Das ist kein Fehler!

Die Autoren dieser Arbeit haben bewiesen, dass man nicht auf den einzelnen Wert schauen darf, sondern auf die Verteilung.

Die richtige Frage: "Wenn ich das Geheimnis ändere, aber alle möglichen Masken durchgehe, ist dann jedes Ergebnis gleich wahrscheinlich?"
Die Antwort: Ja! Wenn man frische, zufällige Masken an jeder Station verwendet, ist das Ergebnis perfekt verteilt. Es sieht für den Hacker aus wie reines Rauschen, egal welches Geheimnis dahintersteckt.

🌉 Der "Adams Bridge"-Fehler

In der Arbeit wird ein reales Beispiel namens Adams Bridge (ein Chip-Design von der Firma CHIPS Alliance) kritisiert.

Was passiert dort? Die Maske wird nur am Anfang des Fließbands neu gesetzt. Auf den folgenden Stationen wird die alte Maske weiterverwendet oder gar keine neue hinzugefügt.
Die Analogie: Stellen Sie sich vor, Sie mischen Ihren Kaffee mit Milch (Maskierung). Am Anfang ist er perfekt gemischt. Aber wenn Sie den Kaffee durch drei weitere Tassen laufen lassen, ohne jedes Mal frische Milch hinzuzufügen, setzen sich die Milchklümpchen am Ende wieder ab. Der Kaffee ist wieder durchsichtig (unsicher).
Das Ergebnis: Der Adams Bridge-Chip ist unsicher, weil er die Regel der "frischen Maske" an jeder Station bricht. Die Autoren haben mathematisch bewiesen, warum das so ist.

🛠️ Was haben die Autoren getan? (Die "Lean 4"-Magie)

Bisher waren solche Beweise nur "auf dem Papier" (mit Stift und Zettel). Das ist wie eine Schatzkarte, die man nicht überprüft hat.
Diese Autoren haben einen Computer-Beweis erstellt, der von einer Software namens Lean 4 geprüft wurde.

Keine Fehler erlaubt: Die Software hat jede einzelne Zeile des Beweises auf Herz und Nieren geprüft. Es gibt keine "vielleicht" oder "hoffentlich".
Das Ergebnis: Sie haben einen unzerstörbaren Beweis geliefert, dass:
1. Die "Punkt-für-Punkt"-Falle real ist (man darf sie nicht prüfen).
2. Die "Verteilungs"-Sicherheit real ist (man muss das prüfen).
3. Die Goldene Regel: Wenn man an jeder Station des Fließbands eine frische, neue Maske hinzufügt, ist das gesamte System sicher.

🎯 Warum ist das wichtig?

Für Ingenieure: Sie haben jetzt eine klare Anleitung: "Mache an jeder Station eine neue Maske!" und einen mathematischen Beweis, den sie Behörden (wie für FIPS-Zertifizierungen) vorzeigen können.
Für die Sicherheit: Sie wissen jetzt genau, welche Chips sicher sind und welche (wie Adams Bridge) einen fundamentalen Fehler haben.
Für die Zukunft: Sie haben den ersten Schritt getan. Die "leichten" Teile (lineare Rechenoperationen) sind jetzt bewiesen. Die "schweren" Teile (komplizierte Multiplikationen) werden in den nächsten Papern behandelt.

Zusammenfassung in einem Satz

Die Autoren haben mit einem Computer-Beweis gezeigt, dass man geheime Zahlen in neuen Sicherheitschips nur dann wirklich schützen kann, wenn man an jeder einzelnen Rechenstation frisches "Rauschen" (Maskierung) hinzufügt – und dass man nicht auf die falschen Warnsignale hereinfallen darf, die einen dazu bringen könnten, gute Designs zu verwerfen.

Titel: Fresh Masking Makes NTT Pipelines Composable: Machine-Checked Proofs for Arithmetic Masking in PQC Hardware

Autoren: Ray Iskander und Khaled Kirah
Kontext: Post-Quanten-Kryptographie (PQC), Hardware-Beschleuniger für ML-KEM (FIPS 203) und ML-DSA (FIPS 204).

1. Problemstellung

Post-Quanten-Kryptographie-Implementierungen (insbesondere für ML-KEM und ML-DSA) nutzen häufig die Zahlentheoretische Transformation (NTT) als zentrale Komponente, die als Pipeline von Cooley-Tukey-Butterfly-Stufen über dem Ring $\mathbb{Z}_q$ implementiert wird. Um Seitenkanalangriffe (z. B. Power Analysis) abzuwehren, wird eine arithmetische Maskierung (Arithmetic Masking) eingesetzt.

Das zentrale Problem liegt in der Kompositionssicherheit:

Es ist intuitiv anzunehmen, dass eine Pipeline sicher ist, wenn jede einzelne Stufe sicher ist.
Bisherige formale Verifikationsframeworks (wie ISW, t-SNI, PINI, DOM) und deren maschinell überprüfte Artefakte (z. B. in EasyCrypt oder Isabelle/HOL) konzentrieren sich fast ausschließlich auf Boolesche Maskierung über $GF(2)$.
Es fehlte ein maschinell überprüfter Nachweis, dass arithmetisch maskierte NTT-Butterfly-Stufen über $\mathbb{Z}_q$ (für $q > 0$ ) sicher komponiert werden können, insbesondere im Fall von frischem Maskierungsmaterial (fresh randomness) zwischen den Stufen.
Ein spezifisches Missverständnis besteht darin, dass Designer oft nach punktweiser Wertunabhängigkeit (pointwise value-independence) suchen, was für Butterfly-Ausgänge jedoch falsch ist und zu falschen Sicherheitsurteilen führt.

Ein konkretes Beispiel für die praktische Relevanz ist der Adams Bridge Accelerator (im CHIPS Alliance Caliptra-Projekt), der strukturell unsicher ist, da er keine frische Maskierung zwischen den NTT-Stufen verwendet.

2. Methodik

Die Autoren verwenden formale Verifikation mittels des Lean 4-Beweisassistenten mit der Bibliothek Mathlib.

Ziel: Erstellung von maschinell überprüften Beweisen ("zero sorry", "zero admit"), die für alle Moduli $q > 0$ gelten.
Modell: Das ISW-Modell für First-Order-Probing (ein Angreifer beobachtet genau eine Leitung pro Taktzyklus).
Ansatz:
1. Schließen einer Lücke aus vorheriger Arbeit (Paper 3) durch die Einführung eines "r-bearing" (frische Zufälligkeit tragenden) Modells.
2. Analyse der algebraischen Struktur der Butterfly-Operation (Affinität in Bezug auf die Maske).
3. Beweis der Per-Context-Uniformität (Uniformität über die frische Maske hinweg, unabhängig vom Geheimnis).
4. Induktiver Beweis für die Komposition einer $k$ -stufigen Pipeline.

3. Schlüsselbeiträge

Das Paper liefert drei Hauptergebnisse, die alle in Lean 4 formalisiert sind:

A. Der "r-bearing Bridge" (Schließen der Lücke)

Problem: Vorherige Arbeiten zeigten, dass Wertunabhängigkeit eine konstante Randverteilung impliziert, aber nur für den Fall ohne frische Zufälligkeit ( $r$ -free).
Lösung: Die Autoren beweisen, dass Wertunabhängigkeit auch unter Einbeziehung frischer Zufälligkeit (via ValueIndependentR) eine konstante Randverteilung impliziert. Dies wird über eine algebraische Proxy-Funktion (MutualInfoZero) formalisiert.
Bedeutung: Dies schließt die theoretische Lücke, dass frische Masken die Sicherheitsgarantien nicht untergraben, sondern sie erst ermöglichen.

B. Butterfly Per-Context Uniformity (Die korrekte Sicherheitseigenschaft)

Warnung vor einem Trugschluss: Die Autoren beweisen, dass punktweise Wertunabhängigkeit (dass der Ausgabewert bei fixierter Maske nicht vom Geheimnis abhängt) für Butterfly-Ausgänge falsch ist. Ein Designer, der dies prüft, würde fälschlicherweise eine sichere Schaltung als unsicher markieren.
Korrekte Eigenschaft: Stattdessen wird ButterflyMarginalVI definiert. Für jeden Ausgabedraht gibt es genau einen Maskenwert, der einen bestimmten Ausgabewert $v$ erzeugt, unabhängig vom Geheimnis.
Ergebnis: Jeder Cooley-Tukey-Butterfly mit frischer Ausgabemaske über $\mathbb{Z}_q$ erfüllt diese Eigenschaft universell für alle $q > 0$ , alle Twiddle-Faktoren und alle Eingaben. Dies ist eine direkte Folge der Affinität der Operation ( $c - m$ ).

C. Pipeline Composition (Komposition der Pipeline)

Haupttheorem: Eine $k$ -stufige NTT-Pipeline mit frischer Maskierung pro Stufe erfüllt die Per-Context-Uniformität an jeder Stufe.
Beweis: Durch Induktion wird gezeigt, dass die Änderung der Maske in einer späteren Stufe ( $j > i$ ) den Zustand früherer Stufen ( $i$ ) nicht beeinflusst (Lemma pipelineStateAt_update_future). Da jede Stufe die Uniformitätseigenschaft erfüllt, gilt dies für die gesamte Pipeline.
Design-Prinzip: Dies etabliert das "Fresh Masking Design Principle": Nur wenn jede Stufe eine unabhängig frisch generierte Maske erhält, ist die Pipeline gegen First-Order-Probing sicher.

4. Ergebnisse

Formaler Beweis: Das Artefakt besteht aus 9 Theoremen in 3 Lean-Dateien (ca. 580 Zeilen Code). Der Build-Prozess umfasst 1.738 Jobs ohne Fehler oder Warnungen.
Universalität: Die Beweise gelten für alle Moduli $q > 0$ (nicht nur Primzahlen), was ML-KEM ( $q=3329$ ), ML-DSA ( $q=8380417$ ) und zukünftige Standards abdeckt.
Analyse von Adams Bridge:
- Der Adams Bridge Accelerator verletzt das Fresh-Masking-Prinzip (Maskierung nur im INTT-Round 0, danach unmaskiert).
- Da die Hypothese des Kompositionstheorems verletzt ist, greift die Sicherheitsgarantie nicht. Dies erklärt die in früheren Arbeiten (Paper 1 & 2) empirisch festgestellten Sicherheitslücken strukturell.
Abgrenzung: Die Arbeit behandelt nur den linearen Fall (Butterfly). Nichtlineare Gadgets (wie Barrett-Reduktion oder Multiplikatoren) sind komplexer und werden in separaten Arbeiten (Paper 3 und kommende Paper) behandelt, die das PF-PINI-Framework nutzen.

5. Bedeutung und Fazit

Praktische Relevanz für FIPS 140-3: Die Arbeit liefert Hardware-Ingenieuren und Zertifizierungsstellen (NIST) den ersten maschinell überprüften, universell quantifizierten Nachweis, dass eine korrekt maskierte NTT-Pipeline sicher ist. Dies kann direkt in Zertifizierungsdokumentationen zitiert werden.
Korrektur von Missverständnissen: Die Arbeit warnt explizit davor, punktweise Wertunabhängigkeit als Sicherheitskriterium für arithmetische Maskierung zu verwenden, und etabliert stattdessen die Randverteilungs-Uniformität als korrektes Kriterium.
Architektonische Einsicht: Sie liefert die mathematische Begründung, warum das Fehlen frischer Maskierung zwischen Pipeline-Stufen (wie bei Adams Bridge) zu struktureller Unsicherheit führt.
Beitrag zur Theorie: Obwohl die mathematische Tiefe geringer ist als bei nichtlinearen Kompositionssätzen (ISW), füllt sie eine kritische Lücke in der formalen Verifikation von PQC-Hardware, indem sie den spezifischen, aber weit verbreiteten Fall der linearen arithmetischen Maskierung in NTTs abdeckt.

Zusammenfassend beweist das Paper, dass frische Maskierung pro Stufe der Schlüssel zur Sicherheit von NTT-Pipelines ist und liefert den ersten maschinell verifizierten Beweis dafür, dass diese Architektur unter dem ISW-Modell sicher komponiert werden kann.