💻 computer science

GCD: Garbled, Corrected, Demonstrandum -- Fixing and Proving Go's Extended GCD Implementation

Dit artikel identificeert en herstelt twee kritieke afwijkingen in de uitgebreide GCD-implementatie van Go die de RSA-sleutelgeneratie compromitteren, en bewijst vervolgens de correctheid en terminatie van de gecorrigeerde code met behulp van de verificatietools Gobra en Lean, terwijl het demonstreert hoe AI-agenten kunnen assisteren bij het verfijnen van formele bewijzen.

Oorspronkelijke auteurs: Linard Arquint

Gepubliceerd 2026-06-05

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Linard Arquint

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

Stel je voor dat je een hoogbeveiligde digitale kluis bouwt (zoals die gebruikt worden voor online bankieren of beveiligde messaging). Om deze kluis te vergrendelen en te ontgrendelen, heb je een zeer specifieke, complexe wiskundige sleutel nodig. In de wereld van de informatica wordt deze sleutel gegenereerd met behulp van een recept genaamd het Extended Greatest Common Divisor (GCD) algoritme.

Dit artikel gaat over een team van onderzoekers die de "keuken" van de programmeertaal Go (een populaire tool voor het bouwen van software) zijn binnengegaan om te controleren of het recept voor deze sleutel correct werd gevolgd. Ze ontdekten dat het recept lichtelijk was gewijzigd, en ze hebben het gecorrigeerd terwijl ze wiskundig bewezen dat de nieuwe versie perfect werkt.

Hier is het verhaal van hun ontdekking, opgedeeld in eenvoudige delen:

1. De "Kopieer-en-Plak" fout

De Go-ontwikkelaars wilden hun software updaten om te voldoen aan strikte overheidsnormen voor veiligheid. Hiervoor namen ze een recept over van een vertrouwde, bekende bron genaamd BoringSSL (een beveiligde bibliotheek gebruikt door Google) en "porteerden" (vertaalden) dit naar Go.

Stel je voor dat een beroemde chef een geheim recept voor een taart aan je geeft. Je besluit het recept in je eigen handschrift te herschrijven om het makkelijker leesbaar te maken. Het artikel beweert dat de Go-ontwikkelaars tijdens het herschrijven per ongeluk twee belangrijke stappen hebben gewijzigd.

Het Probleem: Het originele recept had een strikte regel: "Als je deze twee getallen bij elkaar optelt en het resultaat is te groot, moet je een specifelijk bedrag van beide getallen tegelijkertijd aftrekken." Dit voorkomt dat de taart instort.
De Bug: De Go-versie voerde deze "te groot"-controle apart uit voor elk getal. Het was alsof je de bloem en de suiker onafhankelijk van elkaar controleerde. Dit verbrak de wiskundige balans (de "invarianten") die garandeert dat de sleutel correct is.
De Verrassing: Drie verschillende menselijke experts beoordeelden de code, maar misten deze fout. Het was zo subtiel dat het door het net glipte.

2. Het "Te Groot" ingrediënt

Het tweede probleem ging over de grootte van de toegestane ingrediënten.

De Regel: Het originele recept zei: "Het eerste ingrediënt moet altijd kleiner zijn dan het tweede."
De Verandering: De Go-versie stond toe dat het eerste ingrediënt groter was dan het tweede.
De Fix: De onderzoekers hoefden de code hiervoor niet te veranderen. In plaats daarvan moesten ze het "bewijs" (de wiskundige garantie) bijwerken om aan te tonen dat het recept ook met de grotere ingrediënten nog steeds werkt.

3. De Magische Detective (Gobra)

Om te bewijzen dat ze de bugs hadden opgelost, gebruikten de onderzoekers een tool genaamd Gobra.

De Analogie: Stel je een superstrikte, hyper-aandachtige robotinspecteur voor. Je voert de code en een lijst met regels (specificaties) in. De robot voert de code niet alleen uit; hij simuleert elke mogelijke manier waarop de code zou kunnen draaien, waarbij hij elke pad controleert om er zeker van te zijn dat de regels nooit worden overtreden.
Het Resultaat: De robot bevestigde dat zodra de "synchronisatiebug" was opgelost, de code 100% correct was. Sterker nog, omdat de fix onnodige stappen verwijderde, draaide de nieuwe code zelfs 24% sneller dan de buggy versie.

4. De AI-assistent

De onderzoekers deden het zware werk niet alleen. Ze gebruikten een AI-agent (een slim computerprogramma) om te helpen.

