z3_and_angr_binary_analysis_workshop

Intro ke analisis biner dengan Z3 dan ANGR

Awalnya dikirim oleh Sam Brown di Steelcon dan Hack.lu 2018, ini adalah lokakarya tiga jam yang memperkenalkan peserta untuk menggunakan Z3 dan Anggr untuk analisis biner. Lokakarya ini memberikan pengantar untuk pemecah SMT, pemecah Z3 SMT dan perpustakaan Python -nya dan kerangka analisis biner Anggr.

Melalui latihan lokakarya disediakan yang bertujuan untuk menunjukkan aplikasi teknologi potensial untuk membantu peneliti keamanan dalam melakukan penelitian rekayasa terbalik dan kerentanan.

Slide memberikan panduan kasar untuk konten dan urutan apa untuk mencoba latihan.

Contoh dan latihan

Z3

Nama	Jenis	Keterangan
N Queens	Contoh	'Bagaimana N Queens dapat ditempatkan di papan catur NXN sehingga tidak ada dua dari mereka yang saling menyerang?' Menggunakan Z3 untuk menghasilkan solusi untuk papan catur n * n
Hackvent 15	Contoh	Solusi dan berjalan melalui untuk menyelesaikan tantangan Hackvent 15 CTF dengan Z3
Sudoku	Latihan	Coba selesaikan Sudoku menggunakan Z3
Rng	Latihan	Latihan Opsional - Menggunakan Z3 untuk menemukan nilai benih nomor acak yang tidak aman secara kripografis
x86	50/50	Setengah contoh, setengah DIY - Menerapkan Versi Simiplified dari Instruksi X86 Menggunakan Z3
Predikat buram	Latihan	Gunakan instruksi yang diimplementasikan sebelumnya untuk mengidentifikasi predikat buram dalam urutan kecil instruksi perakitan
Pemeriksaan Kesetaraan	Contoh	Gunakan instruksi yang diimplementasikan sebelumnya untuk mengidentifikasi urutan instruksi yang setara

Anggr

Nama	Jenis	Keterangan
OPAQUE_PREDICATES	Contoh	Menggunakan ANGR untuk mengidentifikasi predikat buram dengan pekerjaan yang jauh lebih sedikit :)
Ioctls	Contoh	Identifikasi kode IOCTL driver windows menggunakan ANGR
Halo dunia	50/50	Latihan dan Walkthrough Menggunakan ANGR untuk menghasilkan argumen yang valid untuk 'validator kunci lisensi' sederhana
Lab bom	Latihan	Latihan DIY menggunakan ANGR untuk menyelesaikan 'lab bom'

Pengaturan

Semua kode ada di Python3 dan Anda hanya perlu menginstal kerangka analisis biner ANGR.

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