💻 computer science

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

Questo articolo identifica e corregge due deviazioni critiche nell'implementazione dell'algoritmo GCD esteso in Go che compromettono la generazione di chiavi RSA, provando successivamente la correttezza e la terminazione del codice corretto utilizzando gli strumenti di verifica Gobra e Lean, dimostrando al contempo come gli agenti IA possano assistere nel raffinamento delle prove formali.

Autori originali: Linard Arquint

Pubblicato 2026-06-05

📖 4 min di lettura☕ Lettura da pausa caffè

CC BY 4.0

Autori originali: Linard Arquint

Articolo originale sotto licenza CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Questa è una spiegazione generata dall'IA dell'articolo qui sotto. Non è stata scritta né approvata dagli autori. Per precisione tecnica, consulta l'articolo originale. Leggi il disclaimer completo

Immagina di stare costruendo una cassaforte digitale ad alta sicurezza (come quelle usate per l'online banking o la messaggistica sicura). Per chiudere e sbloccare questa cassaforte, hai bisogno di una chiave matematica molto specifica e complessa. Nel mondo dell'informatica, questa chiave viene generata utilizzando una ricetta chiamata Massimo Comun Divisore Esteso (GCD).

Questo articolo parla di un team di ricercatori che è entrato nella "cucina" del linguaggio di programmazione Go (uno strumento popolare usato per costruire software) per controllare se la ricetta per questa chiave fosse stata seguita correttamente. Hanno scoperto che la ricetta era stata leggermente alterata, e l'hanno corretta dimostrando matematicamente che la nuova versione funziona perfettamente.

Ecco la storia della loro scoperta, suddivisa in parti semplici:

1. L'errore del "Copia e Incolla"

Gli sviluppatori di Go volevano aggiornare il loro software per soddisfare rigorosi standard di sicurezza governativi. Per farlo, hanno preso una ricetta da una fonte affidabile e ben nota chiamata BoringSSL (una libreria sicura usata da Google) e l'hanno "portata" (tradotta) in Go.

Immagina che sia come se un famoso chef ti desse la ricetta segreta per una torta. Decidi di riscrivere la ricetta con la tua calligrafia per renderla più facile da leggere. L'articolo afferma che, mentre riscriveva la ricetta, gli sviluppatori di Go hanno accidentalmente cambiato due passaggi importanti.

Il Problema: La ricetta originale aveva una regola rigorosa: "Se aggiungi questi due numeri e il risultato è troppo grande, devi sottrarre una quantità specifica da entrambi i numeri nello stesso momento". Questo impedisce alla torta di crollare.
Il Bug: La versione Go ha eseguito questo controllo "troppo grande" separatamente per ogni numero. Era come controllare la farina e lo zucchero in modo indipendente. Questo ha rotto l'equilibrio matematico (gli "invarianti") che garantisce che la chiave sia corretta.
La Sorpresa: Tre diversi esperti umani hanno revisionato il codice ma non hanno notato questo errore. Era così sottile che è sfuggito alla rete.

2. L'ingrediente "Troppo Grande"

Il secondo problema riguardava la dimensione degli ingredienti consentiti.

La Regola: La ricetta originale diceva: "Il primo ingrediente deve essere sempre più piccolo del secondo".
Il Cambiamento: La versione Go permetteva al primo ingrediente di essere più grande del secondo.
La Soluzione: I ricercatori non hanno dovuto cambiare il codice per questo punto. Inveve, hanno dovuto aggiornare la "dimostrazione" (la garanzia matematica) per mostrare che la ricetta funziona anche con ingredienti più grandi.

3. Il Detective Magico (Gobra)

Per dimostrare di aver corretto i bug, i ricercatori hanno usato uno strumento chiamato Gobra.

L'Analogia: Immagina un ispettore robotico super rigoroso e iper-attento. Gli dai il codice e una lista di regole (specifiche). Il robot non si limita a eseguire il codice; simula ogni possibile modo in cui il codice potrebbe girare, controllando ogni singolo percorso per garantire che non violi mai le regole.
Il Risultato: Il robot ha confermato che, una volta risolto il "bug di sincronizzazione", il codice è corretto al 100%. In effetti, poiché la correzione ha rimosso passaggi non necessari, il nuovo codice è stato in realtà il 24% più veloce della versione con il bug.

4. L'Assistente AI

I ricercatori non hanno fatto tutto il lavoro pesante da soli. Hanno usato un agente AI (un programma per computer intelligente) per aiutarli.

Come funzionava: L'AI agiva come un apprendista instancabile. Quando il robot ispettore (Gobra) diceva: "Questa parte non ha senso", l'AI suggeriva modifiche alle regole o al codice.
L'Ostacolo: L'AI inizialmente assumeva che il codice fosse perfetto e cercava di forzare la matematica per adattarsi ad esso. I ricercatori umani hanno dovuto dirle: "No, il codice è effettivamente sbagliato; cerca la differenza". Una volta che l'AI ha capito questo, è diventata incredibilmente utile, suggerendo correzioni e aiutando a scrivere le dimostrazioni matematiche.

5. La Conclusione

L'articolo si conclude con tre lezioni principali:

Anche gli esperti commettono errori sottili: Tre revisori umani hanno mancato un bug critico che uno strumento di prova formale ha invece trovato.
La verifica formale è potente: Usare uno strumento come Gobra è come avere una garanzia matematica che il tuo codice funzioni, invece di sperare che funzioni solo perché ha superato alcuni test.
L'AI è un ottimo partner: L'AI può aiutare gli umani a scrivere queste complesse dimostrazioni, ma gli umani devono comunque guidare l'AI affinché metta in discussione il codice invece di accettarlo passivamente.

In breve: I ricercatori hanno trovato un difetto nascosto in un algoritmo di sicurezza critico nella libreria standard di Go, lo hanno corretto, hanno dimostrato matematicamente che la correzione funziona e hanno mostrato che la correzione ha reso il software più veloce. Hanno fatto tutto questo combinando l'intuizione umana, strumenti di prova automatizzati e l'assistenza dell'IA.

Riassunto Tecnico: GCD: Garbled, Corrected, Demonstrandum

Definizione del Problema

Il documento affronta la correttezza e la verifica dell'implementazione dell'Algoritmo di Euclide Esteso (Extended GCD) all'interno della libreria standard di Go (crypto/internal/fips140/bigmod). Questa implementazione è critica per la generazione delle coppie di chiavi RSA, un componente fondamentale per TLS, SSH e PGP. L'implementazione in Go è stata introdotta in Go 1.24 per supportare nativamente la conformità FIPS 140-3, sostituendo la dipendenza da BoringSSL.

Gli autori hanno identificato una discrepanza critica: sebbene il codice Go fosse presentato come una diretta trasposizione dell'implementazione di BoringSSL (che è formalmente verificata tramite l'assistente alla dimostrazione Rocq via Fiat Cryptography), la versione Go conteneva sottili deviazioni. Queste deviazioni non erano state colte da tre separate revisioni del codice. Le deviazioni interrompevano gli invarianti matematici dell'algoritmo, compromettendo potenzialmente la correttezza del calcolo dell'inverso modulare richiesto per le chiavi private RSA. Inoltre, l'implementazione Go consentiva un dominio di input più ampio rispetto alla versione verificata di BoringSSL, invalidando le assunzioni della prova esistente.