Hoe het werkte: De AI fungeerde als een onvermoeibare leerling. Wanneer de robotinspecteur (Gobra) zei: "Dit deel is niet logisch", suggereerde de AI wijzigingen aan de regels of de code.
De Haken en Stellen: De AI ging er aanvankelijk vanuit dat de code perfect was en probeerde de wiskunde eromheen te dwingen. De menselijke onderzoekers moesten de AI vertellen: "Nee, de code is eigenlijk fout; zoek naar het verschil." Zodra de AI dit begreep, werd het ongelooflijk nuttig door fixes voor te stellen en te helpen bij het schrijven van de wiskundige bewijzen.

5. De Conclusie

Het paper concludeert met drie belangrijke lessen:

Zelfs experts maken subtiele fouten: Drie menselijke reviewers misten een cruciale bug die een formele bewijstool wel vond.
Formele verificatie is krachtig: Het gebruik van een tool als Gobra is als het hebben van een wiskundige garantie dat je code werkt, in plaats van er alleen maar vanuit te gaan dat het werkt omdat het een paar tests heeft doorstaan.
AI is een geweldige partner: AI kan mensen helpen bij het schrijven van deze complexe bewijzen, maar mensen moeten de AI nog steeds aansturen om de code in twijfel te trekken in plaats van deze blind te accepteren.

Kortom: De onderzoekers vonden een verborgen fout in een cruciaal beveiligingsalgoritme in de Go-standaardbibliotheek, herstelden deze, bewezen wiskundig dat de fix werkt, en toonden aan dat de fix de software zelfs sneller maakte. Dit deden ze met een combinatie van menselijk inzicht, geautomatiseerde bewijstools en AI-ondersteuning.

Technische Samenvatting: GCD: Garbled, Corrected, Demonstrandum

Probleemstelling

Het artikel behandelt de correctheid en verificatie van de implementatie van het Uitgebreide Euclidische Algoritme (Extended GCD) binnen de standaardbibliotheek van Go (crypto/internal/fips140/bigmod). Deze implementatie is cruciaal voor de RSA-sleutelpaargeneratie, een fundamenteel onderdeel voor TLS, SSH en PGP. De Go-implementatie werd geïntroduceerd in Go 1.24 om native FIPS 140-3 compliantie te ondersteunen, als vervanging voor de afhankelijkheid van BoringSSL.

De auteurs identificeerden een kritieke discrepantie: hoewel de Go-code werd beweerd een directe port te zijn van de BoringSSL-implementatie (die formeel is geverifieerd via de Rocq proof assistant via Fiat Cryptography), bevatte de Go-versie subtiele afwijkingen. Deze afwijkingen werden niet opgemerkt door drie afzonderlijke code-reviews. De afwijkingen braken de wiskundige invarianten van het algoritme, wat potentieel de correctheid van de berekening van de modulaire inverse die vereist is voor RSA-private sleutels in gevaar brengt. Bovits stond de Go-implementatie een groter invoerdomein toe dan de bewezen BoringSSL-versie, wat de bestaande bewijsveronderstellingen ongeldig maakte.

Methodologie

De auteurs hanteerden een deductieve programmaverificatie-aanpak met behulp van Gobra, een verifieerder voor Go gebaseerd op separation logic. De methodologie omvatte:

