💻 computer science

The 1-Bit Barrier is Universal: k-Stage Pipeline Composition and Unified Leakage Bounds for Standard Modular Reductions in PQC Hardware

Dieser Beitrag präsentiert einen in Lean 4 maschinell verifizierten Beweis, der zeigt, dass beliebig tiefe $k$ -stufige maskierte NTT-Pipelines mit frischem zwischenstufigem Maskieren und PF-PINI( $\leq 2$ )-Gadgets eine universelle Leckagegrenze von $2/q$ pro Beobachtung unabhängig von der Pipeline-Tiefe erreichen, indem zuvor bekannte Kompositionstheoreme verallgemeinert und die Eigenschaften der Montgomery-Reduktion verifiziert werden.

Ursprüngliche Autoren: Ray Iskander, Khaled Kirah

Veröffentlicht 2026-05-07

📖 5 Min. Lesezeit🧠 Tiefgang

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

Das große Ganze: Geheimnisse in einer lauten Fabrik schützen

Stellen Sie sich vor, Sie betreiben eine hochsichere Fabrik, die streng geheime Baupläne (kryptografische Schlüssel) verarbeitet. Um die Baupläne vor Spionen zu schützen, die auf das Geräusch der Maschinen lauschen (Seitenkanalangriffe), senden Sie den Bauplan nicht direkt. Stattdessen teilen Sie den Bauplan in zwei Teile auf: das Geheimnis und eine zufällige Maske. Sie mischen diese zusammen, schicken das Gemisch durch eine Reihe von Maschinen und hoffen, dass das Geräusch der Maschinen das ursprüngliche Geheimnis nicht verrät.

Dieses Papier handelt davon, eine mathematische Garantie zu schaffen, dass dieser Mischprozess funktioniert, egal wie lang die Fertigungsstraße ist.

Das Problem: Die „undichte" Maschine

In der Welt der Post-Quanten-Kryptografie (die neue Art von Mathematik, die benötigt wird, um zukünftige Quantencomputer aufzuhalten), verwendet die Fabrik eine bestimmte Art von Maschine namens Modulare Reduktion (speziell „Barrett"- und „Montgomery"-Reduktionen).

Stellen Sie sich diese Maschinen als spezialisierte Rechner vor.

Die alte Sichtweise: Lange Zeit wussten wir nur, dass der „Barrett"-Rechner ein winziges bisschen Information preisgibt. Wir wussten nichts über den „Montgomery"-Rechner.
Das Risiko: Wenn eine Maschine zu viel preisgibt, kann ein Spion den Stromverbrauch abhören, die zufällige Maske erraten und schließlich den geheimen Bauplan rekonstruieren.

Die Entdeckung: Die „1-Bit-Schranke"

Die Autoren entdeckten, dass sowohl der Barrett- als auch der Montgomery-Rechner ein sehr spezifisches, sicheres Verhalten aufweisen. Sie nennen dies die „1-Bit-Schranke".

Die Analogie:
Stellen Sie sich vor, Sie versuchen, eine Zahl zwischen 1 und 1.000.000 zu erraten.

Wenn eine Maschine schlecht ist, könnte sie Ihre Vermutung auf nur 100 Zahlen eingrenzen. Das ist ein riesiger Leck.
Wenn eine Maschine perfekt ist, gibt sie Ihnen überhaupt keinen Hinweis; Sie müssen immer noch die ganze Million erraten.
Die 1-Bit-Schranke bedeutet, dass die Maschine Ihre Vermutung auf höchstens 2 Zahlen eingrenzt.

In der Sprache des Papiers wird dies als PF-PINI(2) bezeichnet. Das bedeutet, dass es für jede Ausgabe, die die Maschine produziert, nur zwei mögliche Kombinationen aus dem Geheimnis und der zufälligen Maske gibt, die sie hätten erzeugen können. Es ist, als würde die Maschine sagen: „Ich habe dieses Ergebnis erzeugt, und es konnte nur von Geheimnis A oder Geheimnis B stammen." Da es Millionen von Möglichkeiten gibt, ist die Eingrenzung auf nur zwei unglaublich sicher.

Was dieses Papier hinzufügt:

Montgomery ist sicher: Sie bewiesen, dass der Montgomery-Rechner (der in vielen neuen Standards verwendet wird) dieselbe „1-Bit-Schranke" hat wie der Barrett-Rechner.
Die Kettenreaktion: Sie bewiesen, dass wenn Sie diese Rechner in einer langen Reihe (einer Pipeline) verketten, die Sicherheit nicht schlechter wird, nur weil die Reihe länger ist.

Die Lösung: Die „Frische-Maske"-Auffrischungsstation

Das Papier führt eine entscheidende Regel für den Bau dieser Fertigungsstraßen ein: Sie müssen zwischen jeder Maschine eine „Frische Maske" einfügen.

Die Analogie:
Stellen Sie sich ein Staffellauf vor, bei dem Läufer einen Staffelstab weitergeben.

Schlechter Lauf: Wenn Läufer A den Staffelstab an Läufer B weitergibt und Läufer B ihn an Läufer C weitergibt, wird der Stab schmutzig und abgenutzt. Ein Spion, der den ganzen Lauf beobachtet, kann Hinweise von allen drei Läufern zusammensetzen, um das Ziel zu erraten.
Die Lösung (Frische Maske): Zwischen Läufer A und Läufer B stoppen Sie den Lauf. Sie nehmen den Staffelstab, wickeln ihn in eine brandneue, saubere Decke (die frische Maske) und geben ihn an Läufer B weiter. Dann wickeln Sie ihn zwischen B und C in eine weitere brandneue Decke.

Da die Decke jedes Mal neu und zufällig ist, hat der Spion, der Läufer B abhört, keine Ahnung, was Läufer A getan hat. Das „Geräusch" vom ersten Teil des Rennens wird vollständig ausgelöscht.

Das Papier beweist mathematisch, dass solange Sie diese „Frische-Maske"-Auffrischungsstationen verwenden, die Sicherheit der gesamten Linie nur von der allerletzten Maschine abhängt. Die Sicherheit der ersten 99 Maschinen ist weniger wichtig, weil die frischen Masken ihre Lecks wegwaschen.

Das Hauptergebnis: Die „End-to-End"-Garantie

Die Autoren verwendeten einen leistungsstarken Computer-Beweisassistenten (genannt Lean 4), um ihre Mathematik zu überprüfen. Sie haben sie nicht nur aufgeschrieben; sie ließen den Computer jeden einzelnen Schritt verifizieren und stellten sicher, dass es keine logischen Lücken gab.

Ihre Schlussfolgerung:
Wenn Sie eine Pipeline dieser Rechner (Barrett oder Montgomery) bauen und zwischen jeden Schritt eine „Frische Maske" setzen:

Ist die endgültige Ausgabe sicher.
Ist die Menge an Information, die ein Spion stehlen kann, auf diese „1-Bit-Schranke" begrenzt (Eingrenzung der Vermutung auf 2 Möglichkeiten von Millionen).
Gilt diese Sicherheit, egal ob Ihre Pipeline 2 Schritte oder 100 Schritte hat. Die Länge der Pipeline macht sie nicht schwächer.

Die „Adams Bridge"-Fallstudie

Das Papier erwähnt ein reales Hardware-Projekt namens Adams Bridge.

Das Problem: Frühere Forscher stellten fest, dass die Adams-Bridge-Hardware einige Schritte hatte, bei denen sie die „Frische Maske" vergessen hatten oder eine Maschine verwendeten, die nicht perfekt sicher war.
Das Urteil des Papiers: Die Autoren sagten nicht „Adams Bridge ist kaputt". Stattdessen sagten sie: „Adams Bridge besteht den spezifischen Test, den wir gerade bewiesen haben, nicht."
Die Lösung: Sie zeigten, dass Adams Bridge den Test bestehen wird, wenn es die fehlenden „Frische-Maske"-Stationen hinzufügt und sicherstellt, dass jede Maschine einer der sicheren Typen ist.

Zusammenfassung in einem Satz

Dieses Papier beweist, dass wenn Sie sichere mathematische Rechner verketten und zwischen jeden einzelnen eine „frische zufällige Abschirmung" setzen, das gesamte System gegenüber Spionen sicher bleibt, egal wie lang die Kette wird, und dies gilt für beide Haupttypen von Rechnern, die in der zukünftigen quantensicheren Sicherheit verwendet werden.

Technische Zusammenfassung: Die 1-Bit-Barriere ist universell

