كيفية استخدام مانتيكور لإيجاد الأخطاء في العقود الذكية

الهدف من هذا الدرس التعليمي هو توضيح كيفية استخدام مانتيكور للعثور تلقائيًا على الأخطاء في العقود الذكية.

التثبيت

يتطلب مانتيكور إصدار python 3.6 >=. يمكن تثبيته من خلال pip أو باستخدام docker.

مانتيكور من خلال docker

docker pull trailofbits/eth-security-toolbox
docker run -it -v "$PWD":/home/training trailofbits/eth-security-toolbox

الأمر الأخير يشغل eth-security-toolbox في حاوية docker لديها صلاحية الوصول إلى دليلك الحالي. يمكنك تغيير الملفات من مضيفك، وتشغيل الأدوات على الملفات من حاوية docker

داخل حاوية docker، قم بتشغيل:

solc-select 0.5.11
cd /home/trufflecon/

مانتيكور من خلال pip

pip3 install --user manticore

يُنصح باستخدام solc 0.5.11.

تشغيل نص برمجي

لتشغيل نص python برمجي باستخدام python 3:

python3 script.py

مقدمة في التنفيذ الرمزي الديناميكي

التنفيذ الرمزي الديناميكي باختصار

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

1. يتم إنشاؤها باستخدام قيود على مدخلات البرنامج.
2. يتم استخدامها لتوليد مدخلات للبرنامج من شأنها أن تتسبب في تنفيذ المسارات المرتبطة بها.

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

مثال على مسند المسار (Path Predicate)

للحصول على فكرة عن كيفية عمل التنفيذ الرمزي الديناميكي (DSE)، خذ المثال التالي:

1function f(uint a){
2
3  if (a == 65) {
4      // يوجد خطأ
5  }
6
7}
نسخ

بما أن f() تحتوي على مسارين، فإن التنفيذ الرمزي الديناميكي (DSE) سيقوم ببناء مسندين مختلفين للمسار:

• المسار 1: a == 65
• المسار 2: Not (a == 65)

كل مسند مسار هو صيغة رياضية يمكن إعطاؤها لما يسمى محلل SMT (opens in a new tab)، الذي سيحاول حل المعادلة. بالنسبة لـ المسار 1، سيقول المحلل أنه يمكن استكشاف المسار باستخدام a = 65. بالنسبة لـ المسار 2، يمكن للمحلل أن يعطي a أي قيمة بخلاف 65، على سبيل المثال a = 0.

التحقق من الخصائص

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

خذ المثال التالي:

1function unsafe_add(uint a, uint b) returns(uint c){
2  c = a + b; // لا توجد حماية من تجاوز السعة
3  return c;
4}
نسخ

هنا لا يوجد سوى مسار واحد لاستكشافه في الدالة:

• المسار 1: c = a + b

باستخدام مانتيكور، يمكنك التحقق من تجاوز السعة، وإضافة قيود إلى مسند المسار:

• c = a + b AND (c < a OR c < b)

إذا كان من الممكن إيجاد تقييم لـ a و b يكون فيه مسند المسار أعلاه ممكنًا، فهذا يعني أنك قد وجدت تجاوزًا للسعة. على سبيل المثال، يمكن للمحلل إنشاء المدخل a = 10 , b = MAXUINT256.

إذا أخذت في الاعتبار نسخة مصححة:

1function safe_add(uint a, uint b) returns(uint c){
2  c = a + b;
3  require(c>=a);
4  require(c>=b);
5  return c;
6}
نسخ

الصيغة المرتبطة مع التحقق من تجاوز السعة ستكون:

• c = a + b AND (c >= a) AND (c=>b) AND (c < a OR c < b)

لا يمكن حل هذه الصيغة؛ بعبارة أخرى، هذا دليل على أنه في safe_add، ستزداد قيمة c دائمًا.

وبالتالي، يعد التنفيذ الرمزي الديناميكي (DSE) أداة قوية، يمكنها التحقق من القيود العشوائية على النص البرمجي الخاص بك.

التشغيل تحت مانتيكور

سنرى كيف نستكشف عقدًا ذكيًا باستخدام واجهة برمجة تطبيقات مانتيكور. الهدف هو العقد الذكي التالي example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
إظهار الكل
نسخ

تشغيل استكشاف مستقل

