Vad är formell verifiering av smarta kontrakt?

Den här artikeln kommer från vårt community. Författaren är David Tarditi, VP of Engineering på CerTiK, ett revisionsföretag för Web3 och smarta kontrakt.

TL;DR

Formell verifiering av smarta kontrakt säkerställer att de är fria från buggar, sårbarheter och annat oavsiktligt beteende. Den involverar en mänsklig expert som presenterar det smarta kontraktets logik som matematiska uttalanden och sedan kör dem genom en automatiserad process som kontrollerar den faktiska logiken mot modeller av kontraktets förväntade beteende. Kombinationen av formell verifiering och manuell revision ger en omfattande utvärdering av ett smart kontrakts säkerhet.

Introduktion

Smarta kontrakt är program på en blockkedja som körs automatiskt när vissa villkor är uppfyllda. De kan variera från enkla till extremt komplexa instruktioner och kan hålla tillgångar värda miljoner eller till och med miljarder dollar.  

Säkerhetsproblem i koden för smarta kontrakt kan få förödande konsekvenser, inklusive stöld av alla tillgångar som hålls av ett smart kontrakt. Under 2021 stals 50 miljoner dollar från den automatiserade marknadsgaranten (automated market maker/AMM) Uranium Finance, på grund av ett enda skrivfel i ett smart kontrakt.

Samma år gav Compound Finance ut 80 miljoner dollar i felaktiga belöningar på grund av ett enda teckenfel. Under 2022 stals 320 miljoner dollar från Wormhole Bridge på grund av ett fel i ett av dess smarta kontrakt.

Det är viktigt att allt fungerar rätt i programmet för det smarta kontraktet redan från början. Smarta kontrakt är öppen källkod, vilket innebär att koden är allmänt tillgänglig när ett kontrakt har distribuerats. Om en hackare hittar ett fel kan denne dra nytta av detta omedelbart. Dessutom är korrigeringar av säkerhetsproblem i efterhand inte ett alternativ, eftersom koden för ett smart kontrakt vanligtvis inte kan ändras efter distributionen.

Hur fungerar verifiering av smarta kontrakt?  

Formell verifiering av smarta kontrakt fungerar genom att presentera logiken och önskat beteende hos smarta kontrakt som matematiska uttalanden. Revisorerna använder sedan automatiserade verktyg för att kontrollera om dessa uttalanden är korrekta.

Processen innebär följande:

1. Definiera specifikationer och önskade egenskaper för ett kontrakt på ett formellt språk.

2. Översätt kontraktets kod till en formell representation, såsom matematiska modeller eller logik.

3. Använd automatiserade teorembevisare eller modellverifierare för att validera kontraktets specifikationer och egenskaper.

4. Upprepa verifieringsprocessen för att hitta och åtgärda eventuella fel eller avvikelser från de önskade egenskaperna.

Varför verifiering av smarta kontrakt är viktigt

Användningen av matematiska resonemang hjälper till att säkerställa att formellt verifierade smarta kontrakt är fria från buggar, sårbarheter och annat oavsiktligt beteende. Detta bidrar också till att öka förtroendet och tilliten för kontraktet, eftersom dess egenskaper har visat sig vara strikt korrekta. 

Nedan följer några exempel på hur verifiering av smarta kontrakt har bidragit till att förhindra betydande ekonomiska förluster och andra katastrofala resultat.  

Uniswap

Uniswap är en välkänd AMM. När det smarta kontraktet för Uniswap V1 utvecklades, verifierades det formellt. Innan det släpptes hittade och fixade denna formella verifiering avrundningsfel som kunde ha lett till att Uniswap V1 tömdes på tillgångar. 

Balancer

Balancer V2 är en annan AMM som formellt verifierades. Den formella verifieringen hittade och fastställde en felaktig avgiftsberäkning med snabblånefunktionalitet i det smarta kontraktet, vilket kunde ha gjort börsen sårbart för stöld.

SafeMoon

SafeMoon V1 innehöll ett subtilt fel som hittades genom formell verifiering efter att den distribuerades. Det var möjligt för en ägare att avstå från ägandet av kontraktet och sedan återförvärva det, om vissa operationer gjordes innan användaren avstod från ägandet.

Detta fel missades i de flesta manuella granskningar av SafeMoon V1-gafflarna, eftersom det krävdes analys av specifika kombinationer av programmets variabelvärden. Detta är något som är lätt för människor att missa och lätt för en maskin att hitta.

Så fungerar formell verifiering och manuell revision tillsammans

Formell verifiering ger ett systematiskt och automatiserat sätt att kontrollera ett kontrakts logik och beteende mot dess önskade egenskaper. Detta gör det lättare att identifiera och åtgärda eventuella fel eller buggar. Det är särskilt användbart för att hitta komplexa och subtila problem som kan vara svåra att upptäcka under en manuell inspektion.

Manuell granskning innebär expertgranskning av kontraktets kod, design och distribution. Revisorn använder sin erfarenhet och expertis för att identifiera säkerhetsrisker och utvärdera kontraktets övergripande säkerhetsställning. Revisorn kan även bekräfta att den formella verifieringsprocessen utfördes korrekt och kontrollera om det finns problem som kanske inte kan upptäckas med automatiserade verktyg. 

Kombinationen av formell verifiering och manuell revision ger en omfattande och komplett utvärdering av ett smart kontrakts säkerhet. Detta ökar chanserna att hitta och åtgärda eventuella sårbarheter. Resultatet är en djupgående försvarsstrategi för säkerhet som drar nytta av den unika kapaciteten hos både människor och maskiner. 

Sammanfattningsvis

För att bekräfta säkerheten i smarta kontrakt är det viktigt att använda både formell verifiering och manuell revision för att säkerställa en omfattande och grundlig utvärdering av ett smart kontrakts säkerhetsställning.

Även om formell verifiering kan vara resurskrävande, är det en värdefull investering för kontrakt med högt värde eller högriskfaktorer. Att prioritera säkerhet och se till att smarta kontrakt är fria från buggar, sårbarheter och oavsiktligt beteende är trots allt en avgörande faktor.

Mer information

• Vad är smarta kontrakt?

• Vad är en säkerhetsrevision av ett smart kontrakt?

Ansvarsfriskrivning och riskvarning: detta innehåll presenteras för dig "i befintligt skick" och endast som allmän information och i utbildningsändamål, utan representation eller garanti av något slag. Innehållet ska inte tolkas som finansiell rådgivning och det är inte heller avsett att rekommendera köp av någon specifik produkt eller tjänst. Digitala tillgångar kan vara volatila. Värdet på din investering kan gå ner eller upp och du kanske inte får tillbaka det investerade beloppet. Du är ensam ansvarig för dina investeringsbeslut och Binance Academy ansvarar inte för eventuella förluster du kan ådra dig. Detta material ska inte ses som ekonomisk rådgivning.