Denne artikel er et bidrag fra fællesskabet. Forfatteren er David Tarditi, VP for Engineering hos CertiK, et Web3-revisionsselskab af smart contracts.
TL;DR
Formel verifikation af smart contracts sikrer, at de er fri for fejl, sårbarheder og anden utilsigtet adfærd. Det indebærer, at en menneskelig ekspert præsenterer logikken for den pågældende smart contract som matematiske udsagn og derefter kører dem gennem en automatiseret proces, der kontrollerer den faktiske logik i forhold til modeller af kontraktens forventede adfærd. Kombinationen af formel verifikation og manuel revision giver en omfattende evaluering af sikkerheden for en smart contract.
Introduktion
Smart contracts er computerprogrammer, der er implementeret på en blockchain, og som kører automatisk, når visse betingelser er opfyldt. De kan være alt fra enkle til ekstremt komplekse og kan indeholde aktiver til en værdi af millioner eller endda milliarder af dollar.
Sikkerhedssårbarheder i kode til smart contracts kan have ødelæggende konsekvenser, herunder tyveri af alle de aktiver, som en smart contract indeholder. I 2021 blev der stjålet 50 millioner dollar fra den automatiserede market maker (AMM) Uranium Finance på grund af en enkelt tastefejl i en smart contract.
Også i 2021 uddelte Compound Finance 80 millioner dollar i ufortjente belønninger på grund af en fejl med et enkelt tegn. I 2022 blev der stjålet 320 millioner dollar fra Wormhole Bridge på grund af en fejl i én af dens smart contracts.
Det er vigtigt at få smart contract-programmet rigtigt første gang. Smart contracts er open source-kontrakter, hvilket betyder, at koden er offentligt tilgængelig, når en kontrakt er implementeret. Hvis en hacker finder en fejl, kan vedkommende udnytte den med det samme. Desuden er det ikke en mulighed at lappe sikkerhedshuller over tid, da koden i en smart contract typisk ikke kan ændres efter implementeringen.
Hvordan fungerer verifikation af smart contracts?
Formel verifikation af smart contracts fungerer ved at præsentere logikken og den ønskede adfærd i smart contracts som matematiske udsagn. Revisorerne bruger derefter automatiserede værktøjer til at kontrollere, om disse erklæringer er korrekte.
Processen omfatter:
Definition af specifikationer og ønskede egenskaber for en kontrakt i et formelt sprog.
Oversættelse af kontraktens kode til en formel repræsentation, f.eks. matematiske modeller eller logik.
Brug af automatiserede teorembevisere eller modeltjekkere til at validere kontraktens specifikationer og egenskaber.
Gentagelse af verifikationsprocessen for at finde og rette eventuelle fejl eller afvigelser fra de ønskede egenskaber.
Derfor er verifikation af smart contracts vigtig
Brugen af matematisk ræsonnement er med til at sikre, at formelt verificerede smart contracts er frie for fejl, sårbarheder og anden utilsigtet adfærd. Det er også med til at øge tilliden til kontrakten, da dens egenskaber er blevet omhyggeligt bevist som korrekte.
Nedenfor er der nogle eksempler på, hvordan verifikation af smart contracts har hjulpet med at forhindre betydelige økonomiske tab og andre katastrofale resultater.
Uniswap
Uniswap er en velkendt AMM. Da Uniswap V1-smart contracten blev udviklet, blev den formelt verificeret. Inden udgivelsen blev der ved denne formelle verifikation fundet og rettet afrundingsfejl, som kunne have ført til, at Uniswap V1 ville være blevet tømt for midler.
Balancer
Balancer V2 er også en AMM, der blev formelt verificeret. Ved formel verifikation blev der fundet og rettet en ukorrekt beregning af gebyret i forbindelse med flash-lånefunktionen i den pågældende smart contract, hvilket kunne have gjort vekslingen sårbar over for tyveri.
SafeMoon
SafeMoon V1 indeholdt en subtil fejl, der blev fundet ved formel verifikation efter at den var blevet implementeret. Det var muligt for en ejer at give afkald på ejendomsretten til kontrakten og derefter generhverve den, hvis visse handlinger blev udført inden afkaldet på ejendomsretten.
Denne fejl blev overset i de fleste manuelle revisioner af SafeMoon V1-forks, fordi det krævede analyse af specifikke kombinationer af programvariabelværdier at finde den. Dette er noget, som mennesker let kan overse, og som en maskine let kan opfange.
Sådan arbejder formel verifikation og manuel revision sammen
Formel verifikation giver en systematisk og automatiseret måde til at kontrollere en kontrakts logik og adfærd i forhold til de ønskede egenskaber. Det gør det lettere at identificere og rette eventuelle fejl. Det er især nyttigt til at finde komplekse og subtile problemer, som kan være vanskelige at opdage ved manuel inspektion.
Manuel revision omfatter en ekspertgennemgang af en kontrakts kode, design og implementering. Revisorerne bruger deres erfaring og ekspertise til at identificere sikkerhedsrisici og evaluere kontraktens overordnede sikkerhedstilstand. De kan også bekræfte, at den formelle verifikationsproces blev udført korrekt, og kontrollere, om der er problemer, som automatiserede værktøjer måske ikke kan opdage.
Kombinationen af formel verifikation og manuel revision giver en omfattende evaluering af sikkerheden for en smart contract. Det øger chancerne for at finde og rette eventuelle sårbarheder. Resultatet er en tilgang med forsvar i dybden til sikkerhed, der udnytter både menneskers og maskiners unikke evner.
Sammenfatning
For at sikre sikkerheden for en smart contract er det vigtigt at anvende både formel verifikation og manuel revision for at sikre en omfattende og grundig evaluering af sikkerhedstilstanden for en smart contract.
Selv om formel verifikation kan være ressourcekrævende, er det en investering, der er værd at foretage for kontrakter med høj værdi eller høj risiko. I sidste ende er det vigtigt at prioritere sikkerhed og sikre, at smart contracts er fri for fejl, sårbarheder og utilsigtet adfærd.
Yderligere læsning
Ansvarsfraskrivelse og risikoadvarsel: Dette indhold præsenteres for dig "som det er" til generel information og uddannelsesmæssige formål uden erklæring eller garanti af nogen art. Det skal ikke opfattes som økonomisk rådgivning, og det er heller ikke hensigten at anbefale køb af et bestemt produkt eller en bestemt tjeneste. Priserne på digitale aktiver kan være volatile. Værdien af din investering kan gå op eller ned, og du får muligvis ikke det investerede beløb tilbage. Du er eneansvarlig for dine investeringsbeslutninger, og Binance Academy er ikke ansvarlig for eventuelle tab, du måtte lide. Dette materiale skal ikke opfattes som økonomisk rådgivning.