يمكنك تشغيل مانتيكور مباشرة على العقد الذكي بالأمر التالي (project يمكن أن يكون ملف سوليديتي، أو دليل مشروع):

$ manticore project

ستحصل على مخرجات لحالات اختبار مثل هذه (قد يتغير الترتيب):

1...
2... m.c.manticore:INFO: Generated testcase No. 0 - STOP
3... m.c.manticore:INFO: Generated testcase No. 1 - REVERT
4... m.c.manticore:INFO: Generated testcase No. 2 - RETURN
5... m.c.manticore:INFO: Generated testcase No. 3 - REVERT
6... m.c.manticore:INFO: Generated testcase No. 4 - STOP
7... m.c.manticore:INFO: Generated testcase No. 5 - REVERT
8... m.c.manticore:INFO: Generated testcase No. 6 - REVERT
9... m.c.manticore:INFO: Results in /home/ethsec/workshops/Automated Smart Contracts Audit - TruffleCon 2018/manticore/examples/mcore_t6vi6ij3
10...
إظهار الكل

بدون معلومات إضافية، سيستكشف مانتيكور العقد بمعاملات رمزية جديدة حتى يتوقف عن استكشاف مسارات جديدة في العقد. لا يقوم مانتيكور بتشغيل معاملات جديدة بعد معاملة فاشلة (على سبيل المثال: بعد revert).

سيقوم مانتيكور بإخراج المعلومات في دليل mcore_*. من بين أمور أخرى، ستجد في هذا الدليل:

• global.summary: التغطية وتحذيرات المترجم
• test_XXXXX.summary: التغطية، آخر تعليمة، أرصدة الحسابات لكل حالة اختبار
• test_XXXXX.tx: قائمة مفصلة بالمعاملات لكل حالة اختبار

هنا يجد مانتيكور 7 حالات اختبار، والتي تتوافق مع (قد يتغير ترتيب أسماء الملفات):

ملخص الاستكشاف: f(!=65) تشير إلى استدعاء الدالة f بأي قيمة مختلفة عن 65.

كما تلاحظ، يقوم مانتيكور بإنشاء حالة اختبار فريدة لكل معاملة ناجحة أو تم التراجع عنها (reverted).

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

التعامل مع عقد ذكي من خلال واجهة برمجة التطبيقات (API)

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

إنشاء الحسابات

أول شيء يجب عليك فعله هو بدء بلوكتشين جديدة بالأوامر التالية:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
نسخ

يتم إنشاء حساب غير مرتبط بعقد باستخدام m.create_account (opens in a new tab):

1user_account = m.create_account(balance=1000)
نسخ

يمكن نشر عقد سوليديتي باستخدام m.solidity_create_contract (opens in a new tab):

1source_code = '''
2pragma solidity >=0.4.24 <0.6.0;
3contract Simple {
4    function f(uint a) payable public{
5        if (a == 65) {
6            revert();
7        }
8    }
9}
10'''
11# بدء العقد
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
إظهار الكل
نسخ

ملخص

• يمكنك إنشاء حسابات المستخدمين وحسابات العقود باستخدام m.create_account (opens in a new tab) و m.solidity_create_contract (opens in a new tab).

تنفيذ المعاملات

يدعم مانتيكور نوعين من المعاملات:

• المعاملة الأولية (Raw transaction): يتم استكشاف جميع الدوال
• المعاملة المسماة (Named transaction): يتم استكشاف دالة واحدة فقط

المعاملة الأولية

يتم تنفيذ معاملة أولية باستخدام m.transaction (opens in a new tab):

1m.transaction(caller=user_account,
2              address=contract_account,
3              data=data,
4              value=value)
نسخ

يمكن أن يكون المتصل (caller) أو العنوان (address) أو البيانات (data) أو قيمة المعاملة إما ملموسة أو رمزية:

• m.make_symbolic_value (opens in a new tab) ينشئ قيمة رمزية.
• m.make_symbolic_buffer(size) (opens in a new tab) ينشئ مصفوفة بايت رمزية.

على سبيل المثال:

1symbolic_value = m.make_symbolic_value()
2symbolic_data = m.make_symbolic_buffer(320)
3m.transaction(caller=user_account,
4              address=contract_address,
5              data=symbolic_data,
6              value=symbolic_value)
نسخ

