从 TinyGo 到 gc 编译器：扩展 Zorya 共针对实际 Go 二进制文件的浓缩框架
密码学与安全
2026-05-21 v2 符号计算
软件工程
摘要
Zorya 是一个共针执行框架，将编译后的二进制文件提升到 Ghidra 的 P-Code 中间表示，并利用 Z3 SMT 求解器通过推理具体值和符号值来检测漏洞。先前版本仅支持单线程 TinyGo 二进制文件。本文将 Zorya 扩展到由 Go 标准 gc 编译器生成的多线程二进制文件。这通过恢复 gdb 转储中的 OS 线程状态、中和运行时抢占，并引入具备复制-写入语义的覆盖路径分析来实现，用于检测静默漏洞（silent vulnerabilities）在未被采样的分支上。我们对 Zorya 在 11 个现实世界漏洞（来自 Kubernetes、Go-Ethereum 和 CoreDNS 等生产 Go 项目）进行了严格评估。我们的评估表明，Zorya 在二进制层面检测到七个漏洞，其中包括一个静默整数溢出漏洞——其他所评估工具均需依赖手动编写的 oracle 才能发现。
引用
@article{arxiv.2605.03492,
title = {From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries},
author = {Karolina Gorna and Nicolas Iooss and Yannick Seurin and Rida Khatoun and Keith Makan},
journal= {arXiv preprint arXiv:2605.03492},
year = {2026}
}
备注
Preprint. Accepted in the 30th ACM International Conference on Evaluation and Assessment in Software Engineering (EASE 2026)