Mis on nutilepingute ametlik kontrollimine?
Avaleht
Artiklid
Mis on nutilepingute ametlik kontrollimine?

Mis on nutilepingute ametlik kontrollimine?

EdasijÔudnud
Avaldatud Mar 2, 2023VĂ€rskendatud Jul 12, 2023
5m

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.

  1. Lepingu spetsifikatsioonide ja soovitud omaduste mÀÀratlemine ametlikus keeles.

  2. Lepingu koodi tÔlkimine formaalsesse esitusviisi, nÀiteks matemaatilistesse mudelitesse vÔi loogikasse.

  3. Automaatsete teoreemitÔendajate vÔi mudelikontrollijate kasutamine lepingu spetsifikatsioonide ja omaduste valideerimiseks.

  4. 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.