التحقق الرسمي من العقود الذكية

تجعل العقود الذكية من الممكن إنشاء تطبيقات لامركزية ولا تعتمد على الثقة وقوية تقدم حالات استخدام جديدة وتفتح قيمة للمستخدمين. نظرًا لأن العقود الذكية تتعامل مع كميات كبيرة من القيمة، فإن الأمان يعد اعتبارًا بالغ الأهمية بالنسبة للمطورين.

التحقق الرسمي هو إحدى التقنيات الموصى بها لتحسين أمان العقود الذكية. تم استخدام التحقق الرسمي، والذي يستخدم الأساليب الرسمية (opens in a new tab) لتحديد البرامج وتصميمها والتحقق منها، لسنوات عديدة لضمان صحة أنظمة الأجهزة والبرامج الهامة.

عند تنفيذه في العقود الذكية، يمكن للتحقق الرسمي أن يثبت أن منطق عمل العقد يلبي مواصفات محددة مسبقًا. بالمقارنة مع الطرق الأخرى لتقييم صحة كود العقد، مثل الاختبار، فإن التحقق الرسمي يعطي ضمانات أقوى بأن العقد الذكي صحيح وظيفيًا.

ما هو التحقق الرسمي؟

يشير التحقق الرسمي إلى عملية تقييم صحة النظام فيما يتعلق بالمواصفات الرسمية. بعبارات أبسط، يسمح لنا التحقق الرسمي بالتحقق مما إذا كان سلوك النظام يلبي بعض المتطلبات (أي أنه يفعل ما نريد).

يتم وصف السلوكيات المتوقعة للنظام (العقد الذكي في هذه الحالة) باستخدام النمذجة الرسمية، في حين تعمل لغات المواصفات على تمكين إنشاء خصائص رسمية. ومن ثم، يمكن لتقنيات التحقق الرسمية أن تتأكد من أن تنفيذ العقد يتوافق مع مواصفاته، وتستنتج دليلاً رياضياً على صحة العقد. عندما يلبي العقد مواصفاته، يتم وصفه بأنه "صحيح وظيفيًا"، أو "صحيح من حيث التصميم"، أو "صحيح من حيث البناء".

ما هو النموذج الرسمي؟

في علوم الكمبيوتر، النموذج الرسمي (opens in a new tab) هو وصف رياضي لعملية حسابية. يتم تلخيص البرامج في وظائف رياضية (معادلات)، حيث يصف النموذج كيفية حساب مخرجات الوظائف مع إعطاء مدخلات.

توفر النماذج الرسمية مستوى من التجريد يمكن من خلاله تقييم تحليل سلوك البرنامج. إن وجود نماذج رسمية يسمح بإنشاء مواصفات رسمية، والتي تصف الخصائص المرغوبة للنموذج المعني.

يتم استخدام تقنيات مختلفة لنمذجة العقود الذكية للتحقق الرسمي. على سبيل المثال، يتم استخدام بعض النماذج للتفكير في السلوك رفيع المستوى لعقد ذكي. تطبق تقنيات النمذجة هذه وجهة نظر الصندوق الأسود على العقود الذكية، حيث تنظر إليها كأنظمة تقبل المدخلات وتنفذ العمليات الحسابية بناءً على تلك المدخلات.

تُركز النماذج عالية المستوى على العلاقة بين العقود الذكية والوكلاء الخارجيين، مثل الحسابات المملوكة خارجيًا (EOA)، وحسابات العقود، وبيئة blockchain. تعتبر مثل هذه النماذج مفيدة لتحديد الخصائص التي تحدد كيفية تصرف العقد استجابة لتفاعلات مستخدم معينة.

