Ez a cikk egy közösségi beadvány. A szerző David Tarditi, a CertiK, egy Web3 okosszerződéseket auditáló cég műszaki alelnöke.
TL;DR
Az okosszerződések formális jóváhagyása biztosítja, hogy nem tartalmaznak hibákat, sebezhetőségeket és egyéb nem kívánt tulajdonságokat. Ennek során egy emberi szakértő az okosszerződés logikáját matematikai állítások formájában mutatja be, majd lefuttatja egy automatizált folyamaton, amely ellenőrzi a tényleges logikát a szerződés várható viselkedésének modelljével. A formális jóváhagyás és a manuális auditálás kombinációja átfogó értékelést nyújt az okoszerződés biztonságáról.
Bevezetés
Az okosszerződések a blokkláncon tárolt programok, amelyek bizonyos feltételek teljesülése esetén automatikusan futtatásra kerülnek. Lehetnek egyszerűek vagy rendkívül összetettek, és több millió vagy akár több milliárd dollár értékű eszközöket is őrizhetnek.
Az okosszerződések kódjának biztonsági rései pusztító hatással járhatnak, beleértve az okosszerződés által őrzött összes eszköz ellopását. 2021-ben az Uranium Finance automatizált market maker (AMM) 50 millió dollárt lopott el egy okosszerződésben lévő elírás miatt.
Szintén 2021-ben a Compound Finance 80 millió dollárnyi jogosulatlan jutalmat osztott szét egyetlen karakterhiba miatt. 2022-ben 320 millió dollárt loptak el a Wormhole Bridge-ről, mert az egyik okosszerződésben hiba volt.
Fontos, hogy az okosszerződéses programot már elsőre jól készítsék el. Az okosszerződések nyílt forráskódúak, ami azt jelenti, hogy a kód nyilvánosan elérhető lesz, amint a szerződést telepítik. Ha egy hacker hibát talál, azonnal kihasználhatja azt. Ráadásul a biztonsági rések utólagos kijavítására nincs lehetőség, mivel az okosszerződések kódja a telepítés után általában nem módosítható.
Hogyan működik az okosszerződések jóváhagyása?
Az okosszerződések formális jóváhagyása úgy működik, hogy az okosszerződések logikáját és kívánt viselkedését matematikai állítások formájában mutatják be. Az auditálók ezután automatizált eszközökkel ellenőrzik, hogy ezek az állítások helyesek-e.
A folyamat a következőkből áll:
A szerződés specifikációinak és kívánt tulajdonságainak meghatározása formális nyelven.
A szerződés kódjának lefordítása formális reprezentációra, például matematikai modellekre vagy logikára.
Automatizált tételbizonyítók vagy modellellenőrzők használata a szerződés specifikációinak és tulajdonságainak érvényesítésére.
Az ellenőrzési folyamat megismétlése a hibák vagy a nem kívánt tulajdonságok megtalálása és kijavítása érdekében.
Miért fontos az okosszerződések ellenőrzése?
A matematikai érvelés használata segít biztosítani, hogy a formálisan jóváhagyott okosszerződések mentesek legyenek a hibáktól, sebezhetőségektől és egyéb nem kívánt tulajdonságoktól. Segít továbbá növelni a szerződésbe vetett bizalmat, mivel annak tulajdonságai bizonyítottan helytállóak.
Az alábbiakban bemutatunk néhány példát arra, hogy az okosszerződések ellenőrzése hogyan segített megelőzni jelentős pénzügyi veszteségeket és egyéb katasztrofális kimeneteleket.
Uniswap
Az Uniswap egy jól ismert AMM. Amikor az Uniswap V1 okosszerződést kifejlesztették, azt formálisan jóváhagyták. A kiadás előtt ez a formális jóváhagyás olyan kerekítési hibákat talált és javított ki, amelyek a Uniswap V1 pénzeszközök elvesztéséhez vezethettek volna.
Balancer
A Balancer V2 szintén egy AMM, amelyet formálisan jóváhagytak. A formális jóváhagyás megtalálta és kijavította az okosszerződésben a gyorshitel funkciót érintő hibás díjszámítást, ami a tőzsdét sebezhetővé tette volna a lopással szemben.
SafeMoon
A SafeMoon V1 tartalmazott egy apró hibát, amelyet a formális jóváhagyás a telepítés után talált meg. Lehetőség volt arra, hogy a tulajdonos lemondjon a szerződés tulajdonjogáról, majd visszaszerezze azt, ha a tulajdonjogról való lemondás előtt bizonyos műveleteket elvégeztek.
Ez a hiba a SafeMoon V1 forkok legtöbb manuális ellenőrzése során kimaradt, mert a megtalálásához a programváltozók értékeinek speciális kombinációit kellett elemezni. Ez egy olyan dolog, ami felett az emberek könnyen átsiklanak, de egy gép könnyedén észrevesz.
Hogyan működik együtt a formális jóváhagyás és a manuális auditálás?
A formális jóváhagyás szisztematikus és automatizált módot biztosít a szerződés logikájának és viselkedésének ellenőrzésére a kívánt tulajdonságokkal szemben. Ez megkönnyíti az esetleges hibák azonosítását és kijavítását. Különösen hasznos az olyan összetett és apró problémák azonosításában, amelyeket manuális ellenőrzéssel nehéz lenne felismerni.
A manuális auditálás magában foglalja a szerződés kódjának, tervezésének és telepítésének szakértői felülvizsgálatát. Az auditáló a tapasztalatát és szakértelmét felhasználva azonosítja a biztonsági kockázatokat és méri fel a szerződés általános biztonsági helyzetét. Megerősíthetik azt is, hogy a formális jóváhagyási folyamatot helyesen hajtották-e végre, és ellenőrizhetik azokat a problémákat, amelyeket az automatizált eszközökkel esetleg nem lehet felismerni.
A formális jóváhagyás és a manuális auditálás kombinálása átfogó és alapos értékelést biztosít az okosszerződés biztonságáról. Ez növeli a sebezhetőségek megtalálásának és kijavításának esélyét. Az eredmény a biztonság mélyreható védelmi megközelítése, amely az emberek és a gépek egyedi képességeit egyaránt kihasználja.
Záró gondolatok
Az okosszerződések biztonsága érdekében elengedhetetlen mind a formális jóváhagyás, mind a manuális auditálás alkalmazása az okosszerződés biztonsági helyzetének átfogó és alapos felmérése érdekében.
Bár a formális jóváhagyás erőforrás-igényes lehet, a nagy értékű vagy magas kockázati tényezőjű szerződések esetében hasznos befektetés lehet. Végső soron elengedhetetlen a biztonság előtérbe helyezése és annak biztosítása, hogy az okosszerződések ne tartalmazzanak hibákat, sebezhetőségeket és nem kívánt tulajdonságokat.
További olvasnivaló
Felelősségi nyilatkozat és kockázati figyelmeztetés: A jelen bejegyzés tartalmát annak mindenkori formájában bocsátjuk rendelkezésre általános tájékoztatási és oktatási céllal, és semmilyen felelősséget vagy szavatosságot nem vállalunk az alkalmazásával kapcsolatban. Az itt leírtak nem tekintendők pénzügyi tanácsadásnak, sem egy konkrét termék vagy szolgáltatás megvásárlására tett javaslatnak. A digitális eszközök ára erősen ingadozhat. A befektetés értéke csökkenhet vagy nőhet, és az is előfordulhat, hogy nem kapja vissza a befektetett összeget. Ön felel egyedül a befektetési döntéseiért, a Binance nem vállal felelősséget az esetlegesen felmerülő veszteségekért. Az itt leírtak nem minősülnek pénzügyi tanácsnak.