Acest articol a fost trimis de un membru al comunității. Autorul este David Tarditi, Vicepreședinte de inginerie la CertiK, o firmă de audit al contractelor inteligente Web3.
TL;DR
Verificarea formală a contractelor inteligente asigură că acestea nu prezintă erori, vulnerabilități și alte comportamente neintenționate. Aceasta presupune că un expert uman transcrie logica contractului inteligent sub formă de expresii matematice, apoi le rulează printr-un proces automat care verifică această logică în comparație cu modelele de comportament estimate ale contractului. Combinația dintre verificarea formală și auditarea manuală oferă o evaluare completă a securității unui contract inteligent.
Introducere
Contractele inteligente sunt programe informatice stocate pe un blockchain, care sunt rulate automat atunci când sunt îndeplinite anumite condiții. Acestea pot varia de la contracte simple la extrem de complexe și pot conține active în valoare de milioane sau chiar miliarde de dolari.
Vulnerabilitățile de securitate din codul unui contract inteligent pot avea consecințe devastatoare, inclusiv furtul tuturor activelor conținute de un contract inteligent. În 2021, makerului automat pe piață (AMM) Uranium Finance i s-au furat 50 de milioane de dolari din cauza unei singure greșeli de scriere dintr-un contract inteligent.
Tot în 2021, Compound Finance a oferit recompense care nu fuseseră de fapt câștigate, în valoare 80 de milioane de dolari, din cauza unui singur caracter greșit. În 2022, 320 de milioane de dolari au fost furate de la Wormhole Bridge din cauza unei erori în unul dintre contractele sale inteligente.
Este important ca programul contractului inteligent să fie scris corect de la început. Contractele inteligente sunt cu sursă deschisă, ceea ce înseamnă că codul este disponibil public odată ce un contract este implementat. Dacă un hacker găsește o eroare, poate profita imediat de ea. În plus, corectarea vulnerabilităților de securitate în timp nu este o opțiune, deoarece codul unui contract inteligent nu poate fi modificat, de obicei, după implementare.
Cum funcționează verificarea contractelor inteligente?
Verificarea formală a contractelor inteligente funcționează prin prezentarea logicii și a comportamentului vizat al contractelor inteligente sub formă de expresii matematice. Auditorii folosesc apoi instrumente automate pentru a verifica dacă aceste expresii sunt corecte.
Procesul presupune:
Definirea specificațiilor și proprietăților vizate ale unui contract în limbaj formal.
Traducerea codului contractului într-o reprezentare formală, cum ar fi modele matematice sau logice.
Folosirea programelor automate de verificare a teoremelor sau a verificatorilor de model pentru a valida specificațiile și proprietățile contractului.
Repetarea procesului de verificare pentru a găsi și remedia orice erori sau abateri de la proprietățile vizate.
De ce este importantă verificarea contractelor inteligente?
Utilizarea raționamentului matematic asigură că contractele inteligente verificate formal nu prezintă erori, vulnerabilități și alte comportamente neintenționate. De asemenea, ajută la sporirea încrederii în contract, deoarece s-a dovedit în mod riguros că proprietățile acestuia sunt corecte.
Mai jos sunt câteva exemple despre modul în care verificarea contractelor inteligente a ajutat la prevenirea pierderilor financiare semnificative și a altor rezultate dezastruoase.
Uniswap
Uniswap este un AMM foarte cunoscut. Când a fost dezvoltat contractul inteligent Uniswap V1, acesta a fost verificat formal. Înainte de lansarea sa, această verificare formală a găsit și a remediat erori de rotunjire care ar fi putut duce la epuizarea fondurilor Uniswap V1.
Balancer
Balancer V2 este un alt AMM care a fost verificat formal. Verificarea formală a identificat și a remediat în contractul inteligent un calcul incorect al taxelor pentru împrumuturile rapide, ceea ce ar fi putut face bursa vulnerabilă la furt.
SafeMoon
SafeMoon V1 conținea o eroare subtilă identificată prin verificare formală după implementare. Un proprietar putea să renunțe la dreptul de proprietate asupra contractului și apoi să reintre în posesia acestuia, dacă efectua anumite operațiuni înainte de a renunța la dreptul de proprietate.
Această eroare nu a fost observată în majoritatea auditurilor manuale ale bifurcațiilor SafeMoon V1, deoarece găsirea sa a necesitat analizarea unor combinații specifice de valori ale variabilelor programului. Este o eroare care le poate scăpa cu ușurință oamenilor, dar este ușor de găsit de către o mașină.
Cum funcționează împreună verificarea formală și auditul manual
Verificarea formală oferă o modalitate sistematică și automată de a verifica logica și comportamentul unui contract prin comparație cu proprietățile vizate. Acest lucru facilitează identificarea și remedierea eventualelor erori sau greșeli. Este utilă în special pentru a identifica probleme complexe și subtile, care pot fi dificil de detectat prin inspecție manuală.
Auditul manual implică examinarea de către experți a codului, designului și implementării unui contract. Auditorul își folosește experiența și cunoștințele pentru a identifica riscurile de securitate și pentru a evalua situația generală de securitate a contractului. De asemenea, acesta poate confirma că procesul de verificare formală a fost efectuat corect și poate verifica eventualele probleme care ar putea să nu fie detectate de instrumentele automate.
Combinația dintre verificarea formală și auditarea manuală oferă o evaluare complexă și amănunțită a securității unui contract inteligent. Acest lucru crește șansele de a găsi și remedia orice vulnerabilități. Rezultatul este o abordare de apărare în profunzime a securității, care valorifică capacitățile unice atât ale oamenilor, cât și ale mașinilor.
Gânduri de încheiere
Pentru a asigura securitatea contractelor inteligente, este esențial să se utilizeze atât verificarea formală, cât și auditul manual pentru o evaluare completă și amănunțită a securității unui contract inteligent.
În timp ce verificarea formală poate consuma multe resurse, este o investiție care merită în cazul contractelor cu valoare ridicată sau cu factori de risc ridicat. Nu în ultimul rând, prioritizarea securității și asigurarea faptului că contractele inteligente nu prezintă erori, vulnerabilități și comportament neintenționat este vitală.
Materiale suplimentare
Declinarea responsabilității și avertismentul privind riscurile: acest conținut vă este prezentat „ca atare” numai pentru informații generale și în scopuri educaționale, fără a oferi declarații sau garanții de niciun fel. Nu trebuie interpretat ca sfat financiar și nu reprezintă o recomandare de achiziționare a unui anumit produs sau serviciu. Prețurile activelor digitale pot fi volatile. Valoarea investiției dvs. poate scădea sau crește și este posibil să nu primiți înapoi suma investită. Sunteți sigura persoană responsabilă pentru propriile decizii de investiții, iar Academia Binance nu este responsabilă pentru eventualele pierderi suferite. Acest material nu ar trebui interpretat ca o recomandare financiară.