وعلى العكس من ذلك، تركز النماذج الرسمية الأخرى على السلوك منخفض المستوى للعقد الذكي. على الرغم من أن النماذج عالية المستوى يمكن أن تساعد في التفكير في وظيفة العقد، إلا أنها قد تفشل في التقاط التفاصيل حول العمليات الداخلية للتنفيذ. تطبق النماذج منخفضة المستوى عرض الصندوق الأبيض على تحليل البرنامج وتعتمد على تمثيلات منخفضة المستوى لتطبيقات العقود الذكية، مثل تتبعات البرنامج والرسوم البيانية لتدفق التحكم (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: "رصيد المرسل لا يقل أبدًا عن المبلغ المطلوب من الرموز التي سيتم إرسالها.". يمكن ترجمة هذا الوصف باللغة الطبيعية لثابت العقد إلى مواصفات رسمية (رياضية)، والتي يمكن بعد ذلك التحقق من صحتها بدقة.

تؤكد خصائص الحياة أن "شيئًا جيدًا سيحدث في النهاية" وتتعلق بقدرة العقد على التقدم عبر حالات مختلفة. ومن الأمثلة على خاصية الحيوية "السيولة"، والتي تشير إلى قدرة العقد على نقل أرصدته إلى المستخدمين عند الطلب. إذا تم انتهاك هذه الخاصية، فلن يتمكن المستخدمون من سحب الأصول المخزنة في العقد، مثل ما حدث في حادثة محفظة باريتي (opens in a new tab).

مواصفات منخفضة المستوى

تأخذ المواصفات عالية المستوى نموذج الحالة النهائية للعقد كنقطة بداية وتحدد الخصائص المرغوبة لهذا النموذج. على النقيض من ذلك، غالبًا ما تقوم المواصفات منخفضة المستوى (والتي تسمى أيضًا "المواصفات الموجهة نحو الملكية") بنمذجة البرامج (العقود الذكية) كأنظمة تتألف من مجموعة من الوظائف الرياضية وتصف السلوك الصحيح لهذه الأنظمة.

بمصطلحات أبسط، تحلل المواصفات منخفضة المستوى تتبعات البرنامج وتحاول تحديد خصائص العقد الذكي عبر هذه التتبعات. تشير الآثار إلى تسلسلات تنفيذ الوظائف التي تغير حالة العقد الذكي؛ وبالتالي، تساعد المواصفات منخفضة المستوى في تحديد المتطلبات الخاصة بالتنفيذ الداخلي للعقد.

يمكن تقديم المواصفات الرسمية منخفضة المستوى إما كخصائص على غرار Hoare أو كثوابت على مسارات التنفيذ.

خصائص نمط هوار

منطق هوار (opens in a new tab) يوفر مجموعة من القواعد الرسمية للاستدلال على صحة البرامج، بما في ذلك العقود الذكية. يتم تمثيل خاصية نمط هوار بواسطة ثلاثية هوار {P}c{Q}، حيث c هو برنامج و P و Q هما مسندان على حالة c (أي البرنامج)، ويوصفان رسميًا بأنهما الشروط المسبقة و الشروط اللاحقة على التوالي.

الشرط المسبق هو مسند يصف الشروط المطلوبة للتنفيذ الصحيح لوظيفة ما؛ ويجب على المستخدمين الذين يتصلون بالعقد تلبية هذا المطلب. الشرط اللاحق هو مسند يصف الشرط الذي تنشئه الدالة إذا تم تنفيذها بشكل صحيح؛ ويمكن للمستخدمين أن يتوقعوا أن يكون هذا الشرط صحيحًا بعد استدعاء الدالة. الثابت في منطق هوار هو مسند يتم الحفاظ عليه من خلال تنفيذ دالة (أي أنه لا يتغير).

يمكن لمواصفات نمط هوار أن تضمن إما الصحة الجزئية أو الصحة الكلية. يعد تنفيذ وظيفة العقد "صحيحًا جزئيًا" إذا كان الشرط المسبق صحيحًا قبل تنفيذ الوظيفة، وإذا انتهى التنفيذ، يكون الشرط اللاحق صحيحًا أيضًا. يتم الحصول على دليل الصحة الكاملة إذا كان الشرط المسبق صحيحًا قبل تنفيذ الوظيفة، ويتم ضمان إنهاء التنفيذ وعندما يتم ذلك، يظل الشرط اللاحق صحيحًا.

يعد الحصول على دليل على الصحة الكاملة أمرًا صعبًا نظرًا لأن بعض عمليات الإعدام قد تتأخر قبل الانتهاء، أو قد لا تنتهي أبدًا. ومع ذلك، فإن مسألة ما إذا كان التنفيذ سينتهي أم لا هي نقطة خلافية، لأن آلية الغاز في إيثريوم تمنع حلقات البرنامج اللانهائية (ينتهي التنفيذ إما بنجاح أو ينتهي بسبب خطأ "نفاد الغاز").

ستحتوي مواصفات العقد الذكي التي تم إنشاؤها باستخدام منطق Hoare على شروط مسبقة وشروط لاحقة وثوابت محددة لتنفيذ الوظائف والحلقات في العقد. غالبًا ما تتضمن الشروط المسبقة إمكانية إدخالات خاطئة إلى وظيفة، مع وجود شروط لاحقة تصف الاستجابة المتوقعة لمثل هذه المدخلات (على سبيل المثال، طرح استثناء محدد). بهذه الطريقة تصبح خصائص نمط Hoare فعالة في ضمان صحة تنفيذ العقد.

تستخدم العديد من أطر التحقق الرسمية مواصفات نمط Hoare لإثبات صحة الدلالات للوظائف. من الممكن أيضًا إضافة خصائص على غرار هوار (كتأكيدات) مباشرةً إلى كود العقد باستخدام عبارات require وassert في سوليديتي.

تعبر عبارات require عن شرط مسبق أو ثابت وغالبًا ما تُستخدم للتحقق من صحة مدخلات المستخدم، بينما تلتقط assert شرطًا لاحقًا ضروريًا للسلامة. على سبيل المثال، يمكن تحقيق التحكم المناسب في الوصول إلى الوظائف (مثال على خاصية الأمان) باستخدام require كفحص للشرط المسبق على هوية الحساب المستدعي. وبالمثل، يمكن حماية الثابت على القيم المسموح بها لمتغيرات الحالة في العقد (على سبيل المثال، إجمالي عدد الرموز المتداولة) من الانتهاك باستخدام assert لتأكيد حالة العقد بعد تنفيذ الوظيفة.

خصائص على مستوى التتبع

تصف المواصفات المستندة إلى التتبع العمليات التي تنتقل بعقد بين حالات مختلفة والعلاقات بين هذه العمليات. كما تم شرحه سابقًا، فإن الآثار عبارة عن تسلسلات من العمليات التي تؤدي إلى تغيير حالة العقد بطريقة معينة.

يعتمد هذا النهج على نموذج العقود الذكية كأنظمة انتقال الحالة مع بعض الحالات المحددة مسبقًا (الموصوفة بمتغيرات الحالة) إلى جانب مجموعة من التحولات المحددة مسبقًا (الموصوفة بوظائف العقد). علاوة على ذلك، غالبًا ما يتم استخدام مخطط تدفق التحكم (opens in a new tab) (CFG)، وهو تمثيل رسومي لتدفق تنفيذ البرنامج، لوصف الدلالات التشغيلية للعقد. هنا، يتم تمثيل كل أثر كمسار على الرسم البياني لتدفق التحكم.

في المقام الأول، يتم استخدام مواصفات مستوى التتبع للتفكير في أنماط التنفيذ الداخلي في العقود الذكية. من خلال إنشاء مواصفات مستوى التتبع، فإننا نؤكد على مسارات التنفيذ المقبولة (أي انتقالات الحالة) لعقد ذكي. باستخدام تقنيات مثل التنفيذ الرمزي، يمكننا التحقق رسميًا من أن التنفيذ لا يتبع أبدًا مسارًا غير محدد في النموذج الرسمي.

دعنا نستخدم مثالاً لعقد داو يحتوي على بعض الوظائف التي يمكن الوصول إليها بشكل عام لوصف خصائص على مستوى التتبع. هنا، نفترض أن عقد داو يسمح للمستخدمين بإجراء العمليات التالية:

إيداع الأموال
التصويت على الاقتراح بعد إيداع الأموال
المطالبة باسترداد الأموال إذا لم يصوتوا على الاقتراح

يمكن أن تكون خصائص مستوى التتبع على سبيل المثال "المستخدمون الذين لا يودعون أموالاً لا يمكنهم التصويت على اقتراح" أو "يجب أن يكون المستخدمون الذين لا يصوتون على اقتراح قادرين دائمًا على المطالبة باسترداد الأموال". تؤكد كلتا الخاصيتين على التسلسلات المفضلة للتنفيذ (لا يمكن أن يحدث التصويت قبل إيداع الأموال ولا يمكن المطالبة باسترداد الأموال بعد التصويت على الاقتراح).

تقنيات التحقق الرسمي من العقود الذكية

فحص النموذج

التحقق من النموذج هو تقنية تحقق رسمية حيث تقوم الخوارزمية بفحص النموذج الرسمي للعقد الذكي مقابل مواصفاته. في فحص النموذج، غالبًا ما يتم تمثيل العقود الذكية كأنظمة انتقال الحالة، في حين يتم تعريف الخصائص الموجودة في حالات العقد المسموح بها باستخدام المنطق الزمني.

يتطلب فحص النموذج إنشاء تمثيل رياضي مجرد لنظام (أي عقد) والتعبير عن خصائص هذا النظام باستخدام صيغ متجذرة في المنطق الافتراضي (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;
8}

يحتاج تتبع التنفيذ الذي يؤدي إلى فيضان عدد صحيح إلى تلبية الصيغة: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) من غير المرجح حل هذه الصيغة، وبالتالي فهي بمثابة دليل رياضي على أن الدالة safe_add لا تفيض أبدًا.

