From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries

TL;DR

This paper extends the Zorya concolic execution framework to handle multi-threaded Go binaries, enabling detection of real-world vulnerabilities in complex production software.

Contribution

It introduces techniques for restoring thread states, neutralizing preemption, and overlay path analysis to adapt Zorya for multi-threaded binaries from the gc compiler.

Findings

Zorya detects seven bugs in real-world Go binaries.

It finds a silent integer overflow undetected by other tools.

Evaluation on Kubernetes, Go-Ethereum, and CoreDNS demonstrates effectiveness.

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.