Błędy projektowe Wrapped Ether (WETH) ujawnione przez analityka

W Weryfikacja formatu opakowanego ETH (WETH) Stephen Tong zweryfikował dwa parametry kluczowe dla projektu tokenomicznego Wrapped Ether, tokena ERC-20, który odzwierciedla Ether (ETH) w aplikacjach DeFi.

Analityk sprawdził dokładność całkowitej podaży WETH i jej wypłacalność: Wyniki

Dzisiaj, 19 listopada 2022 r., Tong opublikował recenzję dwóch funkcji Wrapped Ethereum (WETH), inteligentnego kontraktu w sieci Ethereum (ETH) zaprojektowanego w celu usprawnienia wykorzystania ETH w DeFi poprzez „zapakowanie” go w zwykły ERC- 20 aktywów.

Błąd w WETH:
Wrapped ETH to inteligentny kontrakt, który był używany w ponad 125 MILIONACH transakcji Ethereum. W tym roku 11.5% wszystkich transakcji wykorzystywało Wrapped ETH.
Ale czy to jest bezpieczne? Formalnie zweryfikowałem dwie krytyczne właściwości bezpieczeństwa za pomocą solvera SMT, Z3.👇🧵https://t.co/KH5vLjxwnm pic.twitter.com/fM7cf3TLAG

— cts (@gf_256) Listopad 19, 2022

Wykorzystał instrumenty Constrained Horn Clause (CHC) do modelowania wszystkich możliwych stanów Wrapped Ethereum (ETH). Następnie sprawdził, czy wskaźnik „całkowitej podaży” inteligentnego kontraktu WETH rzeczywiście odpowiada liczbie wybitych tokenów. 

Próbował też zweryfikować, czy w dowolnym momencie można było wykupić ETH z WETH; Tong nazwał tę funkcję „wypłacalnością”.

Jeśli chodzi o pierwszy punkt, analityk ujawnił, że całkowita podaż niekoniecznie jest równa ilości istniejących tokenów:

Technicznie rzecz biorąc, norma ERC-20 określa, że ​​totalSupply() powinno być równe…”całkowitej podaży”. Co jest trochę niejasne, ale można by założyć, że byłaby to całkowita liczba istniejących tokenów

Dzięki funkcji samozniszczenia, która rozwiązuje umowę lub przekazuje środki z umowy na określony adres, użytkownicy byliby w stanie wybijać tokeny WETH bez faktycznego wysyłania ETH do pakowania, podsumował Tong.

Czy to naprawdę niebezpieczne dla użytkowników WETH?

Pokazał również, że deponent Etherów (ETH) niekoniecznie będzie mógł w dowolnym momencie wypłacić swoje środki z inteligentnych kontraktów.

Nienasycone! Taki wynik chcemy zobaczyć! pic.twitter.com/ls7bhPakY1

— cts (@gf_256) Listopad 19, 2022

W związku z tym przedstawił dwa hipotetyczne modele, aby wykazać brak korelacji między saldem kontraktu WETH a rzeczywistą liczbą wybitych tokenów, a także „wadę wypłacalności”, która może wpłynąć na proces wypłaty.

Zaznaczył jednak, że obie sytuacje są hipotetyczne i wymodelowane jedynie na potrzeby eksperymentu. Błędy w badaniach są „drobne” i „nieszkodliwe”.

Od momentu wprowadzenia na rynek w 2020 roku, Zellic skontrolował szereg protokołów DeFi najwyższego poziomu, w tym 1inch (1INCH), LayerZero i SushiSwap (SUSHI).