CTF对抗-Z3 优化，解题技巧 PlainCTF 2025 prospector 题解

prospector part2

Plainctf prospector 题目出了一个大型的约束求解题目，当时做了一天没做出来。事后发现当时 dump 的约束没啥问题，主要是栽在了 z3 一些特性和使用技巧上面，偷学了别人的一些方法，在这里简单记录一下
题目本身没什么难点，需要留意一个小坑就没啥了
图片描述

精度问题

题目是 arm64，运算都用的是 W0-W30 的 32 位寄存器。虽然输入是 8 位但是部分运算结果可能会超过 8 bit
但 z3 的运算精度应该是取运算中最高的未知量也就是设置数值。这就导致了中间可能会有部分运算不对，应该设置变量为更高的 16 bit 或者 32 bit 再在需要截断的时候 0xff

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])  ))

Z3 Optimize 优化

选项优化，参考 a95K9s2c8@1M7s2y4Q4x3@1q4Q4x3V1k6Q4x3V1k6E0K9h3y4J5L8%4y4G2k6Y4c8Q4x3X3g2Y4K9i4c8Z5N6h3u0Q4x3X3g2A6L8#2)9J5c8Y4Z5K6k6%4g2A6k6r3g2Q4x3V1k6H3M7X3!0Y4M7X3q4E0L8h3W2F1k6#2)9J5c8W2m8S2M7X3q4E0k6i4c8W2M7Y4y4Q4x3V1j5`.

set_param("parallel.enable", True)
set_param("dump_models", True)  
set_param("maxsat_engine", "core_maxsat")  

显示求解过程内容（只能用于 Optimize）

def on_model(m):
    print(m.eval(score), bytes(m[c].as_long() for c in flag))
 
solver.set_on_model(on_model)

添加条件权重 add_soft

1	`solver.add_soft(condition_70,` `6)`

自动化简 simplify

1	`solver.add_soft(simplify(condition_143),` `5)`

如果提前知道 flag 格式，可以对字符限制更多一些，会更快

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
    ))    

使用条件 * 数值比 If(con, addnum, 0) 要简单一点

1	`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)]
 
# 初始分数为0
score = 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("无解或超时")

解题脚本在附件

最后于 4小时前被vior编辑，原因：题目问题

更多【CTF对抗-Z3 优化，解题技巧 PlainCTF 2025 prospector 题解】相关视频教程：www.yxfzedu.com

CTF对抗-Z3 优化，解题技巧 PlainCTF 2025 prospector 题解

prospector part2

精度问题

Z3 Optimize 优化

相关文章推荐

Markdown Editor

友情链接

课程目录

技术交流QQ群