See artikkel on panus kogukonda. Autor on David Tarditi, Web3 nutilepingute audiitorfirma CertiK inseneriosakonna asepresident.
TL;DR
Nutilepingute ametlik kontrollimine tagab, et need ei sisaldaks vigu, haavatavusi ega muud tahtmatut käitumist. See hõlmab seda, et inimekspert esitab nutilepingu loogika matemaatiliste avaldustena, seejärel käitab need automatiseeritud protsessis, mis kontrollib tegelikku loogikat lepingu eeldatava käitumise mudelite suhtes. Ametliku kontrollimise ja käsitsi auditeerimise kombinatsioon annab kõikehõlmava hinnangu nutilepingu turvalisusele.
Sissejuhatus
Nutilepingud on plokiahelas juurutatud arvutiprogrammid, mis käivituvad teatud tingimuste täitmisel automaatselt. Need võivad olla nii lihtsad kui ka väga keerulised ning nende varade väärtus võib ulatuda miljonitesse või isegi miljarditesse dollaritesse.
Nutilepingu koodi turvaaukudel võivad olla laastavad tagajärjed, sealhulgas kõigi nutilepingu poolt hoitavate varade vargus. 2021. aastal varastati automatiseeritud turutegijalt (AMM) Uranium Finance 50 miljonit dollarit nutilepingu ühe kirjavea tõttu.
Samuti andis 2021. aastal Compound Finance ühe tähemärgi vea tõttu välja teenimata preemiaid 80 miljonit dollari eest. 2022. aastal varastati Wormhole'i sillalt 320 miljonit dollarit ühes selle nutilepingus esineva vea tõttu.
On oluline, et nutilepingu programm oleks algusest peale õige. Nutilepingud on avatud lähtekoodiga, mis tähendab, et kood on avalikult kättesaadav, kui leping on kasutusele võetud. Kui häkker leiab vea, saab ta seda kohe ära kasutada. Lisaks ei ole turvaaukude parandamine aja jooksul võimalik, kuna nutilepingu koodi ei saa tavaliselt pärast kasutuselevõttu muuta.
Kuidas toimib nutilepingu kontrollimine?
Nutilepingute ametlik kontrollimine toimib, esitades nutilepingute loogika ja soovitud käitumise matemaatiliste avaldustena. Seejärel kasutavad audiitorid automatiseeritud vahendeid, et kontrollida, kas need avaldused on õiged.
Protsess hõlmab järgmist.
Lepingu spetsifikatsioonide ja soovitud omaduste määratlemine ametlikus keeles.
Lepingu koodi tõlkimine formaalsesse esitusviisi, näiteks matemaatilistesse mudelitesse või loogikasse.
Automaatsete teoreemitõendajate või mudelikontrollijate kasutamine lepingu spetsifikatsioonide ja omaduste valideerimiseks.
Kontrolliprotsessi kordamine, et leida ja parandada kõik vead või kõrvalekalded soovitud omadustest.
Miks on nutilepingu kontrollimine oluline
Matemaatilise arutluse kasutamine aitab tagada, et ametlikult kontrollitud nutilepingud on vabad vigadest, haavatavustest ja muust tahtmatust käitumisest. Samuti aitab see suurendada usaldust ja kindlustunnet lepingu suhtes, kuna selle omadused on rangelt tõestatud.
Allpool on toodud mõned näited sellest, kuidas nutilepingute kontrollimine on aidanud ära hoida märkimisväärset rahalist kahju ja muid katastroofilisi tagajärgi.
Uniswap
Uniswap on hästi tuntud AMM. Kui Uniswap V1 nutileping töötati välja, tehti sellele ametlik kontrollimine. Enne selle välja andmist leiti ja parandati selle ametliku kontrolli käigus ümardamisvigu, mis oleksid võinud põhjustada Uniswap V1 vahendite väljavoolu.
Balancer
Balancer V2 on samuti AMM, mis on ametlikult kontrollitud. Ametlik kontrollimine leidis ja parandas ebaõige tasu arvutamise, mis hõlmas kiirlaenufunktsiooni nutilepingus, mis võis muuta börsi varguse suhtes haavatavaks.
SafeMoon
SafeMoon V1 sisaldas peent viga, mis leiti ametliku kontrollimise käigus pärast selle kasutuselevõttu. Omanikul oli võimalik loobuda lepingu omandiõigusest ja seejärel uuesti omandada, kui enne omandiõigusest loobumist tehti teatavad toimingud.
See viga jäi enamikus SafeMoon V1 harude auditites märkamata, sest selle leidmiseks oli vaja analüüsida konkreetseid programmi muutujate väärtuste kombinatsioone. See on midagi, mida inimestel on lihtne eirata ja mida masinatel on lihtne tähele panna.
Kuidas ametlik kontrollimine ja käsitsi auditeerimine koos toimivad
Ametlik kontrollimine pakub süstemaatilist ja automatiseeritud viisi lepingu loogika ja käitumise kontrollimiseks selle soovitud omaduste suhtes. See lihtsustab võimalike vigade tuvastamist ja parandamist. See on eriti kasulik keeruliste ja peenete probleemide leidmiseks, mida võib olla raske tuvastada käsitsi kontrollimise teel.
Manuaalne auditeerimine hõlmab lepingu koodi, disaini ja kasutuselevõtu eksperthinnangut. Audiitor kasutab oma kogemusi ja eriteadmisi turvariskide tuvastamiseks ja lepingu üldise turvalisuse olukorra hindamiseks. Samuti saavad nad kinnitada, et formaalne ametlik kontrollimisprotsess viidi korrektselt läbi, ja kontrollida probleeme, mida automatiseeritud tööriistad ei pruugi tuvastada.
Ametliku kontrollimise ja käsitsi auditeerimise kombineerimine annab kõikehõlmava hinnangu nutilepingu turvalisusele. See suurendab tõenäosust leida ja parandada kõik haavatavused. Tulemuseks on põhjalik kaitse, mis kasutab nii inimeste kui ka masinate unikaalseid võimeid.
Lõppmärkused
Nutilepingute turvalisuse tagamiseks on oluline kasutada nii ametlikku kontrollimist kui ka käsitsi auditeerimist, et tagada nutilepingu turvalisuse terviklik ja põhjalik hindamine.
Kuigi ametlik kontrollimine võib olla ressursimahukas, on see väärtuslik investeering suure väärtusega või kõrge riskiteguriga lepingute puhul. Lõppkokkuvõttes on esmatähtis seada prioriteediks turvalisus ja tagada, et nutilepingud ei sisaldaks vigu, haavatavusi ega tahtmatut käitumist.
Lisalugemist
Lahtiütlus ja riskihoiatus: seda sisu esitatakse sellisel kujul, nagu see on, ainult üldiseks teabeks ning hariduslikel eesmärkidel, ilma igasuguse esinduse või garantiita. Seda ei tohiks tõlgendada finantsnõustamisena ega kui soovitust konkreetse toote või teenuse ostmiseks. Digitaalsete varade hinnad võivad olla volatiilsed. Sinu investeeringu väärtus võib langeda või tõusta ning sa ei pruugi investeeritud summat tagasi saada. Oma investeerimisotsuste eest vastutad ainult sina ja Binance'i Akadeemia ei vastuta võimalike kahjude eest. Seda materjali ei tohiks tõlgendada kui finantsnõustamist.