Gli smart contract rappresentano uno strumento fondamentale in ambito crypto. Si tratta di programmi informatici che vengono distribuiti su una blockchain in modo da poter essere eseguiti in automatico una volta che si verifichino le condizioni preventivate al loro interno.
I programmi in questione possono essere estremamente semplici, oppure molto complicati. Così come può variare molto il valore in asset che sono chiamati a gestire, il quale può arrivare da cifre non molto elevate a importi miliardari.
Proprio il fatto che possano arrivare a gestire quantità di risorse così elevate rende quindi obbligatorio cercare di eliminare ogni possibile vulnerabilità presente nel loro codice. Difetti che possono infine sfociare nella sottrazione di tutte le risorse finanziarie detenute al loro interno. Questo è il motivo che rende necessario mettere in campo gli strumenti più appropriati per riuscire a metterli in sicurezza. La verifica formale è uno di essi.
Verifica formale degli smart contract: di cosa si tratta?
Nel corso del 2021, Uranium Finance, un Automated Market Maker (AMM), si è visto sottrarre oltre 50 milioni di dollari a causa di un semplice errore di battitura nel codice di un contratto intelligente.
Nello stesso ano anche Compound Finance ha pagato un dazio salato ad un errore analogo, distribuendo 80 milioni di dollari in ricompense non dovute. Ancora peggio, però, è andata nell’anno successivo a Wormhole Bridge, che ha subito il furto di ben 320 milioni di dollari per un bug in uno dei suoi smart contract.
Occorre a questo punto precisare che il codice di un contratto intelligente deve essere immediatamente esente da errori, sin dal momento della pubblicazione. Non solo l’hacker è in grado di approfittare agevolmente di errori nella sua scrittura, ma è anche impossibile correggerli una volta che sia stato distribuito.
Per impedire incidenti di questo genere, uno degli strumenti fondamentali è rappresentato dalla verifica formale degli smart contract. A condurla è un esperto il quale presenta la logica dello smart contract sotto forma di affermazioni matematiche, da sottoporre successivamente a un processo automatizzato teso a verificare la logica effettiva rispetto ai modelli comportamentali che ci si attende dal contratto.
Verifica formale degli smart contract: come funziona?
La verifica formale degli smart contract prevede quindi che la logica e il comportamento indicato al loro interno siano in grado di arrivare in porto alla stregua di affermazioni matematiche. Una volta che sia stata impostata, i revisori saranno chiamati a verificarne la correttezza utilizzando all’uopo strumenti automatizzati.
L’iter procedurale prevede i seguenti passaggi:
- definizione di specifiche e proprietà desiderate in un linguaggio formalmente ineccepibile;
- traduzione del codice del contratto in una rappresentazione formale, sotto forma di modelli matematici o logici;
- utilizzazione di dimostrazioni di teoremi o model checker (controlli di qualità) automatizzati al fine di convalidare specifiche e proprietà del contratto,
- ripetizione del processo di verifica in modo da riuscire a individuare e procedere alla correzione di eventuali errori o scartamenti dalle proprietà desiderate.
Sarà proprio l’utilizzo del ragionamento matematico a consentire il conseguimento da parte degli smart contract verificati di un formato esente da bug, vulnerabilità e altri comportamenti potenzialmente dannosi.
La revisione manuale è fondamentale
La verifica formale è in effetti estremamente preziosa, in quanto è in grado di garantire un modo sistematico e automatizzato di controllo sulla logica e il comportamento di un contratto. In pratica ne assicura la rispondenza alle proprietà preventivate.
Una volta condotta a termine è possibile porre le basi affinché non si possano verificare bug o errori in grado di tramutarsi in un disastro. In particolare, si rivela estremamente utile in fase di individuazione di lacune impercettibili, le quali potrebbero rivelarsi complicate da riscontrare procedendo ad un audit manuale.
Quest’ultimo, però, può rivelarsi non meno importante. Grazie ad esso, infatti, è possibile rilevare eventuali problematiche non riscontrate nel corso della procedura automatizzata. Proprio mettendo insieme i due procedimenti, in definitiva, sarà possibile approntare smart contract in grado di impedire exploit e attacchi tesi a sfruttare la presenza di eventuali vulnerabilità. Considerato come gli stessi siano chiamati a governare processi in cui sono coinvolte spesso ingenti risorse, è sempre buona cosa ricorrere ad entrambe le procedure.
