SMT

概述

可满足性模理论（Satisfiability Modulo Theories，简称 SMT） 可以看作是一个更强大的 “解方程” 工具。它解决的核心问题是：在特定的数学理论（如整数运算、数组、位向量等）背景下，判断一个逻辑公式是否存在一组解

工作原理

主流的 SMT 求解器多采用 “惰性（Lazy）算法”，其工作流程像一个高效的 “猜-验” 循环：

  • 抽象化：将 SMT 公式中的理论部分（如 x > y）替换为布尔变量，交给内部的 SAT 求解器去 “猜” 一个可能的布尔赋值组合

  • 理论验证：将 SAT 求解器 “猜” 出的布尔组合，还原回具体的理论约束，交给对应的理论求解器（如线性算术求解器）去 “验” 证这些约束是否有数学上的解

  • 反馈与迭代：

    有解：如果理论求解器找到了解，则整个 SMT 公式可满足，求解成功

    • 无解：如果理论求解器发现矛盾，它会生成一个 “冲突子句” 反馈给 SAT 求解器，告知它这种 “猜测” 行不通。SAT 求解器会排除这个错误选项，继续 “猜” 下一个组合

  • 结束：重复此过程，直到找到可行解，或 SAT 求解器穷尽所有可能后宣布不可满足

主流 SMT 求解器

目前已有众多功能强大的SMT求解器，以下是一些主流代表

  • Z3：由微软研究院开发，因其鲁棒性、多功能性和频繁更新，被广泛认为是表现最好的求解器之一

  • CVC5：由斯坦福大学等机构开发，是著名求解器 CVC4 的继任者

  • Yices2：由 SRI International 开发

  • Alt-Ergo：在 SMT 竞赛中常见的求解器

实战案例

martricks（矩阵 + SMT 求解）

pasted_1787212314241_tp5bj4.png

IDA 反编译

pasted_1787904858025_fc3dvc.png

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
flag = input()

# 两个 7x7 矩阵，用于后续矩阵乘法校验
A = [[0] * 7 for _ in range(7)]
B = [[0] * 7 for _ in range(7)]

# 填充矩阵：v11 作为 A 的填充位置，按步长 13 在 49 个位置中跳跃
# A[位置] = flag[i] ^ 位置；B[顺序位置] = byte_601060[位置] ^ i
v11 = 23
for i in range(49):
    A[v11 // 7][v11 % 7] = flag[i] ^ v11
    B[i // 7][i % 7] = byte_601060[v11] ^ i
    v11 = (v11 + 13) % 49

# 校验：(A * B)[row][col] 模 256 是否等于 byte_6010A0[v10] ^ v10
v10 = 41
row = 3

for i in range(7):          # row 以步长 3 遍历所有行
    col = 4
    for j in range(7):      # col 以步长 4 遍历所有列
        acc = 0
        t = 5
        for k in range(7):  # t 以步长 5 遍历 0..6，计算行×列内积
            acc += B[t][col] * A[row][t]
            acc &= 0xff      # 累加结果按字节截断
            t = (t + 5) % 7

        if acc != (byte_6010A0[v10] ^ v10):
            print("wrong flag")
            exit()

        v10 = (v10 + 31) % 49  # v10 以步长 31 遍历 49 个校验值
        col = (col + 4) % 7

    row = (row + 3) % 7

print("congrats")

也就是说：

  • A 是由输入 flag 变形得到的矩阵

  • B 是由程序内置数组 byte_601060 变形得到的矩阵

所以后续目标就是根据 byte_601060 和 byte_6010A0 反推出 A，再根据 A 还原 flag

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
from z3 import *

# 常量字符串，长度 49
const_str = b"some legends r told, some turn to dust or to gold"
assert len(const_str) == 49

# 目标校验值（49 字节）
target = [
    0xAA, 0x7A, 0x24, 0x0A, 0xA8, 0xBC, 0x3C, 0xFC, 0x82, 0x4B,
    0x51, 0x52, 0x5E, 0x1C, 0x82, 0x1F, 0x79, 0xBA, 0xB5, 0xE3,
    0x43, 0x04, 0xFD, 0xAC, 0x10, 0xB5, 0x63, 0xBD, 0x8D, 0xE7,
    0x35, 0xD9, 0xD3, 0xE8, 0x42, 0x6D, 0x71, 0x5A, 0x09, 0x54,
    0xE9, 0x9F, 0x4C, 0xDC, 0xA2, 0xAF, 0x11, 0x87, 0x94
]

# 49 个 8 位符号变量表示 flag
flag = [BitVec(f"flag_{i}", 8) for i in range(49)]

s = Solver()

# 限制为可打印 ASCII
for c in flag:
    s.add(UGE(c, 0x20))
    s.add(ULE(c, 0x7e))

# 格式约束：以 "flag{" 开头，以 "}" 结尾
prefix = b"flag{"
for i, c in enumerate(prefix):
    s.add(flag[i] == c)
s.add(flag[48] == ord('}'))

# ---------- 构造矩阵 ----------
# A 矩阵：7x7，元素为符号变量（flag[i] ^ v11）
A = [[None for _ in range(7)] for _ in range(7)]
# B 矩阵：7x7，元素为常量（const_str[v11] ^ i）
B = [[0 for _ in range(7)] for _ in range(7)]

v11 = 23
for i in range(49):
    # 按步长 13 跳跃填充 A 和 B
    A[v11 // 7][v11 % 7] = flag[i] ^ BitVecVal(v11, 8)
    B[i // 7][i % 7] = const_str[v11] ^ i
    v11 = (v11 + 13) % 49

# ---------- 校验 ----------
v10 = 41
v13 = 3

for i in range(7):
    v14 = 4
    for j in range(7):
        acc = BitVecVal(0, 8)
        v7 = 5
        for k in range(7):
            # 内积：A 第 v13 行 与 B 第 v14 列
            acc += BitVecVal(B[v7][v14], 8) * A[v13][v7]
            v7 = (v7 + 5) % 7

        # 约束：acc == target[v10] ^ v10
        s.add(acc == BitVecVal(target[v10] ^ v10, 8))

        v10 = (v10 + 31) % 49
        v14 = (v14 + 4) % 7

    v13 = (v13 + 3) % 7

print("[*] solving...")

if s.check() == sat:
    model = s.model()
    result = b""
    for i in range(49):
        result += bytes([model[flag[i]].as_long()])
    print("[+] FLAG:")
    print(result.decode())
else:
    print("[-] failed")

pasted_1787214415895_ref6h9.png