Formele Specificatie: De auteurs formaliseerden de natuurlijke taal-specificaties van de Go-functies (extendedGCD, InverseVarTime, GCDVarTime) naar Gobra-specificaties, inclusief precondities, postcondities en loop-invarianten.
Afwijkingsanalyse: Door te proberen de bestaande Go-code te verifiëren tegen de specificaties afgeleid van het BoringSSL-bewijs, identificeerden de auteurs twee belangrijke klassen van afwijkingen:
- Niet-gesynchroniseerde Subtracties: De Go-implementatie update de Bézout-coëfficiënten ( $A, B, C, D$ ) onafhankelijk op basis van lokale condities, terwijl de referentie-implementatie gesynchroniseerde reducties vereiste om de loop-invarianten te handhaven.
- Input Domein Expansie: De Go-implementatie stond inputs toe waarbij $a \ge n$ , wat de precondition $a < n$ overtrad die vereist was door het oorspronkelijke bewijs.
Bewijsconstructie:
- Code Fix: De auteurs stelden een fix voor de niet-gesynchroniseerde subtracties voor om de Go-logica af te stemmen op de wiskundige invarianten.
- Bewijs Adaptatie: Ze porteerden het bestaande BoringSSL-bewijs van Rocq naar Gobra. Voor de input domein expansie versoepelden ze de invarianten en postcondities om het geval te dekken waar $a \ge n$ , waarbij ze bewezen dat de GCD-waarde correct blijft, zelfs als de modulaire inverse-eigenschap in dat specifieke geval niet geldt.
- Hybride Verificatie: Voor niet-lineaire rekenkundige lemmata die de Z3 SMT-solver (gebruikt door Gobra) niet kon afhandelen, gebruikten de auteurs de Lean proof assistant om cruciale lemmata te bewijzen en importeerden deze in Gobra als trusted lemmata.
AI-ondersteunde Verificatie: De auteurs maakten gebruik van een AI-agent (Anthropic's Claude Code) om invarianten en lemmata iteratief te verfijnen op basis van de foutmeldingen van Gobra, wat de handmatige inspanning bij de bewijsconstructie aanzienlijk verminderde.

Belangrijkste Bijdragen

Bug Ontdekking: Het artikel legt twee subtiele maar kritieke afwijkingen bloot in de Go Extended GCD-implementatie die algoritmische invarianten breken. Deze bugs waren aanwezig in code die meerdere reviews had ondergaan en die werd beweerd een directe port te zijn van een geverifieerde implementatie.
Prestatie Optimalisatie: De voorgestelde fix voor de niet-gesynchroniseerde subtractie herstelt niet alleen de correctheid, maar resulteert ook in een gemiddelde versnelling van 24% (geometrisch gemiddelde) door onnodige geheugenallocaties en redundante operaties in de loop-body te elimineren.
Formele Verificatie van Go Crypto: De auteurs verifieerden succesvol de gefixte Go-implementatie, de terminatie ervan en de correctheid ervan tegen formele specificaties met behulp van Gobra. Dit is de eerste formele verificatie van dit specifieke component in de Go standaardbibliotheek.
Bewijs Porting en Generalisatie: Ze slaagden erin een bewijs van Rocq (Fiat Cryptography) naar Gobra te porteren en generaliseerden het om een breder input domein te dekken dat door de Go-implementatie wordt toegestaan.
AI in Verificatie: Het werk demonstreert de effectiviteit van AI-agents bij het faciliteren van formele verificatie door autonoom invarianten en lemmata te verfijnen en de grondoorzaken van bewijs-fouten te identificeren (bijv. suggereren dat onafhankelijke coëfficiënt-reductie het probleem was).

Resultaten

Correctheid: De gefixte implementatie werd succesvol geverifieerd in 16,9 seconden op een standaard laptop. De verificatie dekt de extendedGCD functie en de clients InverseVarTime en GCDVarTime.
Prestaties: Benchmarks over diverse limb-groottes (64 tot 8192 bits) toonden aan dat de geverifieerde implementatie consistent sneller is dan de originele. De gemiddelde versnelling was 23,98%, met verbeteringen variërend van 15,6% tot 36% afhankelijk van de inputgrootte. De versnelling wordt toegeschreven aan in-place updates en het elimineren van tussenliggende bufferallocaties.
Openbaarmaking en Impact: De auteurs hebben de afwijkingen gemeld aan de Go cryptografie maintainers. De maintainers bevestigden dat hoewel de afwijkingen theoretisch tot incorrecte modulaire inverses kunnen leiden, defensieve controles in de RSA-sleutelgeneratiecode deze fouten zouden opvangen en een foutmelding zouden teruggeven in plaats van een incorrecte sleutel, wat de impact beperkt tot beschikbaarheid in plaats van een beveiligingscompromis. De fixes zijn onder behandeling voor opname in de Go standaardbibliotheek.
Continuous Integration: Vanwege de snelle verificatietijd is het bewijs geïntegreerd in de Continuous Integration (CI) workflow van het project om toekomstige afwijkingen automatisch te controleren.

Betekenis en Claims

Het artikel claimt dat het werk drie primaire inzichten belicht:

Subtiele Bugs in Gereviewde Code: Zelfs goed gereviewde code, vooral wanneer deze wordt beweerd een directe port van een geverifieerde implementatie te zijn, kan subtiele bugs bevatten die invarianten breken.
Kracht van Formele Verificatie: Formele verificatie is een krachtig middel om dit type bugs te ontdekken die testen en handmatige reviews mogelijk missen.
Rol van AI-Agents: AI-agents kunnen het verificatieproces effectief faciliteren door invarianten en lemmata iteratief te verfijnen op basis van de feedback van de verifieerder, hoewel menselijk toezicht noodzakelijk blijft voor de uiteindelijke opschoning en structurele begrip.

De auteurs benadrukken dat hun werk de kloof tussen de implementatie en het bewijs dicht. Door de Go-code direct te verifiëren in plaats van te vertrouwen op het bestaan van een bewijs voor een andere implementatie (BoringSSL), garanderen ze dat de specifieke code die in productie draait, wiskundig solide is. Ze merken ook op dat hoewel ze vertrouwen op trusted functies voor lage-niveau bit-operaties, het algehele correctheidsargument is opgedeeld in kleine, controleerbare componenten, wat het vertrouwen in de betrouwbaarheid van het systeem vergroot.