使用python z3约束解ctf题目 练手
题目文件：ida反编译查看
分析可知就是将命令行的第二个参数的前7个字符的ascii码相加等于801
那么怎么构造这7个字符呢，我们使用z3约束器
from z3 import *
s = Solver()
pwd =
for i in pwd:
s.add(0x30<i)
s.add(i<120)#设置7个字符的取值范围在48<120之间
s.add(pwd+pwd+pwd+pwd+pwd+pwd+pwd==801) #且相加为801
if s.check() == sat:
print s.model()
其实有很多解，这里只打印了一组
转成字符就是wwwwwwW
学习完z3库，教一下作业
```python
#!/usr/bin/env python
# -*- coding: utf-8 -*-
from z3 import *
# 创建约束解析器
solver = Solver()
# 定义变量
m1 = Int('m1')
m2 = Int('m2')
m3 = Int('m3')
m4 = Int('m4')
m5 = Int('m5')
m6 = Int('m6')
m7 = Int('m7')
# 添加约束条件
# 参数前7个ascii等于0x321
solver.add(m1+m2+m3+m4+m5+m6+m7==0x321)
# 约束每个解的范围都是在可见字符串
solver.add(32<=m1)
solver.add(m1<127)
solver.add(32<=m2)
solver.add(m2<127)
solver.add(32<=m3)
solver.add(m3<127)
solver.add(32<=m4)
solver.add(m4<127)
solver.add(32<=m5)
solver.add(m5<127)
solver.add(32<=m6)
solver.add(m6<127)
solver.add(32<=m7)
solver.add(m7<127)
if solver.check() == sat:
flag = solver.model()
print(flag)
else:
print("no answer")
```
s.add(0x30<i)
s.add(i<120)#设置7个字符的取值范围在48<120之间
为什么取值是这个范围 厉害厉害学习了 谢谢分享。学习的好资料 谢谢分享。学习一下 为什么我运行python程序提示Solver未知，Int未知 我学到了网络爬虫抓取，要考网络工程师了，暂时放下，待我来日慢慢虐它~ 厉害 学习了 学习的好资料 zysanjing1 发表于 2019-3-7 22:40
为什么我运行python程序提示Solver未知，Int未知
检查下python版本 好厉害我记得有一道题 也是 关于这个的 我没有写出来 ~~~~~ 谢谢楼主