Z3简单介绍

2025年05月18日

Z3 是什么

Z3 是一个微软出品的开源约束求解器，能够解决很多种情况下的给定部分约束条件寻求一组满足条件的解的问题（可以简单理解为解方程的感觉，虽然这么比喻其实还差距甚远，请勿吐槽），功能强大且易于使用，本文以近期的 CTF 题为实例，向尚未接触过约束求解器的小伙伴们介绍 Z3 在 CTF 解题中的应用。

Z3 约束求解器是针对 Satisfiability modulo theories Problem 的一种通用求解器。所谓 SMT 问题，在 Z3 环境下是指关于算术、位运算、数组等背景理论的一阶逻辑组合决定性问题。虽然 Z3 功能强大，但是从理论上来说，大部分 SMT 问题的时间复杂度都过高，根本不可能在有限时间内解决。所以千万不要把 Z3 想象得过于万能。

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

Z3 本身提供一个类似于 Lisp 的内置语言，但是实际使用中，一般使用 Python Binding 操作会比较方便。

Z3 入门

Z3 内置了多种变量类型，基本能覆盖常见计算机数据结构。包括整数、浮点数、BitVector、数组等。

先来一个简单的例子看一下 Z3 能做什么：

from z3 import *

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

上面的例子中，定义了两个变量：x 和 y。类型为 Int（注意这里的 Int 可不是 C/C++ 里面包含上下界的 int，Z3 中的 Int 对应的就是数学中的整数，Z3 中的 BitVector 才对应到 C/C++ 中的 int）。

然后就调用了 solve 函数求解三个条件下的满足模型，这三个条件分别是 x 大于 2，y 小于 10，并且 x 加 2 个 y 等于 7。

运行一下结果：

$ python example.py 
[y = 0, x = 7]

可以看出，Z3 找到了 y=0，x=7 这组解。但是 x=5,y=1 也符合条件，却没有显示，原因是 Z3 在默认情况下，只寻找满足所有条件的一组解，而不是找出所有解。

如果想要找出多组解，则需排除之前求得的解：

from z3 import *

x = Int('x')
y = Int('y')

# 定义约束条件
constraints = [x > 2, y < 10, x + 2*y == 7]

# 创建 solver
s = Solver()
s.add(constraints)

# 循环查找所有解
while s.check() == sat:
    m = s.model()
    print(m)
    
    # 构造一个新的约束，排除当前的解
    block = []
    for var in [x, y]:
        block.append(var != m[var])
    
    # 添加新约束到 solver 中
    s.add(Or(block))

关于 Z3 的更多使用细节，可以看这两篇文章：

例题

BYUCTF 2025 Rev LLIR

下载附件发现是 .ll 文件，主函数如下

; Function Attrs: noinline nounwind optnone uwtable
define dso_local i32 @main() #0 {
  %1 = alloca i32, align 4
  %2 = alloca [64 x i8], align 16
  store i32 0, ptr %1, align 4
  %3 = call i32 (ptr, ...) @printf(ptr noundef @.str.1)
  %4 = call i32 (ptr, ...) @printf(ptr noundef @.str.2)
  %5 = call i32 (ptr, ...) @printf(ptr noundef @.str.3)
  %6 = getelementptr inbounds [64 x i8], ptr %2, i64 0, i64 0
  %7 = load ptr, ptr @stdin, align 8
  %8 = call ptr @fgets(ptr noundef %6, i32 noundef 64, ptr noundef %7)
  %9 = getelementptr inbounds [64 x i8], ptr %2, i64 0, i64 0
  %10 = call i32 @checker_i_hardly_know_her(ptr noundef %9)
  %11 = icmp ne i32 %10, 0
  br i1 %11, label %12, label %14

12:                                               ; preds = %0
  %13 = call i32 (ptr, ...) @printf(ptr noundef @.str.4)
  store i32 0, ptr %1, align 4
  br label %16

14:                                               ; preds = %0
  %15 = call i32 (ptr, ...) @printf(ptr noundef @.str.5)
  store i32 1, ptr %1, align 4
  br label %16

16:                                               ; preds = %14, %12
  %17 = load i32, ptr %1, align 4
  ret i32 %17
}

简单分析，可以发现主函数调用了 @checker_i_hardly_know_her 函数

这个函数有三四百行，但是分析的话就可以发现这是一系列约束条件，用 C 语言表示的话就像下面：