لماذا نستخدم التحقق الرسمي للعقود الذكية؟ فوائد التحقق الرسمي

الحاجة إلى الموثوقية

يتم استخدام التحقق الرسمي لتقييم صحة الأنظمة الحرجة للسلامة والتي قد يؤدي فشلها إلى عواقب مدمرة، مثل الوفاة أو الإصابة أو الخراب المالي. العقود الذكية هي تطبيقات عالية القيمة تتحكم في كميات هائلة من القيمة، ويمكن أن تؤدي الأخطاء البسيطة في التصميم إلى خسائر لا يمكن تعويضها للمستخدمين (opens in a new tab). ومع ذلك، فإن التحقق الرسمي من العقد قبل النشر يمكن أن يزيد من الضمانات بأنه سيعمل كما هو متوقع بمجرد تشغيله على blockchain.

تُعد الموثوقية صفة مرغوبة للغاية في أي عقد ذكي، خاصةً وأن الكود الذي تم نشره في إيثريوم Virtual Machine (EVM) يكون عادةً غير قابل للتغيير. وبما أن ترقيات ما بعد الإطلاق ليست في متناول الجميع بسهولة، فإن الحاجة إلى ضمان موثوقية العقود تجعل التحقق الرسمي ضروريا. التحقق الرسمي قادر على اكتشاف المشكلات الصعبة، مثل نقص وتدفق الأعداد الصحيحة، وإعادة الدخول، وتحسينات الغاز الضعيفة، والتي قد تفلت من المدققين والمختبرين.

