pith. sign in

arxiv: 2605.03492 · v2 · pith:TH3HSXTFnew · submitted 2026-05-05 · 💻 cs.CR · cs.SC· cs.SE

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 This is my paper

Pith reviewed 2026-05-21 08:44 UTC · model grok-4.3

classification 💻 cs.CR cs.SCcs.SE
keywords concolic executionGo binariesvulnerability detectionbinary analysismulti-threaded programsinteger overflowpath analysis
0
0 comments X

The pith

Zorya now analyzes multi-threaded Go binaries from the standard compiler and detects seven vulnerabilities including silent integer overflows.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper extends a concolic execution framework that lifts binaries to an intermediate representation and uses an SMT solver to find vulnerabilities by tracking both concrete and symbolic values. Previous work covered only single-threaded programs compiled with TinyGo; the new version handles full multi-threaded programs from Go's gc compiler. It achieves this by capturing thread states from debugger output, disabling runtime preemption, and adding an overlay analysis that explores untaken paths with copy-on-write semantics. A reader would care because many deployed Go programs run in production without source available, so direct binary analysis could surface bugs that source-dependent tools miss.

Core claim

Restoring OS thread states from gdb dumps, neutralizing Go runtime preemption, and introducing overlay path analysis with copy-on-write semantics enables Zorya to analyze multi-threaded gc-compiled Go binaries. On 11 real-world vulnerabilities drawn from projects such as Kubernetes, Go-Ethereum, and CoreDNS, the extended framework detects seven bugs at the binary level, including a silent integer overflow that no other evaluated tool locates without a manually supplied oracle.

What carries the argument

Overlay path analysis with copy-on-write semantics, supported by thread-state restoration from debugger dumps and preemption neutralization, to model observable multi-threaded behavior during concolic execution.

If this is right

  • Vulnerability detection becomes possible directly on compiled binaries of standard Go programs without source code access.
  • Silent integer overflows and similar issues on untaken branches can be identified through symbolic exploration.
  • The same pipeline applies to production codebases such as Kubernetes and CoreDNS.
  • Fewer manual oracles are needed to confirm certain classes of binary-level bugs.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Techniques for capturing and restoring thread states could transfer to other languages whose runtimes manage preemption or scheduling.
  • Overlay analysis might combine with additional binary lifters to cover more architectures or compilers.
  • Automated discovery of silent bugs could reduce dependence on source-level testing for compiled applications.

Load-bearing premise

Restoring OS thread states from gdb dumps, neutralizing Go runtime preemption, and applying overlay path analysis with copy-on-write semantics faithfully reproduces the observable behavior of multi-threaded gc-compiled binaries for the purpose of vulnerability detection.

What would settle it

A concrete multi-threaded gc-compiled Go binary containing a confirmed vulnerability that Zorya reports as safe, or a case where Zorya reports a vulnerability that does not manifest in actual execution.

Figures

Figures reproduced from arXiv: 2605.03492 by Karolina Gorna, Keith Makan, Nicolas Iooss, Rida Khatoun, Yannick Seurin.

Figure 1
Figure 1. Figure 1: Overview of Zorya workflow, including AST exploration and Overlay Concolic Execution. view at source ↗
read the 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The paper extends the Zorya concolic execution framework, previously limited to single-threaded TinyGo binaries, to support multi-threaded binaries produced by Go's standard gc compiler. The extension restores OS thread states from gdb dumps, neutralizes Go runtime preemption, and introduces overlay path analysis with copy-on-write semantics to detect silent vulnerabilities on untaken branches. Evaluation is performed on 11 real-world vulnerabilities from production projects such as Kubernetes, Go-Ethereum, and CoreDNS, with the claim that Zorya detects seven bugs at the binary level, including a silent integer overflow that no other evaluated tool finds without a manually written oracle.

Significance. If the reproduction of observable binary behavior is faithful, the work would advance binary-level vulnerability detection for widely deployed Go software. The focus on silent bugs without manual oracles is a practical strength. However, the evaluation provides no quantitative false-positive rates or full baselines, and the central claim depends on the fidelity of preemption neutralization and thread-state restoration.

major comments (2)
  1. [Extension description and evaluation of the silent integer overflow case] The neutralization of Go runtime preemption (removal of checks at call sites and loop back-edges) collapses scheduler nondeterminism. The paper must show that the reported silent integer overflow does not depend on an interleaving possible only with active preemption; otherwise the detection result may be an artifact of the fixed scheduling order used in overlay path analysis rather than a faithful reproduction of gc-compiled binary behavior. This underpins the strongest evaluation claim.
  2. [Evaluation section] The 11 vulnerabilities are described as 'real-world' from production projects, but the selection criteria, how many are known to be interleaving-dependent, and quantitative false-positive rates for the full set are not reported. Without these, the claim that Zorya detects seven bugs (including one missed by other tools) cannot be fully assessed for soundness.