إذا كانت البيانات رمزية، فسيستكشف مانتيكور جميع دوال العقد أثناء تنفيذ المعاملة. سيكون من المفيد الاطلاع على شرح الدالة الاحتياطية (Fallback Function) في مقال Hands on the Ethernaut CTF (opens in a new tab) لفهم كيفية عمل اختيار الدالة.

المعاملة المسماة

يمكن تنفيذ الدوال من خلال أسمائها. لتنفيذ f(uint var) بقيمة رمزية، من user_account، وبقيمة 0 إيثر، استخدم:

1symbolic_var = m.make_symbolic_value()
2contract_account.f(symbolic_var, caller=user_account, value=0)
نسخ

إذا لم يتم تحديد قيمة المعاملة، فإنها تساوي 0 بشكل افتراضي.

ملخص

• يمكن أن تكون وسائط (arguments) المعاملة ملموسة أو رمزية
• المعاملة الأولية ستستكشف جميع الدوال
• يمكن استدعاء الدالة باسمها

مساحة العمل

m.workspace هو الدليل المستخدم كدليل إخراج لجميع الملفات التي تم إنشاؤها:

1print("النتائج موجودة في {}".format(m.workspace))
نسخ

إنهاء الاستكشاف

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

ملخص: التشغيل تحت مانتيكور

بجمع كل الخطوات السابقة معًا، نحصل على:

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14print("النتائج موجودة في {}".format(m.workspace))
15m.finalize() # إيقاف الاستكشاف
إظهار الكل
نسخ

يمكنك العثور على كل النص البرمجي أعلاه في example_run.py (opens in a new tab)

الحصول على مسارات الطرح (throwing paths)

سنقوم الآن بإنشاء مدخلات محددة للمسارات التي تثير استثناءً (exception) في f(). لا يزال الهدف هو العقد الذكي التالي example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
نسخ

استخدام معلومات الحالة

كل مسار يتم تنفيذه له حالته الخاصة من البلوكتشين. تكون الحالة إما جاهزة (ready) أو مقتولة (killed)، مما يعني أنها تصل إلى تعليمة THROW أو REVERT:

• m.ready_states (opens in a new tab): قائمة الحالات الجاهزة (التي لم تنفذ REVERT/INVALID)
• m.killed_states (opens in a new tab): قائمة الحالات المقتولة
• m.all_states (opens in a new tab): جميع الحالات

1for state in m.all_states:
2    # افعل شيئًا بالحالة
نسخ

يمكنك الوصول إلى معلومات الحالة. على سبيل المثال:

• state.platform.get_balance(account.address): رصيد الحساب
• state.platform.transactions: قائمة المعاملات
• state.platform.transactions[-1].return_data: البيانات التي تم إرجاعها بواسطة آخر معاملة

البيانات التي تم إرجاعها بواسطة آخر معاملة هي مصفوفة يمكن تحويلها إلى قيمة باستخدام ABI.deserialize، على سبيل المثال:

1data = state.platform.transactions[0].return_data
2data = ABI.deserialize("uint", data)
نسخ

كيفية إنشاء حالة اختبار

استخدم m.generate_testcase(state, name) (opens in a new tab) لإنشاء حالة اختبار:

1m.generate_testcase(state, 'BugFound')
نسخ

ملخص

• يمكنك التكرار على الحالة باستخدام m.all_states
• state.platform.get_balance(account.address) تُرجع رصيد الحساب
• state.platform.transactions تُرجع قائمة المعاملات
• transaction.return_data هي البيانات المُرجعة
• m.generate_testcase(state, name) تنشئ مدخلات للحالة

ملخص: الحصول على مسار الطرح (Throwing Path)

1from manticore.ethereum import ManticoreEVM
2
3m = ManticoreEVM()
4
5with open('example.sol') as f:
6    source_code = f.read()
7
8user_account = m.create_account(balance=1000)
9contract_account = m.solidity_create_contract(source_code, owner=user_account)
10
11symbolic_var = m.make_symbolic_value()
12contract_account.f(symbolic_var)
13
14## تحقق مما إذا كان التنفيذ ينتهي بـ REVERT أو INVALID
15
16for state in m.terminated_states:
17    last_tx = state.platform.transactions[-1]
18    if last_tx.result in ['REVERT', 'INVALID']:
19        print('تم العثور على طرح (Throw) {}'.format(m.workspace))
20        m.generate_testcase(state, 'ThrowFound')
إظهار الكل
نسخ

