💻 computer science

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

Dit artikel presenteert een door Lean 4 machine-gecontroleerd bewijs dat willekeurig diepe $k$ -staps gemaskerde NTT-pijplijnen met verse maskering tussen de stadia en PF-PINI( $\leq 2$ )-gadgets een universele leksgrens per observatie van $2/q$ bereiken, onafhankelijk van de pijplijndiepte, door eerdere compositiestellingen te generaliseren en eigenschappen van de Montgomery-reductie te verifiëren.

Oorspronkelijke auteurs: Ray Iskander, Khaled Kirah

Gepubliceerd 2026-05-07

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Ray Iskander, Khaled Kirah

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Het Grote Geheel: Geheimen Beschermen in een Lawaaierige Fabriek

Stel je voor dat je een hoogbeveiligde fabriek runt die topgeheime blauwdrukken (cryptografische sleutels) verwerkt. Om de blauwdrukken veilig te houden voor spionnen die naar het geluid van de machines luisteren (side-channel-aanvallen), stuur je de blauwdruk niet direct. In plaats daarvan splits je de blauwdruk in twee stukken: het Geheim en een Willekeurig Masker. Je mengt ze samen, stuurt het mengsel door een reeks machines, en hoopt dat het lawaai van de machines het oorspronkelijke geheim niet verraadt.

Dit artikel gaat over het bouwen van een wiskundige garantie dat dit mengproces werkt, ongeacht hoe lang de assemblagelijn is.

Het Probleem: De "Lekke" Machine

In de wereld van Post-Quantum Cryptografie (het nieuwe type wiskunde dat nodig is om toekomstige quantumcomputers te stoppen), gebruikt de fabriek een specifiek type machine genaamd Modulaire Reductie (specifiek "Barrett" en "Montgomery" reducties).

Stel je deze machines voor als gespecialiseerde rekenmachines.

Het Oude Inzicht: Lange tijd wisten we alleen dat de "Barrett"-rekenmachine een klein beetje informatie lekte. We wisten niets over de "Montgomery"-rekenmachine.
Het Risico: Als een machine te veel lekt, kan een spion naar het stroomverbruik luisteren, het willekeurige masker raden en uiteindelijk de geheime blauwdruk reconstrueren.

De Ontdekking: De "1-Bit Barrière"

De auteurs ontdekten dat zowel de Barrett- als de Montgomery-rekenmachines een zeer specifiek, veilig gedrag hebben. Ze noemen dit de "1-Bit Barrière".

De Analogie:
Stel je voor dat je een getal moet raden tussen 1 en 1.000.000.

Als een machine slecht is, kan het je gok terugbrengen tot slechts 100 getallen. Dat is een enorme lek.
Als een machine perfect is, geeft het je geen enkel hint; je moet nog steeds het hele miljoen raden.
De 1-Bit Barrière betekent dat de machine je gok terugbrengt tot maximaal 2 getallen.

In de taal van het artikel heet dit PF-PINI(2). Dit betekent dat voor elke output die de machine produceert, er slechts twee mogelijke combinaties zijn van het geheim en het willekeurige masker die dit hadden kunnen veroorzaken. Het is alsof de machine zegt: "Ik heb dit resultaat gemaakt, en het kon alleen maar komen van Geheim A of Geheim B." Aangezien er miljoenen mogelijkheden zijn, is het terugbrengen tot slechts twee ongelooflijk veilig.

Wat dit artikel toevoegt:

Montgomery is Veilig: Ze bewezen dat de Montgomery-rekenmachine (gebruikt in veel nieuwe standaarden) dezezelfde "1-Bit Barrière" heeft, net als de Barrett-machine.
De Kettingreactie: Ze bewezen dat als je deze rekenmachines in een lange lijn koppelt (een pijplijn), de beveiliging niet slechter wordt alleen omdat de lijn langer is.

De Oplossing: Het "Vers Masker" Verversingsstation

