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
