pith. machine review for the scientific record. sign in

arxiv: 2605.03492 · v1 · submitted 2026-05-05 · 💻 cs.CR · cs.SC· cs.SE

Recognition: unknown

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
Authors on Pith no claims yet

Pith reviewed 2026-05-07 15:48 UTC · model grok-4.3

classification 💻 cs.CR cs.SCcs.SE
keywords concolic executionbinary analysisGo gc compilervulnerability detectionZ3 SMT solverGhidra P-Codemulti-threadingsilent integer overflow
0
0 comments X

The pith

Zorya now handles multi-threaded gc-compiled Go binaries to detect 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 the Zorya concolic execution framework from single-threaded TinyGo binaries to multi-threaded binaries produced by Go's standard gc compiler. This extension uses gdb dump restoration for OS thread states, neutralization of runtime preemption, and overlay path analysis with copy-on-write semantics to reason over both taken and untaken branches. Evaluation covers 11 real-world vulnerabilities drawn from production projects including Kubernetes, Go-Ethereum, and CoreDNS. Zorya identifies seven of these bugs directly at the binary level, one of which is a silent integer overflow that other tools require a manually written oracle to surface. A sympathetic reader cares because this brings automated vulnerability detection to deployed Go software without source access.

Core claim

By restoring OS thread states from gdb dumps, neutralizing runtime preemption, and introducing overlay path analysis with copy-on-write semantics, Zorya detects seven out of eleven real-world vulnerabilities in gc-compiled Go binaries, including a silent integer overflow that no other evaluated tool finds without a manually written oracle.

What carries the argument

Overlay path analysis with copy-on-write semantics together with gdb-based OS thread state restoration to enable concolic reasoning over multi-threaded gc Go binaries lifted to Ghidra P-Code.

Load-bearing premise

Restoring OS thread states from gdb dumps and neutralizing runtime preemption preserves the original vulnerability behavior without introducing or masking bugs.

What would settle it

A concrete multi-threaded gc Go binary where the restored thread state causes the silent integer overflow to execute differently or remain undetected compared with native 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 / 1 minor

Summary. The manuscript describes the extension of the Zorya concolic execution framework from single-threaded TinyGo binaries to multi-threaded binaries compiled with Go's gc compiler. Key technical contributions include restoring OS thread states from gdb dumps, neutralizing runtime preemption, and implementing overlay path analysis with copy-on-write semantics for detecting silent vulnerabilities on untaken branches. The framework is evaluated on 11 real-world vulnerabilities from Kubernetes, Go-Ethereum, and CoreDNS, detecting 7 bugs including a unique silent integer overflow.

Significance. If the central claims hold, this work would advance binary-level vulnerability detection for Go programs, which are widely used in production systems. The ability to handle gc-compiled multi-threaded binaries without source code and detect silent issues via overlay analysis represents a meaningful engineering step beyond prior TinyGo support. The use of independently known vulnerabilities from real projects strengthens the evaluation's relevance.

major comments (2)
  1. Evaluation section: The abstract reports detection of 7 out of 11 vulnerabilities but provides no details on false-positive rates, exact test configurations, or how the 11 cases were selected, leaving the central claim only partially supported.
  2. Methodology section (state restoration and preemption neutralization): The approach of restoring OS thread states from gdb dumps and neutralizing runtime preemption is central to supporting multi-threaded binaries, yet no validation (e.g., comparison of execution traces with native runs or reproduction-rate data) is mentioned to confirm it preserves vulnerability manifestation and does not introduce spurious paths, raising a correctness risk for the extension.
minor comments (1)
  1. Abstract: The sentence 'including a silent integer overflow detects no other evaluated tool finds without a manually written oracle' contains a grammatical error and should be rephrased for clarity (e.g., 'including a silent integer overflow that no other evaluated tool finds without a manually written oracle').

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript. We address each major comment point by point below, providing the strongest honest defense of our work while committing to revisions that strengthen the paper without misrepresenting its content.