Het artikel introduceert een cruciale regel voor het bouwen van deze assemblagelijnen: Je moet een "Vers Masker" invoegen tussen elke machine.

De Analogie:
Stel je een estafettewedstrijd voor waar hardlopers een stok doorgeven.

Slechte Wedstrijd: Als Hardloper A de stok doorgeeft aan Hardloper B, en Hardloper B geeft hem door aan Hardloper C, wordt de stok vuil en versleten. Een spion die de hele wedstrijd bekijkt, kan aanwijzingen van alle drie de hardlopers samenvoegen om de finish te raden.
De Oplossing (Vers Masker): Tussen Hardloper A en Hardloper B stop je de wedstrijd. Je pakt de stok, wikkelt hem in een gloednieuwe, schone deken (het verse masker) en geeft hem aan Hardloper B. Dan, tussen B en C, wikkel je hem in een andere gloednieuwe deken.

Omdat de deken elke keer nieuw en willekeurig is, heeft de spion die naar Hardloper B luistert geen idee wat Hardloper A deed. Het "lawaai" van het eerste deel van de wedstrijd is volledig gewist.

Het artikel bewijst wiskundig dat zolang je deze "Vers Masker" verversingsstations gebruikt, de beveiliging van de hele lijn alleen afhangt van de allerlaatste machine. De beveiliging van de eerste 99 machines maakt minder uit, omdat de verse maskers hun lekken wegspoelen.

Het Hoofdresultaat: De "End-to-End" Garantie

De auteurs gebruikten een krachtige computerbewijsassistent (genaamd Lean 4) om hun wiskunde te controleren. Ze schreven het niet alleen op; ze lieten de computer elke stap verifiëren, zodat er geen logische gaten waren.

Hun Conclusie:
Als je een pijplijn bouwt van deze rekenmachines (Barrett of Montgomery) en je plaatst een "Vers Masker" tussen elke stap:

Is de uiteindelijke output veilig.
Is de hoeveelheid informatie die een spion kan stelen beperkt tot die "1-Bit Barrière" (het terugbrengen van de gok tot 2 mogelijkheden van de miljoenen).
Geldt deze veiligheid ongeacht of je pijplijn 2 stappen of 100 stappen heeft. De lengte van de pijplijn maakt het niet zwakker.

De "Adams Bridge" Casestudy

Het artikel noemt een real-world hardware-project genaamd Adams Bridge.

Het Probleem: Eerdere onderzoekers ontdekten dat de Adams Bridge-hardware stappen had waarbij ze het "Vers Masker" waren vergeten te gebruiken of een machine gebruikten die niet perfect veilig was.
Het Oordeel van het Artikel: De auteurs zeiden niet "Adams Bridge is kapot". In plaats daarvan zeiden ze: "Adams Bridge slaagt niet voor de specifieke test die we zojuist bewezen hebben."
De Oplossing: Ze toonden aan dat als Adams Bridge de ontbrekende "Vers Masker"-stations toevoegt en ervoor zorgt dat elke machine een van de veilige types is, het de test zal halen.

Samenvatting in Eén Zin

Dit artikel bewijst dat als je veilige wiskundige rekenmachines aan elkaar koppelt en tussen elke enkele een "vers willekeurig schild" plaatst, het hele systeem veilig blijft tegen spionnen, ongeacht hoe lang de keten wordt, en dit geldt voor beide belangrijke typen rekenmachines die worden gebruikt in toekomstige quantum-proof beveiliging.

Technische Samenvatting: De 1-Bit Barrière is Universeel

Probleemstelling
De Number Theoretic Transform (NTT) fungeert als de computationele ruggengraat voor de NIST-postkwantumcryptografie (PQC)-standaarden ML-DSA (FIPS 204) en ML-KEM (FIPS 203). Hardware-implementaties van deze standaarden vertrouwen op arithmetische masking om weerstand te bieden tegen zijkanalaanvallen, specifiek Differential Power Analysis (DPA). Waar Boolean masking over $GF(2^n)$ gevestigde composability-frameworks heeft (bijv. PINI), stelt arithmetische masking over $\mathbb{Z}_q$ voor priemgetal $q$ unieke uitdagingen.