إثبات الصحة الوظيفية

اختبار البرنامج هو الطريقة الأكثر شيوعًا لإثبات أن العقد الذكي يلبي بعض المتطلبات. يتضمن ذلك تنفيذ عقد مع عينة من البيانات التي من المتوقع معالجتها وتحليل سلوكها. إذا أعاد العقد النتائج المتوقعة لبيانات العينة، فسيكون لدى المطورين دليل موضوعي على صحتها.

ومع ذلك، لا يمكن لهذا النهج إثبات التنفيذ الصحيح لقيم الإدخال التي لا تشكل جزءًا من العينة. لذلك، قد يساعد اختبار العقد في اكتشاف الأخطاء (أي، إذا فشلت بعض مسارات الكود في إرجاع النتائج المرجوة أثناء التنفيذ)، ولكن لا يمكنه إثبات غياب الأخطاء بشكل قاطع.

وعلى العكس من ذلك، يمكن للتحقق الرسمي أن يثبت رسميًا أن العقد الذكي يلبي متطلبات نطاق لا نهائي من عمليات التنفيذ دون تشغيل العقد على الإطلاق. ويتطلب هذا إنشاء مواصفات رسمية تصف بدقة سلوكيات العقد الصحيحة وتطوير نموذج رسمي (رياضي) لنظام العقد. ومن ثم يمكننا اتباع إجراء إثبات رسمي للتحقق من الاتساق بين نموذج العقد ومواصفاته.

مع التحقق الرسمي، فإن مسألة التحقق من أن منطق عمل العقد يلبي المتطلبات هي عبارة عن اقتراح رياضي يمكن إثباته أو دحضه. من خلال إثبات اقتراح رسميًا، يمكننا التحقق من عدد لا نهائي من حالات الاختبار باستخدام عدد محدود من الخطوات. وبهذه الطريقة، تصبح عملية التحقق الرسمي أكثر فعالية في إثبات صحة العقد من الناحية الوظيفية فيما يتصل بالمواصفات.

أهداف التحقق المثالية

يصف هدف التحقق النظام الذي سيتم التحقق منه رسميًا. من الأفضل استخدام التحقق الرسمي في "الأنظمة المضمنة" (قطع صغيرة وبسيطة من البرامج تشكل جزءًا من نظام أكبر). كما أنها مثالية أيضًا للمجالات المتخصصة التي تحتوي على قواعد قليلة، لأن هذا يجعل من الأسهل تعديل الأدوات للتحقق من خصائص المجال المحددة.

إن العقود الذكية - إلى حد ما على الأقل - تلبي كلا المتطلبين. على سبيل المثال، الحجم الصغير لعقود الإيثريوم يجعلها قابلة للتحقق الرسمي. وعلى نحو مماثل، يتبع EVM قواعد بسيطة، مما يجعل تحديد وتأكيد الخصائص الدلالية للبرامج التي تعمل في EVM أسهل.

دورة تطوير أسرع

تعتبر تقنيات التحقق الرسمية، مثل التحقق من النموذج والتنفيذ الرمزي، أكثر كفاءة بشكل عام من التحليل المنتظم لرمز العقد الذكي (الذي يتم إجراؤه أثناء الاختبار أو التدقيق). هذا لأن التحقق الرسمي يعتمد على القيم الرمزية لاختبار التأكيدات ("ماذا لو حاول مستخدم سحب n إيثر؟") على عكس الاختبار الذي يستخدم قيمًا ملموسة ("ماذا لو حاول المستخدم سحب 5 إيثر؟").

يمكن لمتغيرات الإدخال الرمزية أن تغطي فئات متعددة من القيم الملموسة، لذا فإن طرق التحقق الرسمية تعد بتغطية أكبر للكود في إطار زمني أقصر. عند استخدامه بشكل فعال، يمكن للتحقق الرسمي أن يعمل على تسريع دورة التطوير للمطورين.

كما أن التحقق الرسمي يحسن أيضًا عملية بناء التطبيقات اللامركزية (dapps) من خلال تقليل أخطاء التصميم المكلفة. تتطلب ترقية العقود (حيثما أمكن) لإصلاح الثغرات الأمنية إعادة كتابة مكثفة لقواعد التعليمات البرمجية وبذل المزيد من الجهد في التطوير. يمكن للتحقق الرسمي اكتشاف العديد من الأخطاء في تنفيذات العقد التي قد تفلت من اختبارات المختبرين والمراجعين، كما يوفر فرصة كبيرة لإصلاح هذه المشكلات قبل نشر العقد.

عيوب التحقق الرسمي

تكلفة العمل اليدوي

يتطلب التحقق الرسمي، وخاصة التحقق شبه الآلي الذي يرشد فيه الإنسان المثبت إلى استخلاص أدلة الصحة، قدرًا كبيرًا من العمل اليدوي. علاوة على ذلك، فإن إنشاء المواصفات الرسمية يعد نشاطًا معقدًا يتطلب مستوى عاليًا من المهارة.

وتجعل هذه العوامل (الجهد والمهارة) التحقق الرسمي أكثر صعوبة وتكلفة مقارنة بالطرق المعتادة لتقييم صحة العقود، مثل الاختبار والتدقيق. ومع ذلك، فإن دفع تكلفة التدقيق الكامل للتحقق يعد أمرا عمليا، نظرا لتكلفة الأخطاء في تنفيذ العقود الذكية.

السلبيات الكاذبة

لا يمكن للتحقق الرسمي التحقق إلا من تطابق تنفيذ العقد الذكي مع المواصفات الرسمية. ومن ثم، فمن المهم التأكد من أن المواصفات تصف بشكل صحيح السلوكيات المتوقعة من العقد الذكي.

إذا كانت المواصفات مكتوبة بشكل سيئ، فإن انتهاكات الخصائص - والتي تشير إلى عمليات تنفيذ ضعيفة - لا يمكن اكتشافها من خلال التدقيق الرسمي للتحقق. في هذه الحالة، قد يفترض المطور خطأً أن العقد خالٍ من الأخطاء.

مشاكل الأداء

