z3_and_angr_binary_analysis_workshop
1.0.0
最初是由Sam Brown在Steelcon和Hack.lu 2018上交付的，這是一個三個小時的研討會，介紹了與會者使用Z3和ANGR進行二進制分析。該研討會為SMT求解器，Z3 SMT求解器及其Python庫和ANGR二進制分析框架提供了簡介。
提供了講習班練習，旨在展示該技術的潛在應用，以幫助安全研究人員進行反向工程和脆弱性研究。
幻燈片為內容提供了粗略的指南，以及什麼順序嘗試進行練習。
| 姓名 | 類型 | 描述 |
|---|---|---|
| n皇后 | 例子 | “如何將N皇后放在NXN棋盤上，以便沒有兩個皇后相互攻擊？”使用Z3生成N * n棋盤的解決方案 |
| 黑客15 | 例子 | 解決方案並穿過Z3的黑客15 CTF挑戰 |
| Sudoku | 鍛煉 | 嘗試使用Z3解決Sudoku |
| RNG | 鍛煉 | 可選練習 - 使用Z3查找非晶格安全的隨機數發生器種子價值 |
| x86 | 50/50 | 一半示例，一半DIY-使用Z3實現X86指令的模擬版本 |
| 不透明的謂詞 | 鍛煉 | 使用先前實施的說明來識別小組指示序列中的不透明謂詞 |
| 等價檢查 | 例子 | 使用先前實施的指令來識別同等的指令序列 |
| 姓名 | 類型 | 描述 |
|---|---|---|
| opaque_predicates | 例子 | 使用ANGR來識別工作更少的不透明謂詞:) |
| ioctls | 例子 | 使用ANGR識別Windows驅動程序IOCTL代碼 |
| 你好世界 | 50/50 | 練習和演練使用ANGR為簡單的“許可證密鑰驗證器”生成有效的論點 |
| 炸彈實驗室 | 鍛煉 | 使用ANGR解決“炸彈實驗室”的DIY練習 |
所有代碼都在Python3中，您只需要安裝ANGR二進制分析框架即可。
mkvirtualenv --python=$(which python3) angr && python -m pip install angr
workon angr