Vorig werk in het QANARY-programma (Papers 1–6) vestigde structurele afhankelijkheidsanalyses en kwantificeerde veiligheidsmarges voor specifieke componenten, waarbij met name werd bewezen dat Barrett-reductie voldoet aan een "1-Bit Barrière" (PF-PINI(2)). Echter, twee kritieke gaten bleven bestaan:

Willekeurige Pipeline-diepte: Vorige compositiestellingen waren beperkt tot twee stadia. Er was geen formele garantie voor willekeurige $k$ -stadia-pipelines met verse inter-stadia masking.
Montgomery-reductie: Waar Barrett-reductie was gekarakteriseerd, ontbrak er een formele PF-PINI-karakterisering voor Montgomery-reductie – de tweede standaardmodulaire reductie die wordt gebruikt in NTT-hardware (dominant in ML-DSA en sommige ML-KEM-implementaties).
Gecentraliseerde End-to-End-grenzen: Er bestond geen enkele, machine-gecontroleerde kardinaliteitsgrens die de resultaten voor willekeurige pipelines samenvoegde, bestaande uit butterflies, Barrett- en Montgomery-reducties.

Methodologie
Het artikel maakt gebruik van formele verificatie met de Lean 4 bewijsassistent. De aanpak is strikt constructief, met nul sorry (onbewezen aannames) en nul niet-standaard axioma's. De methodologie vertrouwt op:

PF-PINI-definitie: Gebruik van de Prime-Field Probe Isolating Non-Interference (PF-PINI)-parameter, die de lekage van een single-wire gadget onder een enkele arithmetische masker kwantificeert. Een gadget is PF-PINI( $M$ ) als de kardinaliteit van het prebeeld van elke uitvoerwaarde ten hoogste $M$ is.
Pipeline-modellering: Definieren van een $k$ -stadia-pipeline waarbij elke fase $G_i$ een PF-PINI-gadget is, gescheiden door verse willekeurige maskers. De pipeline-uitvoer wordt recursief berekend.
Combinatorische analyse: Bewijzen dat verse inter-stadia masking de lekageparameters van tussenliggende stadia "wist", waardoor de uiteindelijke grens alleen afhankelijk is van de parameter van het laatste stadium.
Hardware-trouwe modellering: Modelleren van Montgomery-reductie om rekening te houden met hardware-registerbreedtes en wraparound-gedrag, met name het analyseren van de botsingsoffset $2^{w-s}$ .

Belangrijkste Bijdragen
Het artikel levert vier primaire bijdragen, allemaal geformaliseerd in Lean 4:

