الاختبار والتحقق الرسمي من Web3 Smart Contract Security

وقت القراءة: 9 دقائق

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

1. الأمن مطلوب دائمًا.

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

عالم Web3 لا يختلف. لا توجد طريقة آمنة لإنقاذ نفسك ، ولكن وجود مدققين ذوي خبرة من QuillAudits يمكن أن يزيد من احتمالات تأمين البروتوكول الخاص بك بشكل كبير وسيضمن أمنك المحدث. في web3 ، هناك آليتان مهمتان تساعدك على فهم مدى أمانك من خلال إجراء بعض الاختبارات على البروتوكول الخاص بك: -

1. اختبار العقد الذكي
2. التحقق الرسمي من العقود الذكية

دعونا نفهمها بالتفصيل ونتعلم كيف تساعدنا في معرفة نقاط الضعف أو نقاط الضعف في عقودنا.

2. اختبار العقد الذكي

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

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

2.1 آلي

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

2.1.1. الاختبار الوظيفي

لنفترض أنك كتبت برنامجًا لأخذ عددين ، أ وب ثم أعادت جمع كلا الرقمين. لذا ، للتحقق من هذا البرنامج ، تعطي 2 و 8 وتغذية النتيجة المتوقعة لتكون 10. الآن عند تشغيل البرنامج ، يجب أن يُرجع 10. إذا كان كذلك ، فعندئذٍ يعمل بشكل جيد ، وكودنا صحيح ، ولكن إذا كان كذلك لا ، فهناك خطأ ما في الكود الخاص بنا. 

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

1. اختبار وحدة: - هذا يتناول اختبار المكونات الفردية للعقد الذكي للتأكد من صحتها. إنها حازمة أو تتطلب عبارات عن المتغيرات.

2. الاندماج النصوصng: - هذه تتعامل مع اختبار عدة مكونات فردية معًا. اختبار التكامل هو مستوى أعلى في التسلسل الهرمي من اختبار الوحدة. يساعدنا في تحديد الأخطاء الناتجة عن تفاعل الوظائف المختلفة ، والتي قد تكون جزءًا من العقود الذكية الأخرى.

3. System النصوصng: - هذا هو الأعلى في التسلسل الهرمي. في هذا ، نقوم باختبار العقد بأكمله كنظام واحد متكامل تمامًا لمعرفة ما إذا كان يعمل وفقًا لاحتياجاتنا. يتم ذلك من وجهة نظر المستخدم ، وأفضل طريقة للقيام بذلك هي نشره على شبكات الاختبار.

2.1.2. التحليل الساكن

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

2.1.3. التحليل الديناميكي

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

دليل 2.2

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

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

2.2.1 عمليات تدقيق رمز: - 

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

 نعم ، أنا أتحدث عن QuillAudits. نحن فريق من المدققين المهرة الذين يمكنهم توجيهك. تتطلب عمليات تدقيق التعليمات البرمجية عقلية المهاجم للعثور على جميع الثغرات الأمنية المحتملة في التعليمات البرمجية المصدر. تدقيق الكود هو تقييم مفصل لرمز العقد الذكي للكشف عن نقاط الضعف والعيوب المحتملة.

2.2.2 مكافأة الأخطاء: -

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

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

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

3.1 ما هي المواصفات الرسمية؟

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

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

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

3.1.1 المواصفات

المواصفات هي وصف واضح لا لبس فيه وكامل لمتطلبات العقد الذكي. يجب أن يصف ما يفترض أن يفعله العقد وما لا يفترض أن يفعله. فيما يلي مثال على مواصفات عقد بسيط وذكي يضيف رقمين:

// Specification: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint) function add(uint a, uint b) public view returns (uint) {
// Implementation details are not relevant to the specification
// …
}

نموذج شنومكس

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

// Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint) function add(uint a, uint b) public view returns (uint) {
return a + b;
}

3.1.3 محرك التحقق

محرك التحقق هو أداة يمكنها تحليل نموذج والتحقق من صحته فيما يتعلق بمواصفات معينة. هناك العديد من محركات التحقق المتاحة للعقود الذكية ، بما في ذلك:

ميثريل: أداة تنفيذ رمزية مفتوحة المصدر يمكنها اكتشاف مجموعة واسعة من الثغرات الأمنية في عقود Solidity الذكية.

IDE ريمكس: بيئة تطوير متكاملة تتضمن أداة تحقق رسمية يمكنها التحقق من صحة العقود الذكية.

إثبات سيرتورا: أداة تجارية يمكنها التحقق من صحة العقود الذكية باستخدام التفكير الرياضي الآلي. فيما يلي مثال على كيفية استخدام التحقق الرسمي للتحقق من صحة العقد الذكي باستخدام Certora Prover:

pragma solidity 0.7.6; // Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint)
function add(uint a, uint b) public pure returns (uint) {
return a + b;
} // Model: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint) function add(uint a, uint b) public pure returns (uint) {
return a + b;
} // Specification: Adds two numbers
// Inputs: a, b (uint)
// Outputs: the sum of a and b (uint) function test_add(uint a, uint b) public pure returns (bool) {
uint expected = a + b;
uint actual = add(a, b);
return expected == actual;
} // Verification: Verify the correctness of the add function contract TestAdd {
function test_add(uint a, uint b) public view returns (bool) {
return CertoraProver.verify(test_add, a, b);
}
}

في المثال أعلاه ، نحدد عقد Solidity الذكي الذي يتضمن نموذجًا لوظيفة الإضافة ، ومواصفات الوظيفة ، ومحرك التحقق (Certora Prover) الذي يمكنه التحقق من صحة الوظيفة. نحدد أيضًا دالة اختبار (test_add) يمكن استخدامها للتحقق من صحة الوظيفة.

3.2 اختبار مقابل التحقق الرسمي

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

3.3 تقنيات التحقق الرسمي

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

3.3.1 فحص النموذج

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

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

يستخدم فحص النموذج تقنية تسمى State Space exploration ، والتي تقوم بشكل أساسي بتجربة جميع الحالات المحتملة التي يمكن أن يكون عقدنا الذكي فيها ثم التحقق مما إذا كان أي منها يؤدي إلى انتهاك الملكية. ومع ذلك ، قد يؤدي هذا إلى عدد لا نهائي من الدول ؛ ومن ثم تعتمد فاحصات النماذج على تقنيات التجريد لإجراء تحليل فعال للعقود الذكية ممكنًا.

3.3.2 إثبات النظرية

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

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

4. اختتام

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

نحن في QuillAudits في مهمة للمساعدة في حماية البروتوكولات الخاصة بك. من خلال فريقنا الماهر وذوي الخبرة ، نتأكد من عدم مرور أي ثغرة أمنية دون أن يلاحظها أحد. قم بزيارة موقعنا على الإنترنت واحصل على مشروع Web3 الخاص بك آمنًا!

28 المشاهدات

• محتوى مدعوم من تحسين محركات البحث وتوزيع العلاقات العامة. تضخيم اليوم.
• بلاتوبلوكشين. Web3 Metaverse Intelligence. تضخيم المعرفة. الوصول هنا.
• المصدر https://blog.quillhash.com/2023/02/16/testing-and-formal-verification/