trailofbits/manticoreأداة تنفيذ رمزي
لم يعد هذا المشروع قيد التطوير والصيانة داخلياً.
Manticore هي أداة تنفيذ رمزي لتحليل العقود الذكية والملفات الثنائية.
يمكن لـ Manticore تحليل الأنواع التالية من البرامج:
ملاحظة: نوصي بتثبيت 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.
Manticore لديه واجهة سطر أوامر يمكنها إجراء تحليل رمزي أساسي لملف ثنائي أو عقد ذكي.
سيتم وضع نتائج التحليل في دليل عمل يبدأ بـ mcore_. للحصول على معلومات حول دليل العمل، راجع wiki.
واجهة 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
تم توفير أداة CLI بديلة تبسط اختبار العقود وتسمح بكتابة طرق الخصائص بنفس اللغة عالية المستوى التي يستخدمها العقد. تحقق من توثيق manticore-verifier documentation. شاهد عرضاً
$ 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
توفر Manticore واجهة برمجة تطبيقات Python يمكن استخدامها لتنفيذ تحليلات مخصصة قوية.
بالنسبة للعقود الذكية لإيثريوم، يمكن استخدام 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)))
من الممكن أيضاً استخدام 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()
يمكن لـ 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])
ulimit -s 100000 أو عن طريق تمرير --ulimit stack=100000000:100000000 إلى docker runsolc في $PATH الخاص بك.crytic-compile على الكود الخاص بك مباشرة لتسهيل تحديد أي مشاكل.يعتمد Manticore على محلل خارجي يدعم smtlib2. حالياً يتم دعم Z3 و Yices و CVC4 ويمكن اختيارهم عبر سطر الأوامر أو إعدادات التكوين.
إذا كان Yices متاحاً، فسيستخدمه Manticore بشكل افتراضي. إذا لم يكن، فسيعود إلى Z3 أو CVC4. إذا كنت ترغب في اختيار المحلل الذي تريد استخدامه يدوياً، يمكنك القيام بذلك على النحو التالي:
manticore --smt.solver Z3
لمزيد من التفاصيل اذهب إلى https://cvc4.github.io/. بخلاف ذلك، فقط احصل على الثنائي واستخدمه.
sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
sudo chmod +x /usr/bin/cvc4
Yices سريع بشكل لا يصدق. مزيد من التفاصيل هنا https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
لا تتردد في زيارة قناتنا #manticore على Slack في Empire Hacking للحصول على المساعدة في استخدام أو توسيع Manticore.
التوثيق متاح في عدة أماكن:
الويكي يحتوي على معلومات حول البدء مع Manticore والمساهمة
مرجع API يحتوي على توثيق أكثر شمولاً وعمقاً حول API الخاص بنا
دليل الأمثلة يحتوي على بعض الأمثلة الصغيرة التي تعرض ميزات API
مستودع manticore-examples يحتوي على بعض الأمثلة الأكثر تعقيداً، بما في ذلك بعض مشاكل CTF الحقيقية
إذا كنت ترغب في تقديم تقرير عن خطأ أو طلب ميزة، فيرجى استخدام صفحة المشكلات.
للأسئلة والتوضيحات، يرجى زيارة صفحة النقاش.
Manticore مرخص وموزع بموجب ترخيص AGPLv3. اتصل بنا إذا كنت تبحث عن استثناء للشروط.
إذا كنت تستخدم Manticore في عمل أكاديمي، فكر في التقديم على جائزة Crytic للأبحاث بقيمة 10 آلاف دولار.
