Tämä artikkeli on yhteisön lähettämä. Kirjoittaja on David Tarditi, joka on VP of Engineering Web3-älysopimusten auditointiyrityksessä CertiKissä.
Tiivistelmä
Älysopimusten muodollisella varmennuksella voidaan varmistaa, että niissä ei ole virheitä tai haavoittuvuuksia ja että ne eivät sisällä muuta tahatonta käyttäytymistä. Siinä ihmisasiantuntija esittää älysopimuksen logiikan matemaattisina lausekkeina ja vie ne sitten läpi automatisoidun prosessin, joka tarkistaa todellisen logiikan sopimuksen odotetun käyttäytymisen mallien perusteella. Muodollisen varmennuksen ja manuaalisen auditoinnin yhdistelmä tarjoaa kattavan arvion älysopimuksen turvallisuudesta.
Johdanto
Älysopimukset ovat lohkoketjussa käyttöön otettuja tietokoneohjelmia, jotka toimivat automaattisesti, kun tietyt ehdot täyttyvät. Ne voivat vaihdella yksinkertaisista erittäin monimutkaisiin, ja ne voivat hallita miljoonien tai jopa miljardien dollarien arvoisia varoja.
Älysopimuskoodin tietoturvahaavoittuvuuksilla voi olla tuhoisia seurauksia, mukaan lukien kaikkien älysopimuksen hallitsemien omaisuuserien varkaus. Vuonna 2021 automatisoidulta markkinatakaajalta (AMM) Uranium Financelta varastettiin 50 miljoonaa dollaria yhden älysopimuksessa olleen kirjoitusvirheen vuoksi.
Myös vuonna 2021 Compound Finance jakoi 80 miljoonan dollarin edestä ansaitsemattomia palkkioita yhden merkkivirheen vuoksi. Vuonna 2022 Wormhole Bridgeltä varastettiin 320 miljoonaa dollaria yhdessä sen älysopimuksessa olleen virheen vuoksi.
On tärkeää luoda älysopimusohjelma oikein ensimmäisellä kerralla. Älysopimukset ovat avoimen lähdekoodin sopimuksia, mikä tarkoittaa, että koodi on julkisesti saatavilla, kun sopimus on otettu käyttöön. Jos hakkeri löytää virheen, hän voi hyödyntää sitä välittömästi. Lisäksi tietoturva-aukkojen korjaaminen ajan myötä ei ole vaihtoehto, koska älysopimuksen koodia ei yleensä voi muokata käyttöönoton jälkeen.
Kuinka älysopimusten varmennus toimii?
Älysopimusten muodollinen varmennus toimii esittämällä älysopimusten logiikka ja haluttu käyttäytyminen matemaattisina lausekkeina. Auditoijat käyttävät sitten automaattisia työkaluja tarkistaakseen, pitävätkö nämä lausekkeet paikkansa.
Prosessiin kuuluu:
Sopimuksen eritelmien ja haluttujen ominaisuuksien määrittely muodollisella kielellä.
Sopimuksen koodin kääntäminen muodolliseksi esitykseksi, kuten matemaattisiksi malleiksi tai logiikaksi.
Automaattisten lauseiden todistajien tai mallitarkistimien käyttäminen sopimuksen teknisten tietojen ja ominaisuuksien vahvistamiseen.
Varmennusprosessin toistaminen virheiden tai haluttujen ominaisuuksien poikkeamien löytämiseksi ja korjaamiseksi.
Miksi älysopimusten varmennus on tärkeää?
Matemaattisen päättelyn käyttö auttaa varmistamaan, että muodollisesti varmennetuissa älysopimuksissa ei ole virheitä tai haavoittuvuuksia ja että ne eivät sisällä muuta tahatonta käyttäytymistä. Se auttaa myös lisäämään luottamusta sopimukseen, koska sen ominaisuudet on osoitettu oikeiksi.
Alla on joitain esimerkkejä siitä, kuinka älysopimusten varmennus on auttanut estämään merkittäviä taloudellisia menetyksiä ja muita tuhoisia tuloksia.
Uniswap
Uniswap on tunnettu AMM. Kun Uniswap V1:n älysopimus kehitettiin, se varmennettiin muodollisesti. Ennen sopimuksen julkaisua tämän muodollisen varmennuksen avulla löydettiin ja korjattiin pyöristysvirheet, jotka olisivat voineet johtaa Uniswap V1:n varojen varastamiseen.
Balancer
Balancer V2 on myös AMM, joka varmennettiin muodollisesti. Muodollisen varmennuksen aikana havaittiin ja korjattiin älysopimuksen flash-lainatoiminnossa ollut virheellinen maksulaskenta, joka olisi voinut tehdä pörssistä alttiin varkauksille.
SafeMoon
SafeMoonin V1-versio sisälsi hienovaraisen virheen, joka löydettiin muodollisen varmennuksen aikana sen käyttöönoton jälkeen. Omistajan oli mahdollista luopua sopimuksen omistuksesta ja hankkia se sitten takaisin, jos tietyt toiminnot tehtiin ennen omistuksesta luopumista.
Tämä virhe jäi huomaamatta useimmissa SafeMoonin V1-haarautumisten manuaalisissa auditoinneissa, koska sen löytäminen edellytti tiettyjen ohjelmamuuttujien arvojen yhdistelmien analysointia. Tämä on seikka, joka ihmisten on helppo olla huomaamatta mutta jonka kone voi huomata helposti.
Kuinka muodollinen varmennus ja manuaalinen auditointi toimivat yhdessä?
Muodollinen varmennus tarjoaa järjestelmällisen ja automatisoidun tavan tarkistaa sopimuksen logiikka ja käyttäytyminen suhteessa sen haluttuihin ominaisuuksiin. Tämä helpottaa mahdollisten virheiden tunnistamista ja korjaamista. Se on erityisen hyödyllinen monimutkaisten ja hienovaraisten ongelmien löytämisessä, joita voi olla vaikea havaita manuaalisen auditoinnin yhteydessä.
Manuaalinen auditointi sisältää sopimuksen koodin, suunnittelun ja käyttöönoton asiantuntijatarkastuksen. Auditoija käyttää kokemustaan ja asiantuntemustaan turvallisuusriskien tunnistamiseen ja sopimuksen yleisen turvallisuustilanteen arviointiin. Hän voi myös vahvistaa, että muodollinen varmennusprosessi suoritettiin oikein, ja tarkistaa mahdolliset ongelmat, joita automaattiset työkalut eivät välttämättä pysty havaitsemaan.
Muodollisen varmennuksen ja manuaalisen auditoinnin yhdistäminen tarjoaa kattavan ja perusteellisen arvioinnin älysopimuksen turvallisuudesta. Tämä lisää mahdollisuuksia löytää ja korjata haavoittuvuuksia. Tuloksena on syvällinen puolustuslähestymistapa turvallisuuteen, joka hyödyntää sekä ihmisten että koneiden ainutlaatuisia ominaisuuksia.
Yhteenveto
Älysopimusten turvallisuuden varmistamiseksi on välttämätöntä käyttää sekä muodollista varmennusta että manuaalista auditointia älysopimuksen turvallisuustilanteen kattavan ja perusteellisen arvioinnin varmistamiseksi.
Vaikka muodollinen varmennus voi vaatia paljon resursseja, se on kannattava investointi sellaisten sopimusten yhteydessä, jotka tulevat käsittelemään suuria määriä varoja tai joihin liittyy suuria riskitekijöitä. Viime kädessä turvallisuuden priorisointi ja sen varmistaminen, että älysopimuksissa ei ole virheitä tai haavoittuvuuksia ja että ne eivät sisällä muuta tahatonta käyttäytymistä, on elintärkeää.
Luettavaa
Vastuuvapauslauseke ja riskivaroitus: Tämä sisältö esitetään sinulle "sellaisenaan" vain yleisiä tiedotus- ja koulutustarkoituksia varten ilman minkäänlaista edustusta tai takuuta. Sitä ei pidä tulkita taloudelliseksi neuvonnaksi, eikä sen tarkoituksena ole suositella minkään tietyn tuotteen tai palvelun ostamista. Digitaalisten omaisuuserien hinnat voivat olla epävakaita. Sijoituksesi arvo voi laskea tai nousta, etkä välttämättä saa takaisin sijoittamaasi summaa. Olet yksin vastuussa sijoituspäätöksistäsi, eikä Binance Academy ole vastuussa mistään tappioista, joita sinulle voi aiheutua. Tätä materiaalia ei tule tulkita taloudelliseksi neuvonnaksi.