Wrapped Ether (WETH) designbuggar avslöjade av analytiker

I sin Formatverifiering av Wrapped ETH (WETH) forskning, verifierade Stephen Tong två parametrar som var avgörande för den tokenomiska designen av Wrapped Ether, en ERC-20-token som speglar Ether (ETH) i DeFi-applikationer.

Analytiker kontrollerade noggrannheten för den totala WETH-försörjningen och dess solvens: Resultat

Idag, den 19 november 2022, publicerade Tong en recension om två funktioner i Wrapped Ethereum (WETH), ett smart kontrakt på Ethereum-nätverket (ETH) utformat för att effektivisera ETH-användning i DeFi genom att "linda in" det i en vanlig ERC- 20 tillgång.

En bugg i WETH:
Wrapped ETH är ett smart kontrakt som har gjorts i över 125 MILJONER Ethereum-transaktioner. I år använde 11.5 % av alla transaktioner Wrapped ETH.
Men är det säkert? Jag verifierade formellt två kritiska säkerhetsegenskaper med en SMT-lösare, Z3.👇🧵https://t.co/KH5vLjxwnm pic.twitter.com/fM7cf3TLAg

— cts (@gf_256) November 19, 2022

Han använde Constrained Horn Clause (CHC) instrument för att modellera alla möjliga tillstånd av Wrapped Ethereum (ETH). Sedan kontrollerade han om måttet "totalt utbud" för WETH smart kontrakt faktiskt är lika med antalet tokens som präglats. 

Han försökte också verifiera om det var möjligt att lösa in ETH från WETH när som helst; Tong kallade denna funktion "solvens".

När det gäller den första punkten avslöjade analytikern att det totala utbudet inte nödvändigtvis är lika med mängden tokens som finns:

Tekniskt sett specificerar ERC-20-standarden att totalSupply() ska vara lika med..."total supply". Vilket är lite vagt, men man skulle anta att det skulle vara de totala tokens som finns

Via funktionen självförstörande, som avslutar ett kontrakt eller överför eventuella kontraktsmedel till en angiven adress, skulle användare kunna prägla WETH-tokens utan att faktiskt skicka ETH för inslagning, avslutade Tong.

Är detta verkligen farligt för WETH-användare?

Han visade också att insättaren av Ethers (ETH) inte nödvändigtvis kommer att kunna ta ut sina pengar från smarta kontrakt när som helst.

Osatt! Det är resultatet vi vill se! pic.twitter.com/ls7bhPakY1

— cts (@gf_256) November 19, 2022

Som sådan tillhandahöll han två hypotetiska modeller för att visa frånvaron av korrelation mellan WETH-kontraktsbalansen och det faktiska antalet tokens som präglats, såväl som "solvensfelet" som kan påverka uttagsprocessen.

Han betonade dock att båda situationerna är hypotetiska och endast modellerade för experimentet. Buggarna i forskningen är "mindre" och "ofarliga".

Sedan lanseringen 2020 har Zellic granskat ett antal DeFi-protokoll av högsta klass, inklusive sådana som 1inch (1INCH), LayerZero och SushiSwap (SUSHI).