[Paper] Zorya：自动化 Concolic 执行单线程 Go 二进制文件

Source: arXiv - 2512.10799v1

概览

本文提出了 Zorya，一种混合符号执行引擎，能够自动分析已编译的单线程 Go 二进制文件。通过将 Go 二进制文件翻译为 Ghidra 的 P‑Code 中间表示，并将符号化工作重点放在可能触发 panic 的路径上，Zorya 使得对 Go 程序进行系统化漏洞检测成为可能——这是现有符号工具一直难以实现的。

关键贡献

• 针对 Go 的二进制翻译：将 Go 二进制转换为 Ghidra P‑Code，保留 Go 运行时语义，以实现精准分析。
• Panic 可达性过滤：多层过滤器，隔离通向 panic 的分支，将符号探索量降低 33‑70 %。
• 具体路径漏洞检测：将混合符号执行扩展至标记在初始运行中未被实际走过的路径上的 bug。
• 函数模式分析：允许 Zorya 从任意函数（例如易受攻击的处理函数）开始符号执行，而不必始终从 main 开始，在复杂代码库上可实现最高 100 倍的加速。
• 实证验证：在基准套件中检测出全部五个已知的 Go 漏洞，优于那些最多漏检三个漏洞的先进工具。

方法论

1. 二进制提升 – 将编译后的 Go 可执行文件导入 Ghidra，提升为其语言无关的 P‑Code IR。此步骤捕获 Go 独有的调用约定、栈布局以及运行时检查（如边界检查、空指针检查）。
2. 混合符号执行引擎 – Zorya 在具体运行（真实输入）的同时，为每个分支构建符号约束。当分支在具体运行中被采纳时，引擎记录相反的（未采纳）路径作为 潜在 符号分支。
3. Panic 可达性过滤 – 静态分析阶段识别所有可能导致 panic 的程序位置。符号探索期间，Zorya 只展开能够到达这些 panic 点的分支，舍弃其余分支。
4. 函数模式入口 – 对于大型二进制，Zorya 可指示从特定函数（如 HTTP 处理器）开始符号执行。引擎从具体运行中重建必要的上下文（参数、全局变量），避免遍历无关的初始化代码，从而降低成本。
5. 漏洞报告 – 当符号路径触发 panic 条件时，Zorya 提取可复现崩溃的具体输入，帮助开发者重现并修复问题。

结果与发现

实验表明，将符号化工作聚焦在与 panic 相关的路径上，可显著降低状态空间而不牺牲覆盖率。此外，能够从任意函数启动的能力消除了许多通用混合符号框架中“初始化瓶颈”的限制。

实际意义

• Go 服务的安全审计 – 团队可以将 Zorya 集成到 CI 流水线中，自动发现 panic 引发的 bug，尤其适用于 Go 广泛使用的微服务。
• 漏洞赏金自动化 – 研究人员可利用 Zorya 为发现的 panic 生成具体利用输入，加速漏洞报告的验证阶段。
• 语言专属工具 – Go 定制的混合符号引擎的成功表明，其他拥有丰富运行时的语言（如 Rust、Swift）也可受益于类似的二进制提升 + 过滤策略。
• 降低手动模糊测试负担 – 通过剪枝无关分支，Zorya 能与模糊测试器互补，使其专注于高影响力的输入空间，以更少的 CPU 周期实现更深的覆盖。

局限性与未来工作

• 单线程聚焦 – Zorya 目前仅支持单线程二进制；扩展到 Go 的 goroutine 模型需要更复杂的调度与同步建模。
• 依赖 Ghidra – 翻译流水线依赖 Ghidra 对 P‑Code 的准确实现；若 Go 运行时支持存在缺口，可能导致漏检。
• 对超大代码库的可扩展性 – 虽然函数模式缓解了初始化开销，但拥有大量导出函数的极大二进制仍可能面临性能挑战。
• 未来方向 – 作者计划 (1) 添加多线程混合符号支持，(2) 集成轻量级污点分析进一步剪枝路径，(3) 开源框架以促进社区为其他 Go 运行时特性扩展贡献。

作者

• Karolina Gorna
• Nicolas Iooss
• Yannick Seurin
• Rida Khatoun

论文信息

• arXiv ID: 2512.10799v1
• 分类: cs.SE, cs.PL
• 发布日期: 2025 年 12 月 11 日
• PDF: Download PDF