Cos'è la verifica formale degli Smart Contract?
Home
Articoli
Cos'è la verifica formale degli Smart Contract?

Cos'è la verifica formale degli Smart Contract?

Avanzato
Pubblicato Mar 2, 2023Aggiornato Jul 12, 2023
5m

Questo articolo è stato inviato dalla community. L'autore è David Tarditi, vicepresidente Engineering di CertiK, una società di auditing di smart contract Web3.

TL;DR

La verifica formale degli smart contract assicura che siano privi di bug, vulnerabilità e altri comportamenti indesiderati. Prevede la partecipazione di un esperto (umano) che presenta la logica dello smart contract sotto forma di affermazioni matematiche, che vengono poi sottoposte a un processo automatizzato che verifica la logica effettiva rispetto ai modelli del comportamento atteso del contratto. La combinazione di verifica formale e audit manuale fornisce una valutazione completa della sicurezza di uno smart contract.

Introduzione

Gli smart contract sono programmi informatici distribuiti su una blockchain che vengono eseguiti automaticamente quando vengono soddisfatte determinate condizioni. Possono spaziare da semplici a estremamente complessi e possono contenere asset per un valore di milioni o addirittura miliardi di dollari.  

Le vulnerabilità di sicurezza nel codice degli smart contract possono avere conseguenze devastanti, tra cui il furto di tutti gli asset detenuti da uno smart contract. Nel 2021, il market maker automatizzato (AMM) Uranium Finance ha subito il furto di 50 milioni di dollari per via di un singolo errore di battitura in uno smart contract.

Sempre nel 2021, Compound Finance ha distribuito 80 milioni di dollari in ricompense non dovute a causa di un errore di un singolo carattere. Nel 2022, 320 milioni di dollari sono stati rubati dal Wormhole Bridge a causa di un bug in uno dei suoi smart contract.

È importante che il codice di uno smart contract sia corretto al primo tentativo. Gli smart contract sono open-source, il che significa che il codice è pubblicamente disponibile una volta che il contratto è stato distribuito. Se un hacker trova un bug, può approfittarne immediatamente. Inoltre, non è possibile correggere le vulnerabilità di sicurezza nel corso del tempo, poiché il codice di uno smart contract non può essere modificato dopo la distribuzione.

Come funziona la verifica degli smart contract?  

La verifica formale degli smart contract funziona presentando la logica e il comportamento desiderato degli smart contract come affermazioni matematiche. In seguito, i revisori utilizzano strumenti automatizzati per verificare la correttezza di tali affermazioni.

Il processo prevede:

  1. Definire le specifiche e le proprietà desiderate di un contratto in un linguaggio formale.

  2. Tradurre il codice del contratto in una rappresentazione formale, come modelli matematici o logici.

  3. Utilizzare dimostrazioni di teoremi o model checker automatizzati per convalidare le specifiche e le proprietà del contratto.

  4. Ripetere il processo di verifica per individuare e correggere eventuali errori o deviazioni dalle proprietà desiderate.

Perché la verifica di uno smart contract è importante

L'uso del ragionamento matematico aiuta a garantire che gli smart contract verificati formalmente siano privi di bug, vulnerabilità e altri comportamenti indesiderati. Inoltre, contribuisce ad aumentare la fiducia nel contratto, in quanto è stato dimostrato in maniera rigorosa che le sue proprietà sono corrette. 

Di seguito sono riportati alcuni esempi di come la verifica degli smart contract abbia contribuito a prevenire perdite finanziarie significative e altri esiti disastrosi.  

Uniswap

Uniswap è un noto AMM. Quando è stato sviluppato lo smart contract Uniswap V1, è stato verificato formalmente. Prima del suo rilascio, questa verifica formale ha individuato e corretto gli errori di arrotondamento che avrebbero potuto far perdere fondi a Uniswap V1. 

Balancer

Anche Balancer V2 è un AMM che è stato verificato formalmente. La verifica formale ha individuato e corretto un calcolo errato delle commissioni che coinvolgeva la funzionalità di prestito flash nello smart contract, che avrebbe potuto rendere l'exchange vulnerabile ad eventuali furti.

SafeMoon

SafeMoon V1 conteneva un bug impercettibile scoperto dalla verifica formale dopo la sua distribuzione. Era possibile per un proprietario rinunciare alla proprietà del contratto e poi riacquistarla, se venivano effettuate determinate operazioni prima di rinunciare alla proprietà.

Questo bug è sfuggito alla maggior parte delle verifiche manuali dei fork di SafeMoon V1 perché per trovarlo era necessario analizzare combinazioni specifiche dei valori delle variabili del programma. Si tratta di un aspetto che viene ignorato facilmente da un essere umano ma è facile da rilevare per una macchina.

Come la verifica formale e la revisione manuale lavorano insieme

La verifica formale fornisce un modo sistematico e automatizzato per controllare la logica e il comportamento di un contratto rispetto alle proprietà desiderate. In questo modo è più facile identificare e risolvere eventuali errori o bug. È particolarmente utile per individuare problemi complessi e impercettibili che potrebbero essere difficili da rilevare con un'ispezione manuale.

L'audit manuale prevede la revisione da parte di esperti del codice, della progettazione e della distribuzione di un contratto. L'auditor utilizza la propria esperienza e competenza per identificare i rischi per la sicurezza e valutare la posizione complessiva del contratto in materia di sicurezza. Possono anche confermare che il processo di verifica formale è stato eseguito correttamente e controllare eventuali problemi che potrebbero non essere rilevabili dagli strumenti automatici. 

La combinazione di verifica formale e audit manuale fornisce una valutazione completa e approfondita della sicurezza di uno smart contract. In questo modo si aumentano le possibilità di trovare e risolvere eventuali vulnerabilità. Il risultato è un approccio alla sicurezza basato sulla difesa in profondità che sfrutta le capacità uniche di uomini e macchine. 

In chiusura

Per garantire la sicurezza degli smart contract, è essenziale utilizzare sia la verifica formale che l'audit manuale per garantire una valutazione completa e approfondita della posizione rispetto alla sicurezza di uno smart contract.

Sebbene la verifica formale possa richiedere un notevole dispendio di risorse, è un investimento che vale la pena fare per i contratti di valore elevato o con fattori di rischio elevati. In definitiva, è fondamentale dare priorità alla sicurezza e garantire che gli smart contract siano privi di bug, vulnerabilità e comportamenti indesiderati.

Letture consigliate

Disclaimer e Avvertenza sui rischi: Questo contenuto viene presentato "così com'è" solo a scopo informativo ed educativo, senza alcuna dichiarazione o garanzia di alcun tipo. Non deve essere interpretato come una consulenza finanziaria, né intende raccomandare l'acquisto di alcun prodotto o servizio specifico. I prezzi degli asset digitali possono essere volatili. Il valore del vostro investimento può diminuire o aumentare e potreste non recuperare l'importo investito. L'utente è l'unico responsabile delle proprie decisioni di investimento e Binance Academy non è responsabile per le eventuali perdite subite. Non è una consulenza finanziaria.