Microsoft sta utilizzando agenti AI per provare matematicamente che il suo codice di crittografia non ha difetti

Punti chiave

• La libreria SymCrypt di Microsoft, il motore di crittografia utilizzato in Windows e Azure, è sottoposta a verifica formale utilizzando una toolchain che combina Rust, Lean e Aeneas a partire dalla metà del 2024.
• I primi algoritmi verificati rilasciati sono SHA-3, uno standard per creare impronte digitali di dati, e ML-KEM, uno schema di crittografia post-quantistica progettato per resistere agli attacchi dei futuri computer quantistici.
• Gli agenti AI, software in grado di svolgere compiti multi-step in autonomia, scrivono i passaggi delle prove matematiche che gli ingegneri umani poi revisionano e verificano indipendentemente.
• Microsoft ha reso open-source il codice verificato, le specifiche e le prove in un ramo pubblico di SymCrypt, rendendo il lavoro disponibile per la revisione esterna.
• Gli algoritmi futuri previsti per lo stesso trattamento includono AES-GCM, FrodoKEM e ML-DSA, tutti i quali proteggono dati in Windows e Linux oggi.

Il codice crittografico, il software che scramble e protegge i dati in ogni app, browser e sistema operativo, è notoriamente implacabile. Un singolo controllo di bounds mancante, cioè un fallimento nel confermare che un numero rimane entro un intervallo sicuro, può far crollare la sicurezza che sembra solida in superficie. I test catturano molti bug. Non catturano tutti.

Microsoft Research sta lavorando a un approccio diverso: provare che il codice è corretto, matematicamente, prima che venga rilasciato.

Il progetto si concentra su SymCrypt, la libreria crittografica open-source di Microsoft che gira dentro Windows e Azure Linux. Gli ingegneri stanno ora scrivendo nuovi algoritmi crittografici in Rust, un linguaggio di programmazione che esclude intere famiglie di errori di sicurezza della memoria per design. Eseguono quindi questi programmi Rust attraverso uno strumento chiamato Aeneas, che traduce il codice in una forma che un assistente di prove chiamato Lean può analizzare.

Lean non è un chatbot. È un framework di prove formali, software che verifica gli argomenti matematici come una calcolatrice verifica l'aritmetica, solo che verifica le prove, e non commette mai errori aritmetici.

L'obiettivo è produrre un teorema: per ogni input valido, questa implementazione restituisce esattamente il risultato che lo standard pubblicato dice debba restituire. Non solitamente. Sempre.

Il primo rilascio pubblico copre SHA-3, un algoritmo standard per creare un'impronta digitale unica di qualsiasi pezzo di dati, e ML-KEM, uno schema di scambio di chiavi post-quantistico. La crittografia post-quantistica significa algoritmi costruiti per rimanere sicuri anche contro i computer quantistici, macchine che potrebbero rompere molti dei moderni metodi di crittografia.

Come si inserisce l'AI in una prova matematica?

Scrivere prove formali è lento. È qui che entrano in gioco gli agenti AI.

Gli agenti gestiscono i passaggi intermedi ripetitivi, bozze di frammenti di prova che collegano i risultati intermedi. Gli ingegneri umani si concentrano sulle parti che richiedono vero giudizio: verificare che la specifica formale corrisponda effettivamente a ciò che lo standard pubblicato dice, e revisionare le proprietà di alto livello che il codice deve soddisfare. La verifica della prova stessa è completamente automatizzata e deterministica, il che significa che la macchina accetta o rifiuta la prova. Non c'è spazio per l'agente per bluffare.

Microsoft descrive questo come una divisione netta: gli agenti scrivono, gli umani revisionano, il verificatore di prove decide.

Per le persone che usano Windows, Azure, o qualsiasi servizio che si affida allo stack di sicurezza di Microsoft, il significato pratico è diretto. La crittografia che protegge i tuoi file, i tuoi dati nel cloud e i tuoi accessi è sottoposta a uno standard più elevato di quanto il solo testing possa fornire. Se le prove passano, il codice fa esattamente quello che lo standard richiede.

Il ramo open-source permette ai ricercatori esterni di ispezionare sia il codice Rust che le prove fianco a fianco, così le affermazioni non sono solo la parola di Microsoft.

Da tenere d'occhio: annunci di build formalmente verificate che raggiungono i rilasci stabili di Windows, e se altre librerie di crittografia adottano flussi di lavoro simili di prove assistite da AI. Questo segnerebbe un vero cambiamento nel modo in cui l'industria pensa alla correttezza del software.