read point-by-point responses

  1. Referee: Evaluation section: The abstract reports detection of 7 out of 11 vulnerabilities but provides no details on false-positive rates, exact test configurations, or how the 11 cases were selected, leaving the central claim only partially supported.

    Authors: We agree that the evaluation presentation can be strengthened with additional details. The 11 cases were selected as independently reported, publicly known vulnerabilities from production Go projects (Kubernetes, Go-Ethereum, CoreDNS) to ensure real-world relevance rather than synthetic benchmarks; this selection process is described in the evaluation section but will be expanded into a dedicated subsection with explicit criteria and references to the original vulnerability reports. Exact test configurations, including binary versions, input seeds, and analysis parameters, are already specified in the evaluation but will be presented more systematically (e.g., via an expanded table). Regarding false-positive rates, Zorya is a targeted concolic tool that reasons over symbolic constraints to detect specific vulnerability classes; it does not perform broad scanning that would produce traditional FP rates. Detections are validated against ground-truth oracles for the known bugs, and the silent integer overflow case is uniquely identified without requiring a manual oracle. We will revise the evaluation section to include a discussion of our detection criteria and verification approach to better support the central claims. revision: yes

  2. Referee: Methodology section (state restoration and preemption neutralization): The approach of restoring OS thread states from gdb dumps and neutralizing runtime preemption is central to supporting multi-threaded binaries, yet no validation (e.g., comparison of execution traces with native runs or reproduction-rate data) is mentioned to confirm it preserves vulnerability manifestation and does not introduce spurious paths, raising a correctness risk for the extension.

    Authors: We acknowledge that explicit validation data would increase confidence in the correctness of the multi-threaded extension. The manuscript provides a detailed description of restoring OS thread states from gdb dumps and neutralizing runtime preemption via targeted modifications to the Go runtime scheduler, but we did not include quantitative validation such as trace comparisons or reproduction rates. We will add a new subsection (or expand the existing methodology) with reproduction-rate statistics for the seven detected vulnerabilities and, where feasible, side-by-side comparisons of key execution paths and thread states against native runs. These additions will directly address preservation of vulnerability manifestation and absence of spurious paths introduced by the state restoration techniques. revision: yes

Circularity Check

0 steps flagged

No circularity in empirical extension and evaluation

full rationale

The paper describes an engineering extension of Zorya to support gc-compiled multi-threaded Go binaries via gdb-based thread-state restoration, preemption neutralization, and overlay path analysis. Its central claims consist of empirical bug detections (seven out of eleven real-world cases from Kubernetes, Go-Ethereum, and CoreDNS) rather than any first-principles derivation, fitted-parameter predictions, or mathematical results. No equations, ansatzes, or uniqueness theorems are invoked; the evaluation uses externally known vulnerabilities as ground truth. Self-citation to prior Zorya work, if present, is not load-bearing for the reported detections. The work is therefore self-contained against independent benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on domain assumptions about Go runtime behavior and binary lifting fidelity rather than new mathematical axioms or fitted parameters.

axioms (2)
  • domain assumption Gdb dumps accurately capture the full OS thread state of a running gc-compiled Go binary at the moment of snapshot.
    Invoked when restoring thread states to enable multi-threaded concolic execution.
  • ad hoc to paper Neutralizing Go runtime preemption does not alter the reachability or manifestation of the target vulnerabilities.
    Required to make symbolic execution tractable on multi-threaded binaries.

pith-pipeline@v0.9.0 · 5465 in / 1349 out tokens · 41308 ms · 2026-05-07T15:48:25.822520+00:00 · methodology

Review history (2 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 · 14 canonical work pages

  1. [1]

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

    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

    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

  10. [10]

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

    2026

  11. [11]

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

    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

    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

    2026

  14. [14]

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

    2026

  15. [15]

    Levin, and David Molnar

    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/

    2018

  17. [17]

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

    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

    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/

    2023

  21. [21]

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

    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

    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

    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

    2024

  27. [27]

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

    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/

    2024

  29. [29]

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

  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

    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/

    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

    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

    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.])

  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