Zorya: Automated Concolic Execution of Single-Threaded Go Binaries

TL;DR

Go binaries pose unique vulnerability-detection challenges due to runtime complexity and safety checks. Zorya extends concolic execution by lifting binaries to Ghidra's P-Code and applying panic-directed, multi-layer filtering to focus on panic-relevant paths, achieving substantial speedups and full vulnerability detection on a Go vulnerability corpus. The approach is shown to be most effective in function-mode analysis for real-world programs, with up to 3.9x speedups when gating eliminates 33-70% of branches. Overall, the work demonstrates that language-aware binary concolic analysis can deliver practical vulnerability detection in ecosystems with runtime safety checks, and opens avenues for multi-threaded Go support and incremental symbolic inputs.

Abstract

Go's adoption in critical infrastructure intensifies the need for systematic vulnerability detection, yet existing symbolic execution tools struggle with Go binaries due to runtime complexity and scalability challenges. In this work, we build upon Zorya, a concolic execution framework that translates Go binaries to Ghidra's P-Code intermediate representation to address these challenges. We added the detection of bugs in concretely not taken paths and a multi-layer filtering mechanism to concentrate symbolic reasoning on panic-relevant paths. Evaluation on five Go vulnerabilities demonstrates that panic-reachability gating achieves 1.8-3.9x speedups when filtering 33-70% of branches, and that Zorya detects all panics while existing tools detect at most two. Function-mode analysis proved essential for complex programs, running roughly two orders of magnitude faster than starting from main. This work establishes that specialized concolic execution can achieve practical vulnerability detection in language ecosystems with runtime safety checks.

Figures (1)

• Figure 1: Overview of Zorya workflow, including the optimizations of the negated-path exploration