manticore
Manticore 0.3.7
لم يعد هذا المشروع يتم تطويره وصيانته داخليًا. ومع ذلك، يسعدنا مراجعة وقبول طلبات السحب الصغيرة والمكتوبة جيدًا من قبل المجتمع. سننظر فقط في إصلاحات الأخطاء والتحسينات الطفيفة.
يجب الرد على أي قضايا ومناقشات جديدة أو مفتوحة حاليًا ودعمها من قبل المجتمع.
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 بمجرد التثبيت، ستكون أداة manticore CLI وPython API متاحة.
للحصول على تثبيت التطوير، راجع wiki الخاص بنا.
لدى Manticore واجهة سطر أوامر يمكنها إجراء تحليل رمزي أساسي للعقد الثنائي أو الذكي. سيتم وضع نتائج التحليل في دليل مساحة العمل الذي يبدأ بـ mcore_ . للحصول على معلومات حول مساحة العمل، راجع wiki.
يكتشف Manticore CLI تلقائيًا أنك تحاول اختبار العقد إذا كان (على سبيل المثال) العقد يحتوي على امتداد .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 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) لإنشاء أدوات تحليل مخصصة لثنائيات Linux. يساعد تخصيص الحالة الأولية على تجنب مشكلات انفجار الحالة التي تحدث عادةً عند استخدام واجهة سطر الأوامر (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 أو توسيعه.
التوثيق متوفر في عدة أماكن:
يحتوي موقع wiki على معلومات حول بدء استخدام Manticore والمساهمة
يحتوي مرجع واجهة برمجة التطبيقات (API) على وثائق أكثر شمولاً وتعمقًا حول واجهة برمجة التطبيقات (API) الخاصة بنا
يحتوي دليل الأمثلة على بعض الأمثلة الصغيرة التي تعرض ميزات واجهة برمجة التطبيقات
يحتوي مستودع أمثلة manticore على بعض الأمثلة الأكثر تعقيدًا، بما في ذلك بعض مشكلات CTF الحقيقية
إذا كنت ترغب في تقديم تقرير خطأ أو طلب ميزة، فيرجى استخدام صفحة المشكلات الخاصة بنا.
للأسئلة والتوضيحات، يرجى زيارة صفحة المناقشة.
تم ترخيص Manticore وتوزيعه بموجب ترخيص AGPLv3. اتصل بنا إذا كنت تبحث عن استثناء للشروط.
إذا كنت تستخدم Manticore في العمل الأكاديمي، ففكر في التقدم للحصول على جائزة Crytic Research Award بقيمة 10 آلاف دولار.
