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

قراردادهای هوشمند امکان ایجاد برنامه‌های غیرمتمرکز، بدون نیاز به اعتماد و قوی را فراهم می‌کنند که موارد استفاده جدیدی را معرفی کرده و ارزش را برای کاربران آزاد می‌کنند. از آنجایی که قراردادهای هوشمند مقادیر زیادی از ارزش را مدیریت می‌کنند، امنیت یک ملاحظه‌ی حیاتی برای توسعه‌دهندگان است.

تأیید رسمی یکی از تکنیک های توصیه شده برای بهبود امنیت قرارداد هوشمند است. تأیید رسمی، که از روش‌های رسمی(opens in a new tab) برای تعیین، طراحی و تأیید برنامه‌ها استفاده می‌کند، سال‌هاست که برای اطمینان از صحت سیستم‌های سخت‌افزاری و نرم‌افزاری حیاتی استفاده می‌شود.

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

تایید رسمی چیست؟

تأیید رسمی به فرآیند ارزیابی صحت یک سیستم با توجه به مشخصات رسمی اشاره دارد. به عبارت ساده‌تر، تأیید رسمی به ما امکان می دهد بررسی کنیم که آیا رفتار یک سیستم برخی از الزامات را برآورده می کند (یعنی آنچه را که ما می خواهیم انجام می دهد).

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

مدل رسمی چیست؟

در علوم کامپیوتر، مدل رسمی(opens in a new tab) توصیفی ریاضی از یک فرآیند محاسباتی است. برنامه‌ها به توابع ریاضی (معادلات) انتزاعی می‌شوند، و مدل نحوه محاسبه خروجی‌های توابع را با توجه به ورودی توصیف می‌کند.

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

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

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

برعکس، سایر مدل‌های رسمی بر رفتار سطح پایین قرارداد هوشمند تمرکز دارند. در حالی که مدل‌های سطح بالا می‌توانند به استدلال در مورد عملکرد قرارداد کمک کنند، ممکن است نتوانند جزئیات مربوط به عملکرد داخلی پیاده‌سازی را ثبت کنند. مدل‌های سطح پایین از نمای جعبه سفید برای تجزیه و تحلیل برنامه استفاده می‌کنند و برای استدلال در مورد ویژگی‌های مربوط به اجرای قرارداد، به نمایش‌های سطح پایین‌تر برنامه‌های قرارداد هوشمند، مانند ردیابی برنامه و گراف‌های جریان کنترل(opens in a new tab) تکیه می‌کنند.

مدل‌های سطح پایین ایده‌آل در نظر گرفته می‌شوند زیرا نشان‌دهنده اجرای واقعی یک قرارداد هوشمند در محیط اجرای اتریوم هستند (یعنی EVM). تکنیک‌های مدل‌سازی سطح پایین به‌ویژه در ایجاد ویژگی‌های ایمنی حیاتی در قراردادهای هوشمند و شناسایی آسیب‌پذیری‌های بالقوه مفید هستند.

مشخصات رسمی چیست؟

یک مشخصات به سادگی یک الزام فنی است که یک سیستم خاص باید برآورده کند. در برنامه نویسی، مشخصات، ایده های کلی در مورد اجرای یک برنامه (یعنی آنچه برنامه باید انجام دهد) را نشان می دهد.

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

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

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

انواع مشخصات رسمی قراردادهای هوشمند

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

مشخصات رسمی با استفاده از عناصر منطق برنامه(opens in a new tab) به دست می‌آیند که امکان استدلال رسمی در مورد ویژگی‌های یک برنامه را فراهم می‌کند. یک منطق برنامه دارای قوانین رسمی است که رفتار مورد انتظار یک برنامه را (به زبان ریاضی) بیان می‌کند. منطق برنامه های مختلف در ایجاد مشخصات رسمی استفاده می شود، از جمله منطق دسترسی پذیری(opens in a new tab)، منطق زمانی(opens in a new tab)، و منطق هوآر(opens in a new tab).

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

مشخصات سطح بالا

همانطور که از نام آن پیداست، یک مشخصات سطح بالا (که "مشخصات مدل گرا" نیز نامیده می شود) رفتار سطح بالای یک برنامه را توصیف می کند. مشخصات سطح بالا یک قرارداد هوشمند را به عنوان یک ماشین حالت متناهی(opens in a new tab) (FSM) مدل‌سازی می‌کند که می‌تواند با انجام عملیات بین حالت‌ها جابه‌جا شود، و از منطق زمانی برای تعریف خواص رسمی برای مدل FSM استفاده می‌شود.

