Tento článek je příspěvkem 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 zajišťuje, že neobsahují chyby, zranitelnosti a další nežádoucí chování. Provádí ho lidský expert, který prezentuje logiku smart kontraktu jako matematické příkazy a poté je provádí automatizovaným procesem, který kontroluje skutečnou logiku s očekávanými modely chování smart kontraktu. Kombinace formálního ověření a manuálního auditu poskytuje komplexní posouzení bezpečnosti chytré smlouvy.
Úvod
Inteligentní smlouvy jsou počítačové programy implementované 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 obsahovat aktiva v hodnotě milionů nebo dokonce miliard dolarů.
Chyby zabezpečení v kódu inteligentních smluv mohou vést k vážným následkům, včetně krádeže všech aktiv inteligentních smluv. V roce 2021 utrpěla společnost Automated Market Maker (AMM) Uranium Finance krádež 50 milionů dolarů kvůli překlepu v chytré smlouvě.
Také v roce 2021 společnost Compound Finance rozdala 80 milionů dolarů v nezasloužených odměnách jen kvůli chybnému charakteru. V roce 2022 bylo z Wormhole Bridge ukradeno 320 milionů dolarů kvůli chybě v jedné z jeho smart kontraktů.
Je důležité, aby program smart contract byl od začátku správný. Inteligentní smlouvy jsou open source, což znamená, že jakmile je smlouva nasazena, kód je k dispozici veřejnosti. Pokud hacker najde chybu, může ji okamžitě zneužít. Záplatování slabých míst zabezpečení navíc není udržitelnou možností, protože kód smlouvy po nasazení obvykle nelze upravit.
Jak funguje chytré ověřování smluv?
Formální ověření chytrých smluv se provádí předložením logiky a požadovaného chování smluv jako matematických příkazů. Auditoři pak pomocí automatizovaných nástrojů ověřují, zda jsou výkazy správné.
Proces zahrnuje:
Definujte specifikace a požadované vlastnosti smlouvy ve formálním jazyce.
Přeložte kód inteligentní smlouvy do formální reprezentace, jako jsou matematické modely a logika.
K ověření specifikací a vlastností smlouvy použijte automatické prověřovače teorémů nebo kontroly modelů.
Opakujte proces ověření, abyste našli a opravili všechny chyby nebo odchylky od požadovaných vlastností.
Proč je chytré ověřování smluv důležité
Použití matematického uvažování pomáhá zajistit, že formálně ověřené smlouvy neobsahují chyby, zranitelnosti a další nežádoucí chování. Pomáhá také zvýšit důvěru ve smlouvu, protože její vlastnosti byly přísně testovány, aby byly 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 vážným výsledkům.
Uniswap
Uniswap je známý AMM. Když byla vyvinuta první verze smart kontraktu Uniswap, byla formálně ověřena. Před jeho spuštěním toto formální ověření našlo a opravilo zaokrouhlovací chyby, které mohly vést k vyčerpání finančních prostředků z Uniswap V1.
Balancer
Balancer V2 je také známý jako AMM, který byl formálně ověřen. Formální ověření zjistilo a opravilo nesprávný výpočet poplatku souvisejícího s funkcí flash půjčky v chytré smlouvě, což mohlo způsobit, že burza bude náchylná ke krádeži.
SafeMoon
SafeMoon V1 obsahoval jemnou chybu, která byla objevena při formálním ověření po implementaci smlouvy. Pokud byly určité transakce provedeny před vzdáním se vlastnictví smlouvy, bylo možné, aby se vlastník smlouvy vzdal vlastnictví a poté jej znovu získal.
Tato chyba zůstala bez povšimnutí ve většině manuálních auditů vidlic SafeMoon V1, protože její nalezení vyžadovalo analýzu konkrétních kombinací hodnot proměnných programu. To je něco, co se snadno vymkne lidské kontrole, ale je snadno objeveno strojem.
Jak formální ověřování a manuální audit spolupracují
Formální ověřování poskytuje systematický a automatizovaný způsob, jak potvrdit logiku a chování smlouvy ve vztahu k jejím požadovaným vlastnostem, což usnadňuje identifikaci a opravu potenciálních chyb a chyb. Je to zvláště užitečné pro hledání složitých a jemných problémů, které mohou zůstat bez povšimnutí při ruční kontrole.
Manuální audit zahrnuje odbornou kontrolu kodexu, návrhu a implementace smlouvy. Auditor využívá své zkušenosti a dovednosti k identifikaci bezpečnostních rizik a vyhodnocení celkové bezpečnostní pozice smlouvy. Můžete také potvrdit, že proces formálního ověření byl dokončen správně, a také zkontrolovat všechny problémy, které nejsou zjistitelné automatickými nástroji.
Kombinace formálního ověřování a manuálního auditu poskytuje komplexní a důkladné posouzení bezpečnosti smart kontraktu, čímž se zvyšuje pravděpodobnost nalezení a opravy všech zranitelností, které může obsahovat. Výsledkem je hloubkový přístup k zabezpečení, který využívá jedinečné schopnosti lidí a strojů.
Závěry
Pro zajištění bezpečnosti smart kontraktů je nezbytné dodržet formální ověření a také manuální audit, čímž je zajištěno komplexní a důkladné posouzení bezpečnostní pozice smart kontraktu.
Ačkoli formální ověření může být náročné na zdroje, vyplatí se investovat do smluv s vysokou hodnotou nebo vysoce rizikovými faktory. Nakonec je nezbytné upřednostnit 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í inteligentní smlouvy?
Zřeknutí se odpovědnosti a varování před rizikem: Tento obsah je prezentován „tak, jak je“ pouze pro obecné informace a vzdělávací účely, bez zastoupení nebo záruky jakéhokoli druhu. Nemělo by být vykládáno jako finanční poradenství, ani není určeno k doporučení nákupu jakéhokoli konkrétního produktu nebo služby. Ceny digitálních aktiv jsou nestálé. Hodnota investice může klesat i stoupat a investovaná částka se vám nemusí vrátit. Pouze vy jste zodpovědní za svá investiční rozhodnutí. Binance Academy nezodpovídá za žádné ztráty, které vám mohou vzniknout. Tento materiál by neměl být považován za finanční poradenství.