Tento článek byl zveřejněn členem komunity. Autorem je David Tarditi, viceprezident pro inženýrství ve společnosti CertiK, společnosti zabývající se auditem chytrých smluv Web3.

souhrn

Formální ověření chytrých smluv je chrání před chybami, zranitelnostmi a dalšími nepříznivými podmínkami. V tomto procesu lidští experti převedou logiku inteligentní smlouvy na matematické příkazy a poté pomocí automatizovaného procesu porovnají skutečnou logiku s modelem očekávaného chování smlouvy. Kombinací formálního ověření a manuálního auditu můžeme provést komplexní posouzení bezpečnosti smart kontraktů.

Úvod

Inteligentní smlouvy jsou počítačové programy nasazené na blockchainu, které se automaticky spustí, když jsou splněny určité podmínky. Inteligentní smlouvy mohou být velmi jednoduché nebo extrémně složité a mohou obsahovat aktiva v hodnotě milionů nebo dokonce miliard dolarů.

Pokud jsou v kódu inteligentní smlouvy bezpečnostní díry, může to mít zničující následky, jako je krádež veškerého majetku drženého zločinci. V roce 2021 bylo odcizeno 50 milionů dolarů od automatizovaného tvůrce trhu (AMM) Uranium Finance kvůli překlepu v chytré smlouvě.

Také v roce 2021 společnost Compound Finance omylem vydala odměny ve výši 80 milionů dolarů kvůli jediné chybě v kódu. V roce 2022 bylo z Wormhole Bridge ukradeno 320 milionů dolarů kvůli chybě v chytré smlouvě.

Proto je důležité pořídit si program chytrých smluv hned od začátku. Inteligentní smlouvy přijímají model s otevřeným zdrojovým kódem, což znamená, že jakmile je smlouva nasazena, kód je zveřejněn. Pokud hacker objeví chybu, může ji okamžitě zneužít. Kromě toho je běžná praxe záplatování slabých míst zabezpečení v průběhu času neúčinná, protože kód inteligentních kontraktů často nelze po nasazení upravit.

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

Formálního ověření smart kontraktů je dosaženo předložením logiky a očekávaného chování smart kontraktu jako matematických příkazů. Auditoři pak pomocí automatizovaných nástrojů zkontrolují, zda jsou tato prohlášení správná.

Proces zahrnuje:

  1. Definujte specifikace a očekávané charakteristiky smlouvy ve formálním jazyce.

  2. Převeďte kód smlouvy na formální prohlášení, jako je matematický model nebo logika.

  3. Ověřte specifikace a vlastnosti smlouvy pomocí automatizovaného dokazování teorémů nebo kontroly modelu.

  4. Opakujte proces ověření, abyste našli a opravili všechny chyby nebo odchylky od očekávaných charakteristik.

Proč je chytré ověřování smluv důležité

Použitím matematického uvažování pomáhá zajistit, že formálně ověřené smart kontrakty neobsahují chyby, zranitelnosti a další nepříznivé situace. Verifikace také pomáhá zvýšit důvěru a důvěru ve smlouvu, protože její vlastnosti byly přísně testovány a jsou správné a spolehlivé.

Tyto příklady níže naznačují, jak může inteligentní ověřování smluv pomoci zabránit významným finančním ztrátám a dalším katastrofickým následkům.

Uniswap

Uniswap je známý AMM. Smart kontrakt Uniswap V1 prošel formálním ověřením během procesu vývoje. Před vydáním toto formální ověření nalezlo a opravilo některé zaokrouhlovací chyby, které zabránily vyčerpání prostředků z Uniswapu V1.

Balancer

Balancer V2 je také osvědčeným AMM. Formální ověření odhalilo a opravilo chybu ve výpočtu poplatku ve funkci flash půjčky v chytré smlouvě, která způsobila, že obchodní platforma byla zranitelná vůči krádeži.

SafeMoon

Po nasazení SafeMoon V1 byla formálním ověřením objevena velmi malá chyba. Pokud nebyla chyba odhalena, pokud vlastník smlouvy provedl určité operace před tím, než se vzdal vlastnictví, mohl ji vlastník smlouvy po vzdání se smlouvy znovu získat.

Většina manuálních auditů vidlice SafeMoon V1 tuto chybu postrádá, protože je třeba analyzovat konkrétní kombinace hodnot programových proměnných, aby ji bylo možné najít. Lidé mohou tento problém snadno minout, ale stroje jej mohou zachytit včas.

Jak formální ověřování a ruční audit spolupracují

Formální ověřování poskytuje systematický a automatizovaný způsob kontroly logiky a chování smlouvy oproti očekávaným charakteristikám. To usnadňuje identifikaci a opravu případných chyb nebo zranitelností. To je zvláště užitečné pro složité, jemné problémy, které by bylo obtížné odhalit ruční kontrolou.

Manuální audit zahrnuje odborníky, kteří kontrolují kód, návrh a nasazení smlouvy. Auditoři využívají své zkušenosti a odborné znalosti k identifikaci bezpečnostních rizik a posouzení celkové bezpečnostní pozice smlouvy. Mohou také potvrdit, že proces formálního ověření byl proveden správně, a zkontrolovat případné problémy, které by automatické nástroje nemusely detekovat.

Kombinací formálního ověření a manuálního auditu můžeme provést komplexní posouzení bezpečnosti smart kontraktů. To zvyšuje šance na nalezení a opravu jakýchkoli zranitelností. Přijímáme přitom hloubkový bezpečnostní přístup, který kombinuje odborné znalosti lidí a strojů.

Závěr

Aby byla zajištěna bezpečnost inteligentních smluv, musí být kombinováno formální ověřování a manuální audit, aby bylo zajištěno komplexní a důkladné posouzení bezpečnostní pozice inteligentních smluv.

I když je formální ověření náročnější na zdroje, u smluv s vysokou hodnotou nebo vysoce rizikovými faktory se vyplatí investice. Koneckonců, bezpečnost je důležitější než cokoli jiného. Ujistěte se, že upřednostňujete zabezpečení a zajistěte, aby chytré smlouvy neobsahovaly chyby, zranitelnosti a nežádoucí neočekávané chování.

Další čtení

  • Co je chytrá smlouva?

  • Co je audit zabezpečení inteligentní smlouvy?

Zřeknutí se odpovědnosti a varování před riziky: Obsah tohoto článku jsou fakta a slouží pouze pro obecné informace a vzdělávací účely a nepředstavují žádné prohlášení ani záruku. Tento článek by neměl být vykládán jako finanční poradenství a nedoporučuje, abyste si zakoupili jakýkoli konkrétní produkt nebo službu. Ceny digitálních aktiv mohou kolísat. Hodnota vaší investice může klesat i stoupat a investovaná jistina se vám nemusí vrátit. Jste výhradně odpovědní za svá vlastní investiční rozhodnutí a Binance Academy nenese odpovědnost za žádné ztráty, které můžete utrpět. Tento materiál nepředstavuje finanční poradenství.