În iunie 2016, entuziasmul că „The DAO”, construit pe blockchain-ul Ethereum, era pe cale să devină primul fond de investiții descentralizat complet digital din lume.
Dar în câteva săptămâni, a devenit, în schimb, posterul pentru hack-urile DeFi, după ce atacatorii au furat eter în valoare de 50 de milioane de dolari din ea.
Pentru a sparge DAO, atacatorul a exploatat o așa-numită vulnerabilitate de reintrare, o vulnerabilitate de concurență în care o metodă a unui anumit contract inteligent este apelată în timp ce o altă metodă este încă în execuție, iar DAO este doar o parte a dezvoltării pe termen lung a contract inteligent.Primul, suferă de astfel de erori.
Succesorii proeminenți includ Uniswap/Lendf.Me, care a avut 25 de milioane de dolari furate în 2020, CREAM, care a avut 18 milioane de dolari furate în 2021 și Fei, care a fost furat de 80 de milioane de dolari în 2022.
Motivul pentru care aceste erori persistă este că pot implica interacțiuni neașteptate cu coduri împrăștiate în întregul contract inteligent, uneori chiar și în diferite contracte inteligente. codul necesar.
În plus, aceste interacțiuni sunt adesea dificil de testat automat și sistematic.
TLA+: Exterminatorul
Introduceți Logica temporală a acțiunilor (TLA+), un limbaj pentru specificarea și validarea sistemelor complexe TLA+ nu numai că găsește erori, ci și verifică existența acestora.
Cum este posibil acest lucru, vă întrebați? TLA+ vine cu un set de instrumente pentru verificarea formală ușoară sub formă de așa-numită verificare a modelului. Prin verificarea modelului, explorează în mod exhaustiv toate interacțiunile concurente posibile ale modelului de cod - zonele care sunt dificil de testat - și găsește erori.
Imaginați-vă un exterminator care luminează fiecare colț pentru a expune și a elimina dăunătorii nedoriți care se ascund în acele colțuri întunecate care sunt adesea ratate sau ignorate. Important este că, după ce modelul de cod este construit, verificarea modelului nu necesită aproape nicio intervenție umană pentru a rula, ceea ce îl face extrem de rentabil.
Pentru a ilustra cu câteva cifre inventate: dacă practicile standard din industrie, cum ar fi testarea și revizuirile de securitate elimină 80% dintre erori, iar verificarea formală „grea” elimină 99%, utilizarea TLA+ elimină 90% cu doar un număr mic de eforturi de verificare grele.
Calculatoare TLA+ și Internet
Echipa noastră de ingineri folosește TLA+ pentru a analiza toate aspectele informatice pe internet, inclusiv contractele inteligente critice pentru securitate care rulează pe platformă. Deși computerele Ethereum și Internet au modele de execuție diferite, erorile de reintrare pot apărea în contractele inteligente pe ambele blockchain-uri.
De fapt, datorită debitului său mare, computerele de pe internet permit apeluri simultane multiple către un singur contract inteligent, ceea ce impune ca autorii de contracte inteligente să fie mai atenți la eliminarea interacțiunilor concurente nedorite. Deoarece securitatea este esențială pentru succesul computerelor de pe Internet, TLA+ este utilizat în multe contracte inteligente pentru a detecta erorile în timpul fazei de dezvoltare.
Un container de analiză TLA+ (contracte inteligente pentru calculatoare de pe internet) a fost realizat recent pe noul lansat Chain-Key Bitcoin (ckBTC), ale cărui rezultate le voi împărtăși mai jos.
contract inteligent ckBTC
Pentru a vorbi despre analiza TLA+ a ckBTC, să începem cu o prezentare generală la nivel înalt a ckBTC. ckBTC este un token nativ pentru computer de internet susținut în siguranță de Bitcoin (BTC) într-un raport de 1:1.
Registrul ckBTC este un contract inteligent de container pe blockchain-ul computerelor de pe Internet care urmărește cât de mult ckBTC deține fiecare utilizator final. Același registru le permite utilizatorilor finali să-și transfere ckBTC către alți utilizatori finali mai rapid și mai ieftin decât transferul BTC în rețeaua Bitcoin.
Pentru a converti ckBTC în BTC și înapoi, utilizatorii finali interacționează cu un alt contract inteligent, ckBTC minter.
La un nivel înalt, operația de conversie din BTC în ckBTC arată astfel:
Pași pentru a obține ckBTC:
1. Utilizatorul final transferă mai întâi unele BTC către o adresă de depozit Bitcoin specifică utilizatorului, toate adresele de depozit sunt controlate complet de codul containerului inteligent ckBTC minter datorită semnăturii ECDSA a cheii de lanț, care creează un nou UTXO deținut de depozit abordare;
2. Utilizatorul final notifică contractul inteligent ckBTC mint despre noul UTXO depus, solicitând monetării să actualizeze soldul utilizatorului;
3. Contractul inteligent minter folosește apoi integrarea Bitcoin a computerelor de pe internet pentru a prelua toate UTXO-urile deținute de adresa de depozit controlată de minter, dar specifică utilizatorului lista de contabilitate internă a UTXO-urilor pe care le-a procesat;
4. În cele din urmă, minterul instruiește registrul să bată ckBTC noi pentru toate UTXO-urile noi într-un raport de 1:1 și, odată finalizat, adaugă UTXO-urile nou descoperite la lista UTXO-urilor procesate.
Disclaimer: Procesul de mai sus omite procesul KYT (Know Your Transaction) pentru simplitate.
Contractul inteligent ckBTC îndeplinește TLA+
Imaginea la nivel înalt prezentată mai sus ascunde de fapt o problemă subtilă de concurență, iar vestea bună este că putem detecta problema folosind setul de instrumente TLA+.
Dar înainte ca TLA+ să poată detecta ceva, trebuie mai întâi să îi oferim două lucruri:
Creați un model al sistemului nostru folosind limbajul TLA+
Specificați proprietățile TLA+ pe care ne așteptăm să le implementeze sistemul
Acest model este o versiune simplificată, dar încă complet definită a sistemului, care în cazul nostru include contractul minter smart, dar și toate celelalte părți relevante ale sistemului, și anume contractul registru și rețeaua Bitcoin.
Pentru fiecare componentă, modelăm starea acesteia și modul în care acțiunile relevante pe care le-ar putea întreprinde un utilizator final (adică transferul BTC sau ckBTC, depunerea BTC sau apelarea diferitelor acțiuni expuse de minter) schimbă starea.
Toate aceste elemente sunt oarecum simplificate în model, cu părți pe care analiza se concentrează (de exemplu, codul minter) modelate mai detaliat, în timp ce alte părți (de exemplu, rețeaua Bitcoin) sunt modelate mai puțin detaliat, de fapt, un model TLA+ este similar cu o specificație de proiectare detaliată a unui sistem.
În mod intuitiv, principala caracteristică pe care dorim să o implementăm este să ne asigurăm că ckBTC este pe deplin acceptat. Cu alte cuvinte, niciun utilizator final nu ar trebui să poată „cheltui dublu” BTC-ul depus pentru a obține mai mult ckBTC decât a depus.
Dar pentru a analiza o astfel de proprietate, trebuie să facem această intuiție foarte precisă, exprimând-o formal în limbajul TLA+. Definiția noastră formală este că oferta totală de ckBTC (adică, suma tuturor soldurilor ckBTC ale utilizatorului final, așa cum sunt stocate de registrul ckBTC) nu depășește cantitatea totală de BTC controlată de containerul de batere (adică, valoarea tuturor UTXO deținute de o adresă de depozit) .
Detectați și rezolvați problemele
Odată ce am creat modelul și proprietățile, setul de instrumente TLA+ poate analiza modelul. Pentru a rula analiza, definim mai întâi setările pentru rularea analizei. De exemplu, configurația noastră pentru ckBTC include doar doi utilizatori finali diferiți și o cantitate mică din oferta totală de Bitcoin (de exemplu, 5 satoshis).
Deși această setare este foarte limitată, studiile empirice arată că marea majoritate a problemelor din sistemele informatice pot fi întâlnite într-un număr mic de entități. Configurația mică permite analizei să exploreze în mod sistematic toate secvențele de acțiuni posibile definite de model și să verifice dacă proprietățile prescrise sunt valabile în orice astfel de secvență.
În plus, analiza rulează complet automat, adică nu necesită nicio intervenție umană și, dacă aceste proprietăți nu sunt valabile, ne oferă secvența exactă a operațiunilor care încalcă acea proprietate.
De exemplu, analiza poate dezvălui că putem încălca proprietatea noastră „fără ckBTC nesecurizat” într-un scenariu precum cel din imaginea de mai jos:
Aici:
Utilizatorii finali depun BTC, la fel ca înainte;
Cu toate acestea, acum utilizatorul final îi instruiește apoi minterului ckBTC să actualizeze soldul de două ori în succesiune rapidă, iar pe un computer de internet aceste actualizări pot fi interacționate cu alte contracte inteligente simultan;
Două actualizări care rulează simultan solicită rețelei Bitcoin toate UTXO-urile depuse de utilizatorul final și ambele primesc ca răspuns același UTXO depus la pasul 1. Deoarece UTXO-ul nu este încă în lista „procesate”, ambele actualizări Cred că UTXO este nou;
Ambele actualizări indică registrului contabil să bată cantitatea corespunzătoare de ckBTC la pasul 4.
Prin urmare, la sfârșitul pasului 4, ne aflăm într-o stare în care oferta ckBTC este de două ori mai mare decât suma UTXO-urilor din adresele de depozit, ceea ce încalcă proprietatea noastră „fără ckBTC neacceptat”.
Rețineți că această eroare apare numai deoarece actualizările soldului utilizatorului final sunt executate concomitent - este de fapt o eroare de reintrare în același stil ca și cea care a dat jos DAO.
O modalitate de a rezolva această problemă este de a preveni rularea în paralel a actualizărilor de sold pentru același utilizator final. Putem face acest lucru prin care minter-ul să stocheze utilizatorul final într-o listă de utilizatori „blocat” atunci când începe actualizarea soldului și să le păstrăm acolo. pe durata listei de actualizare pentru a realiza acest lucru.
Dacă utilizatorul final încearcă să inițieze o altă actualizare concomitentă a soldului, actualizarea va verifica mai întâi și va găsi acest utilizator final specific în lista de utilizatori blocați, apoi va anula.
Rețineți că simplificăm puțin atacul aici: blocarea este de fapt un model destul de comun pentru contractele inteligente IC, iar mintorii ckBTC l-au implementat de la început. Cu toate acestea, blocarea executată incorect deschide ușa atacurilor de mai sus, pe care TLA+ este capabil să le detecteze.
În plus, am găsit câteva cazuri limită care au încălcat „fără ckBTC neacceptat” și alte proprietăți importante și, odată ce am aplicat toate remediile, TLA+ a putut să verifice și să confirme că nu au mai existat încălcări ale proprietăților în configurația definită.
Ar trebui să utilizați TLA+ pentru contractele dvs. inteligente?
Absolut! Bine, bine, poate ar trebui să ofer un răspuns mai nuanțat, pe care echipa noastră de cercetare și dezvoltare îl folosește pentru contracte inteligente critice pe computerele de pe internet ori de câte ori este implicată o concurență netrivială.
De exemplu, analiza TLA+ a descoperit erori subtile de concurență în Internet Computer Governance and Ledger Containers care au fost omise în analizele manuale anterioare de securitate și ar fi putut duce la probleme, cazuri și puncte semnificative - TLA+ a jucat un rol esențial în descoperirea unor astfel de probleme spinoase O explozie absolută.
Desigur, există un preț de plătit în ceea ce privește dobândirea de know-how și apoi construirea modelului, dar empiric prețul este rezonabil, mai ales având în vedere natura cu mize mari a securității blockchain.
Nu trebuie să fii intimidat de limbajul TLA+ în sine, în ciuda numelui intimidant, accesarea funcțiilor sale puternice este destul de simplă. De fapt, o foaie de cheat TLA+ care descrie aproape toate caracteristicile TLA+ ar putea încadra aproximativ pe o pagină:
mbt.informal.systems/docs/tla_basics_tutorials/tla+cheatsheet.html
În plus, efortul necesar pentru a construi modelul este comparabil cu revizuirile manuale standard de securitate. De exemplu, pentru un minter ckBTC, ar dura în total aproximativ 3 săptămâni pentru ca o persoană să înțeleagă designul, să creeze modelul inițial și proprietățile.
Modelul TLA+ rezultat este mult mai simplu decât implementarea, atât pentru că este mai simplu decât codul, cât și datorită naturii de nivel înalt a TLA+. Modelul pentru minterul ckBTC necesită aproximativ 250 de linii de cod în comparație cu miile de linii de implementare Rust. Poate în mod surprinzător, una dintre cele mai grele părți în ceea ce privește efortul este specificarea proprietăților necesare, deoarece adesea se găsesc lacune în specificațiile intuitive.
Odată ce modelul este complet, analiza (verificarea modelului) este finalizată automat. Analiza poate dura mult timp pentru a rula – de exemplu, pentru ckBTC, a durat peste 20 de ore. În cele din urmă, un alt beneficiu al TLA este că modelarea și analiza pot fi făcute în faza de proiectare înainte de implementarea codului, ceea ce ajută la eliminarea refactorizărilor mari din cauza erorilor de proiectare mai târziu.
Unde TLA+ este inutil
Pe partea negativă, TLA+ este mai puțin util pentru programele secvențiale complexe, spre deosebire de programele concurente și, de asemenea, nu este bun la gestionarea protocoalelor criptografice complexe, pentru care există alte instrumente (de exemplu, Tamarin) care sunt mai utile.
În cele din urmă, există problema menținerii modelului TLA+ și implementării efective în sincronizare, deoarece codul de implementare evoluează în timp, este posibil să nu se mai conformeze modelului, ceea ce poate fi dificil de prins fără suport de scule.
De fapt, echipa noastră de cercetare și dezvoltare încearcă să rezolve această problemă – sper să vă putem împărtăși câteva instrumente în curând!
Sper că această prezentare generală v-a trezit interesul pentru utilizarea TLA+ pentru propriile dvs. contracte inteligente critice și, dacă da, rămâneți la curent - o postare ulterioară cu un tutorial mai aprofundat despre cum să utilizați TLA+ pentru contractele inteligente va apărea în curând, și Atașat este un model real TLA+ dezvoltat de echipa noastră de cercetare și dezvoltare.
Conținutul IC la care îți pasă
Progresul tehnologiei |. Evenimente globale
Colectați și urmăriți canalul IC Binance
Fiți la curent cu cele mai recente informații