SBA: กรอบการวิเคราะห์ไบนารีแบบคงที่
กรอบการวิเคราะห์ไบนารีแบบคงที่ควรทำอย่างไร?
- ลดความพยายามในการดำเนินการสำหรับการวิเคราะห์รายบุคคล
- มีเพียง 250 LOCs ใน C ++ ที่จะใช้การวิเคราะห์เพื่อตรวจสอบคุณสมบัติของฟังก์ชั่น
- กำหนดค่าได้สูง
- เฟรมเวิร์กตามการตีความเชิงนามธรรมที่ช่วยให้ผู้ใช้สามารถกำหนดโดเมนนามธรรมและกำหนดค่าการประเมินผลการเรียนการสอน
- เหตุผลและเหตุผลที่แม่นยำเกี่ยวกับหน่วยความจำสแต็ก
- โมเดลหน่วยความจำสแต็กที่ระดับความละเอียดของไบต์และเสียงและการประมาณที่มีประสิทธิภาพสำหรับการอัปเดตที่ไม่แน่นอนบนสแต็ก
- สถาปัตยกรรม
- การวิเคราะห์ decouple จากเฉพาะสถาปัตยกรรมเช่นภาษาแอสเซมบลีและข้อกำหนด ABI
เริ่มต้น
การพึ่งพาอาศัยกัน
sudo apt-get install g++ ocaml camlp4-extra camlp4 tar cmake make
สร้าง SBA
mkdir build && cd build
cmake .. && make -j4
แอปพลิเคชัน
การวิเคราะห์ตารางกระโดด
ในการวิเคราะห์วัตถุไบนารี ~/obj ให้ใช้คำสั่งต่อไปนี้:
./jump_table x86_64.auto ~/obj
โดยค่าเริ่มต้น SBA สร้างไฟล์ชั่วคราวและผลลัพธ์ผลลัพธ์ใน /tmp/sba/ เส้นทางเหล่านี้สามารถระบุได้โดยใช้ -d และ -o ดังนี้:
./jump_table -d /tmp/sba/ -o /tmp/sba/result x86_64.auto ~/obj
สิ่งพิมพ์
SBA ได้มีส่วนร่วมอย่างมีนัยสำคัญในการดำเนินงานต่อไปนี้:
- การวิเคราะห์ตารางการกระโดดที่ปรับขนาดได้เสียงและแม่นยำ ISSTA 2024
- การถอดชิ้นส่วนที่ซับซ้อนของไบนารีที่ซับซ้อนโดยไม่ต้องใช้ข้อมูลเมตาคอมไพเลอร์ Asplos 2023
- ปลอดภัยกว่า: เครื่องมือไบนารีที่มีประสิทธิภาพและทนต่อข้อผิดพลาด USENIX 2023
- การสุ่มรหัสไบนารีแบบละเอียดเชิงปฏิบัติ ACSAC 2020
