این مقاله ارسالی جامعه است. نویسنده دیوید تاردیتی، معاون مهندسی در CertiK، یک شرکت حسابرسی قرارداد هوشمند Web3 است.
تأیید رسمی قراردادهای هوشمند تضمین می کند که آنها عاری از اشکالات، آسیب پذیری ها و سایر رفتارهای ناخواسته هستند. این شامل یک متخصص انسانی است که منطق قرارداد هوشمند را به عنوان گزاره های ریاضی ارائه می کند، سپس آنها را از طریق یک فرآیند خودکار اجرا می کند که منطق واقعی را در برابر مدل های رفتار مورد انتظار قرارداد بررسی می کند. ترکیبی از تأیید رسمی و حسابرسی دستی ارزیابی جامعی از امنیت یک قرارداد هوشمند ارائه می دهد.
معرفی
قراردادهای هوشمند برنامههای رایانهای هستند که بر روی یک بلاک چین مستقر میشوند و در صورت برآورده شدن شرایط خاص بهطور خودکار اجرا میشوند. آنها می توانند از ساده تا بسیار پیچیده متغیر باشند و دارایی هایی به ارزش میلیون ها یا حتی میلیاردها دلار را در خود جای دهند.
آسیب پذیری های امنیتی در کد قرارداد هوشمند می تواند عواقب مخربی داشته باشد، از جمله سرقت تمام دارایی های یک قرارداد هوشمند. در سال 2021، بازارساز خودکار (AMM) Uranium Financeمبلغی بالغ بر 50 میلیون دلار به دلیل یک اشتباه تایپی در یک قرارداد هوشمند به سرقت رفت.
همچنین در سال 2021، Compound Finance به دلیل یک اشتباه شخصیتی 80 میلیون دلار پاداش دریافت نکرد. در سال 2022، 320 میلیون دلار از پل Wormhole به دلیل اشکال در یکی از قراردادهای هوشمند آن به سرقت رفت.
مهم است که برنامه قرارداد هوشمند را در اولین بار درست انجام دهید. قراردادهای هوشمند منبع باز هستند، به این معنی که پس از استقرار یک قرارداد، کد به صورت عمومی در دسترس است. اگر یک هکر باگ را پیدا کند، می تواند فورا از آن استفاده کند. علاوه بر این، اصلاح آسیبپذیریهای امنیتی در طول زمان یک گزینه نیست، زیرا کد قرارداد هوشمند معمولاً پس از استقرار قابل تغییر نیست.
تأیید قرارداد هوشمند چگونه کار می کند؟
تأیید رسمی قراردادهای هوشمند با ارائه منطق و رفتار مطلوب قراردادهای هوشمند به عنوان گزاره های ریاضی عمل می کند. سپس حسابرسان از ابزارهای خودکار برای بررسی درستی این اظهارات استفاده می کنند.
این فرآیند شامل:
- تعریف مشخصات و خواص مورد نظر قرارداد به زبان رسمی.
- ترجمه کد قرارداد به یک نمایش رسمی، مانند مدل های ریاضی یا منطق.
- استفاده از اثباتکنندههای قضیه خودکار یا بررسیکنندههای مدل برای تأیید مشخصات و ویژگیهای قرارداد.
- تکرار فرآیند تأیید برای یافتن و رفع هر گونه خطا یا انحراف از ویژگی های مورد نظر.
چرا تأیید قرارداد هوشمند مهم است؟
استفاده از استدلال ریاضی کمک می کند تا اطمینان حاصل شود که قراردادهای هوشمند تأیید شده رسمی عاری از اشکالات، آسیب پذیری ها و سایر رفتارهای ناخواسته هستند. همچنین به افزایش اعتماد و اطمینان در قرارداد کمک می کند، زیرا ویژگی های آن به طور جدی صحت ثابت شده است.
در زیر چند نمونه از اینکه چگونه تأیید قرارداد هوشمند به جلوگیری از ضرر مالی قابل توجه و سایر نتایج فاجعهبار کمک کرده است آورده شده است.
Unswap
Uniswap یک AMM شناخته شده است. زمانی که قرارداد هوشمند Uniswap V1 توسعه یافت، به طور رسمی تأیید شد. قبل از انتشار، این راستیآزمایی رسمی خطاهای گرد کردنی را که میتوانست منجر به خالی شدن پول Uniswap V1 شود، پیدا کرده و برطرف کرد.
Balancer
Balancer V2 نیز یک AMM است که به طور رسمی تأیید شده است. راستیآزمایی رسمی محاسبه نادرستی کارمزد مربوط به عملکرد وام فلش را در قرارداد هوشمند پیدا و برطرف کرد، که میتوانست صرافی را در برابر سرقت آسیبپذیر کند.
SafeMoon
SafeMoon V1 حاوی یک اشکال ظریف بود که پس از استقرار توسط تأیید رسمی پیدا شد. در صورتی که قبل از انصراف از مالکیت عملیات خاصی انجام شده باشد، ممکن است مالک از مالکیت قرارداد صرف نظر کند و دوباره آن را تصرف کند.
این اشکال در اکثر ممیزیهای دستی فورکهای SafeMoon V1 نادیده گرفته شد، زیرا یافتن آن نیازمند تجزیه و تحلیل ترکیبهای خاصی از مقادیر متغیر برنامه بود. این چیزی است که انسان به راحتی از دست می دهد و برای ماشین به راحتی می تواند آن را بگیرد.
چگونه تأیید رسمی و حسابرسی دستی با هم کار می کنند
راستیآزمایی رسمی روشی سیستماتیک و خودکار برای بررسی منطق و رفتار قرارداد در برابر ویژگیهای مورد نظر آن ارائه میکند. این امر شناسایی و رفع هر گونه خطا یا باگ احتمالی را آسان تر می کند. به ویژه برای یافتن مسائل پیچیده و ظریفی که تشخیص آنها از طریق بازرسی دستی دشوار است مفید است.
حسابرسی دستی شامل بررسی تخصصی کد، طراحی و استقرار یک قرارداد است. حسابرس از تجربه و تخصص خود برای شناسایی خطرات امنیتی و ارزیابی وضعیت امنیتی کلی قرارداد استفاده می کند. آنها همچنین میتوانند تأیید کنند که فرآیند تأیید رسمی به درستی انجام شده است و هرگونه مشکلی را که ممکن است توسط ابزارهای خودکار قابل تشخیص نباشد بررسی کنند.
ترکیب تأیید رسمی و ممیزی دستی، ارزیابی جامع و کاملی از امنیت قرارداد هوشمند ارائه می دهد. این امر شانس یافتن و رفع هر گونه آسیب پذیری را افزایش می دهد. نتیجه یک رویکرد دفاعی عمیق به امنیت است که از قابلیت های منحصر به فرد انسان و ماشین استفاده می کند.
کلام پایانی
برای اطمینان از امنیت قراردادهای هوشمند، استفاده از تأیید رسمی و ممیزی دستی برای اطمینان از ارزیابی جامع و کامل وضعیت امنیتی قرارداد هوشمند ضروری است.
در حالی که تأیید رسمی می تواند منابع فشرده باشد، سرمایه گذاری ارزشمندی برای قراردادهایی با ارزش بالا یا عوامل پرخطر است. در نهایت، اولویت دادن به امنیت و اطمینان از عاری بودن قراردادهای هوشمند از اشکالات، آسیبپذیریها و رفتارهای ناخواسته حیاتی است.