Vitalik Buterin ha affermato che i progressi nell’intelligenza artificiale potrebbero ridefinire il modo in cui i sistemi crypto vengono attaccati e difesi, spingendo l’infrastruttura verso software verificato matematicamente.
Saggio di Buterin descrive la minaccia dell’IA
Il cofondatore di Ethereum ha sostenuto che modelli di IA sempre più potenti renderanno molto più semplice scoprire e sfruttare vulnerabilità in software complessi.
Buterin ha definito i bug nell’infrastruttura crypto ancora più allarmanti una volta che gli strumenti di IA inizieranno ad automatizzare la scoperta delle vulnerabilità, una preoccupazione condivisa in tutta la comunità della ricerca sulla sicurezza.
Ha indicato in particolare l’infrastruttura di Ethereum (ETH), i meccanismi di consenso e la crittografia post-quantistica come bersagli prioritari per difese più solide.
Invece di affidarsi ai tradizionali audit, Buterin ha detto che gli sviluppatori dovrebbero adottare la verifica formale, un approccio che dimostra matematicamente che il codice si comporta come previsto in determinate condizioni.
Da leggere anche: Crypto Funds Bleed $1.07B As Iran Tensions End Six-Week Inflow Run
Verifica formale come difesa
«L’IA ti dà la possibilità di scrivere grandi volumi di codice a scapito dell’accuratezza, e la verifica formale ti restituisce l’accuratezza», ha scritto Buterin.
Ha respinto i ricercatori che sostengono che il software generato dall’IA sia diventato impossibile da fidarsi pienamente, presentando invece una visione più ottimistica.
Buterin ritiene che la programmazione assistita dall’IA, abbinata a strumenti di verifica, possa alla fine produrre software più robusto di quello che gli esseri umani costruiscono da soli.
Ha inoltre richiamato l’attenzione su progetti attivi come Arklib ed evm-asm, che si concentrano sulla messa in sicurezza dell’infrastruttura crittografica e del software della Ethereum Virtual Machine.
Il saggio ha avvertito, tuttavia, che la verifica formale non è una panacea. Anche i sistemi dimostrati matematicamente possono fallire quando gli sviluppatori verificano le ipotesi sbagliate o quando gli exploit si trovano al di fuori del percorso di codice verificato.
Il track record di Buterin sulla sicurezza
Buterin ha delineato un futuro in cui l’infrastruttura digitale sensibile si concentra in piccoli sistemi “core sicuri”, isolati e pesantemente verificati, mentre le applicazioni meno critiche funzionano con permessi limitati.
Il cofondatore di Ethereum è tornato più volte quest’anno sul tema della sicurezza dell’IA. A febbraio ha suggerito di dividere i guadagni di produttività dell’IA tra velocità e sicurezza, e a maggio ha approvato strumenti di verifica formale come Lean per lo sviluppo ad alta affidabilità. Il suo ultimo post estende tali argomentazioni a una tesi più ampia, presentando la prova matematica come la risposta più credibile agli strumenti di attacco guidati dall’IA sia nel mondo blockchain sia nei sistemi tradizionali di internet.
Da leggere dopo: Iran Settles Hormuz Shipping Cover In Bitcoin, Eyes $10B Haul