يعد تحليل الكود الثنائي نشاطًا حاسمًا في العديد من مجالات علوم الكمبيوتر وتخصصات هندسة البرمجيات التي تتراوح من أمان البرمجيات وتحليل البرامج إلى الهندسة العكسية. يعد التحليل الثنائي اليدوي مهمة صعبة وتستغرق وقتًا طويلاً ، وهناك أدوات برامج تسعى إلى أتمتة أو مساعدة المحللين البشريين. ومع ذلك ، فإن معظم هذه الأدوات لديها العديد من القيود الفنية والتجارية التي تحد من الوصول واستخدامها من قبل جزء كبير من المجتمعات الأكاديمية والممارسات. BARF هو إطار تحليل ثنائي مفتوح المصدر يهدف إلى دعم مجموعة واسعة من مهام تحليل الكود الثنائي الشائع في انضباط أمن المعلومات. إنه منصة قابلة للنص التي تدعم رفع التعليمات من بنيات متعددة ، وترجمة ثنائية إلى تمثيل وسيطة ، وإطار عمل قابل للتمديد لإضافات تحليل التعليمات البرمجية والتواصل مع الأدوات الخارجية مثل التصريف وحل SMT وأدوات الأجهزة. تم تصميم الإطار في المقام الأول للتحليل بمساعدة الإنسان ولكن يمكن أن يكون آليًا بالكامل.
يتضمن مشروع BARF BARF والأدوات والحزم ذات الصلة. حتى الآن يتكون المشروع من العناصر التالية:
لمزيد من المعلومات ، راجع:
الوضع الحالي:
| أحدث إصدار | v0.6.0 |
|---|---|
| عنوان URL | https://github.com/programa-stic/barf-project/release/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 --usersudo 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 Solver. على سبيل المثال ، افترض أن لديك الرمز التالي:
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!" )يمكنك رؤية هذه الأمثلة والمزيد من الأمثلة في دليل الأمثلة.
ينقسم الإطار إلى ثلاثة مكونات رئيسية: Core و Arch and Analysis .
يحتوي هذا المكون على وحدات أساسية:
REIL : يوفر تعريفات للغة Reil. كما أنه يطبق محاكيًا ومحللًا .SMT : يوفر وسيلة للواجهة مع Z3 و CVC4 SMT Solver. أيضًا ، يوفر وظائف لترجمة تعليمات REIL إلى تعبيرات SMT.BI : وحدة الواجهة الثنائية هي المسؤولة عن تحميل الملفات الثنائية للمعالجة (فهي تستخدم Pefile و Pyelftools.) يتم توفير كل بنية مدعومة كمكون فرعي يحتوي على الوحدات التالية.
Architecture : يصف الهندسة المعمارية ، أي السجلات ، وحجم عنوان الذاكرة.Translator : يوفر للمترجمين أن يعيدوا لكل تعليمات مدعومة.Disassembler : يوفر وظائف تفكيك (يستخدم Cabstone.)Parser : يحول التعليمات من سلسلة إلى نموذج الكائن. يتكون هذا المكون حتى الآن من وحدات: الرسم البياني لتدفق التحكم ، والرسم البياني للاتصال ومحلل التعليمات البرمجية . الأولان ، يوفر وظائف لاستعادة CFG و CG ، على التوالي. هذا الأخير ، إنه واجهة عالية المستوى للوظائف ذات الصلة SMT Solver.
BARFgadgets هو نص Python مبني على Barf يتيح لك البحث والتصنيف والتحقق من أدوات ROP داخل برنامج ثنائي. تجد مرحلة البحث جميع ret -و jmp call الأدوات داخل الثنائي. تصنف مرحلة التصنيف الأدوات التي تم العثور عليها مسبقًا وفقًا للأنواع التالية:
يتم ذلك من خلال مضاهاة التعليمات. أخيرًا ، تتكون مرحلة التحقق من استخدام SMT Solver للتحقق من الدلالي المعينة لكل أداة في المرحلة الثانية.
usage: BARFgadgets [-h] [--version] [--bdepth BDEPTH] [--idepth IDEPTH] [-u]
[-c] [-v] [-o OUTPUT] [-t] [--sort {addr,depth}] [--color]
[--show-binary] [--show-classification] [--show-invalid]
[--summary SUMMARY] [-r {8,16,32,64}]
filename
Tool for finding, classifying and verifying ROP gadgets.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
--version Display version.
--bdepth BDEPTH Gadget depth in number of bytes.
--idepth IDEPTH Gadget depth in number of instructions.
-u, --unique Remove duplicate gadgets (in all steps).
-c, --classify Run gadgets classification.
-v, --verify Run gadgets verification (includes classification).
-o OUTPUT, --output OUTPUT
Save output to file.
-t, --time Print time of each processing step.
--sort {addr,depth} Sort gadgets by address or depth (number of
instructions) in ascending order.
--color Format gadgets with ANSI color sequences, for output
in a 256-color terminal or console.
--show-binary Show binary code for each gadget.
--show-classification
Show classification for each gadget.
--show-invalid Show invalid gadget, i.e., gadgets that were
classified but did not pass the verification process.
--summary SUMMARY Save summary to file.
-r {8,16,32,64} Filter verified gadgets by operands register size.
لمزيد من المعلومات ، راجع ReadMe.
BARFcfg هو نص Python مبني على BARF يتيح لك استرداد الرسم البياني لتدفق التحكم لبرنامج ثنائي.
usage: BARFcfg [-h] [-s SYMBOL_FILE] [-f {txt,pdf,png,dot}] [-t]
[-d OUTPUT_DIR] [-b] [--show-reil]
[--immediate-format {hex,dec}] [-a | -r RECOVER]
filename
Tool for recovering CFG of a binary.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
-s SYMBOL_FILE, --symbol-file SYMBOL_FILE
Load symbols from file.
-f {txt,pdf,png,dot}, --format {txt,pdf,png,dot}
Output format.
-t, --time Print process time.
-d OUTPUT_DIR, --output-dir OUTPUT_DIR
Output directory.
-b, --brief Brief output.
--show-reil Show REIL translation.
--immediate-format {hex,dec}
Output format.
-a, --recover-all Recover all functions.
-r RECOVER, --recover RECOVER
Recover specified functions by address (comma
separated).
BARFcg هو نص Python مبني على BARF يتيح لك استرداد الرسم البياني للمكالمات لبرنامج ثنائي.
usage: BARFcg [-h] [-s SYMBOL_FILE] [-f {pdf,png,dot}] [-t] [-a | -r RECOVER]
filename
Tool for recovering CG of a binary.
positional arguments:
filename Binary file name.
optional arguments:
-h, --help show this help message and exit
-s SYMBOL_FILE, --symbol-file SYMBOL_FILE
Load symbols from file.
-f {pdf,png,dot}, --format {pdf,png,dot}
Output format.
-t, --time Print process time.
-a, --recover-all Recover all functions.
-r RECOVER, --recover RECOVER
Recover specified functions by address (comma
separated).
Pyasmjit هي حزمة Python لتوليد رمز تجميع ARM X86_64/ARM.
تم تطوير هذه الحزمة من أجل اختبار ترجمة تعليمات BARF من x86_64/ARM إلى Reil. الفكرة الرئيسية هي أن تكون قادرًا على تشغيل أجزاء من الكود أصليًا. ثم ، تتم ترجمة الجزء نفسه إلى إعادة تنفيذها وتنفيذها في reil vm. أخيرًا ، تتم مقارنة كل من السياقين النهائيين (تلك التي تم الحصول عليها من خلال التنفيذ الأصلي والسياقين من المحاكاة) للاختلافات.
لمزيد من المعلومات ، انظر Pyasmjit.
ترخيص BSD 2-Cane. لمزيد من المعلومات ، راجع الترخيص.