تائید رسمی قرارداد هوشمند چیست و چگونه کار می کند؟

Smart Contract یکی از قابلیت‌های بلاکچین است و به گونه‌ای عمل می‌کند که در صورت اجرا، امکان توقف روند آن وجود ندارد. هنگامی که یک قرارداد هوشمند در شبکه بلاکچین اجرا می‌شود، حتی نویسنده آن هم نمی‌تواند مانع ادامه فعالیتش شود. در این میان فرایند تائید رسمی قرارداد هوشمند یا Formal Verification of Smart Contracts تضمین می‌کند که این Contract عاری از اشکال، آسیب‌پذیری و سایر رفتارهای ناخواسته باشد. ترکیب تائید رسمی با ممیزی دستی (Manual Auditing) بسته جامعی از امنیت یک قرارداد هوشمند را به شبکه و کاربران ارائه می‌کند.

نگاهی به مفهوم قرارداد هوشمند

یک برنامه اجرا شده بر بستر بلاکچین است که در صورت برآورده شدن یک سری شرایط خاص به صورت خودکار اجرا می‌شود. قراردادهای هوشمند می‌توانند از ساده تا بسیار پیچیده متغیر بوده و دارایی‌هایی به ارزش میلیون‌ها یا حتی میلیاردها دلار را در خود جای دهند. اصل کار قرارداد هوشمند به این صورت است که اگر اتفاق X رخ داد، این دستور Y را اجرا کن و اگر اتفاق Z رخ داد، دستور متغیر دیگری را اجرا کن. آسیب‌پذیری از نظر امنیتی در کد این قرارداد می‌تواند عواقب مخربی از جمله سرقت تمام دارایی‌هایی آن را به دنبال داشته باشد. به همین دلیل اهمیت دارد که برای اولین بار به درستی انجام شود. این قراردادها منبع باز هستند؛ بنابراین پس از استقرار، کد آن‌ها به صورت عمومی در دسترس است. در این شرایط اگر یک هکر بتواند باگ آن‌ها را پیدا کند، می‌تواند فورا از آن استفاده کند. علاوه بر این اصطلاح آسیب‌پذیری‌های امنیتی در طول زمان امکان‌پذیر نیست؛ زیرا کد Smart Contract پس از استقرار روی بلاکچین و اجرا، قابل تغییر نیست.

تائید رسمی قرارداد هوشمند چگونه کار می‌کند؟

تائید رسمی قرارداد هوشمند به منظور پیشگیری از اشکال و آسیب‌پذیری، از طریق ارائه منطق و رفتار مطلوب Smart Contract به عنوان گزاره‌های ریاضی صورت می‌گیرد. در نهایت از ابزارهای خودکار جهت بررسی صحت این گزاره‌ها استفاده می‌کنند.

فرایند تائید رسمی قرارداد هوشمند شامل موارد زیر می‌شود:

• تعریف مشخصات و ویژگی‌های مورد نظر به زبان رسمی
• ترجمه کد به یک فرم رسمی مانند مدل‌های ریاضی یا منطق
• استفاده از اثبات‌کننده‌های قضیه خودکار یا بررسی‌کننده‌های مدل برای تائید مشخصات و ویژگی‌ها
• تکرار فرآیند تائید به منظور یافتن و رفع هرگونه خطا یا انحراف از ویژگی‌های مورد نظر

چرا تائید رسمی قرارداد هوشمند مهم است؟

استفاده از منطق و استدلال ریاضی در فرایند تائید رسمی قرارداد هوشمند کمک می‌کند تا این اطمینان به وجود آید که نمونه تائید شده عاری از هرگونه اشکال و آسیب‌پذیری و سایر رفتارهای ناخواسته است. همچنین به افزایش اطمینان و اعتماد کمک می‌کند؛ زیرا صحت ویژگی‌های آن به طور جدی ثابت شده است. در ادامه چند نمونه از اثرات تائید رسمی برای جلوگیری از ضرر مالی را بررسی می‌کنیم.

• Uniswap: یکی از شناخته‌شده‌ترین بازارسازهای خودکار (AMM) به حساب می‌آید. زمانی که Uniswap V1 توسعه پیدا کرد، به صورت رسمی تائید شد. قبل از انتشار، در فرایند تائید رسمی قرارداد هوشمند خطاهایی که می‌توانست منجر به خالی شدن پول Uniswap V1 شود شناسایی و برطرف شد.
• Balancer: یکی دیگر از AMMهای شناخته شده است که قرارداد هوشمند Balancer V2 آن به صورت رسمی تائید شد. در این فرایند محاسبه نادرست کارمزد مربوط به وام فلش، که می‌توانست صرافی را در برابر سرقت آسیب‌پذیر کند، شناسایی و برطرف شد.
• SafeMoon: قراردادSafeMoon V1 یک اشکال ظریف داشت که در فرایند Formal Verification of Smart Contracts شناسایی شد. در این مورد چنانچه قبل از انصراف از مالکیت، عملیات خاصی انجام می‌شد ممکن بود مالک پس از صرف‌نظر از قرارداد، مالکیت مجدد آن را تصرف کند.

چگونه تائید رسمی قرارداد هوشمند و ممیزی دستی با هم کار می‌کنند؟

تائید رسمی، یک روش سیستماتیک و خودکار به منظور بررسی منطق و رفتار قرارداد در برابر ویژگی‌های مورد نظر آن ارائه می‌کند. این فرایند، شناسایی و رفع هرگونه خطا یا باگ احتمالی را تسهیل می‌کند. Formal Verification of Smart Contracts به خصوص برای یافتن مسائل پیچیده و ظریف که تشخیص آن‌ها از طریق ممیزی دستی دشوار است، بسیار کاربردی خواهد بود. 

ممیزی دستی شامل بررسی تخصصی کد، طراحی و استقرار یک قرارداد هوشمند در بلاکچین است. در اینجا ممیز از تجربه و تخصص خود بهره گرفته و با ارزیابی امنیتی کل نمونه، خطرات امنیتی آن را شناسایی می‌کند. در این فرایند، ممیز می‌تواند بررسی کند که آیا فرایند تائید رسمی قرارداد هوشمند به نحو درست انجام شده یا خیر؛ آن‌ها می‌توانند هرگونه مشکلی را که ممکن است توسط ابزارهای خودکار شناسایی نشده باشد را شناسایی کنند.

ترکیب این دو فرایند، یعنی ممیزی دستی با تائید رسمی، می‌تواند یک بسته ارزیابی جامع و کامل از امنیت را ارائه کند. در واقع این ترکیب یک رویکرد دفاعی عمیق نسبت به امنیت است که از قابلیت‌های منحصر به فرد انسان و ماشین استفاده می‌کند.

تائید رسمی قرارداد هوشمند؛ فرایند شناسایی و رفع خطا

استفاده از تائید رسمی قرارداد هوشمند به همراه ممیزی دستی به منظور اطمینان از ارزیابی جامع و کامل وضعیت امنیتی Smart Contract ضروری است. با توجه به اینکه آسیب‌پذیری در کد قرادادها می‌توان عواقب و پیامدهای مخربی از جمله از بین رفتن تمام دارایی‌های را به دنبال داشته باشد. تائید رسمی فرایندی است که به صورت سیستماتیک و خودکار انجام می‌شود تا این اطمینان را به وجود آورد که قرارداد هوشمند برای استقرار و اجرا بر روی بلاکچین عاری از هرگونه اشکال، خطا و آسیب‌پذیری است.