منطق‌های زمانی(opens in a new tab) "قوانینی برای استدلال درباره گزاره‌هایی هستند که از نظر زمانی واجد شرایط هستند (مثلاً "من همیشه گرسنه هستم" یا "من در نهایت گرسنه خواهم شد.")" هنگامی که برای تأیید رسمی اعمال می شود، از منطق های زمانی برای بیان ادعاهای مربوط به رفتار صحیح سیستم های مدل سازی شده به عنوان ماشین های حالت استفاده می شود. به طور خاص، یک منطق زمانی وضعیت‌های آینده‌ای را که یک قرارداد هوشمند می‌تواند در آن قرار گیرد و نحوه انتقال آن بین حالت‌ها را توصیف می‌کند.

مشخصات سطح بالا به طور کلی دو ویژگی مهم زمانی را برای قراردادهای هوشمند نشان می دهد: ایمنی و زنده‌مانی. ویژگی های ایمنی بیانگر این ایده است که "هیچ چیز بدی اتفاق نمی افتد" و معمولاً بیانگر تغییر ناپذیری است. یک ویژگی ایمنی ممکن است الزامات کلی نرم‌افزار را تعریف کند، مانند آزادی از قفل شدن(opens in a new tab)، یا خواص خاص دامنه را برای قراردادها بیان کند (به عنوان مثال، ثابت‌های کنترل دسترسی برای توابع، مقادیر مجاز متغیرهای حالت یا شرایط برای انتقال توکن).

به عنوان مثال این الزام ایمنی را در نظر بگیرید که شرایط استفاده از transfer() یا transferFrom() در قراردادهای توکن ERC-20 را پوشش می دهد: "باقیمانده حساب فرستنده هرگز کمتر از مقدار درخواستی توکن‌های ارسال شده نیست.". این توصیف به زبان طبیعی از یک قرارداد ثابت را می توان به یک مشخصات رسمی (ریاضی) ترجمه کرد، که سپس می توان آن را به شدت از نظر اعتبار بررسی کرد.

خواص زنده بودن تأکید می‌کنند که "بالاخره اتفاق خوبی می‌افتد" و مربوط به توانایی یک قرارداد برای پیشرفت از طریق حالات مختلف است. یک مثال از ویژگی زنده بودن "نقدینگی" است که به توانایی یک قرارداد برای انتقال موجودی خود به کاربران در صورت درخواست اشاره دارد. اگر این ویژگی نقض شود، کاربران نمی‌توانند دارایی‌های ذخیره‌شده در قرارداد را برداشت کنند، مانند آنچه در حادثه کیف پول Parity(opens in a new tab) اتفاق افتاد.

مشخصات سطح پایین

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

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

مشخصات رسمی سطح پایین را می توان به عنوان ویژگی های سبک هوآر یا به صورت ثابت در مسیرهای اجرا ارائه کرد.

خواص سبک هوآر

منطق هوآر(opens in a new tab) مجموعه‌ای از قوانین رسمی را برای استدلال در مورد صحت برنامه‌ها، از جمله قراردادهای هوشمند، ارائه می‌کند. یک ویژگی به سبک هوآر با یک سه‌گانه هوآر {P}c{Q} نشان داده می‌شود، که در آن c یک برنامه است و P و Q گزاره‌هایی در مورد حالت c (یعنی برنامه) هستند که به ترتیب به صورت پیش شرط‌ها و پس شرط‌ها توصیف می‌شوند.

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

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

کسب اثبات صحت کامل دشوار است زیرا برخی از اجراها ممکن است قبل از خاتمه به تأخیر بیفتند یا اصلاً هرگز خاتمه نیابند. با این حال، این سؤال که آیا اجرا خاتمه می‌یابد یا خیر، قابل بحث است، زیرا مکانیسم گس اتریوم از حلقه‌های بی‌نهایت برنامه جلوگیری می‌کند (اجرا یا با موفقیت خاتمه می‌یابد یا به دلیل خطای "تمام شدن گس" پایان می‌یابد).

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

