Tento článek je příspěvek od komunity. Autorem je David Tarditi, viceprezident pro inženýrství ve společnosti CertiK, společnosti Web3 pro audit chytrých smluv.

souhrn

Formální ověření zajišťuje, že chytré smlouvy neobsahují chyby, zranitelnosti a další nežádoucí chování. V tomto procesu odborník představuje logiku inteligentní smlouvy v matematickém prohlášení a poté ji provádí automatizovaným procesem, který porovnává skutečnou logiku s modelem očekávaného chování smlouvy. Kombinace formálního ověřování a manuálního auditu poskytuje komplexní vyhodnocení zabezpečení inteligentních smluv.

Úvod

Inteligentní smlouvy jsou počítačové programy implementované na blockchainu, které se automaticky spustí, když jsou splněny určité podmínky. Inteligentní smlouvy se mohou pohybovat od jednoduchých po velmi složité a mohou uchovávat aktiva v hodnotě milionů nebo dokonce miliard dolarů.

Chyby zabezpečení v kódu smart contractu mohou mít škodlivé důsledky, včetně krádeže všech aktiv uložených smart contractem. V roce 2021 byly finanční prostředky společnosti Uranium Finance ve výši 50 milionů dolarů ukradeny kvůli chybě v inteligentní smlouvě.

Také v roce 2021 společnost Compound Finance vydala 80 milionů dolarů v nezasloužených odměnách kvůli chybě jediného znaku. V roce 2022 bylo z Wormhole Bridge ukradeno 320 milionů dolarů kvůli chybě v jednom z chytrých kontraktů.

Na začátku je důležité správně naprogramovat chytré smlouvy. Inteligentní smlouvy jsou open source, což znamená, že kód je po implementaci smlouvy veřejně dostupný. Pokud hacker najde chybu, může ji okamžitě zneužít. Oprava slabých míst zabezpečení v průběhu času navíc není dobrou volbou, protože kód inteligentní smlouvy obvykle nelze po nasazení upravit.

Jak funguje chytré ověřování smluv?

Formální ověřování smart kontraktu funguje tak, že prezentuje logiku a požadované chování smart kontraktu ve formě matematických příkazů. Auditoři pak používají automatizované nástroje, aby zajistili správnost výkazů.

Proces zahrnuje:

  1. Definuje specifikace a požadované vlastnosti smlouvy ve formálním jazyce.

  2. Překlad smluvního kódu do formální reprezentace, jako je matematický nebo logický model.

  3. Použijte teorémy nebo automatické kontroly modelů k ověření specifikací a charakteristik smlouvy.

  4. Opakujte proces ověření, abyste našli a opravili chyby nebo odchylky od požadovaných charakteristik.

Důvody, proč je Smart Contract Verification důležité

Použití matematického uvažování pomáhá zajistit, že chytré smlouvy, které prošly formálním ověřením, neobsahují chyby, zranitelnosti a další nežádoucí chování. To také pomáhá zvýšit důvěru a důvěru ve smlouvu, protože její vlastnosti jsou prokazatelně pravdivé.

Níže uvádíme několik příkladů, které ukazují, že chytré ověřování smluv pomohlo zabránit velkým finančním ztrátám a dalším škodlivým dopadům.

Uniswap

Uniswap je známý AMM. Po implementaci prošla inteligentní smlouva Uniswap V1 formálním ověřením. Před vydáním toto formální ověření odhalilo a opravilo chyby v zaokrouhlování, které mohly způsobit vyčerpání prostředků Uniswap V1.

Balancer

Balancer V2 je také AMM, který prošel formálním ověřením. Formální ověření odhalilo a opravilo nesprávné výpočty poplatků souvisejících s funkcí flash půjčky, které mohly způsobit, že burza bude náchylná ke krádeži.

SafeMoon

SafeMoon V1 obsahoval jemnou chybu, která byla objevena formálním ověřením po nasazení. Vlastník se může vzdát vlastnictví smlouvy a poté ji získat zpět, pokud jsou před vzdáním se vlastnictví provedeny určité operace.

Tato chyba byla přehlédnuta ve většině manuálních auditů vidlice SafeMoon V1, protože k jejímu nalezení vyžadovala analýzu určitých kombinací hodnot programových proměnných. Lidé tyto chyby snadno přehlédnou a stroje je snadno vystopují.

Výhody kombinace formálního ověřování a manuálního auditu

Formální ověřování poskytuje systematický a automatizovaný způsob, jak porovnat logiku a chování smlouvy s jejími požadovanými charakteristikami. To usnadňuje identifikaci a opravu potenciálních chyb nebo chyb. Tento proces je zvláště užitečný pro odhalování složitých, jemných problémů, které může být obtížné odhalit ruční kontrolou.

Při manuálním auditu expert přezkoumá kód, návrh a implementaci smlouvy. Auditoři využívají své zkušenosti a odborné znalosti k identifikaci bezpečnostních rizik a vyhodnocení celkové bezpečnostní pozice smlouvy. Mohou se také ujistit, že proces formálního ověření byl proveden správně, a hledat problémy, které nemusí být odhaleny automatickými nástroji.

Kombinací formálního ověřování a manuálních auditů získáte komplexní a důkladné vyhodnocení zabezpečení chytrých smluv. To zvyšuje šance na nalezení a opravu zranitelností. Výsledkem je přístup k zabezpečení do hloubky, který využívá jedinečné schopnosti lidí a strojů.

Zavírání

Aby byla zajištěna bezpečnost chytrých smluv, je důležité používat formální ověřování a manuální audity, aby bylo zajištěno komplexní a důkladné vyhodnocení bezpečnostní pozice chytrých smluv.

Ačkoli to vyžaduje mnoho zdrojů, formální ověření se vyplatí investovat do smluv s vysokou hodnotou nebo vysoce rizikovými faktory. V konečném důsledku je důležité upřednostňovat zabezpečení a zajistit, aby chytré smlouvy neobsahovaly chyby, zranitelnosti a nežádoucí chování.

Další čtení

  • Co jsou chytré smlouvy?

  • Co je audit zabezpečení Smart Contract?

Zřeknutí se odpovědnosti a varování před riziky: Tento obsah je vám prezentován „tak, jak je“, pouze pro obecné informace a vzdělávací účely, bez zastoupení nebo záruky jakéhokoli druhu. Tento obsah by neměl být považován za finanční poradenství ani není určen k navrhování nákupu jakéhokoli konkrétního produktu nebo služby. Ceny digitálních aktiv mohou být kolísavé. Hodnota vaší investice může klesat nebo stoupat. Investovaná částka se vám nemusí vrátit. Jste plně odpovědní za svá investiční rozhodnutí. Binance Academy nezodpovídá za žádné ztráty, které můžete utrpět. Tento materiál by neměl být považován za finanční poradenství.