Vad Àr formell verifiering av smarta kontrakt?
Hem
Artiklar
Vad Àr formell verifiering av smarta kontrakt?

Vad Àr formell verifiering av smarta kontrakt?

MedelnivÄ
Publicerad Mar 2, 2023Uppdaterad Jul 12, 2023
5m

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

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.