بسیاری از چارچوب‌های تأیید رسمی از مشخصات سبک هوآر برای اثبات صحت معنایی توابع استفاده می‌کنند. همچنین می‌توان خواص به سبک هوآر (به عنوان ادعاها) را به طور مستقیم با استفاده از عبارات require و assert در سالیدیتی به کد قرارداد اضافه کرد.

عبارات require بیانگر یک پیش شرط یا ثابت هستند و اغلب برای اعتبارسنجی ورودی های کاربر استفاده می شوند، در حالی که assert یک شرط پسین لازم برای ایمنی را نشان می دهد. به عنوان مثال، کنترل دسترسی مناسب برای توابع (مثالی از یک ویژگی ایمنی) را می‌توان با استفاده از require به عنوان یک بررسی پیش شرط بر روی هویت حساب فراخوانی کننده به دست‌آورد. به طور مشابه، یک ثابت بر روی مقادیر مجاز متغیرهای حالت در یک قرارداد (به عنوان مثال، کل تعداد توکن‌های در گردش) را می‌توان از نقض با استفاده از assert برای تأیید وضعیت قرارداد پس از اجرای تابع محافظت کرد.

ویژگی‌های سطح ردیابی

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

این رویکرد بر مدل قراردادهای هوشمند به عنوان سیستم‌های انتقال حالت با برخی حالت‌های از پیش تعریف‌شده (توصیف‌شده توسط متغیرهای حالت) به همراه مجموعه‌ای از انتقال‌های از پیش تعریف‌شده (توصیف‌شده توسط توابع قرارداد) متکی است. علاوه بر این، یک گراف جریان کنترل(opens in a new tab) (CFG)، که یک نمایش گرافیکی از جریان اجرای یک برنامه است، اغلب برای توصیف معنایی عملیاتی یک قرارداد استفاده می‌شود. در اینجا، هر ردیابی به عنوان یک مسیر در نمودار جریان کنترل نشان داده می شود.

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

بیایید از نمونه ای از قرارداد DAO استفاده کنیم که دارای برخی از توابع در دسترس عموم برای توصیف ویژگی های سطح ردیابی است. در اینجا، ما فرض می کنیم که قرارداد DAO به کاربران اجازه می دهد تا عملیات زیر را انجام دهند:

• واریز وجه

• رای دادن به یک پیشنهاد پس از واریز وجوه

• درخواست بازپرداخت در صورت عدم رای دادن به یک پیشنهاد

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

تکنیک‌هایی برای تأیید رسمی قراردادهای هوشمند

بررسی مدل

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

بررسی مدل مستلزم ایجاد یک نمایش ریاضی انتزاعی از یک سیستم (به عنوان مثال، یک قرارداد) و بیان ویژگی‌های این سیستم با استفاده از فرمول‌هایی است که ریشه در منطق گزاره‌ای(opens in a new tab) دارند. این کار الگوریتم بررسی مدل را ساده می کند، یعنی ثابت کند که یک مدل ریاضی یک فرمول منطقی معین را برآورده می کند.

بررسی مدل در راستی‌آزمایی رسمی عمدتاً برای ارزیابی ویژگی‌های زمانی استفاده می‌شود که رفتار یک قرارداد را در طول زمان توصیف می‌کنند. ویژگی های موقت قراردادهای هوشمند شامل ایمنی و زندگی است که قبلا توضیح دادیم.

به عنوان مثال، یک ویژگی امنیتی مربوط به کنترل دسترسی (به عنوان مثال، فقط مالک قرارداد می تواند selfdestruct را فراخوانی کند) می تواند در منطق رسمی نوشته شود. پس از آن، الگوریتم بررسی مدل می تواند تأیید کند که آیا قرارداد با این مشخصات رسمی مطابقت دارد یا خیر.

بررسی مدل از کاوش فضای حالت استفاده می‌کند، که شامل ساخت همه حالت‌های ممکن یک قرارداد هوشمند و تلاش برای یافتن حالت‌های قابل دسترسی است که منجر به نقض مالکیت می‌شود. با این حال، این می تواند به تعداد نامحدودی از حالت ها منجر شود (معروف به "مشکل انفجار حالت")، از این رو بررسی کنندگان مدل برای امکان تحلیل کارآمد قراردادهای هوشمند به تکنیک های انتزاعی تکیه می کنند.

اثبات قضیه

