چگونه با تایید رسمی می‌توان از بی‌نقص بودن قراردادهای هوشمند اطمینان یافت؟

در خصوص مدل‌های معنایی ماشین مجازی اتریوم (EVM) و تایید رسمی قراردادهای هوشمند با کمک فریم‌ورک‌های مختلف، تحقیقات آکادمیک بسیاری صورت گرفته است. در این مقاله می‌خواهیم به رویکردی مبتنی بر اجرای سمبلیک و اثبات قضیه‌ی Z3 بپردازیم و به شما نشان دهیم که این روش قادر به شناسایی باگ‌های زیرکانه است، مثلاً باگ‌هایی که از مکانیزم‌های Solidity برای دسترسی به حافظه نشأت گرفته‌اند. در این مطلب به عنوان نمونه از Ownable استفاده می‌کنیم، قراردادی پایه‌ای که علاوه بر متغیر وضعیت مالک، سازنده (Constructor)، اصلاح‌کننده (Modifier) و تابع انتقال مالکیت را هم تعریف می‌کند.

0 88

امنیت قراردادهای هوشمند موضوع مهمی است. در گذشته درباره‌ شناسایی مشکلات امنیتی در بایت‌کد اتریوم گفته بودیم، ولی این آزمایش‌های عمومی چیز زیادی را مشخص نمی‌کنند. در حالت ایده‌آل، باید مطمئن باشیم که قرارداد ما در ۱۰۰ درصد مواقع درست کار می‌کند. تایید رسمی (Formal Verification) به ما ثابت می‌کند که خطاهای مشخص دیگر هرگز رخ نخواهند داد.

رایانش فضای وضعیت

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

موتور اجرای سمبلیک Mythril Classic فضای وضعیت را به روشی کاملاً خودکار محاسبه می‌کند. برای تصویرسازیِ مسیرهای ممکن در برنامه، می‌توانیم نمودار کنترل را با ابزار خط فرمان myth تولید کنیم.

$ myth -g Ownable.html Ownable.sol

نتیجه نموداری خواهد بود که نمای کلی جریان برنامه را به شما نشان می‌دهد. در این نمودار، هر گره نمایان‌گر بلاکی اساسی از کد است، در حالی که لبه‌ها شرایط مسیر را نشان می‌دهند.

chart

نقشه‌برداری کامل از فضای وضعیت همیشه به این سادگی نیست: سازه‌هایی نظیر حلقه‌های نامحدود و فراخوان‌های برگشتیِ درون-قراردادی می‌توانند به افزایش نماییِ تعداد وضعیت‌ها منجر شوند. ولی با توجه به مفهوم سوخت (Gas) در اتریوم، می‌توانیم مطمئن باشیم که اجرای این حالت‌ها همیشه دچار وقفه می‌شود. بعداً درباره‌ی این موضوع مطلبی خواهیم نوشت، ولی فعلاً بگذارید کار را با همین مثال ساده ادامه دهیم.

مشخصات

با توجه به بایت‌کد کامپایل‌شده‌ی قرارداد Ownable، می‌خواهیم ثابت کنیم که Ownable با خصیصه‌ی ایمنی (Safety Property) درست عمل می‌کند:

«مالکیت تنها از طریق مالک قرارداد قابل انتقال است.»

ما این خصیصه را با استفاده از زبان مقاله‌ی زرد یا یلو پیپر (Yellow Paper) اتریوم رسمی‌سازی می‌کنیم: وضعیت سراسری با علامت σ، وضعیت ماشین با علامت μ و بقیه نیز به همین صورت مشخص می‌شوند. برخی از این علائم در تصویر زیر تشریح شده‌اند.

با پیروی از قراردادهای کامپایلرهای Solidity، مالک متغیر با مقداری که در اسلات (Slot) صفر ذخیره گردیده (با بررسی بایت‌کد مربوطه می‌توانید به این موضوع پی ببرید) نمایش داده می‌شود. به همین خاطر ما با آن دسته از زیرمجموعه‌های وضعیت انتقال σ => σ’ کار داریم که محتویات فضای ذخیره‌سازی اسلات صفر در آن‌ها تغییر کرده باشد:

https://cdn-images-1.medium.com/max/1600/1*9TtEzXsAEfWegTSQVe2Dhg.png

با توجه به تعریف زبان EVM، فقط ساختار SSTORE فضای ذخیره‌سازی سراسری را تغییر می‌دهد. پس آسان‌تر می‌توانیم مجموعه‌ی وضعیت‌های ابتداییِ مربوط به σ را با انتخاب جفت‌های وضعیت سراسری و ماشین (σ و μ) به دست بیاوریم. یعنی جایی که:

https://cdn-images-1.medium.com/max/1600/1*qHfy5oQz-Kcmp9A_YF1lsw.png

اگر احقاق این فرمول منطقی ممکن باشد، وضعیت خطا به وجود می‌آید:

Formula

به زبان ساده سعی کردیم ثابت کنیم که رسیدن به نقطه‌ای در برنامه که در آن مالک متغیر تغییر کند غیرممکن است، اما msg.sender با مالک فعلی مطابقت نداشت.

ترجمه‌ مشخصات مربوطه به زبان برنامه‌نویسی پایتون

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

اگر این تحلیل را بر مقادیر برگشتی از Ownable اجرا کنیم، نتیجه‌ زیر حاصل می‌شود:

