Certora , una delle principali piattaforme di sicurezza blockchain, ha reso open source il suo motore di verifica formale più avanzato, Certora Prover, per rendere la sicurezza dei contratti intelligenti più accessibile a tutti nel settore delle criptovalute.
Questa mossa da Certora non sarebbe potuta arrivare in un momento migliore poiché gli hacker proliferano nello spazio delle risorse digitali e rubano fondi.
“La sicurezza rimane una delle maggiori sfide del Web3. I progetti DeFi spendono milioni in audit e spesso impiegano più di un anno per essere lanciati, ma le vulnerabilità continuano a mettere a rischio miliardi di dollari", ha osservato Shelly Grossman, CTO di Certora, aggiungendo: "Sebbene gli exploit di alto profilo siano diventati meno frequenti, garantire contratti intelligenti rimane costoso e fuori dalla portata di molti sviluppatori. Oggi tutto cambia”.
I dati della società di analisi blockchain Chainalysis rivelano che nel 2024 gli hacker hanno rubato ben 2,2 miliardi di dollari , con un aumento del 21% rispetto a un anno fa. Non solo l’importo in dollari è aumentato, ma anche il numero di incidenti.
Man mano che l’adozione delle criptovalute aumenta, guadagnando terreno sia tra i negozi al dettaglio che tra le istituzioni, e il mercato esplode con una capitalizzazione di mercato totale delle criptovalute che supera i 3 trilioni di dollari , i cattivi attori si stanno sicuramente moltiplicando. Questi criminali informatici stanno adottando metodi sempre più sofisticati e ampliando la loro portata sfruttando i punti deboli dei contratti intelligenti, che sono la spina dorsale dei protocolli e dell’ecosistema DeFi.
In questo contesto, Certora offre una potente soluzione agli sviluppatori DeFi, che identifica tutti i possibili bug e poi ne dimostra l’assenza. Supportando più catene popolari, vale a dire. Ethereum (EVM), Solana (sBPF) e Stellar (WASM), Certora assicurano che la stragrande maggioranza dello spazio crittografico sia protetto dagli attacchi dei contratti intelligenti.
Prover è il prodotto di sicurezza di punta di Certora, che utilizza la verifica formale per individuare i bug più difficili e rari. In produzione da “molto tempo”, lo strumento viene finalmente rilasciato al grande pubblico.
Il Certora Prover agisce essenzialmente come un revisore matematico automatizzato, analizzando il codice del contratto intelligente e le regole definite dallo sviluppatore per fornire prova di correttezza. In questo modo si va oltre gli scenari limitati, valutando ogni possibile caso. Gli sviluppatori hanno già scritto oltre 70.000 regole di verifica.
In realtà è stato con l'aiuto della tecnologia di verifica formale di Certora che è stato finalmente individuato un difetto fondamentale nell'equazione DAI di MakerDAO, che non era stato rilevato dal 2018. Risultati come questo mostrano che anche più audit non possono rimuovere completamente le vulnerabilità di uno smart contract, ma una verifica formale può aiutare a scoprirle.
Con questo strumento, Cetora ha anche aiutato aziende del calibro di Aave, Uniswap, Lido, EigenLayer, Solana Foundation e molti altri a proteggere decine di miliardi di dollari in TVL.
Tuttavia, Certora ha avuto il suo codice di tipo closed-source per tutto questo tempo, che sta finalmente cambiando per offrire a tutti gli sviluppatori di Web3 uno strumento potente e assolutamente gratuito per garantire che i loro contratti intelligenti siano sicuri, trasparenti e guidati dalla comunità.
“La sicurezza dei contratti intelligenti non dovrebbe essere un privilegio riservato a team ben finanziati o a persone altamente istruite. L’open source di Certora Prover è un passo avanti verso la trasformazione dei contratti intelligenti a prova di proiettile nella norma”, ha affermato Mooly Sagiv, CEO di Certora.
Disponibile gratuitamente per tutti, Certora sta attualmente invitando sviluppatori, ricercatori sulla sicurezza e la comunità Web3 a utilizzare la soluzione per verificare i loro contratti intelligenti e contribuire a portare avanti i suoi sforzi per rendere sicura la DeFi.