Magnetar, Microsoft porta le proof a conoscenza zero nei programmi C Go e Rust

Microsoft Research presenta Magnetar: genera prove a conoscenza zero per programmi scritti in C, Go e Rust, e consente di verificarle in millisecondi senza rieseguire il calcolo né accedere ai dati usati nell’esecuzione¹.

Gli autori indicano tre freni storici all’adozione: prove lente da produrre, difficili da applicare a programmi comuni senza competenze crittografiche, e basi matematiche da ritenersi affidabili nel lungo periodo. Magnetar affronta tutte e tre le aree, con un’attenzione pratica ai flussi di sviluppo reali¹.

Prestazioni: Magnetar dichiara una velocità da 10 a 39 volte superiore rispetto ai sistemi comparabili più rapidi, ma il guadagno riguarda la sola generazione delle prove. La verifica resta rapida. La fonte non indica tempi assoluti in millisecondi né gli scenari di benchmark che producono l’intervallo 10-39×¹.

Integrazione: il sistema opera direttamente su programmi C, Go e Rust. Non richiede che lo sviluppatore riscriva la logica in DSL dedicate o adatti il codice a modelli sintetici. L’obiettivo è estendere i casi d’uso a software “normale”, scritto nei linguaggi più diffusi in ambito di sistema e rete¹.

Sicurezza: l’architettura si appoggia esclusivamente su funzioni hash standard. Evita assunzioni crittografiche non consolidate e punta a fondamenta che possano restare affidabili per decenni. Questo aspetto mira a ridurre il rischio di dover migrare l’infrastruttura di prova quando cambiano le stime sulla robustezza di schemi meno collaudati¹.

Il modello dichiarato è “proof-based general-purpose computing”. Ogni esecuzione produce un’uscita e una prova dell’esecuzione corretta del programma. Il verificatore controlla la prova in millisecondi, senza ripetere il calcolo e senza conoscere o ricevere i dati originali. La fiducia si sposta dall’esecutore alla validità crittografica della prova¹.

Gli autori presentano Magnetar come l’ultimo risultato di oltre dieci anni di ricerca sulle prove a conoscenza zero. L’obiettivo è rendere praticabile la separazione tra chi esegue e chi verifica, con controlli che restano validi anche quando il calcolo avviene in ambienti eterogenei o non fidati¹.

La promessa è operativa: portare le proof dove girano C, Go e Rust, accelerare la produzione delle prove rispetto alle migliori alternative note, e costruire su primitive standard. Se la traiettoria indicata regge a valutazioni indipendenti, la “nuova forma di computing” descritta dagli autori, in cui la verifica resta indipendente dall’ambiente di esecuzione, sposta il baricentro dal runtime al controllo crittografico. È qui che si giocherà l’adozione, tra prestazioni nella produzione delle prove e frizione minima per gli sviluppatori che lavorano nei linguaggi supportati¹.