// 核心校验函数（对应 LLVM 中的 @checker_i_hardly_know_her 函数）
int checker_i_hardly_know_her(char *input) {
    // 1. 前缀检查（对应 LLVM IR 中的 %166-%168 调用）
    if(strncmp(input, flag_prefix, 6) != 0) return 0; // call i32 @strncmp(...)

    // 2. 固定字符检查（对应 %143-%147 和 %149-%153）
    if(input[6] != '{') return 0;  // %151 = load i8, ptr %150 (position 6)
    if(input[36] != '}') return 0; // %145 = load i8, ptr %144 (position 36)

    // 3. 字符关联检查（对应 LLVM IR 中的 %3-%340 分支逻辑）
    // 每个条件对应一组 ICMP EQ 指令和分支判断
    // 这里 AI 漏了 %12 的部分，后面解密脚本我添加回来了
    if(input[4]  != input[14]) return 0;  // %5 vs %9 (position 4 vs 14)
    if(input[17] != input[23]) return 0;  // %19 vs %29 (position 17 vs 23)
    if(input[23] != input[25]) return 0;  // %29 vs %39 (position 23 vs 25)
    if(input[9]  != input[20]) return 0;  // %45 vs %49 (position 9 vs 20)
    if(input[10] != input[18]) return 0;  // %55 vs %59 (position 10 vs 18)
    if(input[11] != input[15]) return 0;  // %65 vs %69 (position 11 vs 15)
    if(input[15] != input[24]) return 0;  // %69 vs %79 (position 15 vs 24)
    if(input[24] != input[31]) return 0;  // %79 vs %89 (position 24 vs 31)
    if(input[31] != input[27]) return 0;  // %89 vs %99 (position 31 vs 27)
    if(input[13] != input[26]) return 0;  // %105 vs %109 (position 13 vs 26)
    if(input[16] != input[29]) return 0;  // %115 vs %119 (position 16 vs 29)
    if(input[19] != input[28]) return 0;  // %125 vs %130 (position 19 vs 28)
    if(input[28] != input[32]) return 0;  // %135 vs %140 (position 28 vs 32)

    // 4. 数值关系检查（对应 LLVM IR 中的数学运算逻辑）
    // 包含符号扩展(sext)和算术运算
    if(input[8]  != input[7] - 32) return 0; // %157 vs %162-32 (ASCII大小写转换)
    if(input[9] + input[20] != input[31] + 3) return 0; // %173+%177 vs %182+3
    if(input[0] - 3 != input[31] + 3) return 0; // %194 = %189+3 的逆向计算
    if(input[7] + 6 != input[10]) return 0;   // %204+6 vs %200
    if(input[9] + 27 != input[8]) return 0;   // %215+27 vs %211
    if(input[12] != input[13] - 1) return 0;  // %221 vs %225-1
    if(input[13] != input[10] - 3) return 0;  // %225 vs %236-3
    if(input[10] != input[16] - 1) return 0;  // %236 vs %247-1
    if(input[16] != input[14] - 1) return 0;  // %247 vs %258-1

    // 5. 多级依赖检查（对应 %263-%339 的复杂链式依赖）
    if(input[35] != input[5] + 2) return 0;   // %265 vs %270-2
    if(input[5]  != input[21] - 2) return 0;  // %269 vs %280-2
    if(input[21] != input[22] - 1) return 0;  // %279 vs %290-1
    if(input[22] != input[28] * 2) return 0;  // %289 vs %302*2
    if(input[33] != input[32] + 1) return 0;  // %308 vs %312+1
    if(input[34] != input[32] + 4) return 0;  // %324 vs %319+4+3
    if(input[30] != input[7] + 1) return 0;   // %331 vs %336+1

    return 1;
}

这些约束条件就像方程一样，虽然人脑也可以算，但是速度不行，而且会累死人

根据上面的内容写出的解密脚本如下：

from z3 import *  
  
  
def solve_flag():  
    s = Solver()  
   
    flag_len = 37  
    ch = [BitVec(f'c{i}', 8) for i in range(flag_len)]  

	# 确保都是可打印字符
    for c in ch:  
        s.add(c >= 32, c <= 126)  
  
    # 固定前缀 "byuctf"    
    prefix = b'byuctf'  
    for i, val in enumerate(prefix):  
        s.add(ch[i] == val)  
  
    # 固定特殊字符  
    s.add(ch[6] == ord('{'))  # '{'  
    s.add(ch[36] == ord('}'))  # '}'  
  
    # 字符相等性约束  
    s.add(ch[4] == ch[14])  
    s.add(ch[14] == ch[17])  # 这个就是漏掉的条件
    s.add(ch[17] == ch[23])  
    s.add(ch[23] == ch[25])  
    s.add(ch[9] == ch[20])  
    s.add(ch[10] == ch[18])  
    s.add(ch[11] == ch[15])  
    s.add(ch[15] == ch[24])  
    s.add(ch[24] == ch[31])  
    s.add(ch[31] == ch[27])  
    s.add(ch[13] == ch[26])  
    s.add(ch[16] == ch[29])  
    s.add(ch[19] == ch[28])  
    s.add(ch[28] == ch[32])  
  
    # 数值关系约束  
    s.add(ch[0] == ch[31] + 3)  
    s.add(ch[8] == ch[7] - 32)  
    s.add(ch[9] + ch[20] == ch[31] + 3)  
    s.add(ch[7] + 6 == ch[10])  
    s.add(ch[8] == ch[9] + 27)  
    s.add(ch[12] == ch[13] - 1)  
    s.add(ch[13] == ch[10] - 3)  
    s.add(ch[10] == ch[16] - 1)  
    s.add(ch[16] == ch[14] - 1)  
    s.add(ch[35] == ch[5] - 2)  
    s.add(ch[5] == ch[21] - 1)  
    s.add(ch[21] == ch[22] - 1)  
    s.add(ch[22] == ch[28] * 2)  
    s.add(ch[33] == ch[32] + 1)  
    s.add(ch[34] == ch[32] + 4)  
    s.add(ch[30] == ch[7] + 1)  
  
    # 求解  
    if s.check() == sat:  
        model = s.model()  
        flag = ''.join([chr(model.eval(c).as_long()) for c in ch])  
        print(f"Flag found: {flag}")  
        return flag  
    else:  
        print("No solution found!")  
        return None  
  
  
if __name__ == "__main__":  
    solve_flag()

解得 flag：

Flag found: byuctf{lL1r_not_str41ght_to_4sm_458d}