z3_and_angr_binary_analysis_workshop

แนะนำการวิเคราะห์แบบไบนารีด้วย Z3 และ Angr

จัดส่งโดย Sam Brown ที่ Steelcon และ Hack.lu 2018 นี่เป็นการประชุมเชิงปฏิบัติการสามชั่วโมงที่แนะนำผู้เข้าร่วมประชุมเพื่อใช้ Z3 และ Angr สำหรับการวิเคราะห์แบบไบนารี การประชุมเชิงปฏิบัติการให้คำแนะนำเกี่ยวกับนักแก้ปัญหา SMT, Z3 SMT Solver และ Library Python และ Framework การวิเคราะห์ไบนารี Ang

ผ่านการฝึกอบรมเชิงปฏิบัติการซึ่งมีวัตถุประสงค์เพื่อแสดงให้เห็นถึงการใช้งานที่มีศักยภาพของเทคโนโลยีเพื่อช่วยนักวิจัยด้านความปลอดภัยในการดำเนินการวิจัยด้านวิศวกรรมย้อนกลับและความเสี่ยง

สไลด์ให้คำแนะนำคร่าวๆสำหรับเนื้อหาและคำสั่งซื้อแบบฝึกหัดอะไร

ตัวอย่างและแบบฝึกหัด

Z3

ชื่อ	พิมพ์	คำอธิบาย
n ควีนส์	ตัวอย่าง	'N ควีนส์จะถูกวางลงบนกระดานหมากรุก NXN ได้อย่างไรเพื่อที่จะไม่โจมตีกันสองคน?' ใช้ Z3 เพื่อสร้างโซลูชันสำหรับกระดานหมากรุก n * n
HackVent 15	ตัวอย่าง	โซลูชันและเดินผ่านเพื่อแก้ปัญหาการแฮ็ค 15 CTF ด้วย Z3
ซูโดคุ	ออกกำลังกาย	พยายามแก้ Sudoku โดยใช้ Z3
RNG	ออกกำลังกาย	แบบฝึกหัดเสริม - การใช้ Z3 เพื่อค้นหาตัวสร้างตัวเลขสุ่มที่ไม่ปลอดภัย
x86	50/50	ตัวอย่างครึ่งหนึ่ง, ครึ่ง DIY - ใช้คำสั่ง x86 เวอร์ชัน simeplified โดยใช้ Z3
ทึบแสง	ออกกำลังกาย	ใช้คำแนะนำที่ใช้ก่อนหน้านี้เพื่อระบุภาคทึบแสงในลำดับเล็ก ๆ ของคำแนะนำการประกอบ
การตรวจสอบความเท่าเทียมกัน	ตัวอย่าง	ใช้คำแนะนำที่ใช้ก่อนหน้านี้เพื่อระบุลำดับของคำแนะนำที่เทียบเท่า

angr

ชื่อ	พิมพ์	คำอธิบาย
opaque_predicates	ตัวอย่าง	การใช้ Angr เพื่อระบุภาคทึบแสงที่มีงานน้อยกว่ามาก :)
ioctls	ตัวอย่าง	ระบุรหัส Windows Driver IOCTL โดยใช้ ANGR
สวัสดีโลก	50/50	การออกกำลังกายและคำแนะนำในการใช้ ANGR เพื่อสร้างอาร์กิวเมนต์ที่ถูกต้องสำหรับ 'การตรวจสอบคีย์ใบอนุญาต' อย่างง่าย
ห้องปฏิบัติการระเบิด	ออกกำลังกาย	แบบฝึกหัด DIY โดยใช้ Angr เพื่อแก้ 'Bomb Lab'

การตั้งค่า

รหัสทั้งหมดอยู่ใน Python3 และคุณควรติดตั้งกรอบการวิเคราะห์ไบนารี Ang

 mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr