Bug Desain Wrapped Ether (WETH) Diluncurkan oleh Analis

Dalam karyanya Verifikasi Format Wrapped ETH (WETH) penelitian, Stephen Tong memverifikasi dua parameter penting untuk desain tokenomikal dari Wrapped Ether, token ERC-20 yang mencerminkan Ether (ETH) dalam aplikasi DeFi.

Analis memeriksa akurasi pasokan WETH total dan solvabilitasnya: Hasil

Hari ini, pada 19 November 2022, Tong menerbitkan ulasan tentang dua fitur Wrapped Ethereum (WETH), sebuah kontrak pintar pada jaringan Ethereum (ETH) yang dirancang untuk merampingkan penggunaan ETH di DeFi dengan “membungkusnya” menjadi ERC biasa. 20 aset.

Bug di WETH:
Wrapped ETH adalah smart contract yang telah melakukan lebih dari 125 JUTA transaksi Ethereum. Tahun ini, 11.5% dari semua transaksi menggunakan Wrapped ETH.
Tapi apakah itu aman? Saya secara resmi memverifikasi dua properti keselamatan kritis dengan pemecah SMT, Z3.👇🧵https://t.co/KH5vLjxwnm pic.twitter.com/fM7cf3TLag

— ct (@gf_256) November 19, 2022

Dia memanfaatkan instrumen Constrained Horn Clause (CHC) untuk memodelkan semua kemungkinan status Wrapped Ethereum (ETH). Kemudian, dia memeriksa apakah metrik "total pasokan" kontrak pintar WETH benar-benar sama dengan jumlah token yang dicetak. 

Dia juga mencoba memverifikasi apakah mungkin untuk menebus ETH dari WETH kapan saja; Tong menyebut fungsi ini "solvabilitas".

Mengenai poin pertama, analis mengungkap bahwa total pasokan belum tentu sama dengan jumlah token yang ada:

Secara teknis, standar ERC-20 menetapkan bahwa totalSupply() harus sama dengan…”total pasokan”. Yang agak kabur, tapi orang akan berasumsi bahwa itu adalah total token yang ada

Melalui fungsi penghancuran diri, yang mengakhiri kontrak atau mentransfer dana kontrak apa pun ke alamat tertentu, pengguna akan dapat mencetak token WETH tanpa benar-benar mengirim ETH untuk dibungkus, simpul Tong.

Apakah ini benar-benar berbahaya bagi pengguna WETH?

Dia juga menunjukkan bahwa deposan Ethers (ETH) belum tentu dapat menarik dana mereka dari kontrak pintar kapan saja.

Tidak puas! Itulah hasil yang ingin kita lihat! pic.twitter.com/ls7bhPakY1

— ct (@gf_256) November 19, 2022

Dengan demikian, dia memberikan dua model hipotetis untuk menunjukkan tidak adanya korelasi antara saldo kontrak WETH dan jumlah sebenarnya dari token yang dicetak, serta “cacat solvabilitas” yang dapat memengaruhi proses penarikan.

Namun, dia menekankan bahwa kedua situasi tersebut bersifat hipotetis dan hanya dimodelkan untuk percobaan. Bug dalam penelitian ini “minor” dan “tidak berbahaya”.

Sejak diluncurkan pada tahun 2020, Zellic mengaudit sejumlah protokol DeFi tingkat atas, termasuk 1 inci (1INCH), LayerZero, dan SushiSwap (SUSHI).