Metodologia

Gli autori hanno impiegato un approccio di verifica deduttiva dei programmi utilizzando Gobra, un verificatore basato sulla logica di separazione per Go. La metodologia ha previsto:

Specificazione Formale: Gli autori hanno formalizzato le specifiche in linguaggio naturale delle funzioni Go (extendedGCD, InverseVarTime, GCDVarTime) in specifiche Gobra, includendo precondizioni, postcondizioni e invarianti di ciclo.
Analisi delle Deviazioni: Tentando di verificare l'esistente codice Go rispetto alle specifiche derivate dalla prova di BoringSSL, gli autori hanno identificato due classi principali di deviazioni:
- Sottrazioni Non Sincronizzate: L'implementazione Go aggiornava i coefficienti di Bézout ( $A, B, C, D$ ) indipendentemente in base a condizioni locali, mentre l'implementazione di riferimento richiedeva riduzioni sincronizzate per mantenere gli invarianti di ciclo.
- Espansione del Dominio di Input: L'implementazione Go permetteva input in cui $a \ge n$ , violando la precondizione $a < n$ richiesta dalla prova originale.
Costruzione della Prova:
- Correzione del Codice: Gli autori hanno proposto una correzione per le sottrazioni non sincronizzate per allineare la logica Go con gli invarianti matematici.
- Adattamento della Prova: Hanno trasposto la prova esistente di BoringSSL da Rocq a Gobra. Per la deviazione del dominio di input, hanno rilassato gli invarianti e le postcondizioni per coprire il caso in cui $a \ge n$ , dimostrando che il valore GCD rimane corretto anche se la proprietà dell'inverso modulare non è valida in quel caso specifico.
- Verifica Ibrida: Per i lemmata di aritmetica non lineare che il solver SMT Z3 (utilizzato da Gobra) non era in grado di gestire, gli autori hanno utilizzato l'assistente alla dimostrazione Lean per dimostrare lezioni chiave e le hanno importate in Gobra come lemmata trusted.
Verifica Assistita da AI: Gli autori hanno utilizzato un agente AI (Claude Code di Anthropic) per raffinare iterativamente invarianti e lemmata basandosi sui messaggi di errore di Gobra, riducendo significativamente lo sforzo manuale nella costruzione della prova.

