Šo rakstu ievietoja kopienas loceklis. Autors ir Deivids Tarditi, Web3 viedo līgumu audita uzņēmuma CertiK inženierzinātņu viceprezidents.
Kopsavilkums
Viedo līgumu formāla pārbaude pasargā tos no kļūdām, ievainojamībām un citiem nelabvēlīgiem apstākļiem. Šajā procesā cilvēku eksperti pārvērš viedā līguma loģiku matemātiskajos paziņojumos un pēc tam izmanto automatizētu procesu, lai pārbaudītu faktisko loģiku salīdzinājumā ar līguma paredzamās darbības modeli. Apvienojot formālo pārbaudi un manuālo auditu, mēs varam veikt visaptverošu viedo līgumu drošības novērtējumu.
Ievads
Viedie līgumi ir blokķēdē izvietotas datorprogrammas, kas automātiski palaižas, kad ir izpildīti noteikti nosacījumi. Viedie līgumi var būt ļoti vienkārši vai ārkārtīgi sarežģīti, un tajos var būt aktīvi miljoniem vai pat miljardu dolāru vērtībā.
Ja viedā līguma kodā ir drošības robi, tam var būt postošas sekas, piemēram, visu noziedznieku rīcībā esošo īpašumu zādzība. 2021. gadā no automatizētā tirgus veidotāja (AMM) Uranium Finance tika nozagti 50 miljoni dolāru, jo viedā līgumā tika pieļauta drukas kļūda.
Arī 2021. gadā Compound Finance kļūdaini piešķīra atlīdzību 80 miljonu dolāru apmērā vienas kodēšanas kļūdas dēļ. 2022. gadā no Wormhole Bridge tika nozagti 320 miljoni dolāru viedā līguma kļūdas dēļ.
Tāpēc ir svarīgi jau no paša sākuma iegūt savu viedo līgumu programmu. Viedie līgumi izmanto atvērtā pirmkoda modeli, kas nozīmē, ka pēc līguma izvietošanas kods tiek publiskots. Ja hakeris atklāj kļūdu, viņš var to nekavējoties izmantot. Turklāt parastā prakse laika gaitā labot drošības ievainojamības ir neefektīva, jo viedo līgumu kodu pēc izvietošanas bieži nevar mainīt.
Kā darbojas viedā līguma verifikācija?
Viedo līgumu formāla pārbaude tiek panākta, uzrādot viedā līguma loģiku un paredzamo 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:
Formālā valodā definējiet līguma specifikācijas un paredzamos raksturlielumus.
Pārvērtiet līguma kodu formālā paziņojumā, piemēram, matemātiskā modelī vai loģikā.
Pārbaudiet līguma specifikācijas un īpašības, izmantojot automātisku teorēmu pierādīšanu vai modeļa pārbaudi.
Atkārtojiet validācijas procesu, lai atrastu un labotu visas kļūdas vai novirzes no paredzamajiem raksturlielumiem.
Kāpēc viedā līguma pārbaude ir svarīga
Izmantojot matemātisko pamatojumu, tas palīdz nodrošināt, ka formāli pārbaudītajos viedajos līgumos nav kļūdu, ievainojamību un citu nelabvēlīgu situāciju. Pārbaude arī palīdz palielināt uzticību līgumam, jo tā īpašības ir rūpīgi pārbaudītas un ir pareizas un uzticamas.
Tālāk sniegtajos piemēros ir izklāstīts, kā viedā līguma pārbaude var palīdzēt novērst ievērojamus finansiālus zaudējumus un citas katastrofālas sekas.
Unswap
Uniswap ir labi zināms AMM. Uniswap V1 viedais līgums izstrādes procesā tika oficiāli pārbaudīts. Pirms izlaišanas šajā oficiālajā pārbaudē tika atrastas un novērstas dažas noapaļošanas kļūdas, kas neļāva Uniswap V1 iztērēt līdzekļus.
Balansētājs
Balancer V2 ir arī pārbaudīta AMM. Formālā pārbaudē tika atklāta un novērsta maksas aprēķināšanas kļūda zibatmiņas aizdevuma funkcijā viedajā līgumā, kas padarīja tirdzniecības platformu neaizsargātu pret zādzībām.
SafeMoon
Pēc SafeMoon V1 ieviešanas tika atklāta ļoti neliela kļūda, ja kļūda netika atklāta, ja līguma īpašnieks ir veicis noteiktas darbības pirms īpašumtiesību atteikšanas, līguma īpašnieks to varētu atgūt pēc atteikšanās no līguma.
Lielākajai daļai SafeMoon V1 dakšas manuālo auditu šī kļūda netiek ņemta vērā, jo, lai to atrastu, ir jāanalizē noteiktas programmas mainīgo vērtību kombinācijas. Cilvēki var viegli palaist garām šo problēmu, bet mašīnas to var savlaicīgi novērst.
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 darbību, salīdzinot ar tā paredzamajām īpašībām. Tādējādi ir vieglāk identificēt un novērst iespējamās kļūdas vai ievainojamības. Tas ir īpaši noderīgi sarežģītām, smalkām problēmām, kuras būtu grūti atklāt, veicot manuālu pārbaudi.
Manuālajā auditā eksperti pārskata kodu, dizainu un līguma izvietošanu. Auditori izmanto savu pieredzi un zināšanas, lai identificētu drošības riskus un novērtētu kopējo līguma drošības stāvokli. Viņi var arī apstiprināt, ka oficiālais verifikācijas process ir veikts pareizi, un pārbaudīt, vai nav problēmu, kuras automatizētie rīki var neatklāt.
Apvienojot formālo pārbaudi un manuālo auditu, mēs varam veikt visaptverošu viedo līgumu drošības novērtējumu. Tas uzlabo ievainojamību atrašanas un novēršanas iespējas. To darot, mēs izmantojam padziļinātu aizsardzības pieeju, kas apvieno cilvēku un mašīnu zināšanas.
Secinājums
Lai nodrošinātu viedo līgumu drošību, ir jāapvieno formāla pārbaude un manuāla auditēšana, lai nodrošinātu visaptverošu un rūpīgu viedo līgumu drošības stāvokļa novērtējumu.
Lai gan formālā pārbaude ir resursietilpīgāka, tā ir vērtīga investīcija līgumiem ar augstu vērtību vai augsta riska faktoriem. Galu galā drošība ir svarīgāka par visu citu. Noteikti piešķiriet drošībai prioritāti un nodrošiniet, lai viedos līgumos nebūtu kļūdu, ievainojamību un nevēlamu neparedzētu darbību.
Tālāka lasīšana
Kas ir viedais līgums?
Kas ir vieda līgumu drošības audits?
Atruna un brīdinājums par risku: šī raksta saturs ir fakti un ir paredzēts tikai vispārīgai informācijai un izglītojošiem nolūkiem, un tas nav uzskatāms par apliecinājumu vai garantiju. Šis raksts nav jāuztver kā finanšu padoms, un tajā nav ieteikts iegādāties kādu konkrētu produktu vai pakalpojumu. Digitālo aktīvu cenas var svārstīties. Jūsu ieguldījuma vērtība var gan kristies, gan pieaugt, un jūs, iespējams, neatgūsit ieguldīto pamatsummu. 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. Šis materiāls nav uzskatāms par finanšu konsultāciju.
