[Paper] Zorya: Automated Concolic Execution of Single-Threaded Go Binaries

Source: arXiv - 2512.10799v1

Overview

The paper presents Zorya, a concolic execution engine that can automatically analyze compiled, single‑threaded Go binaries. By translating Go binaries into Ghidra’s P‑Code intermediate representation and focusing symbolic effort on paths that can trigger a panic, Zorya makes systematic vulnerability detection feasible for Go programs—something that existing symbolic tools have struggled with.

Key Contributions

• Go‑specific binary translation: Converts Go binaries to Ghidra P‑Code, preserving Go’s runtime semantics for accurate analysis.
• Panic‑reachability gating: A multi‑layer filter that isolates branches leading to a panic, cutting down symbolic exploration by 33‑70 %.
• Concrete‑path bug detection: Extends concolic execution to also flag bugs on paths that are not taken concretely during the initial run.
• Function‑mode analysis: Allows Zorya to start symbolic execution from any function (e.g., a vulnerable handler) instead of always from main, yielding up to 100× speedups on complex codebases.
• Empirical validation: Detects all five known Go vulnerabilities in the benchmark suite, outperforming state‑of‑the‑art tools that miss up to three of them.

Methodology

1. Binary Lifting – The compiled Go executable is fed into Ghidra, which lifts the machine code into its language‑agnostic P‑Code IR. This step captures Go’s unique calling conventions, stack layout, and runtime checks (e.g., bounds, nil‑pointer checks).
2. Concolic Execution Engine – Zorya runs the program concretely (real inputs) while simultaneously building symbolic constraints for each branch. When a branch is taken concretely, the engine records the opposite (untaken) path as a potential symbolic branch.
3. Panic‑Reachability Filtering – A static analysis pass identifies all program locations that can lead to a panic. During symbolic exploration, Zorya only expands branches that can reach any of these panic sites, discarding the rest.
4. Function‑Mode Entry – For large binaries, Zorya can be instructed to start symbolic execution from a specific function (e.g., an HTTP handler). The engine reconstructs the necessary context (arguments, globals) from the concrete run, avoiding the costly traversal of unrelated initialization code.
5. Bug Reporting – When a symbolic path reaches a panic‑triggering condition, Zorya extracts a concrete input that reproduces the crash, enabling developers to reproduce and fix the issue.

Results & Findings

The experiments confirm that focusing symbolic effort on panic‑relevant paths dramatically reduces the state‑space without sacrificing coverage. Moreover, the ability to start from arbitrary functions eliminates the “initialization bottleneck” that crippled many generic concolic frameworks.

Practical Implications

• Security Audits for Go Services – Teams can integrate Zorya into CI pipelines to automatically surface panic‑inducing bugs before deployment, especially in micro‑services where Go is prevalent.
• Bug‑Bounty Automation – Researchers can use Zorya to generate concrete exploit inputs for discovered panics, accelerating the verification phase of vulnerability reports.
• Language‑Specific Tooling – The success of a Go‑tailored concolic engine suggests that other languages with rich runtimes (Rust, Swift) could benefit from similar binary‑lifting + gating strategies.
• Reduced Manual Fuzzing Overhead – By pruning irrelevant branches, Zorya complements fuzzers, allowing them to concentrate on high‑impact input spaces and achieve deeper coverage with fewer CPU cycles.

Limitations & Future Work

• Single‑Threaded Focus – Zorya currently handles only single‑threaded binaries; extending to Go’s goroutine model will require sophisticated scheduling and synchronization modeling.
• Dependency on Ghidra – The translation pipeline hinges on Ghidra’s P‑Code accuracy; any gaps in Go runtime support could lead to missed bugs.
• Scalability to Very Large Codebases – While function‑mode mitigates initialization costs, extremely large binaries with many exported functions may still pose performance challenges.
• Future Directions – The authors plan to (1) add multi‑threaded concolic support, (2) integrate a lightweight taint analysis to further prune paths, and (3) open‑source the framework to foster community‑driven extensions for other Go runtime features.

Authors

• Karolina Gorna
• Nicolas Iooss
• Yannick Seurin
• Rida Khatoun

Paper Information

• arXiv ID: 2512.10799v1
• Categories: cs.SE, cs.PL
• Published: December 11, 2025
• PDF: Download PDF