اثبات قضیه روشی برای استدلال ریاضی درباره صحت برنامه ها از جمله قراردادهای هوشمند است. این شامل تبدیل مدل سیستم قرارداد و مشخصات آن به فرمول های ریاضی (گزاره های منطقی) است.

هدف از اثبات قضیه، تأیید هم ارزی منطقی بین این گزاره ها است. "تعادل منطقی" (که "منطقی دو مفهومی" نیز نامیده می شود) نوعی رابطه بین دو عبارت است به طوری که گزاره اول درست است اگر و فقط اگر گزاره دوم درست باشد.

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

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

در نتیجه، کمک های انسانی اغلب برای راهنمایی اثبات کننده قضیه در استخراج براهین صحت مورد نیاز است. استفاده از تلاش انسانی در اثبات قضیه، استفاده از آن را نسبت به بررسی مدل که کاملاً خودکار است، گران‌تر می‌کند.

اجرای نمادین

اجرای نمادین روشی برای تجزیه و تحلیل قرارداد هوشمند با اجرای توابع با استفاده از مقادیر نمادین (به عنوان مثال، x > 5) به جای مقادیر مشخص ( به عنوان مثال، x == 5). به عنوان یک تکنیک تأیید رسمی، اجرای نمادین برای استدلال رسمی در مورد ویژگی‌های سطح ردیابی در کد قرارداد استفاده می‌شود.

اجرای نمادین یک رد اجرا را به عنوان یک فرمول ریاضی بر روی مقادیر ورودی نمادین نشان می دهد که در غیر این صورت گزاره مسیر نامیده می شود. یک حل‌کننده SMT(opens in a new tab) برای بررسی اینکه آیا یک گزاره مسیر "رضایت‌پذیر" است یا نه استفاده می‌شود (یعنی مقداری وجود دارد که می‌تواند فرمول را برآورده کند). اگر یک مسیر آسیب پذیر قابل رضایت باشد، حل کننده SMT یک مقدار مشخص ایجاد می کند که اجرای آن را به سمت آن مسیر هدایت می کند.

فرض کنید تابع قرارداد هوشمند یک مقدار uint (x) را به عنوان ورودی می گیرد و زمانی که x بزرگتر از 5 باشد برمی گردد. و همچنین کمتر از 10. یافتن مقداری برای x که خطا را با استفاده از یک روش آزمایش معمولی ایجاد می‌کند، مستلزم اجرای ده‌ها تست (یا بیشتر) بدون اطمینان از یافتن ورودی محرک خطا است.

برعکس، یک ابزار اجرای نمادین تابع را با مقدار نمادین اجرا می کند: X > 5 ∧ X < 10 (یعنی x بزرگتر از 5 است و x کمتر از 10 است). گزاره مسیر مرتبط x = X > 5 ∧ X < 10 سپس به حل کننده SMT داده می شود تا حل کند. اگر مقدار خاصی با فرمول x = X > 5 ∧ X < 10، حل‌کننده SMT آن را محاسبه می‌کند - برای مثال، حل‌کننده ممکن است 7 را به عنوان مقدار x تولید کند.

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

علاوه بر این، اجرای نمادین نسبت به سایر تکنیک‌های مبتنی بر ویژگی (مثلاً فازی) که به‌طور تصادفی ورودی‌های یک تابع را تولید می‌کنند، نکات مثبت کاذب کمتری تولید می‌کند. اگر یک حالت خطا در طول اجرای نمادین ایجاد شود، می توان یک مقدار مشخص ایجاد کرد که باعث ایجاد خطا و بازتولید مسئله می شود.

اجرای نمادین همچنین می تواند درجاتی از اثبات ریاضی درستی را ارائه دهد. مثال زیر از یک تابع قرارداد با حفاظت از سرریز را در نظر بگیرید:

