From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries
Karolina Gorna, Nicolas Iooss, Yannick Seurin, Rida Khatoun, Keith Makan
TLDR
Zorya, a concolic execution framework, now supports multi-threaded Go binaries, detecting real-world vulnerabilities, including silent overflows.
Key contributions
- Extends Zorya's concolic execution to multi-threaded Go binaries compiled with the standard `gc` compiler.
- Implements OS thread state restoration, runtime preemption neutralization, and overlay path analysis.
- Detects silent vulnerabilities on untaken branches using copy-on-write semantics.
- Identifies 7 real-world Go bugs, including a unique silent integer overflow, outperforming other tools.
Why it matters
This paper significantly advances concolic execution for Go, extending Zorya to real-world, multi-threaded applications. It provides a powerful new tool for securing critical Go projects by detecting complex, silent vulnerabilities like integer overflows, which other tools miss.
Original Abstract
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.
📬 Weekly AI Paper Digest
Get the top 10 AI/ML arXiv papers from the week — summarized, scored, and delivered to your inbox every Monday.