الرئيسية
/
سوليدتي
/
أدوات تدقيق العقود الذكية : أدوات التحقق الرسمية

محمد

585مشاهده

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

أكتوبر 11, 2023 - 8 دقائق للقرائه

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

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

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

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

التحقق الرسمي والتنفيذ الرمزي (Formal Verification and Symbolic Execution)

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

التحقق الرسمي هو مصطلح واسع يشمل تقنيات مختلفة. ثلاثة من التقنيات الأكثر شيوعًا هي فحص النماذج (model checking)، وإثبات النظرية (theorem proving) ، والتنفيذ الرمزي (symbolic execution) .

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

تستخدم بعض الأدوات هنا مجموعة من تقنيات التحقق الرسمية أو أكثر.

1 . Certora Prover

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

يستخدم Certora Prover مزيجًا من التحليل الثابت و نظريات وحدات الرضا (Satisfiability Modulo Theories) أو SMT .تعتبر SMT تقنية في التحقق الرسمي تجمع بين جوانب إثبات النظرية والتنفيذ الرمزي.

التثبيت:

قم بتثبيت التبعيات التالية لاستخدام Certora Prover:

Python3.8.16 أو الأحدث.
Java Development Kit (JDK) 11 أو الأحدث.
مترجم Solidity (الإصدار 0.5 وما فوق).

بعد ذلك، لتثبيت Certora Prover، قم بتشغيل:

pip3 install certora-cli

mukaeb

كيفية الاستخدام:

يتطلب Certora Prover CLI مفتاح API للتفاعل مع الخدمة السحابية حيث يمكن تصور نتائج التحقق.

توفر Certora أيضًا خدمة سحابية تجريبية مجانية مع أمثلة لمعرفة كيفية عمل الأداة.

تتم كتابة مواصفات Certora Prover بلغة التحقق Certora (CVL)، بدءًا من الكلمة الأساسية للقاعدة.

يتم حفظ المواصفات الموجودة في CVL بامتداد الملف ‎.spec.

يمكن كتابة المواصفات البسيطة التي تضمن تحديث رصيد حامل ERC20 والمستلم في مكالمة التحويل بشكل صحيح على النحو التالي:

methods{
    // declaration of the balanceOf functionfunction balanceOf(address) external returns(uint256) envfree;
}

// the parameters will be fuzzed
rule transferSpec(address holder, address recipient, uint256 amount) 
  description "Verifying that the balances of the ERC20 sender and recipient are updated correctly after a successful transfer"
{
  // Initialize the variables `holderBalBefore`, `recipientBalBefore`,// `holderBalAfter`, and `recipientBalAfter`.uint256 holderBalBefore = balanceOf(holder);
  uint256 recipientBalBefore = balanceOf(recipient);

  // Create an environment object `e` which contains global variables and set the `msg.sender` property to// `holder`.
  env e;
  require e.msg.sender == holder;

  // Call the `transfer` function with the specified `recipient` and `amount`// arguments.
  transfer(e, recipient, amount);

  // Update the variables `holderBalAfter` and `recipientBalAfter` to reflect// the new balances of `holder` and `recipient`.uint256 holderBalAfter = balanceOf(holder);
  uint256 recipientBalAfter = balanceOf(recipient);

  // Assert that the balance of `holder` is decreased by the amount of the// transfer.assert holderBalAfter == assert_uint256(holderBalBefore - amount);

  // Assert that the balance of `recipient` is increased by the amount of the// transfer.assert recipientBalAfter == assert_uint256(recipientBalBefore + amount);
}

mukaeb

مواصفات CVL لها بناء جملة مشابه لـ solidity كما هو موضح في الكود أعلاه.

تشمل الكلمة الأساسية “env” المتغيرات العامة لـ solidity وتشير الكلمة الأساسية “envfree” إلى أن الطريقة أو الوظيفة لا تعتمد على متغير عام.

في CVL 2، تكون نتائج جميع العوامل الحسابية (وليس عوامل البت) من النوع mathint (نوع عدد صحيح لا يتجاوز أو ينقص في CVL)، بغض النظر عن أنواع الإدخال. ولهذا السبب قمنا بكتابة الجانب الأيمن من تأكيداتنا إلى uint256 باستخدام تأكيد_uint256().

سوف نستخدم هذه المواصفات للتحقق رسميًا من عقد ERC20 الضعيف أدناه.

// SPDX-License-Identifier: MITpragma solidity ^0.8.0;contract VulnerableERC20 {
    // A lot has been abstracted away from the contract, leaving only the ERC20 transfer function.mapping(address => uint256) balances;
    event Transfer(address indexed _from, address indexed _to, uint256 _value);

    function transfer(address _to,
        uint256 _value
    ) public returns (bool success) {
        require(balances[msg.sender] >= _value);

        uint fromBalance = balances[msg.sender];
        uint toBalance = balances[_to];

        balances[msg.sender] = fromBalance - _value;
        balances[_to] = toBalance + _value;
        emit Transfer(msg.sender, _to, _value);
        return true;
    }

    function balanceOf(address _owner) public view returns (uint256 balance) {
        return balances[_owner];
    }
}

mukaeb

سنقوم بإنشاء ملف VulnerableERC20.sol وERC20.spec لمواصفات العقد وCVL على التوالي.

(لاحظ أن مفتاح واجهة برمجة التطبيقات (API) الذي تم تعيينه كمتغير بيئة في (export CERTORAKEY=<premium_key>) وهو مطلوب للوصول إلى جميع ميزات المُثبِّت، ويمكنك الدردشة مع فريق Certora على discord حول كيفية الإعداد أو الاستخدام الإصدار التجريبي بجهد حسابي أقل).

يمكننا التحقق من مطابقة العقد للمواصفات عن طريق تشغيل:

certoraRun VulnerableERC20.sol:VulnerableERC20 --verify VulnerableERC20:ERC20.spec

mukaeb

هذه هي النتيجة من التشغيل.

يمكننا أن نرى من النتيجة أن المُثبِّت وجد خطأً ينتهك مواصفاتنا.

انقر لرؤية التقرير الكامل .

من تتبع المكالمة، نرى أن “holdBalBefore” هو 11، ومبلغ الأصل المنقول هو 9.

من المفترض أن يكون “holderBalAfter”هو 11 – 9 = 2 بعد النقل. نظرًا لأن الأرصدة يتم تحديثها بشكل خاطئ بالفعل، فإن هذا الخصم لا يعمل إذا كان كل من مرسل الأصل والمستلم هو نفس العنوان الموضح في النتيجة.

ومع ذلك، لن ينجح هذا الخصم إلا إذا كان مرسل الأصل ومتلقيه عنوانين مختلفين.

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

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

  function transfer(address _to,
        uint256 _value
    ) public returns (bool success) {
        require(balances[msg.sender] >= _value);
        // update balances correctly
        balances[msg.sender] -= _value;
        balances[_to] += _value;
        emit Transfer(msg.sender, _to, _value);
        return true;
    }

mukaeb

سيؤدي هذا إلى تحديث الأرصدة بشكل صحيح.

يتعين علينا أيضًا تحديث مواصفات CVL الخاصة بنا للقبض على الاستثناء حيث يكون عنوان مرسل الأصل والمتلقي متماثلين.

methods{
  function balanceOf(address) external returns(uint256) envfree;
}

rule transferSpec(address holder, address recipient, uint256 amount) 
  description "Verifying that the balances of the ERC20 sender and recipient are updated correctly after a successful transfer"
{
  // Initialize the variables `holderBalBefore`, `recipientBalBefore`,// `holderBalAfter`, and `recipientBalAfter`.uint256 holderBalBefore = balanceOf(holder);
  uint256 recipientBalBefore = balanceOf(recipient);

  // Create an environment object `e` and set the `msg.sender` property to// `holder`.
  env e;
  require e.msg.sender == holder;

  // Call the `transfer` function with the specified `recipient` and `amount`// arguments.
  transfer(e, recipient, amount);

  // Update the variables `holderBalAfter` and `recipientBalAfter` to reflect// the new balances of `holder` and `recipient`.uint256 holderBalAfter = balanceOf(holder);
  uint256 recipientBalAfter = balanceOf(recipient);
  
  // If the `holder` and `recipient` are the same, // assert that the balance of `holder` is the same after the transfer.if(holder == recipient){
    assert holderBalAfter == holderBalBefore;
  } else{
    // Assert that the balance of `holder` is decreased by the amount of the// transfer.assert holderBalAfter == assert_uint256(holderBalBefore - amount);

    // Assert that the balance of `recipient` is increased by the amount of the// transfer.assert recipientBalAfter == assert_uint256(recipientBalBefore + amount);
  }
}