1function safe_add(uint x, uint y) returns(uint z){
2
3  z = x + y;
4  require(z>=x);
5  require(z>=y);
6
7  return z;

یک ردیابی اجرا که منجر به سرریز اعداد صحیح می شود باید این فرمول را برآورده کند: z = x + y AND (z >= x) AND (z=>y) AND (z < x OR z < y) بعید است چنین فرمولی حل شود، از این رو یک اثبات ریاضی است که تابع safe_add هرگز سرریز نمی شود.

چرا از تأیید رسمی برای قراردادهای هوشمند استفاده کنیم؟

نیاز به قابلیت اطمینان

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

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

اثبات صحت عملکرد

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

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

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

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

اهداف تأیید ایده آل

هدف راستی‌آزمایی، سیستمی را که باید به‌طور رسمی تأیید شود، توصیف می‌کند. تأیید رسمی به بهترین وجه در «سیستم‌های تعبیه‌شده» (نرم‌افزارهای کوچک و ساده که بخشی از یک سیستم بزرگ‌تر را تشکیل می‌دهند) استفاده می‌شود. آنها همچنین برای دامنه های تخصصی که قوانین کمی دارند ایده آل هستند، زیرا این کار تغییر ابزارها را برای تأیید ویژگی های خاص دامنه آسان تر می کند.

قراردادهای هوشمند - حداقل تا حدی - هر دو الزام را برآورده می کنند. به عنوان مثال، اندازه کوچک قراردادهای اتریوم باعث می شود که آنها را به تأیید رسمی برساند. به طور مشابه، EVM از قوانین ساده پیروی می کند، که تعیین و تأیید ویژگی های معنایی را برای برنامه های در حال اجرا در EVM آسان تر می کند.

چرخه توسعه سریعتر

تکنیک‌های تأیید رسمی، مانند بررسی مدل و اجرای نمادین، معمولاً کارآمدتر از تجزیه و تحلیل منظم کد قرارداد هوشمند (که در طول آزمایش یا ممیزی انجام می‌شود) هستند. این به این دلیل است که تأیید رسمی برای آزمایش ادعاها به مقادیر نمادین متکی است ("اگر کاربر سعی کند n اتر را خارج کند چه؟" برخلاف آزمایشی که از مقادیر مشخصی استفاده می کند ("اگر کاربر بخواهد 5 اتر را خارج کند چه؟".

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

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

معایب تأیید رسمی

هزینه نیروی کار

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

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

منفی های کاذب

تأیید رسمی فقط می تواند بررسی کند که آیا اجرای قرارداد هوشمند با مشخصات رسمی مطابقت دارد یا خیر. به این ترتیب، مهم است که مطمئن شوید مشخصات به درستی رفتارهای مورد انتظار یک قرارداد هوشمند را توصیف می کند.

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

مسائل مربوط به عملکرد

تأیید رسمی با تعدادی از مشکلات عملکرد مواجه می شود. برای مثال، مشکلات انفجار حالت و مسیر که به ترتیب در حین بررسی مدل و بررسی نمادین با آن مواجه می‌شوند، می‌توانند بر رویه‌های تأیید تأثیر بگذارند. همچنین، ابزارهای تأیید رسمی اغلب از حل کننده های SMT و سایر حل کننده های محدودیت در لایه زیرین خود استفاده می کنند و این حل کننده ها بر رویه های محاسباتی فشرده تکیه می کنند.

همچنین، تعیین اینکه آیا یک ویژگی (که به عنوان یک فرمول منطقی توصیف می‌شود) می‌تواند برآورده شود یا خیر، برای تأییدکنندگان برنامه همیشه امکان‌پذیر نیست («مشکل تصمیم‌پذیری(opens in a new tab)») زیرا ممکن است یک برنامه هرگز خاتمه یابد. به این ترتیب، ممکن است اثبات برخی از خواص برای یک قرارداد، حتی اگر به خوبی مشخص شده باشد، غیرممکن باشد.

ابزارهای تأیید رسمی قراردادهای هوشمند اتریوم

زبان های مشخصات برای ایجاد مشخصات رسمی

Act: _*Act اجازه می‌دهد تا مشخصات به‌روزرسانی‌های ذخیره‌سازی، شرایط قبل/پست و متغیرهای قرارداد را مشخص کنید. مجموعه ابزار آن همچنین دارای پشتیبان‌های اثباتی است که می‌توانند ویژگی‌های زیادی را از طریق Coq، حل‌کننده‌های SMT یا hevm اثبات کنند.**

• گیت‌هاب(opens in a new tab)
• اسناد(opens in a new tab)

Scribble - _*Scribble حاشیه نویسی کد در زبان مشخصات Scribble را به ادعاهای مشخصی تبدیل می کند که مشخصات را بررسی می کند.**

• مستندات(opens in a new tab)

Dafny - _*Dafny یک زبان برنامه نویسی آماده تأیید است که برای استدلال و اثبات درستی کد به حاشیه نویسی های سطح بالا متکی است.**

• گیت‌هاب(opens in a new tab)

تأیید کننده های برنامه برای بررسی صحت

Certora Prover - Certora Prover یک ابزار تأیید رسمی خودکار برای بررسی صحت کد در قراردادهای هوشمند است. مشخصات به زبان CVL (زبان تأیید Certora) نوشته شده است، با استفاده از ترکیبی از تجزیه و تحلیل استاتیک و حل محدودیت، نقض مالکیت شناسایی می‌شود.

• وب‌سایت(opens in a new tab)
• اسناد(opens in a new tab)

Solidity SMTCchecker - _*Solidity's SMTCchecker یک مدل بررسی کننده داخلی است که بر اساس SMT (تئوری های مدول رضایت پذیری) و حل شاخ است. تأیید می کند که کد منبع قرارداد با مشخصات در طول تدوین مطابقت دارد یا خیر و به طور ایستا نقض ویژگی های ایمنی را بررسی می کند.**

• گیت‌هاب(opens in a new tab)

solc-verify - _*solc-verify نسخه توسعه یافته کامپایلر سالیدیتی است که می تواند با استفاده از حاشیه نویسی و تأیید برنامه مدولار، تأیید رسمی خودکار را روی کد سالیدیتی انجام دهد.**

• گیت‌هاب(opens in a new tab)

KEVM - _*KEVM یک معناشناسی رسمی از ماشین مجازی اتریوم (EVM) است که در چارچوب K نوشته شده است. KEVM قابل اجرا است و می‌تواند برخی ادعاهای مربوط به ویژگی را با استفاده از منطق دسترس‌پذیری اثبات کند.**

• گیت‌هاب(opens in a new tab)
• مستندات(opens in a new tab)

چارچوب های منطقی برای اثبات قضیه

Isabelle - Isabelle/HOL یک دستیار اثبات است که به فرمول های ریاضی اجازه می دهد تا به زبان رسمی بیان شوند و ابزارهایی برای اثبات آن فرمول ها فراهم می کند. کاربرد اصلی، رسمی‌سازی اثبات‌های ریاضی و به‌ویژه تأیید رسمی است که شامل اثبات صحت سخت‌افزار یا نرم‌افزار رایانه و اثبات ویژگی‌های زبان‌ها و پروتکل‌های رایانه می‌شود.

• گیت‌هاب(opens in a new tab)
• مستندات(opens in a new tab)

Coq - Coq یک اثبات کننده قضیه تعاملی است که به شما امکان می دهد برنامه ها را با استفاده از قضایا تعریف کنید و به طور تعاملی اثبات صحت بررسی شده توسط ماشین را ایجاد کنید.

• گیت‌هاب(opens in a new tab)
• اسناد(opens in a new tab)

ابزارهای مبتنی بر اجرای نمادین برای تشخیص الگوهای آسیب پذیر در قراردادهای هوشمند

Manticore - _ابزاری برای تجزیه و تحلیل ابزار تجزیه و تحلیل بایت کد EVM بر اساس اجرای نمادین.*

• گیت‌هاب(opens in a new tab)
• مستندات(opens in a new tab)

hevm - _*hevm یک موتور اجرای نمادین و جستجوگر معادل برای بایت کد EVM است.**

• گیت هاب(opens in a new tab)

Mythil - ابزار اجرای نمادین برای شناسایی آسیب‌پذیری‌ها در قراردادهای هوشمند اتریوم

• گیت‌هاب(opens in a new tab)
• مستندات(opens in a new tab)

بیشتر بخوانید

• چگونه تأیید رسمی قراردادهای هوشمند کار می کند؟(opens in a new tab)
• چگونه تأیید رسمی می تواند قراردادهای هوشمند بی عیب و نقص را تضمین کند؟(opens in a new tab)
• مروری بر پروژه های تایید رسمی در اکوسیستم اتریوم(opens in a new tab)
• تایید رسمی اند تو اند قرارداد هوشمند سپرده گذاری اتریوم 2.0(opens in a new tab)
• تایید رسمی محبوب ترین قرارداد هوشمند جهان(opens in a new tab)
• SMTCchecker و تأیید رسمی(opens in a new tab)