minor comments (2)
  1. [Abstract] The abstract sentence 'including a silent integer overflow detects no other evaluated tool finds without a manually written oracle' is grammatically incomplete and should be rephrased.
  2. [Throughout] Ensure consistent first-use definitions for 'P-Code', 'overlay path analysis', and 'copy-on-write semantics' to aid readers unfamiliar with the prior Zorya work.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive and detailed feedback on our extension of Zorya to support gc-compiled Go binaries. We address each major comment below, providing clarifications and indicating the revisions we will incorporate to improve the manuscript.

read point-by-point responses

  1. Referee: [Extension description and evaluation of the silent integer overflow case] The neutralization of Go runtime preemption (removal of checks at call sites and loop back-edges) collapses scheduler nondeterminism. The paper must show that the reported silent integer overflow does not depend on an interleaving possible only with active preemption; otherwise the detection result may be an artifact of the fixed scheduling order used in overlay path analysis rather than a faithful reproduction of gc-compiled binary behavior. This underpins the strongest evaluation claim.

    Authors: We agree that demonstrating independence from preemption-induced interleavings is critical for validating the fidelity of our results. In the revised manuscript, we will add a dedicated analysis subsection for the silent integer overflow case. This will show that the overflow arises from intra-thread arithmetic operations on a specific path (restored from the gdb thread state), which overlay path analysis explores via copy-on-write semantics without requiring any cross-thread scheduling decision that active preemption could enable. We will include a step-by-step trace illustrating that the vulnerable path remains reachable under the neutralized scheduler and does not rely on an interleaving unique to the original runtime. revision: yes

  2. Referee: [Evaluation section] The 11 vulnerabilities are described as 'real-world' from production projects, but the selection criteria, how many are known to be interleaving-dependent, and quantitative false-positive rates for the full set are not reported. Without these, the claim that Zorya detects seven bugs (including one missed by other tools) cannot be fully assessed for soundness.

    Authors: We accept that expanding the evaluation details will strengthen the paper. We will revise the section to describe the selection criteria: the 11 cases were drawn from publicly disclosed CVEs in widely used Go projects (Kubernetes, Go-Ethereum, CoreDNS) that involve integer or memory issues amenable to binary-level concolic analysis. We will also report that four of the eleven are documented as interleaving-dependent in their original vulnerability reports. Quantitative false-positive rates are not provided because our evaluation targets detection of known bugs rather than exhaustive benign-binary testing, which is computationally prohibitive for full concolic exploration of production binaries; we will add an explicit discussion of this methodological choice and its implications. revision: partial

Circularity Check

0 steps flagged

No significant circularity; results rest on external empirical evaluation

full rationale

The paper describes an engineering extension of Zorya to gc-compiled binaries via gdb-based thread restoration, preemption neutralization, and overlay path analysis, then reports detections on 11 independently known real-world vulnerabilities from projects such as Kubernetes and Go-Ethereum. No equations, fitted parameters, or self-citation chains appear in the derivation that reduce the reported bug detections to quantities defined by the authors' own prior fits or inputs. The central claims are grounded in external assessment rather than internal self-definition or renaming of known results.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The approach rests on domain assumptions about Go runtime behavior and the fidelity of gdb thread dumps rather than on new mathematical axioms or invented entities.

axioms (1)
  • domain assumption Go runtime preemption can be neutralized for the duration of concolic analysis without changing the program's observable vulnerability behavior.
    Invoked to stabilize multi-threaded execution during symbolic reasoning.

pith-pipeline@v0.9.0 · 5696 in / 1285 out tokens · 56276 ms · 2026-05-21T08:44:07.127746+00:00 · methodology