De $k$ -Stadia Compositiestelling (Stelling 3.1):
Deze stelling generaliseert het eerdere 2-stadia compositieresultaat naar willekeurige diepte $k \ge 1$ . Het bewijst dat voor een pipeline van gadgets $G_0, \dots, G_{k-1}$ met verse inter-stadia masking, de kardinaliteit van het prebeeld van de uitvoer wordt begrensd door:
$| \{ (m, f) : \text{pipeline uitvoer} = v \} | \le G_{k-1}.\text{maxMult} \cdot q^{2k-2}$
Cruciaal is dat de grens door het laatste stadium bepaald wordt; de parameters van alle tussenliggende stadia worden gewist door de verse maskers.
Montgomery-reductie is PF-PINI(2) (Stelling 4.3):
Het artikel bewijst formeel dat Montgomery-reductie voldoet aan de PF-PINI(2)-eigenschap, waarbij de structuur van Barrett-reductie wordt gespiegeld. Het toont aan dat de hardware-trouwe Montgomery-afbeelding een "twee-takken"-structuur heeft (afhankelijk van of een wraparound optreedt), wat resulteert in een prebeeldkardinaliteit van ten hoogste 2. Stelling 4.7 vestigt verder de strakheid van deze grens, waarbij wordt aangetoond dat voor standaardparameters (ML-KEM en ML-DSA) de multipliciteit exact 2 is.
End-to-End Multipliciteitsgrens (Stelling 5.1):
Door de $k$ -stadia compositiestelling te combineren met de specifieke PF-PINI(2)-resultaten voor Barrett (Paper 5), Montgomery (dit artikel) en butterflies (Paper 4), vestigt het artikel een gecentraliseerde grens. Voor elke $k$ -stadia-pipeline waarbij elke fase voldoet aan $\text{maxMult} \le 2$ , wordt de uitvoerprebeeldkardinaliteit begrensd door:
$2 \cdot q^{2k-2}$
Onder het eerste-orde proberingsmodel met uniforme maskers komt dit overeen met een per-observatie conditionele waarschijnlijkheidsgrens van $2/q$ , onafhankelijk van de pipeline-diepte $k$ .
Formele Verankering van Empirische Bevindingen (Stelling 5.4):
Het artikel biedt een Lean-geverifieerde voorwaarde die stelt dat als elke fase in een pipeline $\text{maxMult} \ge 3$ heeft (bijv. een niet-gemaskerde fase), de hypothese van de end-to-end grens faalt. Dit verankert formeel eerdere empirische en structurele analyses van de "Adams Bridge" PQC-versneller (Papers 1, 2 en externe werken), en bevestigt dat specifieke niet-gemaskerde configuraties in dat ontwerp buiten de voldoende voorwaarden voor de diepte-onafhankelijke grens vallen.

Resultaten

Universaliteit van de 1-Bit Barrière: Het artikel bevestigt dat de "1-Bit Barrière" (een prebeeldkardinaliteit van 2) van toepassing is op zowel standaardmodulaire reducties (Barrett en Montgomery) die worden gebruikt in NIST PQC-hardware.
Diepte-onafhankelijkheid: De formele bewijzen tonen aan dat het toevoegen van stadia aan een pipeline de per-observatie lekagegrens niet verslechtert, mits verse inter-stadia masking wordt gebruikt en elke fase voldoet aan PF-PINI( $\le 2$ ).
Verificatiestatus: Het volledige artefact bestaat uit 20 declaraties over drie theorema-modules, gebouwd in 1.753 taken met nul fouten, nul sorry en geen native besluitprocedures.

Betekenis en Claims
Het artikel positioneert zichzelf als de voltooiing van een formeel verificatieprogramma voor gemaskerde NTT-hardware. De betekenis ligt in het bieden van een kwantitatieve, machine-gecontroleerde compositiebasis voor hardwareontwerpers.

Voor Certificering: De afgeleide kardinaliteitsgrens ( $2 \cdot q^{2k-2}$ ) biedt het specifieke bewijs dat vereist is voor DPA-weerstandargumenten op architectuurniveau, wat de gate-level tools zoals SILVER en maskVerif aanvult.
Voor Ontwerpers: Het biedt een voorschrijvend remediërend pad: om een diepte-onafhankelijke grens te bereiken, moeten ontwerpers ervoor zorgen dat elke fase PF-PINI( $\le 2$ ) is en verse maskers tussen stadia invoegen.
Bescheidenheid van Claims: De auteurs stellen expliciet dat de waarschijnlijkheids- en min-entropie-interpretaties (bijv. $2/q$ ) informele semantische gevolgen zijn van de kardinaliteitsgrenzen en niet mechanisch zijn geformaliseerd in Lean. Wat betreft de Adams Bridge-analyse claimt het artikel slechts dat specifieke configuraties de voldoende voorwaarden van Stelling 5.1 niet halen; het claimt niet dat de hardware "gebroken" of "onveilig" is, en erkent dat alternatieve frameworks of sterkere modellen tot andere conclusies kunnen leiden. Het werk wordt gepresenteerd als een hulpmiddel voor compositieanalyse in plaats van een definitief veiligheidsverdict over specifieke implementaties.