mukaeb

هذه المرة أضفنا عبارة “if” if(holder == Receiver) للتحقق من هذا الاستثناء.

أعد تشغيل الاختبار باستخدام

certoraRun VulnerableERC20.sol:VulnerableERC20 --verify VulnerableERC20:ERC20.spec

mukaeb

نجح الاختبار هذه المرة ولم تفشل أي قاعدة.

انقر لرؤية التقرير الكامل.

يمتلك فريق Certora أيضًا بعض ملحقات VSCode المفيدة التي يمكنك تثبيتها لتشغيل مهام التحقق مباشرة من IDE.

لرؤية المزيد من الأمثلة حول كيفية كتابة مواصفات CVL واستخدامها للتحقق رسميًا من العقود الذكية، قم بزيارة الموقع التجريبي لـ Certora Prover أو شاهد الفيديو التعليمي للبدء .

نقاط القوة

تستخدم Certora التحقق الرسمي التلقائي لتجميع كود العقد الذكي في صيغ رياضية. هذه طريقة دقيقة وفعالة للعثور على الأخطاء من خلال التحقق الرسمي.
على عكس التشويش، يمكن لـ Certora Prover البدء في اختبار العقد الذكي في حالة عشوائية، وبالتالي زيادة تغطية الاختبار.
يمكن تشويش المتغيرات والوظائف في Certora Prover.
يدعم Certora Prover الإعلان عن ثوابت العقود الذكية وطرق مفيدة أخرى.
أنها لا تولد إيجابيات كاذبة.
لغة التحقق Certora سهلة الاستخدام والكتابة.
يدعم التكامل CI.
يحتوي Certora CVL على بناء جملة مماثل لـ solidityوبالتالي فإن تعلمه ليس بالأمر الصعب.
إن الجمع بين SMT والتحليل الثابت يقلل من تعقيد SMTs ويزيل أيضًا الإيجابيات الخاطئة للتحليل الثابت.

نقاط الضعف

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

2. Solidity SMTChecker

Solidity SMTChecker عبارة عن وحدة تحقق رسمية مدمجة في Solidity (solc).

يعتمد SMTChecker على نظريات وحدات الرضا (Satisfiability Modulo Theories) أو SMT وحل القرن (Horn solving) .

يقوم بتشفير منطق البرنامج من solidity إلى عبارات SMT ويستخدم ذلك للتحقق من فشل التأكيد.

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

التثبيت:

يأتي SMTChecker كجزء من (solc).

راجع عملية التثبيت من وثائق solidity .

كيفية الاستخدام:

يمكن تفعيل SMTChecker في ملف solidity عن طريق إضافة

pragma experimental SMTChecker;

للتحقق من الكود باستخدام محرك BMC، يمكننا تشغيل هذا الأمر على ملف solidity:

 solc <solidity-file> --model-checker-engine bmc

mukaeb

لدى SMTChecker عدة خيارات، قم بتشغيل solc لعرضها.

التحقق من العقد التربيعي مع SMTChecker

سوف نقوم بالتحقق من العقد التربيعي من مقالة إختبار الثبات في Foundry مع محرك SMTChecker وBMC.

// SPDX-License-Identifier: GPL-3.0-or-later
pragma experimental SMTChecker;
pragma solidity ^0.8.6;contract Quadratic {
    bool public ok = true;

    function notOkay(int x) external {
        if ((x - 11111) * (x - 11113) < 0) {
            ok = false;
        }
    
        // we "expect" this will never get executedassert(ok == true);
    }
}

mukaeb

احفظ الكود باسم Quadratic.sol وقم بتشغيل، solc Quadratic.sol –model-checker-engine bmc.

نحصل على هذا الإخراج:

يستخدم SMTChecker حل z3 افتراضيًا وكان قادرًا على العثور على الرقم الصحيح الذي يكسر التأكيد.

نقاط القوة

