标签：python Universe print add 2020 128 model check z3

参考文章：python z3库学习

今日做水题，发现了这么一个东西，鉴于将近一个月没更了，遂决定水一篇

Z3介绍以及使用示例

Z3 在工业应用中实际上常见于软件验证、程序分析等。然而由于功能实在强大，也被用于很多其他领域。CTF 领域来说，能够用约束求解器搞定的问题常见于密码题、二进制逆向、符号执行、Fuzzing 模糊测试等。此外，著名的二进制分析框架 angr 也内置了一个修改版的 Z3。

整型(Int)方程求解

from z3 import *

a, s, d = Ints('a s d')
x = Solver()
x.add(a-d == 18)
x.add(a+s == 12)
x.add(s-d == 20)
check = x.check()
print(check)
model = x.model()
print(model)
# sat
# [a = 5, d = -13, s = 7]

有理数(Real)型解方程求解

from z3 import *

x = Real('x')
y = Real('y')
s = Solver()
s.add(x**2 + y**2 == 3)
s.add(x**3 == 2)
check = s.check()
print(check)
model = s.model()
print(model)
# sat
# [y = -1.1885280594?, x = 1.2599210498?]

位向量(BitVec)型解方程

from z3 import *

x, y, z = BitVecs('x y z', 8)
s = Solver()
s.add(x ^ y & z == 12)
s.add(y & z >> 3 == 3)
s.add(z ^ y == 4)
check = s.check()
print(check)
model = s.model()
print(model)
# sat
# [z = 27, y = 31, x = 23]

例题

题目链接：[ACTF新生赛2020]Universe_final_answer

看到主函数以及关键函数 sub_860 部分

使用z3求解（脚本来源：HK_Mayfly）

from z3 import *

v1, v2, v3, v4, v5, v6, v7, v8, v9, v11 = BitVecs('v1 v2 v3 v4 v5 v6 v7 v8 v9 v11', 16)

l = Solver()

l.add(v1 < 128)
l.add(v2 < 128)
l.add(v3 < 128)
l.add(v4 < 128)
l.add(v5 < 128)
l.add(v6 < 128)
l.add(v7 < 128)
l.add(v8 < 128)
l.add(v9 < 128)
l.add(v11 < 128)
l.add(-85 * v9 + 58 * v8 + 97 * v6 + v7 + -45 * v5 + 84 * v4 + 95 * v2 - 20 * v1 + 12 * v3 == 12613)
l.add(
    30 * v11 + -70 * v9 + -122 * v6 + -81 * v7 + -66 * v5 + -115 * v4 + -41 * v3 + -86 * v1 - 15 * v2 - 30 * v8 == -54400)
l.add(-103 * v11 + 120 * v8 + 108 * v7 + 48 * v4 + -89 * v3 + 78 * v1 - 41 * v2 + 31 * v5 - (
            v6 << 6) - 120 * v9 == -10283)
l.add(71 * v6 + (v7 << 7) + 99 * v5 + -111 * v3 + 85 * v1 + 79 * v2 - 30 * v4 - 119 * v8 + 48 * v9 - 16 * v11 == 22855)
l.add(5 * v11 + 23 * v9 + 122 * v8 + -19 * v6 + 99 * v7 + -117 * v5 + -69 * v3 + 22 * v1 - 98 * v2 + 10 * v4 == -2944)
l.add(-54 * v11 + -23 * v8 + -82 * v3 + -85 * v2 + 124 * v1 - 11 * v4 - 8 * v5 - 60 * v7 + 95 * v6 + 100 * v9 == -2222)
l.add(-83 * v11 + -111 * v7 + -57 * v2 + 41 * v1 + 73 * v3 - 18 * v4 + 26 * v5 + 16 * v6 + 77 * v8 - 63 * v9 == -13258)
l.add(81 * v11 + -48 * v9 + 66 * v8 + -104 * v6 + -121 * v7 + 95 * v5 + 85 * v4 + 60 * v3 + -85 * v2 + 80 * v1 == -1559)
l.add(101 * v11 + -85 * v9 + 7 * v6 + 117 * v7 + -83 * v5 + -101 * v4 + 90 * v3 + -28 * v1 + 18 * v2 - v8 == 6308)
l.add(99 * v11 + -28 * v9 + 5 * v8 + 93 * v6 + -18 * v7 + -127 * v5 + 6 * v4 + -9 * v3 + -93 * v1 + 58 * v2 == -1697)

if l.check() == sat:
    print(l.model())
else:
    print ('Error')

整理得到正确输入：F0uRTy_7w@

输入拿到flag：flag{F0uRTy_7w@_42}

标签：python,Universe,print,add,2020,128,model,check,z3
来源： https://www.cnblogs.com/Moomin/p/15196596.html

本站声明： 1. iCode9 技术分享网（下文简称本站）提供的所有内容，仅供技术学习、探讨和分享；
2. 关于本站的所有留言、评论、转载及引用，纯属内容发起人的个人观点，与本站观点和立场无关；
3. 关于本站的所有言论和文字，纯属内容发起人的个人观点，与本站观点和立场无关；
4. 本站文章均是网友提供，不完全保证技术分享内容的完整性、准确性、时效性、风险性和版权归属；如您发现该文章侵犯了您的权益，可联系我们第一时间进行删除；
5. 本站为非盈利性的个人网站，所有内容不会用来进行牟利，也不会利用任何形式的广告来间接获益，纯粹是为了广大技术爱好者提供技术内容和技术思想的分享性交流网站。