التحقق الشكلي من العقود الذكية
تجعل العقود الذكية من الممكن إنشاء تطبيقات لامركزية ومنزوعة الثقة وقوية تقدم حالات استخدام جديدة وتفتح آفاق القيمة للمستخدمين. نظرًا لأن العقود الذكية تتعامل مع كميات كبيرة من القيمة، فإن الأمان يعد اعتبارًا بالغ الأهمية للمطورين.
يعد التحقق الشكلي أحد التقنيات الموصى بها لتحسين أمان العقود الذكية. تم استخدام التحقق الشكلي، الذي يستخدم الطرق الشكلية (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)، والتي يمكن أن تنتقل بين الحالات عن طريق إجراء عمليات، مع استخدام المنطق الزمني لتحديد الخصائص الشكلية لنموذج آلة الحالة المحدودة.
المنطق الزمني (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 في Solidity.
تعبر عبارات 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.
نظرًا لأن التنفيذ الرمزي يعتمد على مدخلات البرنامج، ومجموعة المدخلات لاستكشاف جميع الحالات التي يمكن الوصول إليها قد تكون لا نهائية، فإنه لا يزال شكلاً من أشكال الاختبار. ومع ذلك، كما هو موضح في المثال، فإن التنفيذ الرمزي أكثر كفاءة من الاختبار العادي للعثور على المدخلات التي تؤدي إلى انتهاكات الخصائص.
علاوة على ذلك، ينتج التنفيذ الرمزي نتائج إيجابية كاذبة أقل من التقنيات الأخرى القائمة على الخصائص (مثل اختبار التشويش) التي تولد مدخلات عشوائية لدالة. إذا تم تشغيل حالة خطأ أثناء التنفيذ الرمزي، فمن الممكن إنشاء قيمة ملموسة تؤدي إلى حدوث الخطأ وإعادة إنتاج المشكلة.
يمكن أن يوفر التنفيذ الرمزي أيضًا درجة معينة من الإثبات الرياضي للصحة. ضع في اعتبارك المثال التالي لدالة عقد مع حماية من تجاوز السعة:
function safe_add(uint x, uint y) returns(uint z){
z = x + y;
require(z>=x);
require(z>=y);
return z;
}
تتبع التنفيذ الذي يؤدي إلى تجاوز السعة لعدد صحيح سيحتاج إلى تلبية الصيغة: z = x + y AND (z >= x) AND (z >= y) AND (z < x OR z < y) من غير المرجح أن يتم حل مثل هذه الصيغة، وبالتالي فهي بمثابة إثبات رياضي على أن الدالة safe_add لا تتجاوز سعتها أبدًا.
لماذا نستخدم التحقق الشكلي للعقود الذكية؟
الحاجة إلى الموثوقية
يُستخدم التحقق الشكلي لتقييم صحة الأنظمة الحيوية للسلامة التي يمكن أن يكون لفشلها عواقب وخيمة، مثل الوفاة أو الإصابة أو الخراب المالي. العقود الذكية هي تطبيقات عالية القيمة تتحكم في كميات هائلة من القيمة، ويمكن أن تؤدي الأخطاء البسيطة في التصميم إلى خسائر لا يمكن تعويضها للمستخدمين (opens in a new tab). ومع ذلك، فإن التحقق الشكلي من العقد قبل النشر يمكن أن يزيد من الضمانات بأنه سيعمل كما هو متوقع بمجرد تشغيله على سلسلة الكتل.
الموثوقية هي جودة مرغوبة للغاية في أي عقد ذكي، خاصة لأن الكود المنشور في آلة إيثيريوم الافتراضية (EVM) يكون عادةً غير قابل للتغيير. مع عدم إمكانية الوصول بسهولة إلى ترقيات ما بعد الإطلاق، فإن الحاجة إلى ضمان موثوقية العقود تجعل التحقق الشكلي ضروريًا. التحقق الشكلي قادر على اكتشاف المشكلات الصعبة، مثل تجاوز السعة للأعداد الصحيحة والنقصان، وإعادة الدخول، وضعف تحسينات الغاز، والتي قد تفوت على المدققين والمختبرين.
إثبات الصحة الوظيفية
اختبار البرنامج هو الطريقة الأكثر شيوعًا لإثبات أن العقد الذكي يلبي بعض المتطلبات. يتضمن ذلك تنفيذ عقد مع عينة من البيانات التي يُتوقع أن يتعامل معها وتحليل سلوكه. إذا أرجع العقد النتائج المتوقعة لبيانات العينة، فإن المطورين لديهم إثبات موضوعي على صحته.
ومع ذلك، لا يمكن لهذا النهج إثبات التنفيذ الصحيح لقيم الإدخال التي ليست جزءًا من العينة. لذلك، قد يساعد اختبار العقد في اكتشاف الأخطاء (أي إذا فشلت بعض مسارات الكود في إرجاع النتائج المطلوبة أثناء التنفيذ)، ولكن لا يمكنه إثبات عدم وجود أخطاء بشكل قاطع.
على العكس من ذلك، يمكن للتحقق الشكلي أن يثبت شكليًا أن العقد الذكي يلبي متطلبات نطاق لا نهائي من عمليات التنفيذ دون تشغيل العقد على الإطلاق. يتطلب ذلك إنشاء مواصفات شكلية تصف بدقة سلوكيات العقد الصحيحة وتطوير نموذج شكلي (رياضي) لنظام العقد. ثم يمكننا اتباع إجراء إثبات شكلي للتحقق من الاتساق بين نموذج العقد ومواصفاته.
مع التحقق الشكلي، فإن مسألة التحقق مما إذا كان منطق العمل الخاص بالعقد يلبي المتطلبات هي مقترح رياضي يمكن إثباته أو دحضه. من خلال إثبات مقترح شكليًا، يمكننا التحقق من عدد لا حصر له من حالات الاختبار بعدد محدود من الخطوات. بهذه الطريقة، يتمتع التحقق الشكلي بآفاق أفضل لإثبات أن العقد صحيح وظيفيًا فيما يتعلق بالمواصفات.
أهداف التحقق المثالية
يصف هدف التحقق النظام المراد التحقق منه شكليًا. يُفضل استخدام التحقق الشكلي في "الأنظمة المدمجة" (أجزاء صغيرة وبسيطة من البرامج تشكل جزءًا من نظام أكبر). كما أنها مثالية للمجالات المتخصصة التي تحتوي على قواعد قليلة، حيث يسهل ذلك تعديل الأدوات للتحقق من الخصائص الخاصة بالمجال.
العقود الذكية — على الأقل إلى حد ما — تلبي كلا المتطلبين. على سبيل المثال، الحجم الصغير لعقود إيثيريوم يجعلها قابلة للتحقق الشكلي. وبالمثل، تتبع EVM قواعد بسيطة، مما يجعل تحديد والتحقق من الخصائص الدلالية للبرامج التي تعمل في EVM أسهل.
دورة تطوير أسرع
تقنيات التحقق الشكلي، مثل فحص النموذج والتنفيذ الرمزي، تكون بشكل عام أكثر كفاءة من التحليل العادي لكود العقد الذكي (الذي يتم إجراؤه أثناء الاختبار أو التدقيق). وذلك لأن التحقق الشكلي يعتمد على القيم الرمزية لاختبار التأكيدات ("ماذا لو حاول مستخدم سحب n ether؟") على عكس الاختبار الذي يستخدم قيمًا ملموسة ("ماذا لو حاول مستخدم سحب 5 ether؟").
يمكن لمتغيرات الإدخال الرمزية أن تغطي فئات متعددة من القيم الملموسة، لذلك تعد مناهج التحقق الشكلي بتغطية كود أكبر في إطار زمني أقصر. عند استخدامه بفعالية، يمكن للتحقق الشكلي تسريع دورة التطوير للمطورين.
يعمل التحقق الشكلي أيضًا على تحسين عملية بناء التطبيقات اللامركزية (dapps) عن طريق تقليل أخطاء التصميم المكلفة. تتطلب ترقية العقود (حيثما أمكن) لإصلاح نقاط الضعف إعادة كتابة مكثفة لقواعد الكود وبذل المزيد من الجهد في التطوير. يمكن للتحقق الشكلي اكتشاف العديد من الأخطاء في تطبيقات العقود التي قد تفوت على المختبرين والمدققين ويوفر فرصة واسعة لإصلاح تلك المشكلات قبل نشر العقد.
عيوب التحقق الشكلي
تكلفة العمل اليدوي
يتطلب التحقق الشكلي، وخاصة التحقق شبه الآلي الذي يوجه فيه الإنسان المُثبِت لاستنتاج إثباتات الصحة، عملاً يدويًا كبيرًا. علاوة على ذلك، يعد إنشاء المواصفات الشكلية نشاطًا معقدًا يتطلب مستوى عاليًا من المهارة.
تجعل هذه العوامل (الجهد والمهارة) التحقق الشكلي أكثر تطلبًا وتكلفة مقارنة بالطرق المعتادة لتقييم الصحة في العقود، مثل الاختبار والتدقيق. ومع ذلك، فإن دفع تكلفة تدقيق التحقق الكامل يعد أمرًا عمليًا، نظرًا لتكلفة الأخطاء في تطبيقات العقود الذكية.
السلبيات الكاذبة
يمكن للتحقق الشكلي فقط التحقق مما إذا كان تنفيذ العقد الذكي يتطابق مع المواصفات الشكلية. على هذا النحو، من المهم التأكد من أن المواصفات تصف بشكل صحيح السلوكيات المتوقعة للعقد الذكي.
إذا كانت المواصفات مكتوبة بشكل سيئ، فلا يمكن لتدقيق التحقق الشكلي اكتشاف انتهاكات الخصائص — والتي تشير إلى عمليات تنفيذ ضعيفة. في هذه الحالة، قد يفترض المطور خطأً أن العقد خالٍ من الأخطاء.
مشكلات الأداء
يواجه التحقق الشكلي عددًا من مشكلات الأداء. على سبيل المثال، يمكن أن تؤثر مشكلات انفجار الحالة والمسار التي تتم مواجهتها أثناء فحص النموذج والفحص الرمزي، على التوالي، على إجراءات التحقق. أيضًا، غالبًا ما تستخدم أدوات التحقق الشكلي مُحِلّات SMT ومُحِلّات القيود الأخرى في طبقتها الأساسية، وتعتمد هذه المُحِلّات على إجراءات مكثفة حسابيًا.
أيضًا، ليس من الممكن دائمًا لأدوات التحقق من البرامج تحديد ما إذا كانت الخاصية (الموصوفة كصيغة منطقية) يمكن تلبيتها أم لا ("مشكلة قابلية البت (opens in a new tab)") لأن البرنامج قد لا ينتهي أبدًا. على هذا النحو، قد يكون من المستحيل إثبات بعض الخصائص لعقد حتى لو كان محددًا بشكل جيد.
أدوات التحقق الشكلي للعقود الذكية على إيثيريوم
لغات المواصفات لإنشاء المواصفات الشكلية
Act: يسمح Act بتحديد تحديثات التخزين، والشروط المسبقة/اللاحقة، وثوابت العقد. تحتوي مجموعة أدواته أيضًا على خلفيات إثبات قادرة على إثبات العديد من الخصائص عبر Coq، أو مُحِلّات SMT، أو hevm.
Scribble - يحول Scribble التعليقات التوضيحية للكود في لغة مواصفات Scribble إلى تأكيدات ملموسة تتحقق من المواصفات.
Dafny - Dafny هي لغة برمجة جاهزة للتحقق تعتمد على التعليقات التوضيحية عالية المستوى للتفكير في صحة الكود وإثباتها.
أدوات التحقق من البرامج للتحقق من الصحة
Certora Prover - Certora Prover هي أداة تحقق شكلي تلقائية للتحقق من صحة الكود في العقود الذكية. تُكتب المواصفات بلغة CVL (لغة تحقق Certora)، مع اكتشاف انتهاكات الخصائص باستخدام مزيج من التحليل الثابت وحل القيود.
Solidity SMTChecker - SMTChecker الخاص بـ Solidity هو أداة فحص نموذج مدمجة تعتمد على SMT (نظريات قابلية الإرضاء) وحل Horn. يؤكد ما إذا كان الكود المصدري للعقد يتطابق مع المواصفات أثناء التجميع ويتحقق بشكل ثابت من انتهاكات خصائص الأمان.
solc-verify - solc-verify هو إصدار موسع من مترجم Solidity يمكنه إجراء تحقق شكلي آلي على كود Solidity باستخدام التعليقات التوضيحية والتحقق المعياري من البرنامج.
KEVM - KEVM هي دلالات شكلية لآلة إيثيريوم الافتراضية (EVM) مكتوبة في إطار عمل K. KEVM قابل للتنفيذ ويمكنه إثبات تأكيدات معينة متعلقة بالخصائص باستخدام منطق قابلية الوصول.
الأطر المنطقية لإثبات النظريات
Isabelle - Isabelle/HOL هو مساعد إثبات يسمح بالتعبير عن الصيغ الرياضية بلغة شكلية ويوفر أدوات لإثبات تلك الصيغ. التطبيق الرئيسي هو إضفاء الطابع الشكلي على الإثباتات الرياضية وعلى وجه الخصوص التحقق الشكلي، والذي يتضمن إثبات صحة أجهزة الكمبيوتر أو برامجها وإثبات خصائص لغات الكمبيوتر وبروتوكولاته.
Rocq - Rocq هو مُثبِت نظريات تفاعلي يتيح لك تحديد البرامج باستخدام النظريات وإنشاء إثباتات صحة تم التحقق منها آليًا بشكل تفاعلي.
الأدوات القائمة على التنفيذ الرمزي لاكتشاف الأنماط الضعيفة في العقود الذكية
مانتيكور - أداة لتحليل رمز البايت لـ EVM تعتمد على التنفيذ الرمزي.
hevm - hevm هو محرك تنفيذ رمزي ومدقق تكافؤ لرمز البايت لـ EVM.
Mythril - أداة تنفيذ رمزي لاكتشاف نقاط الضعف في العقود الذكية على إيثيريوم
قراءة إضافية
- كيف يعمل التحقق الشكلي للعقود الذكية (opens in a new tab)
- نظرة عامة على مشاريع التحقق الشكلي في نظام إيثيريوم البيئي (opens in a new tab)
- التحقق الشكلي الشامل للعقد الذكي للإيداع في Ethereum 2.0 (opens in a new tab)
- التحقق الشكلي من العقد الذكي الأكثر شهرة في العالم (opens in a new tab)
- SMTChecker والتحقق الشكلي (opens in a new tab)
آخر تحديث للصفحة: 28 أبريل 2026
