文件名称：z3_and_angr_binary_analysis_workshop:z3 和 angr 研讨会的代码和练习
文件大小：1.36MB
文件格式：ZIP
更新时间：2024-06-20 08:22:37
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