يمكنك العثور على كل النص البرمجي أعلاه في example_run.py (opens in a new tab)

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

إضافة قيود

سنرى كيف يمكن تقييد الاستكشاف. سنفترض أن توثيق f() ينص على أن الدالة لا يتم استدعاؤها أبدًا بـ a == 65، لذا فإن أي خطأ مع a == 65 ليس خطأ حقيقيًا. لا يزال الهدف هو العقد الذكي التالي example.sol (opens in a new tab):

1pragma solidity >=0.4.24 <0.6.0;
2contract Simple {
3    function f(uint a) payable public{
4        if (a == 65) {
5            revert();
6        }
7    }
8}
نسخ

العوامل (Operators)

يسهل وحدة Operators (opens in a new tab) التعامل مع القيود، ومن بين ما توفره:

• Operators.AND،
• Operators.OR،
• Operators.UGT (أكبر من غير المؤشر)،
• Operators.UGE (أكبر من أو يساوي غير المؤشر)،
• Operators.ULT (أقل من غير المؤشر)،
• Operators.ULE (أقل من أو يساوي غير المؤشر).

لاستيراد الوحدة، استخدم ما يلي:

1from manticore.core.smtlib import Operators
نسخ

يُستخدم Operators.CONCAT لربط مصفوفة بقيمة. على سبيل المثال، يجب تغيير return_data لمعاملة ما إلى قيمة ليتم فحصها مقابل قيمة أخرى:

1last_return = Operators.CONCAT(256, *last_return)
نسخ

القيود

يمكنك استخدام القيود بشكل عام أو لحالة معينة.

قيد عام

استخدم m.constrain(constraint) لإضافة قيد عام. على سبيل المثال، يمكنك استدعاء عقد من عنوان رمزي، وتقييد هذا العنوان ليكون قيمًا محددة:

1symbolic_address = m.make_symbolic_value()
2m.constraint(Operators.OR(symbolic == 0x41, symbolic_address == 0x42))
3m.transaction(caller=user_account,
4              address=contract_account,
5              data=m.make_symbolic_buffer(320),
6              value=0)
نسخ

قيد الحالة

استخدم state.constrain(constraint) (opens in a new tab) لإضافة قيد إلى حالة معينة. يمكن استخدامه لتقييد الحالة بعد استكشافها للتحقق من خاصية معينة عليها.

التحقق من القيد

استخدم solver.check(state.constraints) لمعرفة ما إذا كان القيد لا يزال ممكنًا. على سبيل المثال، سيقيد ما يلي symbolic_value لتكون مختلفة عن 65 والتحقق مما إذا كانت الحالة لا تزال ممكنة:

1state.constrain(symbolic_var != 65)
2if solver.check(state.constraints):
3    # الحالة ممكنة
نسخ

ملخص: إضافة القيود

بإضافة قيد إلى النص البرمجي السابق، نحصل على:

1from manticore.ethereum import ManticoreEVM
2from manticore.core.smtlib.solver import Z3Solver
3
4solver = Z3Solver.instance()
5
6m = ManticoreEVM()
7
8with open("example.sol") as f:
9    source_code = f.read()
10
11user_account = m.create_account(balance=1000)
12contract_account = m.solidity_create_contract(source_code, owner=user_account)
13
14symbolic_var = m.make_symbolic_value()
15contract_account.f(symbolic_var)
16
17no_bug_found = True
18
19## تحقق مما إذا كان التنفيذ ينتهي بـ REVERT أو INVALID
20
21for state in m.terminated_states:
22    last_tx = state.platform.transactions[-1]
23    if last_tx.result in ['REVERT', 'INVALID']:
24        # نحن لا نأخذ في الاعتبار المسار الذي يكون فيه a == 65
25        condition = symbolic_var != 65
26        if m.generate_testcase(state, name="BugFound", only_if=condition):
27            print(f'تم العثور على خطأ، النتائج في {m.workspace}')
28            no_bug_found = False
29
30if no_bug_found:
31    print(f'لم يتم العثور على أخطاء')
إظهار الكل
نسخ

يمكنك العثور على كل النص البرمجي أعلاه في example_run.py (opens in a new tab)

آخر تحديث للصفحة: 26 أبريل 2024

n (opens in a new tab)

r (opens in a new tab)

h (opens in a new tab)

+6

عرض المساهمين