بنیاد اتریوم ۱۰۰ هزار دلار برای توسعه کامپایلر تأیید شده رسمی برای وایپر (Vyper) اختصاص داد. وایپر، زبان قرارداد هوشمند با طعم پایتون، در حال حاضر بیش از ۲ میلیارد دلار ارزش کل قفل شده (TVL) را در پروتکلهای دیفای (DeFi) مانند Curve و Yearn پشتیبانی میکند.
ابتکار امنیتی ETHSecurity
این کمک مالی بخشی از دور دوم ابتکارات امنیتی اتریوم (ETHSecurity Initiatives Round Two) است که مجموعاً ۶۰۰ هزار دلار به طور خاص برای بهبودهای امنیتی مرتبط با وایپر اختصاص یافته است. این اقدام به یکی از مشکلات پنهان و خطرناک در توسعه قراردادهای هوشمند میپردازد: شکاف بین آنچه کد در سطح منبع بیان میکند و آنچه کامپایلر در نهایت به عنوان بایتکد EVM تولید میکند.
تأیید رسمی کامپایلر به صورت ریاضی اثبات میکند که فرآیند ترجمه، معنای برنامه اصلی را حفظ میکند. هر ورودی دقیقاً خروجی مشخص شده توسط کد منبع را تولید میکند و هیچ فضایی برای عدم تطابقهای ظریف باقی نمیگذارد.
هدف این کمک مالی بنیاد اتریوم، حرکت به سمت یک حالت “کامپایل تأیید شده” (verified compilation) در دسترس عموم است که مستقیماً در کامپایلر رسمی وایپر تعبیه شود. این امر به توسعهدهندگان و حسابرسان اجازه میدهد تا تأیید کنند که بایتکد در حال اجرا بر روی زنجیره، نمایشی وفادار از کد منبعی است که بررسی کردهاند.
این ابتکار شامل همکاری با بنیاد نرمافزار تأیید شده (Foundation for Verified Software) است، سازمانی که با پروژه Verifereum مرتبط است. این کار بر اساس تحقیقات پیشین در زمینه معناشناسی رسمی (formal semantics) که در HOL4، یک دستیار اثبات مورد استفاده برای تأیید ریاضی دقیق سیستمهای نرمافزاری، انجام شده است، بنا شده است.
تیم توسعه وایپر نیز در این پروژه مشارکت دارد تا اطمینان حاصل شود که کار تأیید با معماری و تکامل واقعی کامپایلر همسو باقی میماند. بنیاد اتریوم به صراحت خواستار مشارکتهای بیشتر از سوی اکوسیستم گستردهتر شده است تا دامنه این ابتکار را فراتر از آنچه تخصیص اولیه ۶۰۰ هزار دلاری پوشش میدهد، گسترش دهد.
اهمیت وایپر در دیفای
حضور وایپر در دیفای قابل توجه است اما گاهی نادیده گرفته میشود. در حالی که Solidity از نظر حجم، چشمانداز قراردادهای هوشمند اتریوم را تسلط دارد، وایپر جایگاه قابل توجهی را در میان پروتکلهایی که سادگی و قابلیت حسابرسی را در اولویت قرار میدهند، ایجاد کرده است. Curve Finance، یکی از بزرگترین صرافیهای غیرمتمرکز از نظر حجم و TVL، برجستهترین نمونه است.
بیش از ۲ میلیارد دلار TVL که توسط قراردادهای وایپر تضمین شده است، به این معنی است که یک اشکال در سطح کامپایلر صرفاً یک مشکل آکادمیک نخواهد بود. این امر میتواند به طور بالقوه وجوه را در چندین پروتکل اصلی به طور همزمان به خطر بیندازد، صرف نظر از اینکه کد منبع چقدر به دقت حسابرسی شده باشد.
در سال ۲۰۲۳، یک آسیبپذیری بازگشتی (reentrancy vulnerability) که به نسخههای خاصی از کامپایلر وایپر مرتبط بود، منجر به سوءاستفادههایی شد که چندین استخر Curve را تحت تأثیر قرار داد. علت اصلی کد منبع معیوب نبود، بلکه یک اشکال کامپایلر بود که یک سازوکار امنیتی را که توسعهدهندگان به درستی پیادهسازی کرده بودند، مختل کرد. این حادثه حدود ۷۰ میلیون دلار را از بین برد و شوکهایی را در سراسر اکوسیستم دیفای ایجاد کرد.
یک کامپایلر تأیید شده رسمی، این دسته از سوءاستفادهها را از نظر ساختاری غیرممکن میسازد. اثبات ریاضی تضمین میکند که اگر کد منبع یک سازوکار امنیتی را به درستی پیادهسازی کند، بایتکد نیز همین کار را انجام خواهد داد.
مبلغ ۱۰۰ هزار دلار در مقایسه با ارزشی که قرار است محافظت شود، ناچیز است. اینکه آیا فراخوان بنیاد اتریوم برای تأمین مالی بیشتر از سوی اکوسیستم مورد توجه قرار میگیرد، احتمالاً تعیینکننده سرعت حرکت این پروژه از مرحله تحقیق به ابزار آماده تولید خواهد بود.
