Denne artikkelen er en innsending fra fellesskapet. Forfatteren er David Tarditi, utviklingsdirektør i CertiK, et Web3-revisjonsfirma for smarte kontrakter.
TL;DR
Formell verifisering av smarte kontrakter sikrer at de er fri for feil, sårbarheter og annen utilsiktet adferd. Det innebærer at en menneskelig ekspert presenterer den smarte kontraktens logikk som matematiske uttrykk, og deretter kjører dem gjennom en automatisert prosess som sjekker den faktiske logikken opp mot modeller av kontraktens forventede adferd. Kombinasjonen av formell verifisering og manuell revisjon gir en omfattende evaluering av en smart kontrakts sikkerhet.
Innledning
Smarte kontrakter er dataprogrammer som er distribuert på en blokkjede, og som kjører automatisk når visse betingelser er oppfylt. De kan variere fra enkle til ekstremt komplekse og kan oppbevare aktiva verdt millioner eller til og med milliarder av dollar.
Sikkerhetssårbarheter i koden til en smart kontrakt kan ha forferdelige konsekvenser, deriblant tyveri av alle aktiva i en smart kontrakt. I 2021 ble den automatiske markedspleieren (AMM) Uranium Finance frastjålet 50 millioner dollar på grunn av en liten skrivefeil i en smart kontrakt.
Og i 2021 delte Compound Finance ut 80 millioner dollar i uopptjente belønninger på grunn av ett feil tegn. I 2022 ble 320 millioner dollar stjålet fra Wormhole Bridge på grunn av en feil i en av de smarte kontraktene.
Det er viktig at programmet til den smarte kontrakten lages riktig første gang. Smarte kontrakter er åpen kildekode, noe som betyr at koden er offentlig tilgjengelig når kontrakten er distribuert. Hvis en hacker finner en feil, kan de utnytte den umiddelbart. I tillegg er oppdateringer for å løse sikkerhetssårbarheter underveis ikke et alternativ, ettersom en smart kontrakts kode vanligvis ikke kan endres etter distribusjon.
Hvordan fungerer verifisering av smarte kontrakter?
Formell verifisering av smarte kontrakter fungerer ved at logikken og ønsket adferd til smarte kontrakter presenteres som matematiske uttrykk. Revisorer bruker deretter automatiserte verktøy for å sjekke om disse uttrykkene er riktige.
Prosessen innebærer:
Definere spesifikasjonene og ønskede egenskaper for en kontrakt på et formelt språk.
Oversette kontraktens kode til en representativ formell, for eksempel matematiske modeller eller logikk.
Bruke automatiserte teoremprøvere eller modellsjekkere for å validere kontraktens spesifikasjoner og egenskaper.
Gjenta verifiseringsprosessen for å finne og løse eventuelle feil eller avvik fra de ønskede egenskapene.
Hvorfor verifisering av smarte kontrakter er viktig
Bruken av matematisk logikk bidrar til å sikre at formelt verifiserte smarte kontrakter er fri for feil, sårbarheter og annen utilsiktet adferd. Det bidrar også til å øke tilliten til kontrakten, ettersom egenskapene har blitt bevist å være korrekte ved hjelp av strenge krav.
Nedenfor er noen eksempler på hvordan verifisering av smarte kontrakter har bidratt til å hindre store økonomiske tap og andre katastrofale konsekvenser.
Uniswap
Uniswap er en kjent AMM. Da Uniswap V1-smartkontrakten ble utviklet, ble den formelt verifisert. Før utgivelse fant og rettet denne formelle verifiseringen avrundingsfeil som kunne ha ført til at Uniswap V1 ble tappet for penger.
Balancer
Balancer V2 er også en AMM som ble formelt verifisert. Formell verifisering fant og rettet en feil med gebyrberegning som involverte lynlånfunksjonalitet i den smarte kontrakten, noe som kunne ha gjort børsen sårbar for tyveri.
SafeMoon
SafeMoon V1 inneholdt en minifeil som ble funnet ved formell verifisering etter at den hadde blitt distribuert. Det var mulig for en eier å gi fra seg eierskapet til kontrakten og så kreve det tilbake, hvis visse operasjoner ble utført før eierskapet ble overdratt.
Denne feilen ble oversett i de fleste manuelle revisjoner av SafeMoon V1-forkene fordi det krevde analysering av spesifikke kombinasjoner av programmets variable verdier. Dette er det lett for mennesker å overse, men lett for en maskin å fange opp.
Hvordan formell verifisering og manuell revisjon fungerer sammen
Formell verifisering er en systematisk og automatisert måte å sjekke en kontrakts logikk og adferd opp mot ønskede egenskaper. Dette gjør det lettere å identifisere og løse eventuelle problemer eller feil. Det er spesielt nyttig for å finne komplekse og ørsmå feil som kan være vanskelige å oppdage ved manuell inspeksjon.
Manuell revisjon involverer ekspertgjennomgang av en kontrakts kode, design og distribusjon. Revisoren bruker sin erfaring og ekspertise til å identifisere sikkerhetsrisikoer og evaluere kontraktens overordnede sikkerhet. De kan også bekrefte at den formelle verifiseringsprosessen ble utført riktig, og se etter problemer som kanskje ikke kan oppdages av automatiserte verktøy.
Kombinasjonen av formell verifisering og manuell revisjon gir en omfattende og grundig evaluering av en smart kontrakts sikkerhet. Dette øker sjansene for å finne og løse eventuelle sårbarheter. Resultatet er en forsvar-i-dybden-tilnærming til sikkerhet som benytter de unike egenskapene til både mennesker og maskiner.
Avsluttende tanker
For å sørge for sikkerheten til smarte kontrakter er det viktig å bruke både formell verifisering og manuell revisjon, som gir en omfattende og grundig evaluering av en smart kontrakts sikkerhet.
Selv om formell verifisering kan være ressurskrevende, er det en investering det er verdt å gjøre for kontrakter med høy verdi eller med høyrisikofaktorer. Til syvende og sist er det viktig å prioritere sikkerheten og sikre at smarte kontrakter er fri for feil, sårbarheter og utilsiktet adferd.
Videre lesning
Ansvarsfraskrivelse og risikoadvarsel: Dette innholdet presenteres for deg «som det er», og er bare til generell informasjon og undervisningsformål, uten representasjon eller garanti av noe slag. Det skal ikke tolkes som økonomisk rådgivning, og det er heller ikke ment å anbefale kjøp av spesifikke produkter eller tjenester. Priser på digitale aktiva kan være volatile. Verdien av investeringen din kan gå ned eller opp, og du får kanskje ikke tilbake det investerte beløpet. Du er selv fullt ansvarlig for investeringsbeslutningene dine, og Binance Academy er ikke ansvarlig for eventuelle tap du påføres. Dette materialet skal ikke tolkes som økonomisk rådgivning.