Questo articolo è un contributo della community. L'autore è David Tarditi, VP of Engineering presso CertiK, una società di revisione dei contratti intelligenti Web3.
Le opinioni in questo articolo appartengono al contributore/autore e non riflettono necessariamente quelle di Binance Academy.
TL;DR
La verifica formale dei contratti intelligenti garantisce che siano esenti da bug, vulnerabilità e altri comportamenti non intenzionali. Coinvolge un esperto umano che presenta la logica del contratto intelligente come affermazioni matematiche, quindi le esegue attraverso un processo automatizzato che verifica la logica effettiva rispetto ai modelli del comportamento previsto del contratto. La combinazione di verifica formale e audit manuale fornisce una valutazione completa della sicurezza di un contratto intelligente.
introduzione
I contratti intelligenti sono programmi informatici distribuiti su una blockchain che vengono eseguiti automaticamente quando vengono soddisfatte determinate condizioni. Possono variare da semplici a estremamente complessi e possono detenere asset per milioni o addirittura miliardi di dollari.
Le vulnerabilità della sicurezza nel codice del contratto intelligente possono avere conseguenze devastanti, incluso il furto di tutte le risorse detenute da un contratto intelligente. Nel 2021, al market maker automatizzato (AMM) Uranium Finance sono stati rubati 50 milioni di dollari a causa di un singolo errore di battitura in uno smart contract.
Sempre nel 2021, Compound Finance ha distribuito 80 milioni di dollari in ricompense non guadagnate a causa di un singolo errore di carattere. Nel 2022, 320 milioni di dollari sono stati rubati dal Wormhole Bridge a causa di un bug in uno dei suoi contratti intelligenti.
È importante ottenere il programma di contratto intelligente giusto la prima volta. I contratti intelligenti sono open source, il che significa che il codice è disponibile pubblicamente una volta implementato un contratto. Se un hacker trova un bug, può trarne immediatamente vantaggio. Inoltre, l’applicazione di patch alle vulnerabilità della sicurezza nel tempo non è un’opzione, poiché il codice di un contratto intelligente in genere non può essere modificato dopo l’implementazione.
Come funziona la verifica del contratto intelligente?
La verifica formale dei contratti intelligenti funziona presentando la logica e il comportamento desiderato dei contratti intelligenti come affermazioni matematiche. I revisori utilizzano quindi strumenti automatizzati per verificare se queste dichiarazioni sono corrette.
Il processo prevede:
Definire le specifiche e le proprietà desiderate di un contratto in linguaggio formale.
Tradurre il codice del contratto in una rappresentazione formale, come modelli matematici o logici.
Utilizzo di dimostratori di teoremi automatizzati o controllori di modelli per convalidare le specifiche e le proprietà del contratto.
Ripetendo il processo di verifica per trovare e correggere eventuali errori o deviazioni dalle proprietà desiderate.
Perché la verifica del contratto intelligente è importante
L’uso del ragionamento matematico aiuta a garantire che i contratti intelligenti formalmente verificati siano esenti da bug, vulnerabilità e altri comportamenti non intenzionali. Aiuta anche ad aumentare la fiducia nel contratto, poiché le sue proprietà sono state rigorosamente dimostrate corrette.
Di seguito sono riportati alcuni esempi di come la verifica dei contratti intelligenti abbia contribuito a prevenire perdite finanziarie significative e altri risultati disastrosi.
Uniswap
Uniswap è un noto AMM. Quando è stato sviluppato lo smart contract Uniswap V1, è stato formalmente verificato. Prima del suo rilascio, questa verifica formale ha rilevato e corretto errori di arrotondamento che avrebbero potuto portare alla perdita di fondi di Uniswap V1.
Bilanciatore
Anche il Balancer V2 è un AMM che è stato formalmente verificato. La verifica formale ha rilevato e corretto un calcolo errato delle commissioni che coinvolgeva la funzionalità di prestito flash nel contratto intelligente, che avrebbe potuto rendere l'exchange vulnerabile al furto.
SafeMoon
SafeMoon V1 conteneva un bug sottile rilevato tramite verifica formale dopo la sua distribuzione. Era possibile per un proprietario rinunciare alla proprietà del contratto e poi riacquistarlo, se venivano effettuate determinate operazioni prima di rinunciare alla proprietà.
Questo bug non è stato rilevato nella maggior parte degli audit manuali dei fork SafeMoon V1 perché per trovarlo era necessario analizzare combinazioni specifiche di valori delle variabili del programma. Questo è qualcosa che è facile non notare per gli esseri umani e facile da cogliere per una macchina.
Come la verifica formale e l'auditing manuale funzionano insieme
La verifica formale fornisce un modo sistematico e automatizzato per verificare la logica e il comportamento di un contratto rispetto alle proprietà desiderate. Ciò semplifica l'identificazione e la correzione di eventuali errori o bug. È particolarmente utile per individuare problemi complessi e sottili che potrebbero essere difficili da rilevare tramite l'ispezione manuale.
L'audit manuale prevede la revisione da parte di esperti del codice, della progettazione e dell'implementazione di un contratto. Il revisore utilizza la propria esperienza e competenza per identificare i rischi per la sicurezza e valutare la situazione di sicurezza complessiva del contratto. Possono anche confermare che il processo di verifica formale è stato eseguito correttamente e verificare eventuali problemi che potrebbero non essere rilevabili dagli strumenti automatizzati.
La combinazione di verifica formale e audit manuale fornisce una valutazione completa e approfondita della sicurezza di un contratto intelligente. Ciò aumenta le possibilità di trovare e correggere eventuali vulnerabilità. Il risultato è un approccio di difesa approfondito alla sicurezza che sfrutta le capacità uniche sia degli esseri umani che delle macchine.
Pensieri conclusivi
Per garantire la sicurezza dei contratti intelligenti, è essenziale utilizzare sia la verifica formale che l'audit manuale per garantire una valutazione completa e approfondita della posizione di sicurezza di un contratto intelligente.
Anche se la verifica formale può richiedere molte risorse, si tratta di un investimento utile per i contratti con un valore elevato o fattori di rischio elevati. In definitiva, è fondamentale dare priorità alla sicurezza e garantire che i contratti intelligenti siano esenti da bug, vulnerabilità e comportamenti non intenzionali.
Ulteriori letture
Cosa sono i contratti intelligenti?
Che cos'è un audit di sicurezza del contratto intelligente?
Dichiarazione di non responsabilità e avviso di rischio: questo contenuto viene presentato "così com'è" solo a scopo informativo generale e didattico, senza dichiarazioni o garanzie di alcun tipo. Non deve essere interpretato come consulenza finanziaria, legale o di altro tipo, né è inteso a raccomandare l'acquisto di alcun prodotto o servizio specifico. Dovresti chiedere il tuo consiglio a consulenti professionali appropriati. Laddove l'articolo sia fornito da un collaboratore di terze parti, tieni presente che le opinioni espresse appartengono al contributore di terze parti e non riflettono necessariamente quelle di Binance Academy. Si prega di leggere il nostro disclaimer completo qui per ulteriori dettagli. I prezzi degli asset digitali possono essere volatili. Il valore del tuo investimento potrebbe diminuire o aumentare e potresti non recuperare l'importo investito. Sei l'unico responsabile delle tue decisioni di investimento e Binance Academy non è responsabile per eventuali perdite che potresti subire. Questo materiale non deve essere interpretato come consulenza finanziaria, legale o di altro tipo. Per ulteriori informazioni, consultare i nostri Termini di utilizzo e Avvertenza sui rischi.
