تائید رسمی قرارداد هوشمند چیست و چگونه کار می کند؟نگاهی به مفهوم قرارداد هوشمند قرارداد هوشمند، یک برنامه اجرا شده بر بستر بلاکچین است که در صورت برآورده شدن یک سری شرایط خاص، به صورت خودکار اجرا می‌شود. این قراردادها از ساده تا بسیار پیچیده متغیر بوده و دارایی‌هایی به ارزش میلیون‌ها یا حتی میلیاردها دلار را در خود جای داده‌اند. اصل کار قرارداد هوشمند به این صورت است که اگر اتفاق X رخ داد، دستور Y را اجرا کن، و اگر اتفاق Z رخ داد، دستور متغیر دیگری را اجرا کن.
تائید رسمی قرارداد هوشمند چیست و چگونه کار می کند؟
آسیب‌پذیری از نظر امنیتی در کد این قرارداد می‌تواند عواقب مخربی از جمله سرقت تمام دارایی‌ها را به دنبال داشته باشد. بنابراین، اهمیت دارد که این قراردادها به درستی تدوین شوند، زیرا پس از استقرار، کد آن‌ها به صورت عمومی در دسترس است. اگر یک هکر بتواند باگ آن‌ها را پیدا کند، می‌تواند فورا از آن استفاده کند. علاوه بر این، اصطلاح آسیب‌پذیری‌های امنیتی در طول زمان امکان‌پذیر نیست، زیرا کد Smart Contract پس از استقرار روی بلاکچین و اجرا، قابل تغییر نیست.
تائید رسمی قرارداد هوشمند چگونه کار می‌کند؟
تائید رسمی قرارداد هوشمند به منظور پیشگیری از اشکال و آسیب‌پذیری، از طریق ارائه منطق و رفتار مطلوب Smart Contract به عنوان گزاره‌های ریاضی صورت می‌گیرد. این فرایند شامل مراحل زیر است:
- تعریف مشخصات و ویژگی‌های مورد نظر به زبان رسمی.
- ترجمه کد به یک فرم رسمی مانند مدل‌های ریاضی یا منطق.
- استفاده از اثبات‌کننده‌های قضیه خودکار یا بررسی‌کننده‌های مدل برای تائید مشخصات و ویژگی‌ها.
- تکرار فرآیند تائید به منظور یافتن و رفع هرگونه خطا یا انحراف از ویژگی‌های مورد نظر.
چرا تائید رسمی قرارداد هوشمند مهم است؟
استفاده از منطق و استدلال ریاضی در تائید رسمی قرارداد هوشمند کمک می‌کند تا اطمینان حاصل شود که نمونه تائید شده عاری از هرگونه اشکال، خطا و آسیب‌پذیری و سایر رفتارهای ناخواسته است. همچنین به افزایش اطمینان و اعتماد کمک می‌کند؛ زیرا صحت ویژگی‌های آن به طور جدی ثابت شده است.
نمونه‌هایی از تاثیرات تائید رسمی بر جلوگیری از ضرر مالی:
- Uniswap: قبل از انتشار Uniswap V1، در فرآیند تائید رسمی خطاهایی که ممکن بود منجر به خالی شدن پول Uniswap V1 شود شناسایی و برطرف شد.
- Balancer: در فرآیند تائید رسمی Balancer V2، محاسبه نادرست کارمزد مربوط به وام فلش که می‌توانست صرافی را در برابر سرقت آسیب‌پذیر کند، شناسایی و برطرف شد.
- SafeMoon: در Formal Verification of Smart Contracts، خطای ظریفی در قرارداد SafeMoon V1 شناسایی شد که در صورت انصراف از مالکیت، مالکیت مجدد آن تصرف می‌کرد.
چگونه تائید رسمی قرارداد هوشمند و ممیزی دستی با هم کار می‌کنند؟
تائید رسمی، یک روش سیستماتیک و خودکار به منظور بررسی منطق و رفتار قرارداد در برابر ویژگی‌های مورد نظر آن ارائه می‌کند. ممیزی دستی شامل بررسی تخصصی کد، طراحی و استقرار یک قرارداد هوشمند در بلاکچین است. ترکیب این دو فرایند، یعنی ممیزی دستی با تائید رسمی، می‌تواند یک بسته ارزیابی جامع و کامل از امنیت را ارائه کند. این ترکیب یک رویکرد دفاعی عمیق نسبت به امنیت است که از قابلیت‌های منحصر به فرد انسان و ماشین استفاده می‌کند.
