Šis straipsnis yra bendruomenės pasiūlymas. Jo autorius – David Tarditi, Web3 išmaniųjų sandorių audito įmonės CertiK inžinerijos viceprezidentas.
TL;DR
Formalus išmaniųjų sandorių patvirtinimas užtikrina, kad juose nebūtų klaidų, pažeidžiamumų ir kitų nenumatytų dalykų. Ekspertas pateikia išmaniojo sandorio logiką kaip matematinius teiginius, o tada vykdo juos per automatizuotą procesą, kurio metu tikrinama jų logika ir lyginama su sandorio numanomos elgsenos modeliais. Formalaus patvirtinimo ir rankinio audito kombinacija padeda išsamiai įvertinti išmaniojo sandorio saugumą.
Įvadas
Išmanieji sandoriai – kompiuterinės programos, įdiegtos blokų grandinėje ir paleidžiamos automatiškai, įvykdžius tam tikras sąlygas. Jie gali būti tiek paprasti, tiek sudėtingi ir gali apimti milijonų ar net milijardų dolerių vertės turtą.
Išmaniojo sandorio kodo saugumo spragos gali turėti pražūtingų pasekmių, pvz., gali būti pavogtas visas turtas, susijęs su išmaniuoju sandoriu. 2021 m. iš automatizuoto rinkos kūrėjo (AMM) „Uranium Finance“ pavogta 50 mln. USD suma dėl vienos išmaniojo sandorio rašybos klaidos.
Taip pat 2021 m. „Compound Finance“ skyrė 80 mln. USD nepelnytą atlygį dėl vieno simbolio klaidos. 2022 m. iš „Wormhole Bridge“ pavogta 320 mln. USD dėl klaidos viename iš išmaniųjų sandorių.
Svarbu išmaniojo sandorio programą nustatyti teisingai iš pirmo karto. Išmanieji sandoriai yra atvirojo kodo, o tai reiškia, kad kodas yra viešai prieinamas, kai sutartis įdiegiama. Jei įsilaužėlis aptinka klaidą, jis gali iškart ja pasinaudoti. Be to, laikui bėgant negalima pataisyti saugos spragų, nes įdiegto išmaniojo sandorio kodo paprastai negalima pakeisti.
Kaip veikia išmaniojo sandorio patvirtinimas?
Formalus išmaniųjų sandorių patvirtinimas veikia pateikiant išmaniųjų sandorių logiką ir pageidaujamą elgesį kaip matematinius teiginius. Tada auditoriai automatiniais įrankiai tikrina, ar šie teiginiai yra teisingi.
Procesas apima:
Sutarties specifikacijų ir pageidaujamų savybių apibrėžimą formalia kalba.
Sutarties kodo formalų atvaizdavimą, pvz., matematiniais modeliais ar logika.
Automatinių teoremų arba modelių tikrinimo priemonių naudojimą sutarties specifikacijoms ir savybėms patvirtinti.
Patvirtinimo procesą kartojimą, siekiant surasti ir ištaisyti visas klaidas ar nukrypimus nuo norimų savybių.
Kodėl svarbu patvirtinti išmanųjį sandorį
Matematinių samprotavimų naudojimas padeda užtikrinti, kad formaliai patvirtintuose išmaniuosiuose sandoriuose nebūtų klaidų, pažeidžiamumų ir kito nenumatyto elgesio. Tvirtai įrodžius, kad sandorio savybės teisingos, taip pat galima padidinti pasitikėjimą sandoriu.
Toliau pateikiami keli pavyzdžiai, kaip išmaniojo sandorio patvirtinimas padėjo išvengti didelių finansinių nuostolių ir kitų pražūtingų padarinių.
Uniswap
Uniswap – gerai žinomas AMM. Sukurtas Uniswap V1 išmanusis sandoris oficialiai patvirtintas. Prieš išleidžiant Uniswap V1, šio oficialaus patvirtinimo metu aptiktos ir ištaisytos apvalinimo klaidos, dėl kurių Uniswap V1 galėjo būti išeikvotos lėšos.
Balancer
Balancer V2 taip pat yra oficialiai patvirtintas AMM. Formalaus patvirtinimo metu aptiktas ir ištaisytas neteisingas mokesčio apskaičiavimas, susijęs su „Flash“ paskolos funkcija išmaniajame sandoryje, dėl kurios biržoje galėjo būti vagysčių.
SafeMoon
SafeMoon V1 turėjo nedidelę klaidą, nustatytą formalaus patvirtinimo metu jau po įdiegimo. Savininkas galėjo atsisakyti nuosavybės teisės į sandorį, o vėliau ją atgauti, jei prieš atsisakant nuosavybės teisės atliko tam tikras operacijas.
Ši klaida praleista atliekant ne vieną neautomatinį SafeMoon V1 išsišakojimų auditą, nes norint ją aptikti reikėjo išanalizuoti konkrečius programos kintamųjų verčių derinius. Žmonės gali to nepastebėti, o mašina aptinka lengvai.
Kaip kartu veikia formalus patvirtinimas ir neautomatinis auditas
Formalus patvirtinimas – sistemingas ir automatizuotas būdas patvirtinti sandorio logiką ir elgesį, palyginti juos su norimomis savybėmis. Taip lengviau nustatyti ir ištaisyti galimas klaidas. Tai ypač naudinga ieškant sudėtingų ir subtilių problemų, kurias gali būti sunku aptikti atliekant neautomatinę patikrą.
Neautomatinis auditas apima ekspertinę sutarties kodo, dizaino ir diegimo patikrą. Naudodamasis savo patirtimi ir žiniomis, auditorius nustato saugumo riziką ir vertina bendrą sandorio saugumo padėtį. Jis taip pat gali patvirtinti, ar formalaus patvirtinimo procesas atliktas teisingai, ir patikrinti, ar nėra problemų, kurių gali neaptikti automatiniai įrankiai.
Formalaus patvirtinimo ir rankinio audito kombinacija suteikia išsamų ir nuoseklų išmaniojo sandorio saugumo įvertinimą. Tai padidina tikimybę rasti ir ištaisyti pažeidžiamumus. Rezultatas – visapusis požiūris į saugumą, išnaudojant unikalias žmonių ir mašinų galimybes.
Baigiamosios mintys
Siekiant užtikrinti išmaniųjų sandorių saugumą, būtina naudoti tiek formalų patvirtinimą, tiek neautomatinį auditą, kad būtų užtikrintas išsamus ir nuodugnus išmaniųjų sandorių saugos padėties įvertinimas.
Nors formalus patvirtinimas gali pareikalauti daug išteklių, tai yra vertinga investicija į didelės vertės arba didelės rizikos sandorius. Galiausiai, labai svarbu teikti pirmenybę saugumui ir užtikrinti, kad išmaniuosiuose sandoriuose nebūtų klaidų, pažeidžiamumų ir nenumatytų dalykų.
Papildoma literatūra
Atsakomybės atsisakymas ir įspėjimas apie riziką: šis turinys jums pateikiamas „toks, koks yra“ tik bendro informavimo ir švietimo tikslais, nesuteikia jokios garantijos ir nieko neteigia. Šis tekstas neturėtų būti suprantamas kaip finansinis patarimas, taip pat nesiekiama rekomenduoti įsigyti kokį nors konkretų produktą ar paslaugą. Skaitmeninių išteklių kainos gali būti nepastovios. Jūsų investicijos vertė gali sumažėti arba padidėti, o investuotos sumos galite ir neatgauti. Tik jūs esate atsakingas už savo investicinius sprendimus, o Binance Academy nėra atsakinga už jokius jūsų patirtus nuostolius. Tai ne finansinis patarimas.