Zorya is a concolic execution framework that lifts compiled binaries to Ghidra's P-Code intermediate representation and uses the Z3 SMT solver to detect vulnerabilities by reasoning over both concrete and symbolic values. Previous versions supported only single-threaded TinyGo binaries. In this paper, we extend Zorya to multi-threaded binaries produced by Go's standard gc compiler. This is achieved by restoring OS thread states from gdb dumps, neutralizing runtime preemption, and introducing overlay path analysis with copy-on-write semantics to detect silent vulnerabilities on untaken branches. We rigorously assess Zorya on 11 real-world vulnerabilities from production Go projects such as Kubernetes, Go-Ethereum, and CoreDNS. Our evaluation shows that Zorya detects seven bugs at the binary level, including a silent integer overflow detects no other evaluated tool finds without a manually written oracle.

翻译：Zorya是一个混合执行框架，它将编译后的二进制文件提升至Ghidra的P-Code中间表示形式，并利用Z3 SMT求解器通过对具体值和符号值的推理来检测漏洞。先前版本仅支持单线程TinyGo二进制文件。本文中，我们将Zorya扩展到由Go标准gc编译器生成的多线程二进制文件。这一扩展通过从gdb转储恢复操作系统线程状态、消除运行时抢占、以及引入带写时复制语义的覆盖路径分析来检测未采取分支上的隐蔽漏洞得以实现。我们对来自生产级Go项目（如Kubernetes、Go-Ethereum和CoreDNS）的11个真实世界漏洞进行了严格评估。评估结果显示，Zorya在二进制级别检测到7个漏洞，包括一个无需手动编写预言机即可被检测到的、其他评估工具未能发现的静默整数溢出漏洞。