Šis ir kopienas iesniegts raksts. Tā autors ir Web3 viedo līgumu revīzijas uzņēmuma CertiK inženierijas viceprezidents Deivids Tarditi (David Tarditi).
TL;DR
Viedo līgumu formālā verifikācija nodrošina, ka tiem nav kļūdu, ievainojamības un citu neparedzētu faktoru. Tās ietvaros cilvēks (eksperts) prezentē viedā līguma loģiku matemātisku apgalvojumu veidā un pēc tam piemēro tiem automatizētu procesu, kura laikā tiek pārbaudīta faktiskā loģika, salīdzinot ar līguma sagaidāmās darbības modeļiem. Apvienojot formālo verifikāciju ar manuālu revīziju, tiek iegūts visaptverošs viedā līguma drošības novērtējums.
Ievads
Viedie līgumi ir blokķēdē saglabātas datorprogrammas, kas pie konkrētiem nosacījumiem automātiski izpilda noteiktas darbības. Tas var būt vienkāršas vai ārkārtīgi sarežģītas un ietvert vairākus miljonus vai pat miljardus dolāru vērtus aktīvus.
Ja viedā līguma kods nav pietiekami aizsargāts, tam var būt graujošas sekas, kas var ietvert pat visu viedajā līgumā glabāto aktīvu nozagšanu. 2021. gadā automatizētajam tirgus veidotājam (AMM) Uranium Finance tika nozagti 50 miljoni USD tikai tāpēc, ka viedajā līgumā bija viena pareizrakstības kļūda.
Tajā pašā 2021. gadā Compound Finance izmaksāja 80 miljonus USD nenopelnītās atlīdzībās vienas kļūdainas rakstzīmes dēļ. 2022. gadā 320 miljoni USD tika nozagti no Wormhole Bridge, jo vienā no tā viedajiem līgumiem bija kļūda.
Ir svarīgi jau pašā sākumā nodrošināt pareizu viedā līguma programmas darbību. Viedie līgumi ir atvērtā pirmkoda risinājumi, kas nozīmē, ka to kods pēc līguma izvietošanas blokķēdē ir publiski pieejams. Ja hakeris atrod kļūdu, tas var nekavējoties izmantot to savā labā. Arī drošības ielāpu uzstādīšana laika gaitā nevar atrisināt situāciju, jo viedo līgumu kods pēc ieviešanas parasti nav maināms.
Kā darbojas viedo līgumu verifikācija?
Viedo līgumu formālā verifikācija notiek, formulējot viedo līgumu loģiku un vēlamo darbību matemātisku apgalvojumu veidā. Pēc tam revidenti, izmantojot automatizētus rīkus, pārbauda šo apgalvojumu pareizību.
Šis process ietver:
Specifikāciju un līguma vēlamo īpašību definēšanu formālā valodā.
Līguma koda pārveidošanu formālā attēlojumā, piemēram, matemātiskos modeļos vai loģikā.
Automatizētu teorēmu vai modeļu pārbaudītāju izmantošanu, lai apstiprinātu līguma specifikācijas un īpašības.
Verifikācijas procesa atkārtošanu, lai atrastu un novērstu jebkādas kļūdas vai novirzes no vēlamajām īpašībām.
Kāpēc ir svarīgi veikt viedo līgumu verifikāciju?
Matemātisku argumentu izmantošana palīdz garantēt, ka formāli verificētiem viedajiem līgumiem nav kļūdu, ievainojamību vai cita veida nevēlamu faktoru. Tā veicina arī uzticēšanos līgumam, jo tā īpašības ir rūpīgi pārbaudītas.
Tālāk ir sniegti daži piemēri tam, kā viedo līgumu verifikācija ir palīdzējusi novērst būtiskus finanšu zaudējumus un citas postošas sekas.
Uniswap
Uniswap ir populārs AMM. Kad tika izstrādāts Uniswap 1. versijas viedais līgums, tas tika formāli verificēts. Pirms līguma ieviešanas veiktajā formālajā verifikācijā tika konstatētas un novērstas noapaļošanas kļūdas, kuru rezultātā no Uniswap 1. versijas platformas būtu bijis iespējams nopludināt līdzekļus.
Balancer
Arī Balancer 2. versija ir AMM, kas tika formāli verificēts. Formālajā verifikācijā tika konstatēts un izlabots nepareizs komisijas maksas aprēķinu mehānisms, kas ietvēra zibaizdevumu funkcionalitāti viedajā līgumā, – tas būtu pakļāvis biržu zādzību riskam.
SafeMoon
SafeMoon 1. versijā bija neliela kļūda, kuru pēc līguma ieviešanas konstatēja formālā verifikācijā. Īpašniekam bija iespēja atteikties no līguma īpašumtiesībām un pēc tam tās atgūt, ja pirms atteikšanās no īpašumtiesībām tika veiktas noteiktas darbības.
Šī kļūda tika palaista garām lielākajā daļā SafeMoon 1. versijas protokola uzlabojumu manuālo revīziju, jo, lai to atrastu, bija jāanalizē programmas mainīgo vērtību noteiktas kombinācijas. Cilvēks to var viegli nepamanīt, bet mašīnai to nav grūti konstatēt.
Kā formālā verifikācija un manuāla revīzija papildina viena otru?
Formālā verifikācija sniedz sistemātisku un automatizētu veidu, kā pārbaudīt līguma loģiku un darbību atbilstoši vēlamajām īpašībām. Tas ļauj vieglāk identificēt un novērst jebkādas iespējamās kļūdas. Īpaši lietderīgi tas ir, meklējot sarežģītas vai grūti pamanāmas problēmas, ko varētu būt grūti identificēt manuālā pārbaudē.
Manuālā revīzijā eksperts pārbauda līguma kodu, struktūru un ieviešanu. Revidents, izmantojot savu pieredzi un zināšanas, cenšas identificēt drošības riskus un novērtēt līguma vispārīgo drošību. Tas var arī apstiprināt, vai formālās verifikācijas process ir veikts pareizi, kā arī pārbaudīt, vai nav tādu kļūdu, ko automatizētie rīki nevarētu konstatēt.
Apvienojot formālo verifikāciju ar manuālu revīziju, tiek iegūts visaptverošs un detalizēts viedā līguma drošības novērtējums. Tas palielina izredzes atrast un novērst jebkādas nepilnības. Rezultātā tiek iegūta padziļināta pieeja drošības aspektu novērtēšanai, izmantojot gan cilvēku, gan mašīnu unikālās iespējas.
Noslēgumā
Lai garantētu viedo līgumu drošību, ir svarīgi izmantot gan formālo verifikāciju, gan manuālo revīziju, tādējādi iegūstot visaptverošu un detalizētu viedā līguma drošības novērtējumu.
Lai gan formālās verifikācijas veikšanai var būt nepieciešami apjomīgi resursi, tas ir lietderīgs ieguldījums līgumiem ar lielu vērtību vai augsta riska faktoriem. Galu galā ir ļoti svarīgi par prioritāti izvirzīt drošību un pārliecināties, ka viedajiem līgumiem nav kļūdu, ievainojamības un citu nevēlamu faktoru.
Turpini lasīt
Atruna un brīdinājums par risku: šis saturs tiek tev nodrošināts nemainītā veidā un ir paredzēts tikai vispārīgai informācijai un izglītojošiem mērķiem; tas neietver nekādus apliecinājumus vai garantijas. Tas nav uzskatāms par finanšu padomu un nav paredzēts kā ieteikums iegādāties kādu konkrētu produktu vai pakalpojumu. Digitālo aktīvu cenas var būt svārstīgas. Tavu ieguldījumu vērtība var samazināties vai pieaugt, kā arī tu vari neatgūt ieguldīto summu. Tu uzņemies pilnu atbildību par saviem ieguldījumu lēmumiem, un Binance Akadēmija neatbild par taviem iespējamajiem zaudējumiem. Šis materiāls nav uzskatāms par finanšu padomu.