يواجه التحقق الرسمي عددًا من مشكلات الأداء. على سبيل المثال، يمكن أن تؤثر مشكلات انفجار الحالة والمسار التي يتم مواجهتها أثناء فحص النموذج والفحص الرمزي، على التوالي، على إجراءات التحقق. بالإضافة إلى ذلك، غالبًا ما تستخدم أدوات التحقق الرسمية حلول SMT وحل القيود الأخرى في طبقتها الأساسية، وتعتمد هذه الحلول على إجراءات مكثفة حسابيًا.

أيضًا، ليس من الممكن دائمًا لمحققي البرامج تحديد ما إذا كانت خاصية ما (موصوفة كصيغة منطقية) يمكن تحقيقها أم لا ("مشكلة القابلية للتقرير (opens in a new tab)") لأن البرنامج قد لا ينتهي أبدًا. وبناء على ذلك، قد يكون من المستحيل إثبات بعض خصائص العقد حتى لو تم تحديدها بشكل جيد.

أدوات التحقق الرسمي لعقود إيثريوم الذكية

لغات المواصفات لإنشاء المواصفات الرسمية

Act: يسمح Act بتحديد تحديثات التخزين، والشروط المسبقة/اللاحقة وثوابت العقد. تحتوي مجموعة أدواتها أيضًا على واجهات خلفية للإثبات قادرة على إثبات العديد من الخصائص عبر Coq، أو محللات SMT، أو hevm.

سكربل - يقوم سكربل بتحويل التعليقات التوضيحية للكود في لغة مواصفات سكربل إلى تأكيدات ملموسة تتحقق من المواصفات.

التوثيق (opens in a new tab)

Dafny - Dafny هي لغة برمجة جاهزة للتحقق تعتمد على التعليقات التوضيحية عالية المستوى للاستدلال على صحة الكود وإثباتها.

غيت هاب (opens in a new tab)

مدققات البرامج للتحقق من الصحة

سيرتورا Prover - Certora Prover هي أداة تحقق رسمية تلقائية للتحقق من صحة الكود في العقود الذكية. تتم كتابة المواصفات بلغة CVL (لغة التحقق سيرتورا)، مع اكتشاف انتهاكات الخصائص باستخدام مزيج من التحليل الثابت وحل القيود.

سوليديتي SMTChecker - SMTChecker الخاص بـ سوليديتي هو مدقق نموذج مدمج يعتمد على SMT (نظريات قابلية الإرضاء المعيارية) وحل Horn. يؤكد ما إذا كان الكود المصدري للعقد يتطابق مع المواصفات أثناء التجميع ويتحقق بشكل ثابت من انتهاكات خصائص السلامة.

غيت هاب (opens in a new tab)

solc-verify - solc-verify هو إصدار موسع من مُصرِّف سوليديتي يمكنه إجراء تحقق رسمي تلقائي على كود سوليديتي باستخدام التعليقات التوضيحية والتحقق البرنامجي النمطي.

غيت هاب (opens in a new tab)

KEVM - KEVM هي دلالات رسمية لآلة إيثريوم الافتراضية (EVM) مكتوبة في إطار عمل K. KEVM قابل للتنفيذ ويمكنه إثبات بعض التأكيدات المتعلقة بالخصائص باستخدام منطق الوصول.

الأطر المنطقية لإثبات النظريات

Isabelle - Isabelle/HOL هو مساعد إثبات يسمح بالتعبير عن الصيغ الرياضية بلغة رسمية ويوفر أدوات لإثبات تلك الصيغ. التطبيق الرئيسي هو إضفاء الطابع الرسمي على البراهين الرياضية، والتحقق الرسمي على وجه الخصوص، والذي يتضمن إثبات صحة أجهزة الكمبيوتر أو برامجه وإثبات خصائص لغات وبروتوكولات الكمبيوتر.

Rocq - Rocq هو أداة إثبات نظرية تفاعلية تتيح لك تعريف البرامج باستخدام النظريات وتوليد أدلة صحة يتم فحصها آليًا بشكل تفاعلي.

أدوات تعتمد على التنفيذ الرمزي للكشف عن الأنماط الضعيفة في العقود الذكية

مانتيكور - أداة لتحليل كود البايت الخاص بـ EVM استنادًا إلى التنفيذ الرمزي.

hevm - hevm هو محرك تنفيذ رمزي ومدقق تكافؤ لكود البايت الخاص بـ EVM.

غيت هاب (opens in a new tab)

ميثريل - أداة تنفيذ رمزية للكشف عن الثغرات الأمنية في عقود إيثريوم الذكية