-
-
[原创]Z3 优化，解题技巧 PlainCTF 2025 prospector 题解
-
发表于: 2025-4-9 15:51
-
Plainctf prospector 题目出了一个大型的约束求解题目，当时做了一天没做出来。事后发现当时 dump 的约束没啥问题，主要是栽在了 z3 一些特性和使用技巧上面，偷学了别人的一些方法，在这里简单记录一下
题目本身没什么难点，需要留意一个小坑就没啥了
题目是 arm64，运算都用的是 W0-W30 的 32 位寄存器。虽然输入是 8 位但是部分运算结果可能会超过 8 bit
但 z3 的运算精度应该是取运算中最高的未知量也就是设置数值。这就导致了中间可能会有部分运算不对，应该设置变量为更高的 16 bit 或者 32 bit 再在需要截断的时候 0xff
选项优化，参考 7a0K9s2c8@1M7s2y4Q4x3@1q4Q4x3V1k6Q4x3V1k6E0K9h3y4J5L8%4y4G2k6Y4c8Q4x3X3g2Y4K9i4c8Z5N6h3u0Q4x3X3g2A6L8#2)9J5c8Y4Z5K6k6%4g2A6k6r3g2Q4x3V1k6H3M7X3!0Y4M7X3q4E0L8h3W2F1k6#2)9J5c8W2m8S2M7X3q4E0k6i4c8W2M7Y4y4Q4x3V1j5`.
显示求解过程内容（只能用于 Optimize）
添加条件权重 add_soft
自动化简 simplify
如果提前知道 flag 格式，可以对字符限制更多一些，会更快
使用条件 * 数值比 If(con, addnum, 0) 要简单一点
总体脚本片段
解题脚本在附件
flag = [BitVec(f'flag_{i}', 16) for i in range(56)]
def Trvnc8(num):
return num & 0xff
condition_0 = And(( ((flag[3] + flag[26]) & flag[32]) < Trvnc8(flag[9] + flag[25] - flag[28]), ((flag[15] - flag[16]) & flag[18]) <= 0x26, Trvnc8(flag[14] + flag[23] * flag[2]) < Trvnc8((flag[24] + flag[25]) * flag[26]) ))
flag = [BitVec(f'flag_{i}', 16) for i in range(56)]
def Trvnc8(num):
return num & 0xff
condition_0 = And(( ((flag[3] + flag[26]) & flag[32]) < Trvnc8(flag[9] + flag[25] - flag[28]), ((flag[15] - flag[16]) & flag[18]) <= 0x26, Trvnc8(flag[14] + flag[23] * flag[2]) < Trvnc8((flag[24] + flag[25]) * flag[26]) ))
set_param("parallel.enable", True)
set_param("dump_models", True)
set_param("maxsat_engine", "core_maxsat")
set_param("parallel.enable", True)
set_param("dump_models", True)
set_param("maxsat_engine", "core_maxsat")
def on_model(m):
print(m.eval(score), bytes(m[c].as_long() for c in flag))
solver.set_on_model(on_model)def on_model(m):
print(m.eval(score), bytes(m[c].as_long() for c in flag))
solver.set_on_model(on_model)solver.add_soft(condition_70, 6)
solver.add_soft(condition_70, 6)
solver.add_soft(simplify(condition_143), 5)
solver.add_soft(simplify(condition_143), 5)
for i in range(5,55):
solver.add( Or(
And(flag[i] >= ord('0'), flag[i] <= ord('9')), # 0-9
And(flag[i] >= ord('a'), flag[i] <= ord('f')) # a-f
))
for i in range(5,55):
solver.add( Or(
And(flag[i] >= ord('0'), flag[i] <= ord('9')), # 0-9
And(flag[i] >= ord('a'), flag[i] <= ord('f')) # a-f
))
score += condition_0 * 8
score += condition_0 * 8
from z3 import *
# 创建求解器set_param("parallel.enable", True)
set_param("dump_models", True)
set_param("maxsat_engine", "core_maxsat")
def Trvnc8(num):
return num & 0xff
def on_model(m):
print(m.eval(score), bytes(m[c].as_long() for c in flag))
solver = Optimize()
solver.set_on_model(on_model)flag = [BitVec(f'flag_{i}', 16) for i in range(56)]
# 初始分数为0score = 0
for i in range(5,55):
solver.add( Or(
And(flag[i] >= ord('0'), flag[i] <= ord('9')), # 0-9
And(flag[i] >= ord('a'), flag[i] <= ord('f')) # a-f
))
condition_vars = []
condition_0 = And(( ((flag[3] + flag[26]) & flag[32]) < Trvnc8(flag[9] + flag[25] - flag[28]), ((flag[15] - flag[16]) & flag[18]) <= 0x26, Trvnc8(flag[14] + flag[23] * flag[2]) < Trvnc8((flag[24] + flag[25]) * flag[26]) ))
solver.add_soft(condition_0, 8)
score += condition_0 * 8
condition_1 = And(( Trvnc8(flag[2] * flag[37] - flag[43]) <= 0xC7, Trvnc8(flag[47] - flag[41] + flag[11]) >= 0x3D, Trvnc8(flag[49] + flag[33] - flag[5]) >= 0x4D, (Trvnc8(flag[13] * flag[46]) ^ flag[10]) > Trvnc8(flag[23] - (flag[8] + flag[46])) ))
solver.add_soft(condition_1, 1)
score += condition_1 * 1
...condition_399 = And(( Trvnc8((flag[35] | flag[13]) + flag[20]) < Trvnc8(flag[45] + flag[19] - flag[48]), (Trvnc8(flag[41] * flag[12]) | flag[34]) >= 0x7C ))
solver.add_soft(condition_399, 4)
score += condition_399 * 4
# 设置求解超时时间solver.add(flag[0] == ord('P'))
solver.add(flag[1] == ord('C'))
solver.add(flag[2] == ord('T'))
solver.add(flag[3] == ord('F'))
solver.add(flag[4] == ord('{'))
solver.add(flag[55] == ord('}'))
score = simplify(score)
solver.maximize(score)# 最终检查if solver.check() == sat:
model = solver.model()
flag_str = ""
for i in flag:
print(model.eval(i, model_completion=True), end=' ')
flag_str += chr(model.eval(i, model_completion=True).as_long())
print(f"找到解: {flag_str}")
print(f"最终分数: {score}")
else:
model = solver.model()
# qwq = [model.evaluate() for i in range(56)]
# print(qwq)
flag_str = ""
for i in flag:
print(model.eval(i, model_completion=True), end=' ')
flag_str += chr(model.eval(i, model_completion=True).as_long())
# flag_values = [model.evaluate(qwq).as_long() for i in range(56)]
# flag_str = ''.join(chr(c) for c in flag_values if 32 <= c <= 126)
print(f"找到解: {flag_str}")
print(f"最终分数: {score}")
print("无解或超时")
from z3 import *
# 创建求解器set_param("parallel.enable", True)
set_param("dump_models", True)
set_param("maxsat_engine", "core_maxsat")
def Trvnc8(num):
return num & 0xff
def on_model(m):
print(m.eval(score), bytes(m[c].as_long() for c in flag))
solver = Optimize()
solver.set_on_model(on_model)flag = [BitVec(f'flag_{i}', 16) for i in range(56)]
# 初始分数为0score = 0
for i in range(5,55):
solver.add( Or(
[培训]内核驱动高级班，冲击BAT一流互联网大厂工作，每周日13:00-18:00直播授课
最后于 2025-4-9 15:52
被vior编辑
，原因： 题目问题
|
|
|---|---|
|
|
|
