Tento článek je příspěvkem od naší komunity. Autorem je David Tarditi, technický viceprezident společnosti CertiK, která audituje chytré kontrakty Webu 3.
TL;DR
Formální ověření zajišťuje, že chytré kontrakty neobsahují chyby ani slabá místa a nechovají se nežádoucím způsobem. Provádí ho odborník, který předkládá logiku chytrého kontraktu v podobě matematických výroků a pak je nechá projít automatizovaným procesem, který skutečnou logiku zkontroluje proti modelům očekávaného chování kontraktu. Kombinace formálního ověření a ručního auditu poskytuje komplexní vyhodnocení bezpečnosti chytrého kontraktu.
Úvod
Chytré kontrakty jsou počítačové programy nasazené na blockchainu, které fungují automaticky v návaznosti na splnění určitých podmínek. Jejich složitost se pohybuje od naprosto jednoduchých až po extrémně komplikované a mohou držet aktiva v hodnotě milionů nebo dokonce miliard dolarů.
Bezpečnostní chyby v kódu chytrých kontraktů mohou mít katastrofální následky, včetně krádeže veškerých držených aktiv. V roce 2021 přišel automatizovaný tvůrce trhu (AMM) Uranium Finance kvůli jedinému překlepu v chytrém kontraktu o 50 milionů dolarů.
V roce 2021 rozdala společnost Compound Finance v nezasloužených odměnách kvůli jednomu chybnému znaku 80 milionů dolarů. V roce 2022 bylo z kryptoměnového mostu Wormhole kvůli chybě v jednom z jeho chytrých kontraktů odcizeno 320 milionů dolarů.
Chytrý kontrakt musí být bezchybný hned od začátku. Chytré kontrakty používají otevřený zdrojový kód, což znamená, že tento kód je po nasazení kontraktu veřejně dostupný. Když v něm hacker najde chybu, může ji okamžitě zneužít. Pozdější oprava chyb zabezpečení navíc nepřipadá v úvahu, protože kód chytrého kontraktu už obvykle nelze po spuštění upravit.
Jak ověřování chytrých kontraktů funguje?
Formální ověření chytrých kontraktů funguje tak, že logika a požadované chování chytrých kontraktů se předkládají v podobě matematických výroků. Auditoři pak pomocí automatizovaných nástrojů kontrolují, zda jsou tato tvrzení správná.
Postupuje se následovně:
Definování specifikací a požadovaných vlastností kontraktu ve formálním jazyce.
Převod kódu kontraktu do formální reprezentace, jako jsou matematické modely nebo logika.
Použití automatických dokazovacích algoritmů matematických vět nebo nástrojů pro kontrolu modelů k ověření platnosti specifikací a vlastností kontraktu.
Opakování procesu ověření s cílem najít a opravit případné chyby nebo odchylky od požadovaných vlastností.
Proč je ověření chytrých kontraktů důležité?
Použití matematického odůvodnění pomáhá zajistit, že formálně ověřené chytré kontrakty nebudou obsahovat chyby ani slabá místa a nebudou se chovat nežádoucím způsobem. Zároveň zvyšuje důvěru v kontrakt, protože správnost jeho vlastností byla důkladně prokázána.
Níže uvádíme několik příkladů, jak se ověřením chytrých kontraktů podařilo zabránit značným finančním ztrátám a dalším katastrofálním následkům.
Uniswap
Uniswap je renomovaný AMM. Vývoj chytrého kontraktu Uniswap V1 byl formálně ověřen. Před jeho nasazením byly během tohoto formálního ověření nalezeny a opraveny chyby v zaokrouhlování, které mohly vést k odčerpání finančních prostředků.
Balancer
Balancer V2 je také AMM, který byl formálně ověřen. Při formálním ověření byl v chytrém kontraktu nalezen a opraven nesprávný výpočet poplatků související s funkcí bleskových půjček, která mohla způsobit náchylnost burzy vůči krádežím.
SafeMoon
SafeMoon V1 obsahoval drobnou chybu, kterou formální verifikace objevila po jeho spuštění. Vlastník se mohl vzdát vlastnictví kontraktu a pak ho znovu získat, pokud by před vzdáním se vlastnictví provedl určité operace.
Tato chyba byla při většině ručních auditů forků chytrého kontraktu SafeMoon V1 přehlédnuta, protože její nalezení vyžadovalo analýzu specifických kombinací proměnných hodnot programu. Člověk něco takového snadno přehlédne, ale stroj to snadno zachytí.
Jak se formální ověření a ruční audit doplňují?
Formální ověření poskytuje systematický a automatizovaný způsob kontroly logiky a chování kontraktu s ohledem na jeho požadované vlastnosti. To usnadňuje identifikaci a opravu případných chyb nebo nedostatků. Je to užitečné zejména při hledání komplikovaných nebo drobných problémů, které by bylo obtížné odhalit ruční kontrolou.
Ruční audit se skládá z odborné kontroly kódu, návrhu a nasazení kontraktu. Auditor pomocí svých zkušeností a odborných znalostí identifikuje bezpečnostní rizika a vyhodnocuje celkový stav zabezpečení kontraktu. Může také potvrdit, že formální ověření proběhlo správně, a zkontrolovat případné problémy, které automatické nástroje nemusí odhalit.
Kombinace formálního ověření a ručního auditu poskytuje komplexní a důkladné vyhodnocení bezpečnosti chytrého kontraktu. Zvyšuje se tím pravděpodobnost nalezení a opravy případných slabých míst. Výsledkem je hloubkový přístup k zabezpečení, který využívá jedinečných schopností jak lidí, tak i strojů.
Závěrem
Při zajišťování bezpečnosti chytrých kontraktů je nezbytné používat formální ověření i manuální audit, aby zajištění bezpečného stavu chytrého kontraktu bylo komplexní a důkladné.
Formální ověření může být sice nákladné, ale u kontraktů s vysokou hodnotou nebo rizikovými faktory se vyplatí do něj investovat. V konečném důsledku je důležité upřednostnit bezpečnost a zajistit, aby chytré kontrakty neobsahovaly chyby ani slabá místa a nechovaly se nezamýšleným způsobem.
Související články:
Vyloučení odpovědnosti a upozornění na rizika: tento obsah je vám předkládán ve stavu, v jakém je, pouze pro obecné informační a vzdělávací účely, bez jakéhokoli prohlášení nebo záruky. Neměl by být chápán jako finanční poradenství ani není jeho cílem doporučit nákup jakéhokoli konkrétního produktu nebo služby. Ceny digitálních aktiv mohou být volatilní. Hodnota vaší investice může klesnout i stoupnout a investovaná částka se vám nemusí vrátit. Za svá investiční rozhodnutí nesete výhradní odpovědnost vy sami a Akademie Binance nenese odpovědnost za žádné ztráty, které vám mohou vzniknout. Tento materiál by neměl být považován za finanční poradenství.