programa-stic/barf-projectBARF : إطار عمل مفتوح المصدر متعدد المنصات لتحليل الثنائيات وهندسة البرمجيات العكسية
يُعد تحليل الشفرة الثنائية نشاطًا حاسمًا في العديد من مجالات علوم الكمبيوتر وهندسة البرمجيات، بدءًا من أمن البرمجيات وتحليل البرامج وصولاً إلى الهندسة العكسية. التحليل اليدوي للشفرة الثنائية مهمة صعبة وتستغرق وقتًا طويلاً، وتوجد أدوات برمجية تسعى إلى أتمتة أو مساعدة المحللين البشريين. ومع ذلك، فإن معظم هذه الأدوات لها قيود تقنية وتجارية تحد من الوصول إليها واستخدامها من قبل جزء كبير من المجتمعات الأكاديمية والممارسين. BARF هو إطار عمل مفتوح المصدر لتحليل الشفرة الثنائية يهدف إلى دعم مجموعة واسعة من مهام تحليل الشفرة الثنائية الشائعة في تخصص أمن المعلومات. إنها منصة قابلة للبرمجة تدعم رفع التعليمات من معماريات متعددة، والترجمة الثنائية إلى تمثيل وسيط، وإطار عمل قابل للتوسع لمكونات تحليل الكود، والتفاعل مع الأدوات الخارجية مثل المصححات وحلول SMT وأدوات التتبع. صُمم الإطار بشكل أساسي للتحليل بمساعدة الإنسان ولكنه يمكن أتمتته بالكامل.
يشمل مشروع BARF BARF والأدوات والحزم ذات الصلة. حتى الآن، يتكون المشروع من العناصر التالية:
لمزيد من المعلومات، انظر:
الحالة الحالية:
| أحدث إصدار | v0.6.0 |
|---|---|
| الرابط | https://github.com/programa-stic/barf-project/releases/tag/v0.6.0 |
| سجل التغييرات | https://github.com/programa-stic/barf-project/blob/v0.6.0/CHANGELOG.md |
تم اختبار جميع الحزم على Ubuntu 16.04 (x86_64).
BARF هي حزمة Python لتحليل الشفرة الثنائية والهندسة العكسية. يمكنها:
ELF, PE, إلخ)،إنها حاليًا قيد التطوير.
يعتمد BARF على حلول SMT التالية:
يقوم الأمر التالي بتثبيت BARF على نظامك:
$ sudo python setup.py install
يمكنك أيضًا تثبيته محليًا:
$ sudo python setup.py install --user
sudo pip install pyasmjitsudo apt-get install graphvizهذا مثال بسيط يوضح كيفية فتح ملف ثنائي وطباعة كل تعليمة مع ترجمتها إلى اللغة الوسيطة (REIL).
from barf import BARF
# Open binary file.
barf = BARF("examples/misc/samples/bin/branch4.x86")
# Print assembly instruction.
for addr, asm_instr, reil_instrs in barf.translate():
print("{:#x} {}".format(addr, asm_instr))
# Print REIL translation.
for reil_instr in reil_instrs:
print("\t{}".format(reil_instr))
يمكننا أيضًا استعادة CFG وحفظه في ملف .dot.
# Recover CFG.
cfg = barf.recover_cfg()
# Save CFG to a .dot file.
cfg.save("branch4.x86_cfg")
يمكننا التحقق من القيود على الكود باستخدام حل SMT. على سبيل المثال، افترض أن لديك الكود التالي:
80483ed: 55 push ebp
80483ee: 89 e5 mov ebp,esp
80483f0: 83 ec 10 sub esp,0x10
80483f3: 8b 45 f8 mov eax,DWORD PTR [ebp-0x8]
80483f6: 8b 55 f4 mov edx,DWORD PTR [ebp-0xc]
80483f9: 01 d0 add eax,edx
80483fb: 83 c0 05 add eax,0x5
80483fe: 89 45 fc mov DWORD PTR [ebp-0x4],eax
8048401: 8b 45 fc mov eax,DWORD PTR [ebp-0x4]
8048404: c9 leave
8048405: c3 ret
وتريد معرفة القيم التي يجب تعيينها لمواقع الذاكرة ebp-0x4 و ebp-0x8 و ebp-0xc للحصول على قيمة محددة في مسجل eax بعد تنفيذ الكود.
أولاً، نضيف التعليمات إلى مكون المحلل.
from barf import BARF
# Open ELF file
barf = BARF("examples/misc/samples/bin/constraint1.x86")
# Add instructions to analyze.
for addr, asm_instr, reil_instrs in barf.translate(0x80483ed, 0x8048401):
for reil_instr in reil_instrs:
barf.code_analyzer.add_instruction(reil_instr)
ثم، نقوم بتوليد تعبيرات لكل متغير مهم ونضيف القيود المطلوبة عليها.
ebp = barf.code_analyzer.get_register_expr("ebp", mode="post")
# Preconditions: set range for variable a and b
a = barf.code_analyzer.get_memory_expr(ebp-0x8, 4, mode="pre")
b = barf.code_analyzer.get_memory_expr(ebp-0xc, 4, mode="pre")
for constr in [a >= 2, a <= 100, b >= 2, b <= 100]:
barf.code_analyzer.add_constraint(constr)
# Postconditions: set desired value for the result
c = barf.code_analyzer.get_memory_expr(ebp-0x4, 4, mode="post")
for constr in [c >= 26, c <= 28]:
barf.code_analyzer.add_constraint(constr)
أخيرًا، نتحقق مما إذا كان يمكن حل القيود التي وضعناها.
if barf.code_analyzer.check() == 'sat':
print("[+] Satisfiable! Possible assignments:")
# Get concrete value for expressions
a_val = barf.code_analyzer.get_expr_value(a)
b_val = barf.code_analyzer.get_expr_value(b)
c_val = barf.code_analyzer.get_expr_value(c)
# Print values
print("- a: {0:#010x} ({0})".format(a_val))
print("- b: {0:#010x} ({0})".format(b_val))
print("- c: {0:#010x} ({0})".format(c_val))
assert a_val + b_val + 5 == c_val
else:
print("[-] Unsatisfiable!")
يمكنك رؤية هذه الأمثلة والمزيد في دليل examples.
ينقسم الإطار إلى ثلاثة مكونات رئيسية: النواة و المعمارية و التحليل.
يحتوي هذا المكون على وحدات أساسية:
REIL: يوفر تعريفات للغة REIL. كما ينفذ محاكيًا و محللًا لغويًا.SMT: يوفر وسائل للتفاعل مع حلي SMT [Z3] و [CVC4]. كما يوفر وظائف لترجمة تعليمات REIL إلى تعبيرات SMT.BI: وحدة الواجهة الثنائية مسؤولة عن تحميل الملفات الثنائية للمعالجة (تستخدم [PEFile] و [PyELFTools]).كل معمارية مدعومة تُقدم كمكون فرعي يحتوي على الوحدات التالية:
Architecture: تصف المعمارية، أي المسجلات، حجم عنوان الذاكرة.Translator: يوفر مترجمات إلى REIL لكل تعليمة مدعومة.Disassembler: يوفر وظائف فك التجميع (يستخدم [Capstone]).Parser: يحول التعليمة من سلسلة نصية إلى شكل كائن.يتكون هذا المكون حتى الآن من وحدات: رسم بياني لتدفق التحكم و رسم بياني للاستدعاءات و محلل الكود. الأولان يوفران وظائف لاستعادة CFG و CG على التوالي. الأخير هو واجهة عالية المستوى لوظائف حل SMT ذات الصلة.
BARFgadgets هو سكربت Python مبني على BARF يتيح لك البحث عن أدوات ROP داخل برنامج ثنائي وتصنيفها والتحقق منها. مرحلة البحث تجد جميع الأدوات المنتهية بـ ret و jmp و call داخل الثنائي. مرحلة التصنيف تصنف الأدوات التي تم العثور عليها سابقًا وفقًا للأنواع التالية: