فهرست
در او تأیید قالب ETH پیچیده شده (WETH) تحقیقات، استفان تانگ دو پارامتر حیاتی برای طراحی توکنومیکال Wrapped Ether، یک توکن ERC-20 که اتر (ETH) را در برنامه‌های DeFi منعکس می‌کند، تأیید کرد.
تحلیلگر دقت عرضه کل WETH و پرداخت بدهی آن را بررسی کرد: نتایج
امروز، در 19 نوامبر 2022، تانگ بررسی دو ویژگی Wrapped Ethereum (WETH) را منتشر کرد، یک قرارداد هوشمند در شبکه اتریوم (ETH) که برای ساده کردن استفاده از ETH در DeFi با “پیچیدن” آن در یک ERC معمولی طراحی شده است. 20 دارایی
یک اشکال در WETH:
Wrapped ETH یک قرارداد هوشمند است که در بیش از 125 میلیون تراکنش اتریوم انجام شده است. امسال 11.5 درصد از کل تراکنش ها از Wrapped ETH استفاده کردند.
اما آیا امن است؟ من به طور رسمی دو ویژگی ایمنی حیاتی را با یک حل کننده SMT، Z3 تأیید کردم.👇🧵https://t.co/KH5vLjxwnm pic.twitter.com/fM7cf3TLAg— cts (@gf_256) 19 نوامبر 2022
او از ابزارهای Constrained Horn Clause (CHC) برای مدل سازی همه حالت های ممکن اتریوم پیچیده شده (ETH) استفاده کرد. سپس، او بررسی کرد که آیا معیار «تامین کل» قرارداد هوشمند WETH واقعاً برابر با تعداد توکن‌های ضرب شده است یا خیر.
او همچنین سعی کرد بررسی کند که آیا امکان بازخرید ETH از WETH در هر زمان وجود دارد یا خیر. تانگ این تابع را «پرداخت بدهی» نامید.
با توجه به نکته اول، تحلیلگر پرده برداری کرد که مجموع عرضه لزوماً برابر با مقدار توکن های موجود نیست:
از نظر فنی، استاندارد ERC-20 مشخص می‌کند که totalSupply() باید برابر با…”مجموع عرضه” باشد. که تا حدودی مبهم است، اما می توان فرض کرد که کل توکن های موجود است
تانگ نتیجه گرفت که از طریق تابع selfdestruct، که قرارداد را خاتمه می دهد یا هرگونه وجه قرارداد را به یک آدرس مشخص منتقل می کند، کاربران می توانند توکن های WETH را بدون ارسال ETH برای بسته بندی، ضرب کنند.
آیا این واقعا برای کاربران WETH خطرناک است؟
او همچنین نشان داد که سپرده گذار اترها (ETH) لزوماً نمی تواند در هر زمانی وجوه خود را از قراردادهای هوشمند برداشت کند.
ناسات! این نتیجه ای است که ما می خواهیم ببینیم! pic.twitter.com/ls7bhPakY1
— cts (@gf_256) 19 نوامبر 2022
به این ترتیب، او دو مدل فرضی را برای نشان دادن عدم همبستگی بین مانده قرارداد WETH و تعداد واقعی توکن‌های ضرب شده، و همچنین «نقص پرداخت بدهی» که می‌تواند بر روند برداشت تأثیر بگذارد، ارائه کرد.
با این حال، او تاکید کرد که هر دو موقعیت فرضی هستند و فقط برای آزمایش مدل شده اند. اشکالات موجود در تحقیق “جزئی” و “بی ضرر” هستند.
از زمان راه اندازی آن در سال 2020، Zellic تعدادی از پروتکل های سطح بالای DeFi، از جمله پروتکل های 1inch (1INCH)، LayerZero و SushiSwap (SUSHI) را ممیزی کرد.