$ ./analysis.py Ownable.sol

Analysis completed.

از آن‌جایی که هیچ مثال نقضی پیدا نشد، می‌توانیم نتیجه بگیریم که Ownable با همان مشخصات متغیر وضعیت مالک در امان است، هرچند نقایص معدودی مشاهده می‌شود:

  • فرض می‌کنیم که ماشین مجازی اتریوم همیشه به‌درستی کار می‌کند؛
  • این نتیجه‌گیری فقط در حال ایزوله به قرارداد Ownable صدق می‌کند، نه لزوماً برای قراردادهایی که از آن مشتق شده است.

شناسایی باگ‌های نه-چندان-واضح

نتیجه‌ فرآیندهای بالا چندان غافل‌گیرکننده نبود: به کد Solidity نگاه کنید، پر واضح است که این مشخصات همیشه درست خواهد بود. نکته‌ی جالب توجه اما این است که ابزار تحلیلی ما هر گونه نقض وضعیت، از جمله باگ‌های زیرکانه‌ای را که ممکن است در نگاه اول به چشم نیایند، شناسایی می‌کند. فرض کنید Pwnable.sol نسخه‌ی تغییریافته‌ی Ownable.sol است که یک آرایه‌ی پویا به آن اضافه شده:

با یک نگاه اجمالی، کد بالا آن‌قدرها هم بد به نظر نمی‌رسد: چرا که ()transferOwnership همچنان تنها تابعی است که برای متغیر مالک نوشته می‌شود. این تابع تحت حفاظت اصلاح‌کننده‌ی ()onlyOwner قرار دارد. اما ابزار تحلیلی این دفعه شکایت می‌کند:

$ python analysis.py Pwnable.sol

Violation found! Function: _function_0x7ca5dcce, address: 410

storage_1 = 0x4ef1d2ad89edf8c4d91132028e8195cdf30bb4b5053d4f8cd260341d48080000

caller = 0x0

storage_0 = 0xffffffffffffffffffffffffffffffffffffffff00

calldata__0 = 0x7ca5dcce00000000000000000000000000000000000000000000000000000000

calldatasize_ = 0x4

calldata__4 = 0x4ef1d2ad89edf8c4d91132028e8195cdf30bb4b5053d4f8cd260341d4805f30a

callvalue = 0x0

Analysis completed.

 

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

  • طول آرایه در فضای اسلات ۱ ذخیره شده.
  • داده‌ها در آدرس ذخیره‌سازی keccak(1) + offset ذخیره شده.

وقتی آفست معادل ((MAX_UINT — keccac(1) باشد، این مقدار به صفر اضافه شده و آدرس ذخیره‌سازی اسلات صفر را مدنظر قرار می‌دهیم. به یاد داشته باشید که علت این اتفاق فقط به خاطر این است که a1.length عمداً در قسمت Constructor کمتر از کد عادی در نظر گرفته شده. ولی موارد مشابه این مشکل گاه و بیگاه در عمل رخ می‌دهند: در Solidity، متغیر طول آرایه معمولاً به طور مستقیم کنترل می‌شود، و array.length نیز یک الگوی رایج است.

بهره‌گیری

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

  • Calldata_0: هش امضای تابع (fun (unit256,address
  • Calldata_4: آفستی که توسط حل‌کننده پیدا شده باید با \[ 2**256-keccak256(1) \]  مطابقت داشته باشد

می‌توان از مقدار آفستی که توسط حل‌کننده به دست آمده به همان صورتی هست استفاده کرد. ولی برای شفافیت بیشتر، نحوه‌ی محاسبه‌ آن در پایتون به شکل زیر است:

>>> from ethereum import utils

>>> hash = utils.sha3("\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01")

>>> hash_num = int.from_bytes(hash, byteorder="big")

>>> 2**256 — hash_num

35707666377435648211887908874984608119992236509074197713628505308453184860938

>>> hex(2**256-hash_num)

'0x4ef1d2ad89edf8c4d91132028e8195cdf30bb4b5053d4f8cd260341d4805f30a'

 

در نهایت به فراخوان تابع زیر می‌رسیم:

fun(35707666377435648211887908874984608119992236509074197713628505308453184860938,”0x11223344556677889900112233445566deadbeef”)

برای این که مطمئن شویم این خروجی کار می‌کند، می‌توانیم Pwnable.sol را در سرویس Remix پیاده‌سازی کرده و فراخوان تابع مربوطه را از طریق رابط کاربری آن اجرا کنیم (فراموش نکنید که آرگومان عدد صحیح یا Integer باید در نقل قول نوشته شود). بعد از اجرای فراخوان و خواندن محتویات متغیر مالک، آدرس جدید برگردانده می‌شود.

python

جمع‌بندی

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

مطالعه‌ی بیشتر

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

  • خراب کردن قراردادهای هوشمند برای سرگرمی و سودبری واقعی
  • مخزن تایید رسمیِ Yoichi Hira در گیت‌هاب
  • راهنمای جامع Sidney Amani در خصوص تایید بایت‌کد قراردادهای هوشمند
  • استفاده از حل‌کننده‌ی SMT برای تایید برنامه‌ها

پیرامون پلتفرم میتریل

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

شاید از این مطالب هم خوشتان بیاید.

ارسال پاسخ

آدرس ایمیل شما منتشر نخواهد شد.