Nel giugno 2016, l’entusiasmo era forte per il fatto che “The DAO”, costruito sulla blockchain di Ethereum, stesse per diventare il primo fondo di investimento decentralizzato completamente digitale al mondo.
Ma nel giro di poche settimane, è diventato invece il simbolo degli hack DeFi dopo che gli aggressori hanno rubato da esso ether per un valore di 50 milioni di dollari.
Per violare The DAO, l'aggressore ha sfruttato una cosiddetta vulnerabilità di rientro, una vulnerabilità di concorrenza in cui viene richiamato un metodo di uno specifico contratto intelligente mentre un altro metodo è ancora in esecuzione, e The DAO è solo una parte dello sviluppo a lungo termine del contratto intelligente.Il primo soffre di tali errori.
Successori di spicco includono Uniswap/Lendf.Me, a cui sono stati rubati 25 milioni di dollari nel 2020, CREAM, a cui sono stati rubati 18 milioni di dollari nel 2021, e Fei, a cui sono stati rubati 80 milioni di dollari nel 2022.
Il motivo per cui questi bug persistono è che possono comportare interazioni di codice inaspettate sparse in tutto lo smart contract, a volte anche in contratti intelligenti completamente diversi. Il numero di tali interazioni di codice può essere molto elevato, rendendo difficile per gli esseri umani rilevare ed eliminare contratti intelligenti non intenzionali codice richiesto.
Inoltre, queste interazioni sono spesso difficili da testare in modo automatico e sistematico.
TLA+: Lo Sterminatore
Entra nella Logica Temporale delle Azioni (TLA+), un linguaggio per specificare e validare sistemi complessi. TLA+ non solo trova gli errori ma ne verifica anche l'esistenza.
Com'è possibile, chiedi? TLA+ viene fornito con una serie di strumenti per la verifica formale leggera sotto forma del cosiddetto controllo del modello. Attraverso il controllo del modello, esplora in modo esaustivo tutte le possibili interazioni simultanee del modello di codice - proprio le aree difficili da testare - e trova i bug.
Immagina un disinfestatore che illumina ogni angolo e fessura per esporre ed eliminare i parassiti indesiderati nascosti in quegli angoli bui che spesso vengono trascurati o ignorati. È importante sottolineare che, una volta creato il modello di codice, l'esecuzione del model check non richiede quasi alcun input umano, il che lo rende estremamente conveniente.
Per illustrarlo con alcuni numeri inventati: se le pratiche standard del settore come i test e le revisioni della sicurezza eliminano l’80% dei bug e la verifica formale “pesante” ne elimina il 99%, l’utilizzo di TLA+ elimina il 90% con un solo numero limitato di sforzi di verifica pesanti.
TLA+ e computer Internet
Il nostro team di ingegneri utilizza TLA+ per analizzare tutti gli aspetti dell'informatica Internet, compresi i contratti intelligenti critici per la sicurezza eseguiti sulla piattaforma. Sebbene i computer Ethereum e Internet abbiano modelli di esecuzione diversi, errori di rientro possono comparire nei contratti intelligenti su entrambe le blockchain.
Infatti, a causa del suo elevato throughput, i computer Internet consentono più chiamate simultanee a un singolo contratto intelligente, il che richiede che gli autori dei contratti intelligenti siano più attenti a eliminare le interazioni simultanee indesiderate. Poiché la sicurezza è fondamentale per il successo dei computer su Internet, TLA+ viene utilizzato in molti contratti intelligenti per rilevare errori durante la fase di sviluppo.
Recentemente è stato condotto un contenitore di analisi TLA+ (contratti intelligenti per computer su Internet) sul nuovo Chain-Key Bitcoin (ckBTC), i cui risultati condividerò di seguito.
Contratto intelligente ckBTC
Per parlare dell’analisi TLA+ di ckBTC, iniziamo con una panoramica di alto livello di ckBTC. ckBTC è un token nativo per computer Internet supportato in modo sicuro da Bitcoin (BTC) con un rapporto 1:1.
Il registro ckBTC è un contratto intelligente contenitore sulla blockchain del computer di Internet che tiene traccia della quantità di ckBTC posseduti da ciascun utente finale. Questo stesso registro consente agli utenti finali di trasferire i propri ckBTC ad altri utenti finali in modo più rapido ed economico rispetto al trasferimento di BTC sulla rete Bitcoin.
Per convertire ckBTC in BTC e viceversa, gli utenti finali interagiscono con un diverso contratto intelligente, il ckBTC Minter.
Ad alto livello, l'operazione di conversione da BTC a ckBTC si presenta così:
Passaggi per ottenere ckBTC:
1. L'utente finale trasferisce prima alcuni BTC a un indirizzo di deposito Bitcoin specifico dell'utente, tutti gli indirizzi di deposito sono completamente controllati dal codice del contenitore intelligente ckBTC minter grazie alla firma ECDSA della chiave della catena, che crea un nuovo UTXO di proprietà del deposito indirizzo;
2. L'utente finale notifica allo smart contract ckBTC mint l'UTXO appena depositato chiedendo alla zecca di aggiornare il saldo dell'utente;
3. Il contratto intelligente del minter utilizza quindi l'integrazione Bitcoin dei computer Internet per recuperare tutti gli UTXO di proprietà dell'indirizzo di deposito controllato ma specifico dell'utente. Il minter seleziona poi i nuovi UTXO dalla rete Bitcoin inviando loro controlli incrociati il suo elenco contabile interno degli UTXO elaborati;
4. Infine, il minter ordina al registro di coniare nuovi ckBTC per tutti i nuovi UTXO con un rapporto 1:1 e, una volta completato, aggiunge gli UTXO appena scoperti all'elenco degli UTXO elaborati.
Dichiarazione di non responsabilità: il processo di cui sopra omette il processo KYT (Know Your Transaction) per semplicità.
Il contratto intelligente ckBTC soddisfa TLA+
Il quadro di alto livello presentato sopra nasconde in realtà un sottile problema di concorrenza e la buona notizia è che possiamo rilevare il problema utilizzando il toolkit TLA+.
Ma prima che TLA+ possa rilevare qualcosa, dobbiamo prima fornirgli due cose:
Crea un modello del nostro sistema utilizzando il linguaggio TLA+
Specificare le proprietà TLA+ che ci si aspetta che il sistema implementi
Questo modello è una versione semplificata ma ancora completamente definita del sistema, che nel nostro caso include il contratto intelligente del minter, ma anche tutte le altre parti rilevanti del sistema, vale a dire il contratto di registro e la rete Bitcoin.
Per ciascun componente, modelliamo il suo stato e il modo in cui le azioni rilevanti che un utente finale potrebbe intraprendere (ad esempio trasferire BTC o ckBTC, depositare BTC o richiamare diverse azioni esposte dal minter) modificano lo stato.
Tutti questi elementi sono in qualche modo semplificati nel modello, con le parti su cui si concentra l'analisi (ad esempio il codice Minter) modellate in modo più dettagliato, mentre altre parti (ad esempio la rete Bitcoin) sono modellate in modo meno dettagliato, infatti, un modello TLA+ è simile a una specifica di progettazione dettagliata di un sistema.
Intuitivamente, la caratteristica principale che vogliamo implementare è garantire che il nostro ckBTC sia completamente supportato. In altre parole, nessun utente finale dovrebbe essere in grado di “spendere due volte” i BTC depositati per ottenere più ckBTC di quelli depositati.
Ma per analizzare tale proprietà dobbiamo rendere questa intuizione molto precisa esprimendola formalmente nel linguaggio TLA+. La nostra definizione formale è che l'offerta totale di ckBTC (ovvero la somma di tutti i saldi ckBTC degli utenti finali, come archiviato nel registro ckBTC) non supera la quantità totale di BTC controllata dal contenitore di conio (ovvero il valore di tutti UTXO posseduti da un indirizzo di deposito).
Rileva e risolvi i problemi
Una volta creato il modello e le proprietà, il toolkit TLA+ può analizzare il modello. Per eseguire l'analisi, definiamo innanzitutto le impostazioni per l'esecuzione dell'analisi. Ad esempio, la nostra configurazione per ckBTC include solo due diversi utenti finali e una piccola quantità dell'offerta totale di Bitcoin (ad esempio 5 satoshi).
Sebbene questo contesto sia molto limitato, gli studi empirici mostrano che la stragrande maggioranza dei problemi nei sistemi informatici può essere riscontrata in un numero limitato di entità. Il piccolo setup consente all'analisi di esplorare sistematicamente tutte le possibili sequenze di azioni definite dal modello e di verificare se le proprietà prescritte valgono in ciascuna di tali sequenze.
Inoltre l’analisi viene eseguita in modo completamente automatico, cioè non richiede alcun input umano, e se queste proprietà non valgono ci fornisce l’esatta sequenza di operazioni che violano quella proprietà.
Ad esempio, l'analisi può rivelare che possiamo violare la nostra proprietà "nessun ckBTC non protetto" in uno scenario come quello illustrato di seguito:
Qui:
Gli utenti finali depositano BTC, come prima;
Tuttavia, ora l'utente finale ordina al minatore ckBTC di aggiornare il saldo due volte in rapida successione e su un computer Internet questi aggiornamenti possono essere interagiti contemporaneamente con altri contratti intelligenti;
Due aggiornamenti in esecuzione simultaneamente chiedono alla rete Bitcoin tutti gli UTXO depositati dall'utente finale, ed entrambi ricevono in risposta lo stesso UTXO depositato nel passaggio 1. Poiché l'UTXO non è ancora nell'elenco "elaborati", entrambi gli aggiornamenti pensano che UTXO sia nuovo;
Entrambi gli aggiornamenti indicano al registro di coniare la quantità corrispondente di ckBTC nel passaggio 4.
Pertanto, alla fine del passaggio 4, ci troviamo in uno stato in cui l'offerta di ckBTC è il doppio della somma degli UTXO negli indirizzi di deposito, il che viola la nostra proprietà "no ckBTC non supportato".
Tieni presente che questo errore si verifica solo perché gli aggiornamenti al saldo dell'utente finale vengono eseguiti contemporaneamente: in realtà è un errore rientrante nello stesso stile di quello che ha bloccato The DAO.
Un modo per risolvere questo problema è impedire che gli aggiornamenti del saldo vengano eseguiti in parallelo per lo stesso utente finale, possiamo farlo facendo in modo che il minter memorizzi l'utente finale in un elenco di utenti "bloccati" quando inizia l'aggiornamento del saldo e li mantenga lì per tutta la durata dell'elenco di aggiornamento per raggiungere questo obiettivo.
Se l'utente finale tenta di avviare un altro aggiornamento simultaneo del saldo, l'aggiornamento prima controllerà e troverà questo specifico utente finale nell'elenco degli utenti bloccati, quindi verrà interrotto.
Tieni presente che qui stiamo leggermente semplificando l'attacco: il blocco è in realtà un modello abbastanza comune per i contratti intelligenti IC e i minatori di ckBTC lo hanno implementato fin dall'inizio. Tuttavia, un bloccaggio eseguito in modo errato apre la porta agli attacchi di cui sopra, che TLA+ è in grado di rilevare.
Inoltre, abbiamo riscontrato alcuni casi limite che violavano "nessun ckBTC non supportato" e altre proprietà importanti e, una volta applicate tutte le correzioni, TLA+ è stata in grado di verificare e confermare che non vi erano più violazioni di proprietà nella nostra configurazione definita.
Dovresti utilizzare TLA+ per i tuoi contratti intelligenti?
Assolutamente! Ok, ok, forse dovrei fornire una risposta più sfumata, che il nostro team di ricerca e sviluppo utilizza per contratti intelligenti critici sui computer Internet ogni volta che è coinvolta una concorrenza non banale.
Ad esempio, l'analisi TLA+ ha scoperto sottili bug di concorrenza nella governance informatica di Internet e nei contenitori contabili che non erano stati rilevati nelle precedenti revisioni manuali della sicurezza e che avrebbero potuto portare a problemi, casi e punti importanti: TLA+ nello scoprire questioni così spinose Un vero spasso.
Naturalmente, c’è un prezzo da pagare in termini di acquisizione del know-how e quindi di costruzione del modello, ma empiricamente il prezzo è ragionevole, soprattutto considerando la natura ad alta posta in gioco della sicurezza blockchain.
Non bisogna lasciarsi intimidire dal linguaggio TLA+ stesso, nonostante il nome intimidatorio, accedere alle sue potenti funzionalità è abbastanza semplice. In effetti, un cheat sheet di TLA+ che descrive quasi tutte le funzionalità di TLA+ potrebbe stare più o meno in una pagina:
mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
Inoltre, lo sforzo richiesto per creare il modello è paragonabile alle revisioni manuali standard della sicurezza. Ad esempio, per un minatore di ckBTC, occorrerebbero un totale di circa 3 settimane affinché 1 persona comprenda il progetto, crei il modello iniziale e le proprietà.
Il modello TLA+ risultante è molto più semplice dell'implementazione, sia perché è più semplice del codice sia per la natura di alto livello di TLA+. Il modello per il minter ckBTC richiede circa 250 righe di codice rispetto alle migliaia di righe dell'implementazione di Rust. Forse sorprendentemente, una delle parti più difficili in termini di impegno è specificare le proprietà richieste, poiché spesso si trovano lacune nelle specifiche intuitive.
Una volta completato il modello, l'analisi (controllo del modello) viene completata automaticamente. L'esecuzione dell'analisi può richiedere molto tempo: ad esempio, per ckBTC, sono state necessarie più di 20 ore per essere completata. Infine, un altro vantaggio di TLA è che la modellazione e l'analisi possono essere eseguite nella fase di progettazione prima dell'implementazione del codice, il che aiuta a eliminare successivi refactoring di grandi dimensioni dovuti a errori di progettazione.
Dove TLA+ è inutile
Il lato negativo è che TLA+ è meno utile per programmi sequenziali complessi, rispetto a programmi concorrenti, e non è adatto anche a gestire protocolli crittografici complessi, per i quali esistono altri strumenti (ad esempio Tamarin) che sono più utili.
Infine, c'è il problema di mantenere sincronizzati il modello TLA+ e l'effettiva implementazione, poiché man mano che il codice di implementazione si evolve nel tempo potrebbe non essere più conforme al modello, il che può essere difficile da rilevare senza il supporto degli strumenti.
In effetti, il nostro team di ricerca e sviluppo sta cercando di risolvere questo problema: spero che presto potremo condividere alcuni strumenti con te!
Spero che questa panoramica abbia suscitato il tuo interesse nell'utilizzo di TLA+ per i tuoi contratti intelligenti critici e, in tal caso, resta sintonizzato: presto arriverà un post di follow-up con un tutorial più approfondito su come utilizzare TLA+ per i contratti intelligenti, e in allegato è presente un modello TLA+ effettivo sviluppato dal nostro team di ricerca e sviluppo.
Contenuti IC che ti interessano
Progresso tecnologico |. Informazioni sul progetto |
Raccogli e segui il canale IC Binance
Rimani aggiornato con le informazioni più recenti