【文件属性】：
文件名称：z3_and_angr_binary_analysis_workshop:z3 和 angr 研讨会的代码和练习
文件大小：1.36MB
文件格式：ZIP
更新时间：2021-05-31 14:35:57
workshop reverse-engineering z3 binary-analysis smt-solver
使用 Z3 和 angr 进行二元分析介绍
该研讨会最初由Sam Brown在Steelcon和hack.lu 2018上发布，为期3小时，向与会者介绍如何使用Z3和angr进行二进制分析。 研讨会介绍了 SMT 求解器、Z3 SMT 求解器及其 Python 库和 angr 二进制分析框架。
在整个研讨会期间提供了练习，旨在展示该技术的潜在应用，以帮助安全研究人员进行逆向工程和漏洞研究。
幻灯片提供了内容的粗略指南以及尝试练习的顺序。
例子和练习
Z3
名称
类型
描述
例子
“如何将 N 个皇后放在 NxN 棋盘上，这样它们中的两个就不会互相攻击？” 使用 Z3 生成 N * N 棋盘的解决方案
例子
使用 Z3 解决 Hackvent 15 CTF 挑战的解决方案和演练
锻炼
尝试使用Z3解决数独
锻炼
可选练习 - 使用 Z3 查找非加密安全的随机数生成器种子值
50/5