z3介绍
Z3 是一个微软出品的开源约束求解器,能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题,功能强大且易于使用,常用于解决CTF当中的密码题或逆向题,Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大,也被用于很多其他领域。CTF 领域来说,能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外,著名的二进制分析框架 angr 也内置了一个修改版的 Z3。
z3安装
由于os下安装失败了,所以我在我的虚拟机ubuntu16.04下安装
千万不要用pip install z3或者pip install z3-solver来安装,会发现使用不了
用源码安装就很舒服
1 | #创建一个用于z3的虚拟python环境 |
z3的使用
1 | (z3) ☁ exp bpython |
z3 in CTF
这里我们拿angr的一道例题简单练练手
题目逻辑很简单,就是输入一个key,然后通过4个校验就输出correct,否则wrong
直接上脚本:
1 | from z3 import * |
以后做到其他逆向题的时候再深入研究
参考文章: