用 Gemini 与 Z3 补查 Go 越界漏洞

Go 代码写了边界检查，fuzz 也跑过，为什么还是会藏着越界 bug？作者给出的答案有两层：检查本身可能算错，而 Go 切片多出来的容量又可能让错误逃过测试。他把编译器留下的越界检查交给 Gemini 和 Z3 分析，再用真实 Go 测试确认，找出了 3 个人工植入的 bug，以及 skill-lint 中的 3 个潜在问题。

这套方法最值得带走的，未必是求解器流水线。对多数 Go 项目，先给 fuzz 输入补一行容量限制，就能堵上一个容易忽视的测试盲区。

写了长度检查，为什么还是会越界

作者维护着 Google 的 agent skills 项目，涉及 175 个技能文件。他为此开发了 Go CLI 工具 skill-lint，负责检查 SKILL.md，并应用 LLM 生成的行级修改。Markdown 解析和行号计算中，一个很小的偏差就可能触发 panic。

他先用 3 个安全解析器和 3 个故意写错的解析器验证方法。其中，ParseTwoChunkFrame 很适合说明问题：它检查文件头，再按头部给出的两个长度切分数据。

func ParseTwoChunkFrame(buf []byte) ([]byte, []byte) {
	if len(buf) < 4 || buf[0] != 0xA5 || buf[1] != 0x5A {
		return nil, nil
	}
	hdrLen, bodyLen := buf[2], buf[3]
	total := hdrLen + bodyLen
	if int(total)+4 > len(buf) {
		return nil, nil
	}
	endHdr := 4 + int(hdrLen)
	endBody := endHdr + int(bodyLen)
	return buf[4:endHdr], buf[endHdr:endBody]
}

关键在 total := hdrLen + bodyLen。两个操作数都是 uint8，结果先按 8 位回绕，再被转成 int；后面的 endBody 却先转 int 再相加。检查和使用，算的是两个不同的值。

Z3 找到的反例长 59 字节，hdrLen 为 48，bodyLen 为 236。两者实际相加是 284，uint8 回绕后却成了 28，于是 28 + 4 ≤ 59 通过检查，真正切片时却访问到索引 288。

奇怪的是，在长度固定为 59 字节时，所有长度字段组合中有 19.4% 会触发这个错误，fuzz 却没找到。作者用 Go 1.27.3 做了无种子测试：一次 3 秒、三次各 60 秒，每次清空 fuzz 缓存，仍然漏掉。

原因是双下标切片的上界可以延伸到 cap，而不只到 len。作者另做了 10 秒探测，记录 386,741 次调用：89% 的输入来自约 100 MB 共享缓冲区的视图，只有 0.07% 满足 cap == len。这里 endBody 最大只有 514，富余容量足以容纳错误访问，函数便返回了逻辑输入之外的数据。

下面这一行让 fuzz 输入的容量与长度一致，越过逻辑末尾就会 panic：

f.Fuzz(func(t *testing.T, data []byte) {
	data = data[:len(data):len(data)] // cap == len: slicing past the end now panics
	ParseTwoChunkFrame(data)
})

要看的是三下标表达式 data[:len(data):len(data)]，它没有复制数据，只限制了切片容量。修改后，ParseTwoChunkFrame 和另一个引号解析器 ExtractQuotedToken 在三轮测试中全部被抓到，中位耗时分别为 0.28 秒和 0.17 秒。后者只需 2 字节输入 []byte{'"', '\\'} 就能触发。

第三个解析器 ParseMagicPacket 因 int8 长度产生负索引，不受富余容量保护，修改前后都被 fuzz 找到。

为什么让模型看汇编，再让 Z3 找输入

Go 编译器的 SSA prove pass 会先消除能够证明安全的边界检查。剩下通往 runtime.panicBounds 的分支，就成了作者优先分析的候选位置。

他的编译命令是 GOOS=linux GOARCH=riscv64 go build -gcflags="-S -d=ssa/check_bce/debug=1"：-S 打印汇编，ssa/check_bce/debug=1 标出仍然存在的边界检查。选择 RISC-V，是为了沿用所参考的 Anthropic 实验架构，Go 本身也支持交叉编译。

Gemini 4 Argon 同时读取源码和汇编，把到达这些分支的条件翻译成 Z3 约束。在前面的例子中，汇编里的 MOVBU 明确暴露了 uint8 截断，后续未截断的整数加法也清楚可见。模型需要把位宽、长度和容量逐项写出来。

Z3 的 check-sat 返回 sat，表示模型中的条件有解；返回 unsat，表示这些条件无解。找到输入后，再由 go test 喂给真实函数执行。作者报告，模型翻译约需每个函数一分钟，Z3 求解只需毫秒。

只有真实 Go 测试复现了 panic，才算确认找到 bug。

模型可能漏掉路径，也可能翻错机器语义，因此 unsat 不能当成正确性证明。作者参考的 Rocq 路线有机器语义模型和证明检查；这里依赖 LLM 直接建立约束，可信边界不同。

实验范围也很具体：作者检查单个函数，输入是最多 64 字节、cap(buf) == len(buf) 的新切片。它不等同于参考方案在 64 MB 预算下检查完整二进制。原文另提到 theorem-labs/oss-verify 提供 Go 1.27 runtime overlay，可让运行时单线程、确定性执行，但这不是本次流水线的能力。

真正落到工具代码，问题常出在状态变化之后

整份 CLI 并不适合直接交给求解器。作者举例，一个 10 行解析器就会链接 1,559 个运行时符号；28 MB 的 skill-lint 二进制共有 32,321 个符号。

因此，他按 Functional Core, Imperative Shell 的思路，把计算逻辑从文件 I/O 中抽出来。命令行参数、网络和文件操作继续交给 go test -fuzz、go test -race，求解器只分析纯函数和切片辅助函数。

受测的 5 个函数中，两个扫描器返回 unsat，其中一个 CRLF 分行器仍有 6 处边界检查；另外 3 个存在问题。

最典型的是 ApplyReplacementChunks。它先按初始行数验证 {StartLine, EndLine}，再按 StartLine 从大到小应用修改。这能避免普通编辑造成行号位移，却没有排除区间重叠。

一个 4 行文件先把第 3 至 4 行替换成一行，文件便只剩 3 行。第二个修改如果仍覆盖第 2 至 4 行，抽出的辅助函数会执行 lines[4:]，触发 [4:3] 越界。正式 ApplyChunks 有逐轮检查，会返回容易误导的范围错误；若重叠后仍未超界，则可能静默覆盖之前的修改。排序后拒绝重叠区间，才能同时处理这两类后果。

另外两个问题也与计算依据失效有关：本地 fixer 在删除行前验证过行号，删除后若继续处理第二个 chunk，就可能越界，不过当前 DeleteLineFix 只返回一个 chunk；提示词打包器固定预留 100 字节，实际包装约占 70 字节再加文件路径，路径超过约 30 字节就可能突破正式代码的 2 MB 上下文预算，抽取版本则会 panic。

这几种后果要分清，不能一概写成线上崩溃。

抽取后的函数还必须带上入口校验，否则求解器可能构造调用方原本不允许的输入。作者报告，6 个有问题的函数，其首个 sat 解都直接复现了 panic；去掉源码注释重跑，仍能找到 skill-lint 的 3 个问题，并对两个扫描器和三个补丁返回 unsat。

不过，抽离 I/O 后，3 秒 fuzz 也找到了这 3 个问题。

我的判断

我赞成它把编译器、模型、求解器和真实测试串起来：模型负责翻译，求解器负责找满足条件的输入，测试负责确认结果。每一步都有清楚的用途，比只让模型读源码挑错更容易核验。

但文章不足以证明这套组合普遍优于 fuzz。样本来自作者自己的解析器和工具，只有 3 个人工 bug、3 个潜在问题；容量限制修正后，fuzz 很快找到了前两个漏报，抽取辅助函数后也找到了工具里的问题。作者没有给出足够广泛的对照数据，不能把「每函数多花一分钟」直接解释成稳定收益。

对日常团队，更合理的顺序是先改善测试边界和函数结构，再分析剩余的可疑检查。unsat 也只能作为当前模型下的分析结果。

这套单线程模型不覆盖竞态和死锁。并发问题仍应使用 race detector、确定性并发测试，以及原文提到的 Go 1.27 goroutine leak profiles。

能拿来做什么

• 给 Go 解析器补 fuzz 时，加入 cap == len 的输入条件，特别检查根据多个长度字段计算切片范围的代码。富余容量可能掩盖逻辑越界。
• 为 AI 生成的批量行编辑增加重叠校验，并覆盖「前一次替换缩短文件，后一次仍使用旧行号」的情况。倒序应用不能代替冲突检测。
• 把 Go 工具中的行号计算、内容截断和上下文预算计算抽成带入口校验的纯函数，先跑短时 fuzz，再考虑分析编译器留下的边界检查。
• 让 AI 辅助编程时提交可执行的复现测试。Z3 给出的输入要经过 go test 确认，模型返回的补丁也应保留对应回归用例。