⚠️ المشروع مؤرشف ⚠️

لم يعد هذا المشروع قيد التطوير والصيانة داخلياً.

Manticore

Manticore هي أداة تنفيذ رمزي لتحليل العقود الذكية والملفات الثنائية.

الميزات

• استكشاف البرامج: يمكن لـ Manticore تنفيذ برنامج مع مدخلات رمزية واستكشاف جميع الحالات الممكنة التي يمكنه الوصول إليها
• توليد المدخلات: يمكن لـ Manticore إنتاج مدخلات ملموسة تلقائياً تؤدي إلى حالة برنامج معينة
• اكتشاف الأخطاء: يمكن لـ Manticore اكتشاف الأعطال وحالات الفشل الأخرى في الملفات الثنائية والعقود الذكية
• التضمين: توفر Manticore تحكماً دقيقاً في استكشاف الحالة عبر استدعاءات الأحداث وخطافات التعليمات
• الواجهة البرمجية: تعرض Manticore وصولاً برمجياً إلى محرك التحليل الخاص بها عبر واجهة برمجة تطبيقات Python

يمكن لـ Manticore تحليل الأنواع التالية من البرامج:

• العقود الذكية لإيثريوم (EVM bytecode)
• ملفات ELF الثنائية لنظام لينكس (x86, x86_64, aarch64, و ARMv7)
• وحدات WASM

التثبيت

ملاحظة: نوصي بتثبيت Manticore في بيئة افتراضية لمنع التعارض مع المشاريع أو الحزم الأخرى

الخيار 1: التثبيت من PyPI:

pip install manticore

الخيار 2: التثبيت من PyPI، مع التبعيات الإضافية اللازمة لتنفيذ الملفات الثنائية الأصلية:

pip install "manticore[native]"

الخيار 3: تثبيت إصدار تطويري ليلي:

pip install --pre "manticore[native]"

الخيار 4: التثبيت من فرع master:

git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"

الخيار 5: التثبيت عبر Docker:

docker pull trailofbits/manticore

بمجرد التثبيت، ستكون أداة CLI manticore وواجهة برمجة التطبيقات Python متاحة.

للتثبيت التطويري، راجع wiki.

الاستخدام

CLI

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

EVM

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

$ manticore examples/evm/umd_example.sol 
 [9921] m.main:INFO: Registered plugins: DetectUninitializedMemory, DetectReentrancySimple, DetectExternalCallAndLeak, ...
 [9921] m.e.manticore:INFO: Starting symbolic create contract
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 0
 [9921] m.e.manticore:INFO: 4 alive states, 6 terminated states
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 1
 [9921] m.e.manticore:INFO: 16 alive states, 22 terminated states
[13761] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
[13754] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
...
[13743] m.c.manticore:INFO: Generated testcase No. 36 - THROW(3 txs)
[13740] m.c.manticore:INFO: Generated testcase No. 37 - THROW(3 txs)
[9921] m.c.manticore:INFO: Results in ~/manticore/mcore_gsncmlgx

Manticore-verifier

تم توفير أداة CLI بديلة تبسط اختبار العقود وتسمح بكتابة طرق الخصائص بنفس اللغة عالية المستوى التي يستخدمها العقد. تحقق من توثيق manticore-verifier documentation. شاهد عرضاً

Native

$ manticore examples/linux/basic
[9507] m.n.manticore:INFO: Loading program examples/linux/basic
[9507] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Results in ~/manticore/mcore_7u7hgfay
[9507] m.n.manticore:INFO: Total time: 2.8029580116271973

API

توفر Manticore واجهة برمجة تطبيقات Python يمكن استخدامها لتنفيذ تحليلات مخصصة قوية.

EVM

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

from manticore.ethereum import ManticoreEVM
contract_src="""
contract Adder {
    function incremented(uint value) public returns (uint){
        if (value == 1)
            revert();
        return value + 1;
    }
}
"""
m = ManticoreEVM()

user_account = m.create_account(balance=10000000)
contract_account = m.solidity_create_contract(contract_src,
                                              owner=user_account,
                                              balance=0)
value = m.make_symbolic_value()

contract_account.incremented(value)

for state in m.ready_states:
    print("can value be 1? {}".format(state.can_be_true(value == 1)))
    print("can value be 200? {}".format(state.can_be_true(value == 200)))

Native

من الممكن أيضاً استخدام API لإنشاء أدوات تحليل مخصصة للملفات الثنائية لنظام لينكس. يساعد تخصيص الحالة الأولية في تجنب مشاكل انفجار الحالة التي تحدث عادة عند استخدام CLI.

# example Manticore script
from manticore.native import Manticore

m = Manticore.linux('./example')

@m.hook(0x400ca0)
def hook(state):
  cpu = state.cpu
  print('eax', cpu.EAX)
  print(cpu.read_int(cpu.ESP))

  m.kill()  # tell Manticore to stop

m.run()

WASM

يمكن لـ Manticore أيضاً تقييم دوال WebAssembly على مدخلات رمزية للتحقق من الخصائص أو التحليل العام.

from manticore.wasm import ManticoreWASM

m = ManticoreWASM("collatz.wasm")

def arg_gen(state):
    # Generate a symbolic argument to pass to the collatz function.
    # Possible values: 4, 6, 8
    arg = state.new_symbolic_value(32, "collatz_arg")
    state.constrain(arg > 3)
    state.constrain(arg < 9)
    state.constrain(arg % 2 == 0)
    return [arg]


# Run the collatz function with the given argument generator.
m.collatz(arg_gen)

# Manually collect return values
# Prints 2, 3, 8
for idx, val_list in enumerate(m.collect_returns()):
    print("State", idx, "::", val_list[0])

المتطلبات

• يتطلب Manticore Python 3.7 أو أحدث
• يدعم Manticore رسمياً أحدث إصدار LTS من Ubuntu الذي توفره Github Actions
  • Manticore لديه دعم تجريبي لـ EVM و WASM (وليس الملفات الثنائية الأصلية لنظام لينكس) على MacOS
• نوصي بالتشغيل مع زيادة حجم المكدس. يمكن القيام بذلك عن طريق تشغيل ulimit -s 100000 أو عن طريق تمرير --ulimit stack=100000000:100000000 إلى docker run