Contributi Chiave

Scoperta di Bug: Il documento svela due deviazioni sottili ma critiche nell'implementazione dell'Extended GCD in Go che rompono gli invarianti algoritmici. Questi bug erano presenti in un codice che aveva subito molteplici revisioni ed era stato presentato come una diretta trasposizione di un'implementazione verificata.
Ottimizzazione delle Prestazioni: La correzione proposta per la deviazione delle sottrazioni non sincronizzate non solo ripristina la correttezza, ma produce anche un incremento di velocità del 24% (media geometrica) eliminando allocazioni di memoria non necessarie e operazioni ridondanti nel corpo del ciclo.
Verifica Formale della Crypto in Go: Gli autori hanno verificato con successo la versione corretta dell'implementazione Go, la sua terminazione e la sua correttezza rispetto alle specifiche formali utilizzando Gobra. Questa è la prima verifica formale di questo specifico componente nella libreria standard di Go.
Porting e Generalizzazione della Prova: Hanno trasposto con successo una prova da Rocq (Fiat Cryptography) a Gobra e l'hanno generalizzata per coprire il più ampio dominio di input permesso dall'implementazione Go.
AI nella Verifica: Il lavoro dimostra l'efficacia degli agenti AI nel facilitare la verifica formale attraverso l'iterazione autonoma su specifiche e l'identificazione delle cause radice dei fallimenti della prova (ad esempio, suggerendo che la riduzione indipendente dei coefficienti fosse il problema).

Risultati

Correttezza: L'implementazione corretta è stata verificata con successo in 16,9 secondi su un laptop standard. La verifica copre la funzione extendedGCD e i suoi client InverseVarTime e GCDVarTime.
Prestazioni: I benchmark su varie dimensioni di limb (da 64 a 8192 bit) hanno mostrato che l'implementazione verificata è costantemente più veloce dell'originale. L'incremento di velocità medio è stato del 23,98%, con miglioramenti compresi tra il 15,6% e il 36% a seconda della dimensione dell'input. Il miglioramento è attribuito agli aggiornamenti in place e all'eliminazione delle allocazioni di buffer intermedi.
Divulgazione e Impatto: Gli autori hanno divulgato le deviazioni ai manutentori della crittografia di Go. I manutentori hanno confermato che, sebbene le deviazioni possano teoricamente portare a inversi modulari errati, i controlli difensivi nel codice di generazione delle chiavi RSA intercetterebbero questi errori restituendo un errore invece di una chiave errata, limitando l'impatto alla disponibilità piuttosto che a un compromesso della sicurezza. Le correzioni sono in fase di revisione per l'inclusione nella libreria standard di Go.
Integrazione Continua: Grazie al rapido tempo di verifica, la prova è stata integrata nel workflow di Integrazione Continua (CI) del progetto per controllare automaticamente eventuali future deviazioni.

Significato e Rivendicazioni

Il documento afferma che il lavoro evidenzia tre intuizioni primarie:

Bug Sottili in Codice Revisionato: Anche il codice ben revisionato, specialmente quando viene presentato come una diretta trasposizione di un'implementazione verificata, può contenere bug sottili che rompono gli invarianti.
Potenza della Verifica Formale: La verifica formale è uno strumento potente per scoprire questo tipo di bug che il testing e la revisione manuale potrebbero mancare.
Ruolo degli Agenti AI: Gli agenti AI possono facilitare efficacementamente la verifica raffinando iterativamente invarianti e lemmata basandosi sul feedback del verificatore, sebbene la supervisione umana rimanga necessaria per la pulizia finale e la comprensione strutturale.

Gli autori sottolineano che il loro lavoro colma il divario tra l'implementazione e la sua prova. Verificando direttamente il codice Go anziché affidarsi all'esistenza di una prova per un'implementazione diversa (BoringSSL), assicurano che il codice specifico in esecuzione in produzione sia matematicamente solido. Notano inoltre che, sebbene facciano affidamento su funzioni trusted per le operazioni di basso livello sui bit, l'argomento complessivo di correttezza è suddiviso in componenti piccole e revisionabili, aumentando la fiducia nell'affidabilità del sistema.