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

مقدمه

قراردادهای هوشمند، برنامه‌های کامپیوتری هستند که روی بلاک‌چین مستقر شده و در صورت برقراری شرایطی خاص، به صورت خودکار اجرا می‌شوند. این قراردادها می‌توانند بسیار ساده یا پیچیده باشند و بعضی از آنها کنترل میلیون‌ها یا حتی میلیاردها دلار دارایی را در اختیار دارند.

آسیب‌پذیری‌های امنیتی در کد قرارداد هوشمند می‌توانند عواقب بسیار بدی داشته باشند از جمله سرقت دارایی‌های تحت کنترل قرارداد هوشمند. در سال 2021 یک بازارگردان خودکار (AMM) به نام Uranium Finance به دلیل وجود یک خطای تایپی در یک قرارداد هوشمند، 50 میلیون دلار دارایی را از دست داد.

همچنین در همان سال، Compound Finance به دلیل اشتباه در تایپ یک کاراکتر، 80 میلیون دلار پاداش دریافت نشده را از دست داد. در سال 2022 به دلیل وجود یک باگ در قرارداد هوشمند پل Wormhole، این سیستم 320 میلیون دلار متضرر شد.

با توجه به این نکات، لازم است که از همان ابتدا کدهای قرارداد هوشمند درست نوشته شوند. قراردادهای هوشمند، اپن سورس هستند یعنی وقتی قرارداد مستقر شد، همه می‌توانند کد آن را ببینند. اگر هکری موفق به پیدا کردن یک باگ شود، می‌تواند بلافاصله از آن سوء استفاده کند. بعلاوه، از آنجایی که معمولاً پس از استقرار کد قرارداد هوشمند امکان تغییر آن وجود ندارد، نصب وصله‌های امنیتی در رابطه با این قراردادها جزء راهکارهای عملی نیست.

تأیید قرارداد هوشمند چگونه انجام می‌شود؟

فرایند اعتبارسنجی قراردادهای هوشمند با نشان دادن منطق و رفتار مطلوب قرارداد هوشمند در قالب عبارات محاسباتی انجام می‌شود. سپس بازرسان از ابزارهای خودکار برای بررسی درستی این عبارات استفاده می‌کنند.

این فرایند شامل انجام کارهای زیر است:

1. تعریف مشخصات و ویژگی‌های مطلوب قرارداد به یک زبان رسمی.
2. ترجمه کد قرارداد هوشمند به یک حالت رسمی مثل منطق یا مدل‌های محاسباتی.
3. استفاده از ابزارهای خودکار اثبات قضیه یا بررسی مدل برای اعتبارسنجی مشخصات و ویژگی‌های قرارداد.
4. تکرار فرایند اعتبارسنجی برای یافتن و حل هر گونه خطا یا انحراف از ویژگی‌های مطلوب.

چرا اعتبارسنجی قرارداد هوشمند مهم است؟

استفاده از منطق ریاضی به کسب اطمینان از اینکه قراردادهای هوشمند تأیید شده عاری از باگ، آسیب‌پذیری و هر رفتار ناخواسته دیگری هستند کمک می‌کند. همچنین این کار باعث افزایش اطمینان و اعتماد نسبت به قرارداد می‌شود.

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

یونی سواپ

یونی سواپ یک AMM مشهور است. قرارداد هوشمند نسخه 1 یونی سواپ پس از تکمیل، به صورت رسمی تأیید شد. در این فرایند، خطاهایی پیدا و رفع شدند که امکان تخلیه کامل دارایی‌ها را از یونی سواپ فراهم می‌کردند.

بالانسر

بالانسر نسخه 2 هم یک AMM است که به صورت رسمی اعتبارسنجی و تأیید شده است. در این فرایند، یک اشتباه در محاسبه کارمزدها برای وام‌های فلش در این قرارداد هوشمند پیدا شد که امکان سرقت دارایی‌ها را از این اکسچنج فراهم می‌کرد.

سیف مون

سیف مون نسخه 1 هم یک باگ مخفی داشت که پس از استقرار آن شناسایی شد. این باگ، به مالک قرارداد امکان می‌داد که آن را واگذار کرده و بعداً دوباره مالکیت آن را پس بگیرد (اگر مالک قرارداد پیش از واگذاری آن یکسری عملیات خاص را انجام می‌داد).

این باگ در بیشتر بررسی‌های دستی انشعابات نسخه اول سیف مون نادیده گرفته شده بود چون پیدا کردن آن نیاز به تحلیل ترکیبات خاصی از مقادیر متغیرهای برنامه داشت. از قلم انداختن چنین مقادیری توسط انسان‌ها و پیدا کردن آنها توسط سیستم‌های کامپیوتری بسیار راحت است.

ترکیب بررسی دستی و تأیید رسمی

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

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

ترکیب بازرسی‌های دستی و تأیید رسمی به ارزیابی کامل و جامع امنیت قراردادهای هوشمند کمک می‌کند. به این ترتیب شانس پیدا کردن و رفع آسیب‌پذیری‌ها افزایش پیدا می‌کند. نتیجه این فرایند، به وجود آمدن یک رویکرد «دفاع در عمق» برای حفاظت از امنیت است که در آن از قابلیت‌های منحصربفرد انسان‌ها و ماشین‌ها استفاده می‌شود.

جمع بندی

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

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