Šis raksts ir kopienas iesniegums. Autors ir Deivids Tarditi, Web3 viedo līgumu auditorfirmas CertiK inženierzinātņu viceprezidents.
Šajā rakstā sniegtie viedokļi ir līdzstrādnieka/autora skatījumi, un tie ne vienmēr atspoguļo Binance akadēmijas viedokļus.
TL;DR
Viedo līgumu formāla pārbaude nodrošina, ka tajos nav kļūdu, ievainojamību un citas neparedzētas darbības. Tas ietver cilvēku ekspertu, kurš parāda viedā līguma loģiku kā matemātiskus paziņojumus, pēc tam izpilda tos, izmantojot automatizētu procesu, kas pārbauda faktisko loģiku, salīdzinot ar līguma paredzamās darbības modeļiem. Formālās verifikācijas un manuālās auditēšanas kombinācija nodrošina visaptverošu viedā līguma drošības novērtējumu.
Ievads
Viedie līgumi ir datorprogrammas, kas izvietotas blokķēdē un darbojas automātiski, kad ir izpildīti noteikti nosacījumi. Tie var būt no vienkāršiem līdz ārkārtīgi sarežģītiem, un tajos var būt aktīvi miljoniem vai pat miljardu dolāru vērtībā.
Viedā līguma koda drošības ievainojamībai var būt postošas sekas, tostarp visu viedā līguma aktīvu zādzība. 2021. gadā automatizētajam tirgus veidotājam (AMM) Uranium Finance tika nozagti 50 miljoni ASV dolāru, jo viedajā līgumā tika pieļauta viena drukas kļūda.
Arī 2021. gadā uzņēmums Compound Finance piešķīra nenopelnīto atlīdzību 80 miljonu dolāru apmērā vienas rakstzīmes kļūdas dēļ. 2022. gadā no Wormhole tilta tika nozagti 320 miljoni USD, jo vienā no tā viedajiem līgumiem bija kļūda.
Ir svarīgi, lai viedā līguma programma būtu pareiza pirmajā reizē. Viedie līgumi ir atvērtā pirmkoda, kas nozīmē, ka kods ir publiski pieejams, tiklīdz līgums ir izvietots. Ja hakeris atrod kļūdu, viņš var nekavējoties to izmantot. Turklāt laika gaitā nav iespējams labot drošības ievainojamības, jo viedā līguma kodu parasti nevar mainīt pēc izvietošanas.
Kā darbojas viedā līguma pārbaude?
Viedo līgumu formāla pārbaude darbojas, uzrādot viedo līgumu loģiku un vēlamo uzvedību kā matemātiskus paziņojumus. Pēc tam auditori izmanto automatizētus rīkus, lai pārbaudītu, vai šie apgalvojumi ir pareizi.
Process ietver:
Līguma specifikāciju un vēlamo īpašību definēšana formālā valodā.
Līguma koda tulkošana formālā attēlojumā, piemēram, matemātiskajos modeļos vai loģikā.
Izmantojot automatizētus teorēmu pārbaudītājus vai modeļu pārbaudītājus, lai apstiprinātu līguma specifikācijas un īpašības.
Verifikācijas procesa atkārtošana, lai atrastu un labotu visas kļūdas vai novirzes no vēlamajiem rekvizītiem.
Kāpēc vieda līguma pārbaude ir svarīga?
Matemātiskā pamatojuma izmantošana palīdz nodrošināt, ka formāli pārbaudītos viedos līgumos nav kļūdu, ievainojamību un citas neparedzētas darbības. Tas arī palīdz palielināt uzticību līgumam, jo ir stingri pierādīts, ka tā īpašības ir pareizas.
Tālāk ir sniegti daži piemēri, kā viedā līguma pārbaude ir palīdzējusi novērst ievērojamus finansiālus zaudējumus un citus postošus rezultātus.
Unswap
Uniswap ir labi zināms AMM. Kad Uniswap V1 viedais līgums tika izstrādāts, tas tika oficiāli pārbaudīts. Pirms tā izlaišanas šajā oficiālajā pārbaudē tika atrastas un novērstas noapaļošanas kļūdas, kuru dēļ Uniswap V1 varēja tikt iztērēti līdzekļi.
Balansētājs
Balancer V2 ir arī oficiāli verificēta AMM. Formālā pārbaudē tika atrasts un izlabots nepareizs maksas aprēķins, kas viedajā līgumā ietver zibatmiņas aizdevuma funkcionalitāti, kas varēja padarīt biržu neaizsargātu pret zādzībām.
SafeMoon
SafeMoon V1 ietvēra smalku kļūdu, kas tika atklāta oficiālas pārbaudes laikā pēc tā izvietošanas. Īpašniekam bija iespēja atteikties no līguma īpašumtiesībām un pēc tam to atgūt, ja pirms atteikšanās no īpašumtiesībām tika veiktas noteiktas darbības.
Šī kļūda tika izlaista lielākajā daļā SafeMoon V1 dakšu manuālo auditu, jo, lai to atrastu, bija jāanalizē noteiktas programmas mainīgo vērtību kombinācijas. Tas ir kaut kas tāds, ko cilvēki var viegli palaist garām, bet mašīna to var viegli uztvert.
Kā formālā pārbaude un manuālā auditēšana darbojas kopā
Formālā pārbaude nodrošina sistemātisku un automatizētu veidu, kā pārbaudīt līguma loģiku un uzvedību, salīdzinot ar tā vēlamajām īpašībām. Tādējādi ir vieglāk identificēt un novērst iespējamās kļūdas vai kļūdas. Tas ir īpaši noderīgi, lai atrastu sarežģītas un smalkas problēmas, kuras var būt grūti noteikt, veicot manuālu pārbaudi.
Manuālā auditēšana ietver līguma koda, dizaina un izvietošanas ekspertu pārbaudi. Revidents izmanto savu pieredzi un zināšanas, lai identificētu drošības riskus un novērtētu līguma vispārējo drošības stāvokli. Viņi var arī apstiprināt, ka oficiālais verifikācijas process tika veikts pareizi, un pārbaudīt, vai nav problēmu, ko nevar noteikt ar automatizētiem rīkiem.
Apvienojot formālu verifikāciju un manuālu auditu, tiek nodrošināts visaptverošs un rūpīgs viedā līguma drošības novērtējums. Tas palielina iespēju atrast un novērst jebkādas ievainojamības. Rezultāts ir padziļināta aizsardzības pieeja drošībai, kas izmanto gan cilvēku, gan mašīnu unikālās iespējas.
Noslēguma domas
Lai nodrošinātu viedo līgumu drošību, ir svarīgi izmantot gan formālu verifikāciju, gan manuālu auditu, lai nodrošinātu visaptverošu un rūpīgu viedo līgumu drošības stāvokļa novērtēšanu.
Lai gan formāla pārbaude var būt resursietilpīga, tā ir vērtīgs ieguldījums līgumiem ar augstu vērtību vai augsta riska faktoriem. Galu galā ir ļoti svarīgi noteikt drošības prioritāti un nodrošināt, ka viedos līgumos nav kļūdu, ievainojamību un neparedzētas darbības.
Tālāka lasīšana
Kas ir viedie līgumi?
Kas ir viedā līguma drošības audits?
Atruna un brīdinājums par risku: šis saturs jums tiek piedāvāts “tāds, kāds ir” tikai vispārīgas informācijas un izglītošanas nolūkos, bez jebkāda veida pārstāvniecības vai garantijas. To nevajadzētu interpretēt kā finansiālu, juridisku vai citu profesionālu padomu, kā arī tas nav paredzēts, lai ieteiktu iegādāties kādu konkrētu produktu vai pakalpojumu. Jums jālūdz savs padoms no atbilstošiem profesionāliem konsultantiem. Ja rakstu ir pievienojis trešās puses līdzautors, lūdzu, ņemiet vērā, ka šie paustie viedokļi pieder trešās puses līdzautoram un ne vienmēr atspoguļo Binance Academy uzskatus. Lūdzu, izlasiet mūsu pilno atrunu šeit, lai iegūtu sīkāku informāciju. Digitālo aktīvu cenas var būt nepastāvīgas. Jūsu ieguldījuma vērtība var samazināties vai pieaugt, un jūs, iespējams, neatgūsit ieguldīto summu. Jūs esat pilnībā atbildīgs par saviem ieguldījumu lēmumiem, un Binance Academy nav atbildīgs par jebkādiem zaudējumiem, kas jums var rasties. Šo materiālu nevajadzētu uzskatīt par finansiālu, juridisku vai citu profesionālu padomu. Lai iegūtu papildinformāciju, skatiet mūsu lietošanas noteikumus un brīdinājumu par risku.
