Tento článek je příspěvek komunity. Autorem je David Tarditi, viceprezident pro inženýrství ve společnosti CertiK, auditorské společnosti Web3 smart contract.

Pohledy v tomto článku pocházejí od přispěvatele/autora a nemusí nutně odrážet pohledy Binance Academy.

TL;DR

Formální ověření chytrých smluv zajišťuje, že neobsahují chyby, zranitelnosti a další nezamýšlené chování. Zahrnuje lidského experta, který prezentuje logiku chytré smlouvy jako matematické příkazy a poté je provádí automatizovaným procesem, který kontroluje skutečnou logiku s modely očekávaného chování smlouvy. Kombinace formálního ověřování a manuálního auditu poskytuje komplexní vyhodnocení bezpečnosti inteligentní smlouvy.

Úvod

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

Chyby zabezpečení v kódu inteligentní smlouvy mohou mít zničující následky, včetně krádeže všech aktiv držených inteligentní smlouvou. V roce 2021 bylo společnosti AMM (automated market maker) Uranium Finance ukradeno 50 milionů dolarů kvůli jedinému překlepu v chytré smlouvě.

Také v roce 2021 společnost Compound Finance rozdala 80 milionů dolarů v nezasloužených odměnách kvůli jediné chybě postavy. V roce 2022 bylo z mostu Wormhole Bridge ukradeno 320 milionů dolarů kvůli chybě v jedné z jeho smart kontraktů.

Je důležité získat program chytrých smluv hned napoprvé. Inteligentní smlouvy jsou open source, což znamená, že kód je po nasazení smlouvy veřejně dostupný. Pokud hacker najde chybu, může toho okamžitě využít. Kromě toho není možná oprava bezpečnostních zranitelností v průběhu času, protože kód inteligentní smlouvy obvykle nelze po nasazení upravit.

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

Formální ověřování chytrých smluv funguje tak, že logiku a požadované chování chytrých smluv prezentujeme jako matematické příkazy. Auditoři pak pomocí automatizovaných nástrojů zkontrolují, zda jsou tato prohlášení správná.

Proces zahrnuje:

  1. Definování specifikací a požadovaných vlastností smlouvy ve formálním jazyce.

  2. Překlad kódu smlouvy do formální reprezentace, jako jsou matematické modely nebo logika.

  3. Použití automatických ověřovacích teorémů nebo kontrolorů modelů k ověření specifikací a vlastností smlouvy.

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

Proč je chytré ověření smlouvy důležité

Použití matematického uvažování pomáhá zajistit, aby formálně ověřené smart kontrakty neobsahovaly chyby, zranitelnosti a další nezamýšlené chování. Pomáhá také zvýšit důvěru a důvěru ve smlouvu, protože její vlastnosti byly důsledně prokázány jako správné. 

Níže uvádíme několik příkladů toho, jak chytré ověřování smluv pomohlo zabránit významným finančním ztrátám a dalším katastrofálním následkům.  

Uniswap

Uniswap je známý AMM. Když byla vyvinuta inteligentní smlouva Uniswap V1, byla formálně ověřena. Před jeho vydáním toto formální ověření našlo a opravilo chyby v zaokrouhlování, které mohly vést k vyčerpání prostředků z Uniswapu V1. 

Balancer

Balancer V2 je také AMM, která byla formálně ověřena. Formální ověření zjistilo a opravilo nesprávný výpočet poplatku zahrnující funkci flash půjčky v chytré smlouvě, což mohlo způsobit, že burza bude náchylná ke krádeži.

SafeMoon

SafeMoon V1 obsahoval drobnou chybu zjištěnou formálním ověřením poté, co byl nasazen. Vlastník se mohl vzdát vlastnictví smlouvy a poté ji znovu získat, pokud byly určité operace provedeny před vzdáním se vlastnictví.

Tato chyba byla přehlédnuta ve většině manuálních auditů vidlic SafeMoon V1, protože její nalezení vyžadovalo analýzu konkrétních kombinací hodnot programových proměnných. To je něco, co lidé snadno přehlédnou a stroj to snadno vezme.

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

Formální ověřování poskytuje systematický a automatizovaný způsob kontroly logiky a chování smlouvy oproti požadovaným vlastnostem. To usnadňuje identifikaci a opravu případných chyb nebo chyb. Je to zvláště užitečné pro hledání složitých a jemných problémů, které může být obtížné odhalit ruční kontrolou.

Manuální audit zahrnuje odbornou kontrolu kódu smlouvy, návrhu a nasazení. Auditor využívá své zkušenosti a odborné znalosti k identifikaci bezpečnostních rizik a vyhodnocení 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é nemusí být zjistitelné automatickými nástroji. 

Kombinace formálního ověření a manuálního auditu poskytuje komplexní a důkladné vyhodnocení zabezpečení inteligentní smlouvy. To zvyšuje šance na nalezení a opravu případných zranitelností. Výsledkem je hloubkový přístup k zabezpečení, který využívá jedinečné schopnosti lidí i strojů. 

Závěrečné myšlenky

Pro zajištění bezpečnosti inteligentních smluv je nezbytné používat jak formální ověřování, tak manuální audit, aby bylo zajištěno komplexní a důkladné vyhodnocení bezpečnostní pozice inteligentní smlouvy.

Zatímco formální ověření může být náročné na zdroje, u smluv s vysokou hodnotou nebo vysoce rizikovými faktory se vyplatí. V konečném důsledku je důležité upřednostnit zabezpečení a zajistit, aby chytré smlouvy neobsahovaly chyby, zranitelnosti a nezamýšlené chování.

Další čtení

  • Co jsou chytré smlouvy?

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

Zřeknutí se odpovědnosti a varování před rizikem: Tento obsah je vám prezentován „tak, jak je“, pouze pro obecné informační a vzdělávací účely, bez jakéhokoli zastoupení nebo záruky. Nemělo by být vykládáno jako finanční, právní nebo jiné odborné poradenství, ani není určeno k doporučení nákupu jakéhokoli konkrétního produktu nebo služby. Měli byste vyhledat vlastní radu od příslušných profesionálních poradců. V případě, že článek přispěl přispěvatelem třetí strany, vezměte prosím na vědomí, že tyto vyjádřené názory patří přispěvateli třetí strany a nemusí nutně odrážet názory Binance Academy. Pro další podrobnosti si prosím přečtěte naše úplné prohlášení o vyloučení odpovědnosti zde. Ceny digitálních aktiv mohou být kolísavé. Hodnota vaší investice může klesat nebo stoupat a investovaná částka se vám nemusí vrátit. Jste výhradně odpovědní za svá investiční rozhodnutí a Binance Academy nenese odpovědnost za jakékoli ztráty, které vám mohou vzniknout. Tento materiál by neměl být vykládán jako finanční, právní nebo jiné odborné poradenství. Další informace naleznete v našich podmínkách použití a varování před riziky.