يأتي مباشرة مع Solidity ولا يحتاج إلى أي تعقيد لاستخدامه.
يدعم SMTChecker محركين لفحص النماذج، Bounded Model Checker (BMC) وبنود القرن المقيدة (CHC). يستكشف BMC عددًا محدودًا من الحالات أو مسارات تنفيذ البرنامج (العقود الذكية في هذه الحالة) ويتحقق مما إذا كان أي من المسارات ينتهك التأكيد، بينما يستكشف CHC جميع المسارات.
يعد SMTChecker أسرع في الاستخدام من معظم أدوات التحقق الرسمية عند استخدام محرك BMC.
يمكنه التحقق من التدفق الحسابي والتجاوز، والقسمة على صفر، الأكواد التي لا يمكن الوصول إليها، وإظهار مصفوفة فارغة، والوصول إلى الفهرس خارج الحدود، وعدم كفاية الأموال للتحويل.

نقاط الضعف

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

3. Halmos

Halmos هي أداة تنفيذ رمزية (symbolic execution) مفتوحة المصدر لعقود Ethereum الذكية التي طورها فريق a16z.

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

التثبيت:

لتثبيت الهالموس، قم بتشغيل:

pip install halmos

mukaeb

تحقق من تثبيت halmos مع:

halmos -h

mukaeb

كيفية الاستخدام:

لإجراء اختبار تنفيذ رمزي باستخدام halmos، قم بتشغيل أمر halmos في مشروع solidity .

سنقوم باختبار العقد من قسم dapptools في هذه المقال.

// SPDX-License-Identifier: GPL-3.0-or-later
pragma solidity ^0.8.0;
contract Code {
    uint256 private password;

    constructor() payable {
        require(msg.value >= 1 ether);
        password = 25;
    }

    function withdraw(uint256 password_) public {
        if (password_ == password) {
            (bool success, ) = msg.sender.call{value: address(this).balance}(
                ""
            );
            require(success, "failed to send");
        }
    }

    function balance() public view returns (uint) {
        return address(this).balance;
    }
}

mukaeb

بدلاً من تشويش العقد، سنقوم باختبار العقد رمزيًا باستخدام halmos لمعرفة ما إذا كان سيجد كلمة المرور الخاصة بالعقد.

نقوم بتشغيل halmos في دليل المشروع ونحصل على هذه النتيجة.

من النتيجة التي توصلنا إليها، يمكننا أن نرى أن halmos تمكنت من العثور على كلمة المرور الخاصة بالعقد من خلال الاختبار الرمزي.

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

تمثل “bounds” الحدود العليا والسفلى لمتغيرات المدخلات للعقد أثناء عملية الاختبار.

نقاط القوة

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

نقاط الضعف

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

4. HEVM

Hevm هو تطبيق لجهاز Ethereum Virtual Machine مكتوب بلغة Haskell تم تصميمه فقط للعثور على الأخطاء في عقود Ethereum الذكية والتحقق من صحتها باستخدام التنفيذ الرمزي.

التثبيت:

يأتي Hevm مع dapptools، يمكنك مراجعة المقالة التي تحدثنا فيها هنا dapptools لمعرفة طريقة التثبيت.

كيفية الاستخدام:

لدى Hevm عدة أوامر، لكن الاختبار الرمزي باستخدام hevm يبدأ بالكلمة الأساسية hevm.

التحقق من العقد التربيعي مع HEVM.

سنعرض كيفية الاختبار محليًا باستخدام hevm.

سوف نتحقق من العقد التربيعي مرة أخرى.

// SPDX-License-Identifier: GPL-3.0-or-laterpragma solidity ^0.8.6;contract Quadratic {
    bool public ok = true;

    function notOkay(int x) external {
        if ((x - 11111) * (x - 11113) < 0) {
            ok = false;
        }

        assert(ok == true);
    }
}

mukaeb

الهدف هو العثور على عدد صحيح يجعل كلمة “ok” خاطئة.

يتعين علينا تجميع الكود إلى البايت كود قبل أن نتمكن من اختبار التأكيد باستخدام hevm.

لهذا قم بتشغيل الأمر التالي:

solc --bin-runtime -o <destination/path> <path/to/Quadratic.sol> --overwrite

mukaeb