Review history (3 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

  1. [1]

    aemmitt ns. 2025. aemmitt-ns/radius2. https://github.com/aemmitt-ns/radius2 original-date: 2021-04-25T03:45:10Z

    work page 2025

  2. [2]

    Roberto Baldoni, Emilio Coppa, Daniele Cono D’elia, Camil Demetrescu, and Irene Finocchi. 2018. A Survey of Symbolic Execution Techniques.ACM Comput. Surv.51, 3 (May 2018), 50:1–50:39. doi:10.1145/3182657

    work page doi:10.1145/3182657 2018

  3. [3]

    Stefan Bucur, Vlad Ureche, Cristian Zamfir, and George Candea. 2011. Parallel symbolic execution for automated real-world software testing. InProceedings of the sixth conference on Computer systems (EuroSys ’11). Association for Computing Machinery, New York, NY, USA, 183–198. doi:10.1145/1966445.1966463

    work page doi:10.1145/1966445.1966463 2011

  4. [4]

    Carmen Carrión. 2022. Kubernetes Scheduling: Taxonomy, Ongoing Issues and Challenges.ACM Comput. Surv.55, 7 (Dec. 2022), 138:1–138:37. doi:10.1145/ 3539606

    work page 2022

  5. [5]

    Vitaly Chipounov, Volodymyr Kuznetsov, and George Candea. 2011. S2E: a platform for in-vivo multi-path analysis of software systems.SIGPLAN Not.46, 3 (March 2011), 265–278. doi:10.1145/1961296.1950396

    work page doi:10.1145/1961296.1950396 2011

  6. [6]

    Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. InTools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer, Berlin, Heidelberg, 337–340. doi:10.1007/978-3-540-78800-3_24

    work page doi:10.1007/978-3-540-78800-3_24 2008

  7. [7]

    Will Dietz, Peng Li, John Regehr, and Vikram Adve. 2015. Understanding Integer Overflow in C/C++.ACM Trans. Softw. Eng. Methodol.25, 1 (Dec. 2015), 2:1–2:29. doi:10.1145/2743019

    work page doi:10.1145/2743019 2015

  8. [8]

    Adel Djoudi and Sébastien Bardin. 2015. BINSEC: Binary Code Analysis with Low-Level Regions. InTools and Algorithms for the Construction and Analysis of Systems, Christel Baier and Cesare Tinelli (Eds.). Springer, Berlin, Heidelberg, 212–217. doi:10.1007/978-3-662-46681-0_17

    work page doi:10.1007/978-3-662-46681-0_17 2015

  9. [9]

    Go-Community. [n. d.]. Introduction to the Go compiler. https://go.dev/src/cmd/ compile/README

    work page

  10. [10]

    Go-Community. 2026. go-delve/delve. https://github.com/go-delve/delve original-date: 2014-05-20T19:24:43Z

    work page 2026

  11. [11]

    Go-Community. 2026. Go Fuzzing - The Go Programming Language. https: //go.dev/doc/security/fuzz/

    work page 2026

  12. [12]

    Go-Community. 2026. go/src/runtime/race.go at master·golang/go. https: //github.com/golang/go/blob/master/src/runtime/race.go

    work page 2026

  13. [13]

    Go-Community. 2026. govulncheck command - golang.org/x/vuln/cmd/govulncheck - Go Packages. https://pkg.go.dev/ golang.org/x/vuln/cmd/govulncheck

    work page 2026

  14. [14]

    Go-Community. 2026. nm command - cmd/nm - Go Packages. https://pkg.go. dev/cmd/nm

    work page 2026

  15. [15]

    Queue 10(1), 20:20–20:27 (2012)

    Patrice Godefroid, Michael Y. Levin, and David Molnar. 2012. SAGE: Whitebox Fuzzing for Security Testing: SAGE has had a remarkable impact at Microsoft. Queue10, 1 (Jan. 2012), 20–27. doi:10.1145/2090147.2094081

    work page doi:10.1145/2090147.2094081 2012

  16. [16]

    Google. 2018. StaticCheck : Golang static analyzer. https://staticcheck.dev/docs/

    work page 2018

  17. [17]

    Google. 2024. GoVet : Golang static analyzer. https://pkg.go.dev/cmd/vet

    work page 2024

  18. [18]

    Karolina Gorna, Nicolas Iooss, Yannick Seurin, and Rida Khatoun. 2025. Zorya: Automated Concolic Execution of Single-Threaded Go Binaries. doi:10.1145/ 3748522.3779940 arXiv:2512.10799 [cs]

    work page arXiv 2025

  19. [19]

    Karolina Gorna, Nicolas Iooss, Yannick Seurin, and Rida Khatoun. 2026. Concolic Execution Optimized for Go Binaries using Ghidra’s P-Code. InSoftware Engi- neering and Management: Theory and Applications: Volume 18. Springer Nature, 161–176. Google-Books-ID: Q7LCEQAAQBAJ

    work page 2026

  20. [20]

    Sonal Mahajan. 2023. NilAway: Practical Nil Panic Detection for Go. https: //www.uber.com/en-EG/blog/nilaway-practical-nil-panic-detection-for-go/

    work page 2023

  21. [21]

    NSA. 2017. Ghidra. https://ghidra-sre.org/

    work page 2017

  22. [22]

    Sebastian Poeplau and Aurélien Francillon. 2020. Symbolic execution with {SymCC}: Don’t interpret, compile!. In29th USENIX Security Symposium (USENIX Security 20). 181–198

    work page 2020

  23. [23]

    Sebastian Poeplau and Aurélien Francillon. 2021. SymQEMU: Compilation-based symbolic execution for binaries. InNDSS 2021, Network and Distributed System Security Symposium (2021 Network and Distributed Systems Security Symposium (NDSS 2021)). Internet Society, San Diego (virtuel), United States. doi:10.14722/ NDSS.2021.24118

    work page arXiv 2021

  24. [24]

    Ralf’s Ramblings. 2025. There is no memory safety without thread safety. https: //www.ralfj.de/blog/2025/07/24/memory-safety.html

    work page 2025

  25. [25]

    Rasmussen and Michael A

    Rasmus V. Rasmussen and Michael A. Trick. 2008. Round robin scheduling – a survey.European Journal of Operational Research188, 3 (Aug. 2008), 617–636. doi:10.1016/j.ejor.2007.05.046

    work page doi:10.1016/j.ejor.2007.05.046 2008

  26. [26]

    Securego. 2024. GoSec : Golang static analyzer. https://github.com/securego/ gosec original-date: 2016-07-18T18:01:08Z

    work page 2024

  27. [27]

    Security-Research-Labs. 2026. srlabs/golibafl. https://github.com/srlabs/golibafl original-date: 2025-04-01T15:13:33Z

    work page 2026

  28. [28]

    GitHub Staff. 2024. Octoverse: AI leads Python to top language as the number of global developers surges. https://github.blog/news-insights/octoverse/octoverse- 2024/

    work page 2024

  29. [29]

    Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna

    work page

  30. [30]

    In Proceedings 2016 Network and Distributed System Security Symposium

    Driller: Augmenting Fuzzing Through Selective Symbolic Execution. In Proceedings 2016 Network and Distributed System Security Symposium. Internet Society, San Diego, CA. doi:10.14722/ndss.2016.23368

    work page doi:10.14722/ndss.2016.23368 2016

  31. [31]

    TinyGo-Org. 2019. Tinygo: Go compiler for small places. https://github.com/ tinygo-org/tinygo

    work page 2019

  32. [32]

    Manh Dat Tran, Lan Anh Nguyen, Hyung Tae Lee, Jeongyeup Paek, Sungrae Cho, and Yongseok Son. 2024. A Survey on Copy-on-Write File Systems. In 2024 15th International Conference on Information and Communication Technology Convergence (ICTC). 436–441. doi:10.1109/ICTC62082.2024.10826721 ISSN: 2162- 1241

    work page doi:10.1109/ictc62082.2024.10826721 2024

  33. [33]

    Kevin Valerio. 2025. Detect Go’s silent arithmetic bugs with go- panikint. https://blog.trailofbits.com/2025/12/31/detect-gos-silent-arithmetic- bugs-with-go-panikint/

    work page 2025

  34. [34]

    Dmitry Vyukov. 2024. dvyukov/go-fuzz: randomized testing for Go. https: //github.com/dvyukov/go-fuzz original-date: 2015-04-15T13:07:50Z

    work page 2024

  35. [35]

    Fish Wang and Yan Shoshitaishvili. 2017. Angr - The Next Generation of Binary Analysis. In2017 IEEE Cybersecurity Development (SecDev). IEEE, 8–9. doi:10. 1109/SecDev.2017.14

    work page 2017

  36. [36]

    Tielei Wang, Tao Wei, Zhiqiang Lin, and Wei Zou. [n. d.]. IntScope: Automati- cally Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution. ([n. d.])

    work page

  37. [37]

    Hui Xu, Yangfan Zhou, Yu Kang, and Michael R. Lyu. 2017. Concolic Execution on Small-Size Binaries: Challenges and Empirical Study. In2017 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE/IFIP, 181–188. doi:10.1109/DSN.2017.11

    work page doi:10.1109/dsn.2017.11 2017

  38. [38]

    Tao Zhang, Pan Wang, and Xi Guo. 2020. A Survey of Symbolic Execution and Its Tool KLEE.Procedia Computer Science166 (Jan. 2020), 330–334. doi:10.1016/j. procs.2020.02.090

    work page doi:10.1016/j 2020