Questo articolo è stato pubblicato da un membro della comunità. L'autore è David Tarditi, Vice President of Engineering presso CertiK, una società di auditing di contratti intelligenti Web3.
Riepilogo
La verifica formale dei contratti intelligenti li protegge da errori, vulnerabilità e altre condizioni avverse. In questo processo, gli esperti umani convertono la logica del contratto intelligente in dichiarazioni matematiche e quindi utilizzano un processo automatizzato per verificare la logica effettiva rispetto a un modello del comportamento previsto del contratto. Combinando verifica formale e audit manuale, possiamo condurre una valutazione completa della sicurezza dei contratti intelligenti.
introduzione
I contratti intelligenti sono programmi informatici distribuiti sulla blockchain che vengono eseguiti automaticamente quando vengono soddisfatte determinate condizioni. I contratti intelligenti possono essere molto semplici o estremamente complessi e possono contenere asset per milioni o addirittura miliardi di dollari.
Se ci fossero buchi di sicurezza nel codice del contratto intelligente, ciò potrebbe avere conseguenze devastanti, come il furto di tutti i beni detenuti dai criminali. Nel 2021, 50 milioni di dollari sono stati rubati al market maker automatizzato (AMM) Uranium Finance a causa di un errore di battitura in uno smart contract.
Sempre nel 2021, Compound Finance ha erroneamente emesso 80 milioni di dollari in premi a causa di un singolo errore di codifica. Nel 2022, 320 milioni di dollari furono rubati da Wormhole Bridge a causa di un errore nello smart contract.
Pertanto, è importante ottenere il tuo programma di contratto intelligente fin dall’inizio. I contratti intelligenti adottano un modello open source, il che significa che una volta implementato il contratto, il codice viene reso pubblico. Se un hacker scopre un bug, può sfruttarlo immediatamente. Inoltre, la normale pratica di applicare patch alle vulnerabilità della sicurezza nel tempo è inefficace perché il codice dei contratti intelligenti spesso non può essere modificato dopo l’implementazione.
Come funziona la verifica del contratto intelligente?
La verifica formale dei contratti intelligenti si ottiene presentando la logica e il comportamento previsto del contratto intelligente come affermazioni matematiche. I revisori utilizzano quindi strumenti automatizzati per verificare se queste dichiarazioni sono corrette.
Il processo prevede:
Definire le specifiche e le caratteristiche attese del contratto in un linguaggio formale.
Convertire il codice di un contratto in una dichiarazione formale, come un modello matematico o logico.
Verifica le specifiche e le proprietà del contratto utilizzando la dimostrazione automatizzata di teoremi o il controllo del modello.
Ripeti il processo di convalida per trovare e correggere eventuali errori o deviazioni dalle caratteristiche previste.
Perché la verifica del contratto intelligente è importante
Applicando il ragionamento matematico, aiuta a garantire che i contratti intelligenti formalmente verificati siano esenti da errori, vulnerabilità e altre situazioni avverse. La verifica aiuta anche ad aumentare la fiducia e la fiducia nel contratto perché le sue proprietà sono state rigorosamente testate e sono corrette e affidabili.
Gli esempi riportati di seguito illustrano come la verifica dei contratti intelligenti può aiutare a prevenire perdite finanziarie significative e altre conseguenze catastrofiche.
Uniswap
Uniswap è un noto AMM. Il contratto intelligente Uniswap V1 è stato sottoposto a verifica formale durante il processo di sviluppo. Prima del rilascio, questa verifica formale ha rilevato e corretto alcuni errori di arrotondamento, impedendo che Uniswap V1 venisse prosciugato di fondi.
Bilanciatore
Balancer V2 è anche un AMM collaudato. La verifica formale ha scoperto e corretto un errore di calcolo delle commissioni nella funzione di prestito flash nello smart contract che rendeva la piattaforma di trading vulnerabile al furto.
SafeMoon
Dopo l'implementazione di SafeMoon V1, è stato scoperto un errore molto piccolo attraverso la verifica formale. Se l'errore non veniva scoperto, se il proprietario del contratto eseguiva determinate operazioni prima di rinunciare alla proprietà, il proprietario del contratto potrebbe riacquistarla dopo aver rinunciato al contratto.
La maggior parte degli audit manuali del fork SafeMoon V1 non rilevano questo bug perché è necessario analizzare combinazioni specifiche di valori delle variabili del programma per trovarlo. Gli esseri umani possono facilmente ignorare questo problema, ma le macchine possono rilevarlo in tempo.
Come funzionano insieme la verifica formale e l'auditing manuale
La verifica formale fornisce un modo sistematico e automatizzato per verificare la logica e il comportamento di un contratto rispetto alle sue caratteristiche previste. Ciò semplifica l'identificazione e la correzione di eventuali bug o vulnerabilità. Ciò è particolarmente utile per problemi complessi e sottili che sarebbero difficili da rilevare tramite un'ispezione manuale.
L'audit manuale coinvolge esperti che esaminano il codice, la progettazione e l'implementazione del contratto. I revisori utilizzano 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 gli strumenti automatizzati potrebbero non rilevare.
Combinando verifica formale e audit manuale, possiamo condurre una valutazione completa della sicurezza dei contratti intelligenti. Ciò aumenta le probabilità di trovare e correggere eventuali vulnerabilità. In tal modo, adottiamo un approccio di sicurezza di difesa approfondita che combina le competenze di esseri umani e macchine.
Conclusione
Per garantire la sicurezza dei contratti intelligenti, la verifica formale e l’audit manuale devono essere combinati per garantire una valutazione completa e approfondita della situazione di sicurezza dei contratti intelligenti.
Sebbene la verifica formale richieda più risorse, rappresenta un investimento utile per contratti con valore elevato o fattori di rischio elevati. Dopotutto, alla fine, la sicurezza è più importante di qualsiasi altra cosa. Assicurati di dare priorità alla sicurezza e di garantire che i contratti intelligenti siano esenti da bug, vulnerabilità e comportamenti avversi imprevisti.
Ulteriori letture
Cos’è un contratto intelligente?
Che cos'è l'audit di sicurezza del contratto intelligente?
Dichiarazione di non responsabilità e avvertenza sui rischi: i contenuti di questo articolo sono fatti e sono solo a scopo informativo generale e didattico e non costituiscono alcuna dichiarazione o garanzia. Questo articolo non deve essere interpretato come un consiglio finanziario e non consiglia l'acquisto di alcun prodotto o servizio specifico. I prezzi delle risorse digitali possono variare. Il valore del vostro investimento potrebbe diminuire così come aumentare e potreste non recuperare il capitale investito. Sei l'unico responsabile delle tue decisioni di investimento e Binance Academy non è responsabile per eventuali perdite che potresti subire. Questo materiale non costituisce consulenza finanziaria.
