💻 computer science

Prime-Field PINI: Machine-Checked Composition Theorems for Post-Quantum NTT Masking

Dieser Beitrag stellt die ersten maschinell verifizierten Kompositionstheoreme für arithmetische Maskierung über Primkörper vor, beweist, dass frische zufällige Maskierung zwischen Pipeline-Stufen die Sicherheitsunabhängigkeit von vorherigen Stufen gewährleistet, und nutzt diese formalen Ergebnisse, um einen kritischen Maskierungsfehler zwischen den Stufen im PQC-Beschleuniger Adams Bridge von Microsoft zu diagnostizieren.

Ursprüngliche Autoren: Ray Iskander, Khaled Kirah

Veröffentlicht 2026-04-29

📖 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

Stellen Sie sich vor, Sie versuchen, eine geheime Nachricht durch eine Fabrikfließbandanlage zu senden. Die Nachricht ist sensibel, daher möchten Sie nicht, dass jemand, der die Linie beobachtet, herausfindet, was sie ist. Um sie zu schützen, zerlegen Sie die Nachricht in Teile und mischen jedes Teil mit einem zufälligen „Rauschen" (einer Maske), bevor es zur nächsten Station weitergeleitet wird. Dies nennt man Maskierung.

In der Welt der Computersicherheit gibt es zwei Hauptarten von Rauschen:

Boolesches Rauschen: Wie das Umschalten von Schaltern (ein/aus). Wir haben bereits ein perfektes Regelbuch dafür, wie man diese Schalter sicher stapelt.
Arithmetisches Rauschen: Wie das Addieren von Zahlen auf einer Uhr (wo 12 + 1 = 1). Dies ist das, was moderne „Post-Quanten"-Kryptographie verwendet. Bis jetzt hatten wir kein Regelbuch, um diese zahlenbasierten Masken sicher zu stapeln.

Dieser Artikel liefert das fehlende Regelbuch. Hier ist die Geschichte dessen, was sie fanden, einfach erklärt.

1. Das Problem: Die „undichte" Mitte

Stellen Sie sich eine zweistufige Fließbandanlage vor:

Station A: Nimmt Ihr Geheimnis, fügt etwas Rauschen hinzu und leitet es weiter.
Station B: Nimmt das, was Station A weitergegeben hat, fügt mehr Rauschen hinzu und sendet das Endergebnis.

Die Forscher entdeckten einen gefährlichen Fehler in der Art und Weise, wie diese Stationen in einem berühmten Microsoft-Sicherheitschip (genannt „Adams Bridge") miteinander verbunden waren.

Im fehlerhaften Design gab Station A ihr verrauschtes Ergebnis direkt an Station B weiter. Aufgrund der Funktionsweise der Mathematik (speziell einem Schritt namens „Barrett-Reduktion", der wie eine komplexe Art der Division ist), war das aus Station A kommende „Rauschen" nicht perfekt zufällig. Es hatte ein Muster.

Die Analogie: Stellen Sie sich vor, Station A ist ein Mixer. Er mischt Ihr Geheimnis mit Eis. Aber aufgrund der Art, wie die Klingen rotieren, sind die herauskommenden Eisstücke leicht ungleichmäßig – an einigen Stellen gibt es mehr Eis, an anderen weniger. Wenn ein Spion (ein Hacker) genau zwischen Station A und Station B steht und die Eisstücke zählt, kann er einen Teil Ihres Geheimnisses erraten. Dies nennt man einen Seitenkanalangriff.

2. Die Lösung: Die „Frische Maske" (Das Erneuerungsargument)

Der große „Aha!"-Moment des Artikels ist überraschend einfach. Sie bewiesen, dass wenn Sie eine frische, brandneue zufällige Maske zwischen Station A und Station B einfügen, das Problem sofort verschwindet.

Die Analogie:

Ohne die Korrektur: Station A übergibt einen leicht ungleichmäßigen Eisberg an Station B. Station B versucht, es zu reparieren, aber die Unebenheit ist bereits eingebacken.
Mit der Korrektur: Station A übergibt ihren ungleichmäßigen Berg einer „Reset-Taste". Diese Taste kippt den Berg in einen riesigen, perfekt durchmischten Eimer mit frischem Wasser (die neue Maske). Jetzt, wenn Station B einen Löffel aus diesem Eimer nimmt, ist es wieder perfekt zufällig.

Der Artikel beweist mathematisch, dass diese frische Maske das Gedächtnis von Station A vollständig löscht. Es spielt keine Rolle, ob Station A unordentlich oder perfekt war; sobald die frische Maske angewendet wird, ist die Leitung, die zu Station B führt, perfekt gleichmäßig. Die Sicherheit der gesamten Linie hängt dann nur noch davon ab, wie gut Station B ist.

3. Die „1-Bit-Barriere"

Die Forscher stellten fest, dass das Rauschen für die spezifische Mathematik, die in diesen Chips verwendet wird (Barrett-Reduktion), für sich genommen nie perfekt zufällig ist. Es hat ein „Leck" von bis zu 1 Bit Information.

Stellen Sie sich das wie eine leicht beschwerte Münze vor. Es ist keine faire Münze; sie landet etwas häufiger auf „Kopf".
Dies ist kein Fehler im Design; es ist eine fundamentale Eigenschaft der Mathematik. Der Artikel nennt dies die „1-Bit-Barriere".
Der Artikel beweist jedoch, dass wenn Sie den Trick mit der „Frischen Maske" zwischen den Stufen anwenden, dieses 1-Bit-Leck im frischen Rauschen versteckt wird und für einen Spion nutzlos wird.

4. Der Beweis: Maschinenüberprüft

Die Autoren haben dies nicht nur auf Papier niedergeschrieben; sie verwendeten ein Computerprogramm namens Lean 4, um jeden einzelnen Schritt ihrer Logik zu überprüfen.

Sie schrieben 18 spezifische Beweise.
Der Computer verifizierte sie alle mit null Fehlern und null „Ich mache das später"-Notizen (genannt „sorry stubs").
Das bedeutet, die Mathematik ist steinhart. Es ist nicht nur eine Theorie; es ist ein verifiziertes Faktum.

5. Die Diagnose: Warum Microsofts Chip anfällig war

Das Team wandte ihr neues Regelbuch auf Microsofts „Adams Bridge"-Chip an.

Die Feststellung: Der Chip hatte zwei Stufen (Butterfly und Barrett), aber keine frische Maske zwischen ihnen.
Das Ergebnis: Die Leitung, die diese beiden Stufen verbindet, war „undicht". Sie war nicht gleichmäßig. Dies bestätigte, warum andere Forscher diesen Chip bereits erfolgreich mittels Leistungsanalyse (Messung des Stromverbrauchs) gehackt hatten.
Die Korrektur: Der Artikel schreibt eine einfache Korrektur vor: Fügen Sie zwischen den Stufen einen zusätzlichen Zufallszahlengenerator und einen Subtraktionsschritt hinzu. Dies macht die Zwischenleitung perfekt sicher.

Zusammenfassung

Dieser Artikel löst ein fehlendes Puzzleteil für sichere Computerchips.

Das Problem: Wenn man mathematische Operationen miteinander verketten, kann das „Rauschen", das verwendet wird, um Geheimnisse zu verstecken, in der Mitte unordentlich werden und Informationen durchsickern lassen.
Die Korrektur: Fügen Sie zwischen jedem Schritt eine frische, zufällige „Reset"-Funktion ein.
Der Beweis: Sie verwendeten einen Computer, um zu beweisen, dass dieses Reset die mittlere Leitung perfekt sicher macht, unabhängig davon, wie unordentlich der erste Schritt war.
Die Anwendung: Sie zeigten genau, warum ein berühmter Microsoft-Chip anfällig war und wie man ihn mit einer einfachen architektonischen Änderung repariert.

Kurz gesagt: Wenn Sie ein Geheimnis durch einen mehrstufigen Prozess verstecken wollen, verlassen Sie sich nicht nur auf die Verkleidung des ersten Schritts. Werfen Sie zwischen jedem Schritt eine frische Verkleidung hinzu, und das Geheimnis bleibt sicher.

1. Problemstellung

Das Papier adressiert eine kritische Lücke in der formalen Sicherheitsverifikation von Post-Quantum-Kryptographie (PQC)-Hardware, speziell für Number Theoretic Transform (NTT)-Implementierungen, die in NIST-Standards (ML-KEM und ML-DSA) verwendet werden.

Der Kontext: Hardware-Implementierungen von NTT verlassen sich auf arithmetische Maskierung über Primfeldern ( $\mathbb{Z}_q$ ), um Seitenkanalangriffen wie der Differential Power Analysis (DPA) zu widerstehen.
Die Lücke: Während boolesche Maskierung (über $GF(2^n)$ ) über eine ausgereifte Kompositionstheorie (NI, SNI, PINI) mit maschinengeprüften Beweisen verfügt, fehlen für die arithmetische Maskierung über Primfelder analoge Kompositionstheoreme.
Das spezifische Problem: Bei der arithmetischen Maskierung interagieren Operationen wie die Modulo-Reduktion (z. B. Barrett-Reduktion) auf nicht-triviale Weise mit den Masken. Im Gegensatz zum booleschen XOR, bei dem die Maskierung die Gleichverteilung perfekt bewahrt, kann die arithmetische Maskierung zu nicht-gleichverteilten Ausgabeverteilungen führen (Multiplizität > 1).
Die Schwachstelle: Frühere empirische Analysen und strukturelle Studien identifizierten Schwachstellen im PQC-Beschleuniger „Adams Bridge" von Microsoft, bei denen intermediate Leitungen zwischen Pipeline-Stufen nicht gleichverteilt waren und DPA-Angriffe ermöglichten. Eine formale theoretische Erklärung dafür, warum dies geschieht und wie es durch Kompositionstheoreme behoben werden kann, fehlte jedoch.

2. Methodik

Die Autoren verwenden formale Verifikation mit dem Beweisassistenten Lean 4, um Kompositionstheoreme für die arithmetische Maskierung abzuleiten und zu beweisen.

Formales Modell: Sie definieren eine quantitative Sicherheitsmetrik namens PF-PINI(k) (Prime-Field Probe Isolating Non-Interference).
- Im Gegensatz zu binären Sicherheitsbegriffen (sicher/unsicher) misst PF-PINI die Multiplizität von Ausgabewerten relativ zum Maskenraum.
- $k=1$ impliziert eine perfekt gleichverteilte Verteilung.
- $k=2$ impliziert eine maximale Multiplizität von 2, was bis zu 1 Bit Information pro Leitung preisgibt.
Das „Renewal Argument": Der zentrale theoretische Erkenntnisgewinn ist, dass die Anwendung eines frischen Zufallsmasken zwischen zwei Pipeline-Stufen den Sicherheitsparameter ( $k_1$ ) der ersten Stufe von der intermediären Leitung vollständig „löscht", unabhängig davon, wie nicht-gleichverteilt die Ausgabe der ersten Stufe war.
Hardware-Brücke: Die Autoren überbrücken formal die Lücke zwischen abstrakten algebraischen Modellen ( $\mathbb{Z}_q$ ) und hardware-treuer natürlicher Zahlenarithmetik (Nat), wie sie in RTL-Designs verwendet wird, speziell für die Barrett-Reduktion.
Verifikationsumfang: Die gesamte Arbeit besteht aus 18 maschinengeprüften Theoremen mit keinem sorry-Stub (keine unbewiesenen Annahmen), was Garantien mit hoher Zuverlässigkeit sicherstellt.

3. Hauptbeiträge

Das Papier leistet sechs primäre Beiträge:

Das Renewal-Theorem (Theorem 4.1): Beweist, dass, wenn eine frische Zufallsmaske zwischen zwei Stufen ( $G_1 \to G_2$ ) angewendet wird, die intermediäre Leitung perfekt gleichverteilt wird. Die Menge der Maskenpaare, die einen spezifischen intermediären Wert erzeugen, hat genau die Kardinalität $q$ , unabhängig vom Sicherheitsparameter von $G_1$ .
Positives Kompositionstheorem (Theorem 4.4): Zeigt, dass eine zweistufige Pipeline mit frischer Maskierung PF-PINI( $k_2$ ) erfüllt. Die Sicherheit der zusammengesetzten Ausgabe hängt nur vom Parameter der zweiten Stufe ( $k_2$ ) ab; die Schwäche der ersten Stufe ( $k_1$ ) wird vollständig gelöscht.
Negative Kompositionstheoreme (Theoreme 5.1–5.3): Beweist, dass ohne frische Maskierung die intermediäre Leitung die Multiplizität der ersten Stufe ( $k_1$ ) beibehält. Wenn $k_1 > 1$ ist, ist die Leitung nicht gleichverteilt, was eine notwendige Bedingung für DPA-Angriffe darstellt.
Algebraisch-Hardware-Brücke (Theorem 6.1): Beweist formal, dass die algebraische Barrett-Reduktionsabbildung unter Standard-Scope-Bedingungen ( $q \le 2^s$ ) äquivalent zur hardware-treuen Nat-Arithmetikabbildung ist. Dies validiert, dass die theoretischen Grenzen direkt auf Silizium-Implementierungen anwendbar sind.
Adams-Bridge-Diagnose: Instanziiert die Theoreme formal, um den Microsoft Adams-Bridge-Beschleuniger zu diagnostizieren. Der Beweis bestätigt, dass das Fehlen einer frischen inter-stufigen Maskierung Barrett-Ausgangsleitungen nicht-gleichverteilt lässt (PF-PINI(2)) und erklärt damit den Erfolg früherer empirischer DPA-Angriffe.
Universelle 1-Bit-Barriere: Liefert rechnerische Beweise, dass die PF-PINI(2)-Schranke für Modulo-Reduktionen (sowohl Barrett als auch Montgomery) universell ist, was auf eine fundamentale „1-Bit-Barriere" für diese Operationen hindeutet.

4. Hauptergebnisse

Formaler Beweis der Komposition: Das Papier stellt fest, dass frische inter-stufige Maskierung die notwendige und hinreichende Bedingung ist, um arithmetische Gadgets sicher zu komponieren.
Quantitative Sicherheit:
- Mit frischer Maskierung: Die intermediäre Leitung ist gleichverteilt ( $k=1$ ). Die finale Ausgabe wird durch den Parameter der zweiten Stufe ( $k_2$ ) begrenzt.
- Ohne frische Maskierung: Die intermediäre Leitung ist nicht gleichverteilt (bis zu $k_1$ ). Diese Nicht-Gleichverteilung ist die Ursache für die bei empirischen Angriffen beobachteten Seitenkanal-Lecks.
Adams-Bridge-Fix: Die Diagnose bestätigt, dass das Hinzufügen eines einzelnen frischen Zufallsmaskenregisters und einer Subtraktionsoperation zwischen der Butterfly- und der Barrett-Stufe in der Adams-Bridge-Pipeline die DPA-Schwachstelle auf den intermediären Leitungen beseitigen würde, ohne den Sicherheitsparameter der finalen Ausgabe zu ändern.
Verfügbarkeit des Artefakts: Der vollständige Lean-4-Quellcode, einschließlich 18 Theoreme und eines Reproduktionsskripts, ist öffentlich verfügbar und ermöglicht eine unabhängige Verifikation der Beweise.

5. Bedeutung

Erste maschinengeprüfte arithmetische Komposition: Dies ist die erste Arbeit, die maschinengeprüfte Kompositionstheoreme für die arithmetische Maskierung über Primfelder bereitstellt und damit eine große theoretische Lücke in der PQC-Hardwaresicherheit schließt.
Überbrückung von Theorie und Praxis: Durch die formale Verknüpfung abstrakter algebraischer Beweise mit hardware-treuer Arithmetik bietet das Papier eine rigorose Grundlage für die Verifikation realer Silizium-Designs und geht über empirische Tests hinaus.
Design-Leitlinie: Es etabliert eine klare, beweisbare Designregel für PQC-Hardware: Fügen Sie immer frische Maskierung zwischen Pipeline-Stufen ein. Diese einfache architektonische Änderung garantiert, dass die Sicherheit der komponierten Pipeline ausschließlich durch das schwächste Glied in der finalen Stufe bestimmt wird, nicht durch die intermediären.
Konvergenz der Beweise: Der formale Beweis stimmt perfekt mit drei unabhängigen vorherigen Analysen überein (empirische Leistungsanalyse, Code-Review und strukturelle Abhängigkeitsanalyse) und bestätigt, dass der identifizierte architektonische Fehler im Adams-Bridge-Beschleuniger tatsächlich die Ursache seiner Schwachstelle ist.

Zusammenfassend bietet dieses Papier das mathematische und formal-verifikatorische Rückgrat, das erforderlich ist, um sichere, komponierbare und seitenkanalresistente Hardware-Beschleuniger für die neue Ära der Post-Quantum-Kryptographie zu entwerfen.