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进行了严格评估。评估表明，Zorya在二进制层面检测到了7个缺陷，包括一个在没有手动编写断言的情况下其他已评估工具均无法发现的隐蔽整数溢出。