-
-
[原创]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
选项优化，参考 db6K9s2c8@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 * 8score += condition_0 * 8from z3 import *# 创建求解器set_param("parallel.enable", True)set_param("dump_models", True) set_param("maxsat_engine", "core_maxsat") def Trvnc8(num): return num & 0xffdef 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 = 0for 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 * 8condition_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 & 0xffdef 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 = 0for i in range(5,55): solver.add( Or([培训]Windows内核深度攻防：从Hook技术到Rootkit实战！
最后于 2025-4-9 15:52
被vior编辑
，原因： 题目问题
|
|
|---|---|
|
|
|
