barf project
1.0.0
การวิเคราะห์รหัสไบนารีเป็นกิจกรรมที่สำคัญในหลาย ๆ ด้านของสาขาวิทยาศาสตร์คอมพิวเตอร์และสาขาวิชาวิศวกรรมซอฟต์แวร์ตั้งแต่ความปลอดภัยของซอฟต์แวร์และการวิเคราะห์โปรแกรมไปจนถึงวิศวกรรมย้อนกลับ การวิเคราะห์ไบนารีด้วยตนเองเป็นงานที่ยากและใช้เวลานานและมีเครื่องมือซอฟต์แวร์ที่พยายามทำให้นักวิเคราะห์มนุษย์เป็นอัตโนมัติหรือช่วยเหลือนักวิเคราะห์มนุษย์ อย่างไรก็ตามเครื่องมือเหล่านี้ส่วนใหญ่มีข้อ จำกัด ด้านเทคนิคและเชิงพาณิชย์หลายประการที่ จำกัด การเข้าถึงและการใช้งานโดยชุมชนวิชาการและผู้ปฏิบัติงานส่วนใหญ่ BARF เป็นกรอบการวิเคราะห์ไบนารีโอเพ่นซอร์สที่มีจุดมุ่งหมายเพื่อสนับสนุนงานการวิเคราะห์รหัสไบนารีที่หลากหลายซึ่งเป็นเรื่องธรรมดาในวินัยความปลอดภัยของข้อมูล มันเป็นแพลตฟอร์มสคริปต์ที่รองรับการยกคำสั่งจากสถาปัตยกรรมที่หลากหลายการแปลแบบไบนารีไปยังการเป็นตัวแทนระดับกลางซึ่งเป็นเฟรมเวิร์กที่ขยายได้สำหรับปลั๊กอินการวิเคราะห์รหัสและการทำงานร่วมกันด้วยเครื่องมือภายนอกเช่น debuggers นักแก้ปัญหา SMT และเครื่องมือเครื่องมือ เฟรมเวิร์กได้รับการออกแบบมาเป็นหลักสำหรับการวิเคราะห์ที่มีความช่วยเหลือจากมนุษย์ แต่สามารถเป็นไปโดยอัตโนมัติได้อย่างสมบูรณ์
โครงการ BARF รวมถึง BARF และเครื่องมือและแพ็คเกจที่เกี่ยวข้อง จนถึงตอนนี้โครงการประกอบด้วยรายการต่อไปนี้:
สำหรับข้อมูลเพิ่มเติมโปรดดู:
สถานะปัจจุบัน:
| รุ่นล่าสุด | v0.6.0 |
|---|---|
| url | 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 --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 register หลังจากดำเนินการรหัส
ก่อนอื่นเราเพิ่มคำแนะนำลงในส่วนประกอบวิเคราะห์
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!" )คุณสามารถดูตัวอย่างเหล่านี้และเพิ่มเติมได้ในไดเรกทอรีตัวอย่าง
เฟรมเวิร์กถูกแบ่งออกเป็นสามองค์ประกอบหลัก: แกน , ซุ้มประตู และ การวิเคราะห์
ส่วนประกอบนี้มีโมดูลที่จำเป็น:
REIL : ให้คำจำกัดความสำหรับภาษา Reil นอกจากนี้ยังใช้ เครื่องจำลอง และ ตัวแยกวิเคราะห์SMT : ให้วิธีการเชื่อมต่อกับ Z3 และ CVC4 SMT Solver นอกจากนี้ยังมีฟังก์ชั่นการแปลคำแนะนำของ Reil เป็นนิพจน์ SMTBI : โมดูล อินเตอร์เฟสไบนารี มีหน้าที่ในการโหลดไฟล์ไบนารีสำหรับการประมวลผล (ใช้ pefile และ pyelftools) สถาปัตยกรรมที่ได้รับการสนับสนุนแต่ละรายการนั้นมีให้เป็นองค์ประกอบย่อยซึ่งมีโมดูลต่อไปนี้
Architecture : อธิบายถึงสถาปัตยกรรมเช่นการลงทะเบียนขนาดที่อยู่หน่วยความจำTranslator : ให้นักแปลเพื่อ reil สำหรับคำสั่งที่รองรับแต่ละคำแนะนำDisassembler : ให้ฟังก์ชันการแยกชิ้นส่วน (ใช้ capstone)Parser : แปลงคำสั่งจากสตริงเป็นรูปแบบวัตถุ จนถึงตอนนี้ส่วนประกอบนี้ประกอบด้วยโมดูล: กราฟการควบคุมการไหล กราฟโทร และ ตัววิเคราะห์รหัส สองคนแรกให้ฟังก์ชั่นสำหรับการกู้คืน CFG และ CG ตามลำดับ หลังมันเป็นอินเทอร์เฟซระดับสูงกับฟังก์ชั่นที่เกี่ยวข้องกับ SMT Solver
BARFgadgets เป็นสคริปต์ Python ที่สร้างขึ้นบน BARF ที่ให้คุณ ค้นหา classifiy และ ตรวจสอบ อุปกรณ์ ROP ภายในโปรแกรมไบนารี ขั้นตอน การค้นหา พบ ret ทั้งหมด -, jmp -และ call แกดเจ็ตที่จบลงภายในไบนารี ขั้นตอน การจำแนกประเภท การจำแนกอุปกรณ์ก่อนหน้านี้พบแกดเจ็ตตามประเภทต่อไปนี้:
สิ่งนี้ทำผ่านการจำลองการเรียนการสอน ในที่สุดขั้นตอน การตรวจสอบ ประกอบด้วยการใช้ตัวแก้ SMT เพื่อตรวจสอบความหมายที่กำหนดให้กับแกดเจ็ตแต่ละตัวในขั้นตอนที่สอง
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 สำหรับการสร้างรหัสและการดำเนินการชุดประกอบ X86_64/ARM
แพ็คเกจนี้ได้รับการพัฒนาเพื่อทดสอบการแปลคำสั่ง BARF จาก X86_64/ARM เป็น Reil แนวคิดหลักคือการสามารถเรียกใช้ชิ้นส่วนของรหัสโดยธรรมชาติ จากนั้นชิ้นส่วนเดียวกันจะถูกแปลเป็น Reil และดำเนินการใน Reil VM ในที่สุดบริบทสุดท้ายทั้งสอง (อันที่ได้จากการดำเนินการดั้งเดิมและอีกบริบทจากการจำลอง) จะเปรียบเทียบความแตกต่าง
สำหรับข้อมูลเพิ่มเติมดู Pyasmjit
ใบอนุญาต BSD 2 ข้อ สำหรับข้อมูลเพิ่มเติมดูใบอนุญาต