Problemstellung
Die Zahlentheoretische Transformation (NTT) dient als rechnerisches Rückgrat für die NIST-Post-Quanten-Kryptografie-Standards (PQC) ML-DSA (FIPS 204) und ML-KEM (FIPS 203). Hardware-Implementierungen dieser Standards verlassen sich auf arithmetische Maskierung, um Seitenkanalangriffen, insbesondere der Differentiellen Leistungsanalyse (DPA), zu widerstehen. Während die boolesche Maskierung über $GF(2^n)$ etablierte Kompositionsrahmenwerke (z. B. PINI) aufweist, stellt die arithmetische Maskierung über $\mathbb{Z}_q$ für eine Primzahl $q$ einzigartige Herausforderungen dar.

Vorarbeiten im QANARY-Programm (Papiere 1–6) etablierten strukturelle Abhängigkeitsanalysen und quantifizierten Sicherheitsmargen für spezifische Komponenten, wobei insbesondere nachgewiesen wurde, dass die Barrett-Reduktion eine „1-Bit-Barriere" (PF-PINI(2)) erfüllt. Zwei kritische Lücken blieben jedoch bestehen:

Beliebige Pipeline-Tiefe: Bisherige Kompositionstheoreme waren auf zwei Stufen beschränkt. Es gab keine formale Garantie für beliebige $k$ -stufige Pipelines mit frischer Zwischenstufen-Maskierung.
Montgomery-Reduktion: Während die Barrett-Reduktion charakterisiert war, fehlte eine formale PF-PINI-Charakterisierung für die Montgomery-Reduktion – die zweite Standardmodulreduktion, die in NTT-Hardware verwendet wird (dominant in ML-DSA und einigen ML-KEM-Implementierungen).
Vereinheitlichte End-to-End-Schranken: Es existierte keine einzelne, maschinengeprüfte Kardinalitätsschranke, die die Ergebnisse für beliebige Pipelines zusammensetzte, die aus Butterfly-Operationen, Barrett- und Montgomery-Reduktionen bestehen.

Methodik
Der Artikel verwendet formale Verifikation mit dem Lean-4-Beweisassistenten. Der Ansatz ist strikt konstruktiv, mit null sorry (unbewiesenen Annahmen) und null nicht-standard Axiomen. Die Methodik stützt sich auf:

PF-PINI-Definition: Verwendung des Parameters Prime-Field Probe Isolating Non-Interference (PF-PINI), der die Leckage eines Ein-Draht-Gadgets unter einer einzelnen arithmetischen Maske quantifiziert. Ein Gadget ist PF-PINI( $M$ ), wenn die Kardinalität des Urbilds eines beliebigen Ausgabewerts höchstens $M$ beträgt.
Pipeline-Modellierung: Definition einer $k$ -stufigen Pipeline, wobei jede Stufe $G_i$ ein PF-PINI-Gadget ist, getrennt durch frische Zufallsmasken. Der Pipeline-Ausgang wird rekursiv berechnet.
Kombinatorische Analyse: Beweis, dass frische Zwischenstufen-Maskierung die Leckageparameter der Zwischenstufen „löscht", sodass die finale Schranke nur vom Parameter der letzten Stufe abhängt.
Hardware-treue Modellierung: Modellierung der Montgomery-Reduktion unter Berücksichtigung von Hardware-Registerbreiten und Wraparound-Verhalten, insbesondere die Analyse des Kollisionsoffsets $2^{w-s}$ .

Hauptbeiträge
Der Artikel leistet vier Hauptbeiträge, alle in Lean 4 formalisiert:

Das $k$ -Stufen-Kompositionstheorem (Theorem 3.1):
Dieses Theorem verallgemeinert das vorherige 2-Stufen-Kompositionsergebnis auf beliebige Tiefe $k \ge 1$ . Es beweist, dass für eine Pipeline von Gadgets $G_0, \dots, G_{k-1}$ mit frischer Zwischenstufen-Maskierung die Kardinalität des Urbilds des Ausganges begrenzt ist durch:
$| \{ (m, f) : \text{Pipeline-Ausgang} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$
Entscheidend ist, dass die Schranke durch die letzte Stufe bestimmt ist; die Parameter aller Zwischenstufen werden durch die frischen Masken gelöscht.
Montgomery-Reduktion ist PF-PINI(2) (Theorem 4.3):
Der Artikel beweist formal, dass die Montgomery-Reduktion die PF-PINI(2)-Eigenschaft erfüllt und die Struktur der Barrett-Reduktion widerspiegelt. Er zeigt, dass die hardware-treue Montgomery-Abbildung eine „Zwei-Zweig"-Struktur aufweist (abhängig davon, ob ein Wraparound auftritt), was zu einer Urbild-Kardinalität von höchstens 2 führt. Theorem 4.7 etabliert zudem die Schärfe dieser Schranke und zeigt, dass für Standardparameter (ML-KEM und ML-DSA) die Multiplizität exakt 2 beträgt.
End-to-End-Multiplizitätsschranke (Theorem 5.1):
Durch Kombination des $k$ -Stufen-Kompositionstheorems mit den spezifischen PF-PINI(2)-Ergebnissen für Barrett (Paper 5), Montgomery (dieser Artikel) und Butterfly-Operationen (Paper 4) etabliert der Artikel eine vereinheitlichte Schranke. Für jede $k$ -stufige Pipeline, bei der jede Stufe $\text{maxMult} \le 2$ erfüllt, ist die Urbild-Kardinalität des Ausganges begrenzt durch:
$2 \cdot q^{2k-2}$
Unter dem Probing-Modell erster Ordnung mit uniformen Masken entspricht dies einer bedingten Wahrscheinlichkeitsschranke pro Beobachtung von $2/q$ , unabhängig von der Pipeline-Tiefe $k$ .
Formale Verankerung empirischer Befunde (Theorem 5.4):
Der Artikel liefert eine in Lean verifizierte Bedingung, die besagt, dass wenn irgendeine Stufe in einer Pipeline $\text{maxMult} \ge 3$ aufweist (z. B. eine unmaskierte Stufe), die Hypothese der End-to-End-Schranke versagt. Dies verankert formale empirische und strukturelle Analysen des „Adams Bridge" PQC-Beschleunigers (Papiere 1, 2 und externe Arbeiten) und bestätigt, dass spezifische unmaskierte Konfigurationen in diesem Design außerhalb der hinreichenden Bedingungen für die tiefenunabhängige Schranke fallen.

Ergebnisse

Universalität der 1-Bit-Barriere: Der Artikel bestätigt, dass die „1-Bit-Barriere" (eine Urbild-Kardinalität von 2) für beide in NIST-PQC-Hardware verwendeten Standardmodulreduktionen (Barrett und Montgomery) gilt.
Tiefenunabhängigkeit: Die formalen Beweise zeigen, dass das Hinzufügen von Stufen zu einer Pipeline die Leckageschranke pro Beobachtung nicht verschlechtert, sofern frische Zwischenstufen-Maskierung verwendet wird und jede Stufe PF-PINI( $\le 2$ ) erfüllt.
Verifikationsstatus: Das gesamte Artefakt besteht aus 20 Deklarationen über drei Theorem-Module hinweg, kompiliert in 1.753 Jobs mit null Fehlern, null sorry und ohne native Entscheidungsprozeduren.

Bedeutung und Behauptungen
Der Artikel positioniert sich als Vollendung eines formalen Verifikationsprogramms für maskierte NTT-Hardware. Seine Bedeutung liegt in der Bereitstellung einer quantitativen, maschinengeprüften kompositionellen Grundlage für Hardware-Designer.

Für die Zertifizierung: Die abgeleitete Kardinalitätsschranke ( $2 \cdot q^{2k-2}$ ) liefert den spezifischen Nachweis, der für DPA-Widerstandsargumente auf Architekturebene erforderlich ist, und ergänzt Gate-Level-Tools wie SILVER und maskVerif.
Für Designer: Sie bietet einen präskriptiven Remedierungs-Pfad: Um eine tiefenunabhängige Schranke zu erreichen, müssen Designer sicherstellen, dass jede Stufe PF-PINI( $\le 2$ ) erfüllt und frische Masken zwischen den Stufen eingefügt werden.
Bescheidenheit der Behauptungen: Die Autoren stellen ausdrücklich fest, dass die Wahrscheinlichkeits- und Min-Entropie-Interpretationen (z. B. $2/q$ ) informelle semantische Konsequenzen der Kardinalitätsschranken sind und nicht mechanisch in Lean formalisiert wurden. Ferner behauptet der Artikel bezüglich der Adams-Bridge-Analyse nur, dass spezifische Konfigurationen die hinreichenden Bedingungen von Theorem 5.1 nicht erfüllen; er behauptet nicht, dass die Hardware „defekt" oder „unsicher" sei, und erkennt an, dass alternative Rahmenwerke oder stärkere Modelle zu anderen Schlussfolgerungen führen könnten. Die Arbeit wird als Werkzeug für die kompositionelle Analyse und nicht als endgültiges Sicherheitsurteil über spezifische Implementierungen gerahmt.