دليل المراجعة التلقائية للعقود الذكية. الجزء 3: الأسطورة

تحذير

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

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

الإعداد والتحضير للإطلاق

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

أولاً ، دعنا نبني صورة Docker الخاصة بنا عن Mythril (لا يهم ما نريد تغييره فيه؟):

git clone https://github.com/ConsenSys/mythril-classic.git cd mythril-classic docker build -t myth . 

حاول الآن تشغيله وفقًا contracts/flattened.sol (يمكنني استخدام نفس العقد الذي تمت مناقشته في المقدمة ) ، حيث يوجد عقدين رئيسيين ، Ownable من Zeppelin Ownable . لا تزال لدينا مشكلة في إصدار برنامج التحويل البرمجي ، لقد قمت بإصلاحه بنفس الطريقة كما في المقالة السابقة ، مع إضافة سطور إلى Dockerfile ستحل محل إصدار برنامج التحويل البرمجي:

 COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin 

بعد إعادة بناء الصورة ، يمكنك محاولة إجراء تحليل العقد. دعنا نستخدم على -v4 و --verbose-report عن رؤية جميع التحذيرات. دعنا نذهب:

 docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ -v4 \ --verbose-report \ -x contracts/flattened.sol 

نحن هنا نعمل مع عقد بالارض دون تبعية. لتحليل عقد Booking.sol منفصل ولجعل Mythril يستلم كل التبعيات ، يمكنك استخدام شيء مثل هذا:

 docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ --solc-args="--allow-paths /tmp/node_modules/zeppelin-solidity/ zeppelin-solidity=/tmp/node_modules/zeppelin-solidity" \ -v4 \ --verbose-report \ -x contracts/Booking.sol 

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

 docker run -v $(pwd):/tmp -w /tmp myth:latest -x contracts/flattened.sol:Booking -v4 --verbose-report 

بدء ونشر العقد

نبدأ المحلل بالخط أعلاه ، وننظر إلى المخرجات ، ونحصل ، من بين أشياء أخرى ، على هذا الخط:

 mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) The analysis was completed successfully. No issues were detected. 

اتضح أنه لم يتم إنشاء عقدنا و "ثابت" في المحاكي. لهذا السبب أوصي باستخدام علامة -v4 لجميع أنواع التحليل لرؤية جميع الرسائل وعدم تفويت رسالة واحدة مهمة. دعونا معرفة ما هو الخطأ. الحل لهذه المشكلة العملية مهم جدا لفهم كيفية استخدام Mythril بشكل صحيح.

لذلك ، نحن نقرأ عن Mythril: It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities . إذا لم تكن معتادًا على هذه المصطلحات ، فإنني أوصي بـ wiki حول اختبار concolic هنا ، ولكن هنا عرض تقديمي جيد حول التحقق من الملوثات لـ x86. باختصار: Mythril يحاكي تنفيذ العقد ، يلتقط الفروع التي يمكن تنفيذ التنفيذ من خلالها ويحاول تحقيق "كسر" حالة العقد ، والفرز من خلال مجموعات مختلفة من المعلمات ومحاولة الالتفاف على جميع المسارات الممكنة. فيما يلي رسم تخطيطي لعينة من المقالة أعلاه:

 1.      .   symbolic-,        . 2.      ,     ,   trace .    ,      ,    . 3.     . 4.       trace-. 5.  symbolic execution   trace,   symbolic ,    ,     ,     . 6.     ,          .    , . 7.   :   ,   ,   input-,     ,      .   input-   ,   .6    . 8.   .4 

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

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

في هذه العملية ، يستخدم Mythril مفهوم "الحالة" - هذا هو رمز العقد وبيئته ومؤشر للأمر الحالي وتخزين العقد وحالة المكدس. هنا الوثائق:

 The machine state μ is defined as the tuple (g, pc, m, i, s) which are the gas available, the program counter pc ∈ P256, the memory contents, the active number of words in memory (counting continuously from position 0), and the stack contents. The memory contents μm are a series of zeroes of size 256. 

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

الآن نفهم إلى حد ما ما ستفعله Mythril ، وسنستمر في فهم سبب عدم تحليل العقد ومن أين جاء [WARNING]: No contract was created during the execution of contract creation . في البداية ، قمت --create-timeout --max-depth (على النحو الموصى به) ، ولكني لم أحصل على النتيجة ، اعتقدت أن المُنشئ كان مسؤولاً - لم ينجح شيء فيه. هنا هو رمزه:

 function Booking( string _description, string _fileUrl, bytes32 _fileHash, uint256 _price, uint256 _cancellationFee, uint256 _rentDateStart, uint256 _rentDateEnd, uint256 _noCancelPeriod, uint256 _acceptObjectPeriod ) public payable { require(_price > 0); require(_price > _cancellationFee); require(_rentDateStart > getCurrentTime()); require(_rentDateEnd > _rentDateStart); require(_rentDateStart+_acceptObjectPeriod < _rentDateEnd); require(_rentDateStart > _noCancelPeriod); m_description = _description; m_fileUrl = _fileUrl; m_fileHash = _fileHash; m_price = _price; m_cancellationFee = _cancellationFee; m_rentDateStart = _rentDateStart; m_rentDateEnd = _rentDateEnd; m_noCancelPeriod = _noCancelPeriod; m_acceptObjectPeriod = _acceptObjectPeriod; } 

أذكر خوارزمية عمل Mythril. لتشغيل التتبع ، تحتاج إلى استدعاء مُنشئ العقد ، لأن كل التنفيذ اللاحق سيعتمد على المعلمات التي تم استدعاء المنشئ معها. على سبيل المثال ، إذا قمت بالاتصال _price == 0 باستخدام _price == 0 ، فسوف يقوم المنشئ بإلقاء استثناء عند require(_price > 0) . حتى إذا تكررت Mythril على العديد من قيم _price ، _price المُنشئ يكسر إذا ، على سبيل المثال ، _price <= _cancellationFee . في هذا العقد ، هناك اثنتي عشرة معلمة مرتبطة بقيود صارمة ، ولا يستطيع Mythril ، بالطبع ، تخمين المجموعات الصحيحة من المعلمات. يحاول الانتقال إلى الفرع التالي من التنفيذ ، حيث يصنّف معايير المُنشئ ، لكن ليس لديه أي فرصة عملية للتخمين - فهناك العديد من مجموعات المعلمات. لذلك ، لا ينجح حساب العقد - كل الطرق تعتمد على نوع من require(...) ، ونواجه المشكلة أعلاه.

الآن لدينا طريقتان: الأولى هي تعطيل جميع require في المنشئ عن طريق التعليق عليها. عندها سيكون Mythril قادرًا على الاتصال بالمنشئ باستخدام أي مجموعة من المعلمات وكل شيء سوف يعمل. لكن هذا يعني أنه من خلال فحص العقد باستخدام مثل هذه المعلمات ، سيجد Mythril أخطاء ممكنة مع تمرير قيم غير صحيحة إلى المُنشئ. ببساطة ، إذا عثر Mythril على خطأ ينشأ إذا قام مُنشئ العقد بتحديد _cancellationFee مليار مرة سعر الإيجار لـ _mprice ، فلن يكون هناك أي فائدة في هذا الخطأ - فلن يتم حظر هذا العقد أبدًا وسيتم إنفاق الموارد على العثور على الأخطاء. نحن نعني أن العقد لا يزال عالقًا بمعلمات أكثر أو أقل تناسقًا ، لذلك من المنطقي تحديد معلمات مُنشئ أكثر واقعية بحيث لا يبحث Mythril عن الأخطاء التي لن تحدث أبدًا إذا تم إغلاق العقد بشكل صحيح.

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

  function Booking( ) public payable { m_description = "My very long booking text about hotel and beautiful sea view!"; m_fileUrl = "https://ether-airbnb.bam/some-url/"; m_fileHash = 0x1628f3170cc16d40aad2e8fa1ab084f542fcb12e75ce1add62891dd75ba1ffd7; m_price = 1000000000000000000; // 1 ETH m_cancellationFee = 100000000000000000; // 0.1 ETH m_rentDateStart = 1550664800 + 3600 * 24; // current time + 1 day m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // current time + 4 days m_acceptObjectPeriod = 3600 * 8; // 8 hours m_noCancelPeriod = 3600 * 24; // 1 day require(m_price > 0); require(m_price > m_cancellationFee); require(m_rentDateStart > 1550664800); require(m_rentDateEnd > m_rentDateStart); require((m_rentDateStart + m_acceptObjectPeriod) < m_rentDateEnd); require(m_rentDateStart > m_noCancelPeriod); } 

بالإضافة إلى ذلك ، لبدء كل شيء ، يجب عليك أيضًا تعيين المعلمة max-depth . لقد --max-depth=34 هذا الأمر مع هذا المُنشئ --max-depth=34 على مثيل AWS t2.medium. في الوقت نفسه ، على جهاز الكمبيوتر المحمول ، وهو أكثر قوة ، يبدأ كل شيء دون أي max-depth . إذا حكمنا من خلال استخدام هذه المعلمة ، من الضروري إنشاء فروع للتحليل ، وقيمتها الافتراضية هي اللانهاية ( الكود ). لذلك ، قم بتدوير هذه المعلمة ، ولكن تأكد من تحليل العقد المطلوب. يمكنك فهم هذا عن طريق رسائل مثل:

 mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: ............. 

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

البحث عن الاخطاء

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

أولاً ، دعنا نرى ما أصدره Mythril لعقد Booking طالت معاناته. الإنذار الأول:

 ==== Dependence on predictable environment variable ==== SWC ID: 116 Severity: Low Contract: Booking Function name: fallback PC address: 566 Estimated Gas Usage: 17908 - 61696 Sending of Ether depends on a predictable variable. The contract sends Ether depending on the values of the following variables: - block.timestamp Note that the values of variables like coinbase, gaslimit, block number and timestamp are predictable and/or can be manipulated by a malicious miner. Don't use them for random number generation or to make critical decisions. -------------------- In file: contracts/flattened.sol:142 msg.sender.transfer(msg.value-m_price) 

وينشأ بسبب

 require(m_rentDateStart > getCurrentTime()); 

في وظيفة الاحتياطية.

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

دعونا نرى ما إذا كان Mythril يرى تبعية على block.timestamp إذا block.timestamp المتغير في مكالمة متداخلة مثل:

 function getCurrentTime() public view returns (uint256) { - return now; + return getCurrentTimeInner(); } + function getCurrentTimeInner() internal returns (uint256) { + return now; + } 

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

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

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

 function collectTaxes() external onlyState(State.PAID) { msg.sender.transfer(address(this).balance / 5); } 

وجدت ميثريل المشكلة:

 ==== Unprotected Ether Withdrawal ==== SWC ID: 105 Severity: High Contract: Booking Function name: collectTaxes() PC address: 2492 Estimated Gas Usage: 2135 - 2746 Anyone can withdraw ETH from the contract account. Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent a equivalent amount of ETH to it. This is likely to be a vulnerability. -------------------- In file: contracts/flattened.sol:149 msg.sender.transfer(address(this).balance / 5) -------------------- -------------------- Transaction Sequence: { "2": { "calldata": "0x", "call_value": "0xde0b6b3a7640000", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" }, "3": { "calldata": "0x01b613a5", "call_value": "0x0", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" } } 

عظيم ، أي قام Mythril بإبراز عمليتين ، مما يؤدي إلى حقيقة أنه يمكنك الحصول على الأثير من العقد. الآن قم بتغيير شرط State.RENT إلى State.RENT ، مثل هذا:

 - function collectTaxes() external onlyState(State.PAID){ + function collectTaxes() external onlyState(State.RENT) { 

الآن يمكن استدعاء State.RENT collectTaxes() فقط عندما يكون العقد في حالة State.RENT ، وفي هذه اللحظة لا يوجد شيء في الميزان ، لأنه أرسل العقد بالفعل البث الكامل إلى المالك. والشيء المهم هنا هو أن Mythril هذه المرة لا يخرج الخطأ ==== Unprotected Ether Withdrawal ==== ! تحت الشرط onlyState(State.RENT) ، لم يصل المحلل إلى فرع الكود الذي يرسل الأثير من العقد برصيد غير صفري. مر Mythril بخيارات مختلفة للمعلمات ، لكن يمكنك الدخول إلى State.RENT فقط عن طريق إرسال كل البث إلى المؤجر. لذلك ، من المستحيل الوصول إلى هذا الفرع من الشفرة برصيد غير صفري ، ولا يضايق Mythril المدقق!

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

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

الخاتمة

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

لا يزال Mythril برنامجًا شابًا إلى حد ما ، وهذا ليس IDA Pro ، وهناك عدد قليل جدًا من الوثائق باستثناء مقالات قليلة. لا يمكن قراءة قيمة العديد من المعلمات إلا في رمز Mythril ، بدءًا من cli.py. آمل أن يظهر وصف كامل ومتعمق لتشغيل كل معلمة في الوثائق.

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

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

لتلخيص ، توصيات لاستخدام Mythril هي:

1. تضييق شروط بدء العقد قيد الدراسة قدر الإمكان. إذا قضى Mythril أثناء التحليل الكثير من الموارد على الفروع التي لن يتم تنفيذها على أرض الواقع ، فستفقد القدرة على العثور على أخطاء مهمة حقًا ، لذلك يجب عليك دائمًا محاولة تضييق نطاق الفروع المحتملة.
2. تأكد من بدء تحليل العقد ، لا تفوت رسائل مثل mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) ، وإلا فقد تفكر بالخطأ في عدم وجود أخطاء.
3. يمكنك تعطيل الفروع بشكل تعسفي في رمز العقد ، مما يعطي Mythril تباينًا أقل في اختيار الفروع وتوفير الموارد. حاول الاستغناء عن القيود المفروضة على max-depth ، حتى لا "تقطع" التحليل ، ولكن احرص على عدم إخفاء الخطأ.
4. انتبه لكل تحذير ، حتى التعليقات الخفيفة تستحق في بعض الأحيان أن تضيف تعليقًا على الأقل إلى رمز العقد ، مما يسهل على المطورين الآخرين.

في المقالة التالية ، سنتعامل مع محلل Manticore ، ولكن هنا جدول محتويات المقالات الجاهزة أو المخطط للكتابة:

الجزء 1. مقدمة. تجميع ، تسطيح ، إصدارات من الصلابة
الجزء 2. انزلق
3. Mythril ( )
4. Manticore ( )
5. Echidna ( )