(استبدل <destination/path> و<path/to/Quadratic.sol> بمسارات الملفات المناسبة).

يؤدي هذا إلى إنشاء ملف “Quadratic.bin-runtime” الذي يحتوي على البايت كود لوقت التشغيل للعقد الذكي.

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

hevm symbolic --code $(<Quadratic.bin-runtime) --sig "notOkay(int x)" --solver cvc4

mukaeb

(تشير علامة –solver إلى أي برنامج حل smt يجب استخدامه، في هذه الحالة CVC4. مع كون الافتراضي هو Z3).

نحصل على هذا الإخراج عندما نقوم بتشغيل الأمر.

تمكنت Hevm من الحصول على القيمة الصحيحة في محاولة واحدة، على عكس Foundry Fuzzer الذي كان يحتاج إلى قيم محددة للحصول على الرقم.

ويمكننا التحقق من أن الرقم صحيح فعلاً وأقل من الصفر باستخدام chisel.

يمكننا أيضًا إضافة علامتي –show-tree و –smttimeout <INTEGER> لطباعة الفروع التي تم استكشافها أثناء التنفيذ في عرض الشجرة وزيادة أو تقليل مهلة الاختبار.

لرؤية جميع الأوامر المتاحة للاختبار الرمزي، قم بتشغيل hevm symbolic -h.

نقاط القوة

يمكن استخدام Hevm لإجراء اختبار الوحدة وتصحيح العقود الذكية.
إنه ذو أداء عالٍ وفعال في الاختبار الرمزي.
يستخدم Hevm أيضًا أدوات حل smt مثل z3 وcvc4 لإثبات صحة الكود.

نقاط الضعف

يمكن أن يكون استخدام Hevm معقدًا، لأنه يتطلب الكثير من أوامر سطر الأوامر.
إنه بطيء عند اختبار قواعد التعليمات البرمجية الكبيرة.

5. Manticore(symbolic execution)

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

يدعم Manticore عقود Ethereum الذكية وثنائيات Linux ELF ووحدات WASM.

التثبيت:

يوصى بتثبيت manticore في بيئة python الافتراضية باستخدام python >=3.8 <=3.9.x. وذلك لأن manticore يستخدم إصدارات أخرى من بعض التبعيات التي قد تؤثر على أدوات أخرى في جهاز الكمبيوتر الخاص بك.

لإنشاء بيئة افتراضية، قم بتشغيل الأوامر التالية:

pip install venv
python3 -m venv venv
source venv/bin/activate

mukaeb

قم بعد ذلك بتثبيت manticore في البيئة الافتراضية.

pip install manticore

mukaeb

طريقة الإستخدام:

لاستخدام مانتيكور وبدء اختبار رمزي على العقد المحدد، قم بتشغيل:

manticore <path/to/file.sol>

mukaeb

إذا كانت هناك رسالة إرجاع غير مرسلة، فهذا يعني أن المحلل لم يتمكن من إيجاد حل للصيغة المحددة.

في حالة وقوعك في خطأ مثل هذا:

1. قم بتخفيض حزمة protobuf إلى الإصدار 3.20 . × أو أقل .

2. اضبط PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION = python ( لكن هذا سيستخدم تحليل Python الخالص وسيكون أبطأ بكثير ) .

قم بتشغيل هذا الأمر لحل هذه المشكلة (نظام التشغيل MacOS/Linux):

pip install protobuf==3.20.0
export PROTOCOL_BUFFERS_PYTHON_IMPLEMENTATION=python

# Rerun manticore
manticore

mukaeb

نقاط القوة

Manticore هو محرك تنفيذ رمزي قوي يمكنه التفكير في مسارات التنفيذ المختلفة وحالات البرنامج وتسلسل المعاملات. وهذا يجعلها فعالة في العثور على الأخطاء التي قد يكون من الصعب أو المستحيل العثور عليها باستخدام طرق الاختبار التقليدية (على سبيل المثال، الاختبار اليدوي والتحليل الثابت).
تتمتع بدورة حياة مرنة لإدارة الحالة تسمح باستخدامها لتحليل أنواع مختلفة من البرامج مثل عقود Ethereum الذكية وثنائيات Linux ELF ووحدات WASM.

نقاط الضعف

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

ختاماً

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