pith. sign in

arxiv: 2505.20183 · v1 · submitted 2025-05-26 · 💻 cs.SE · cs.CR

Exposing Go's Hidden Bugs: A Novel Concolic Framework

Karolina Gorna , Nicolas Iooss , Yannick Seurin , Rida Khatoun This is my paper

Pith reviewed 2026-05-19 12:48 UTC · model grok-4.3

classification 💻 cs.SE cs.CR
keywords concolic executionGo programming languageruntime panicssymbolic executionprogram analysisTinyGo compilerinvariant checkingsoftware security
0
0 comments X

The pith

Zorya combines concrete and symbolic execution on Ghidra P-Code to find runtime panics in Go programs.

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

The paper introduces Zorya, a methodology that pairs concrete execution with symbolic exploration to analyze Go programs more thoroughly than unit tests or fuzzing alone. It translates code into Ghidra's P-Code intermediate representation so that path exploration can uncover panics and check both generic and custom invariants. The authors show the approach works on the TinyGo compiler and note that the generic nature of P-Code opens the door to similar analysis for C and other languages. This targets gaps in handling Go's runtime and concurrency that earlier symbolic tools left open.

Core claim

The authors present Zorya as a concolic execution framework that uses Ghidra's P-Code to model Go execution paths, detect runtime panics in the TinyGo compiler, and verify both generic and custom invariants while mitigating path explosion through the mix of concrete and symbolic steps.

What carries the argument

Zorya, the concolic engine that lifts Go binaries or source to Ghidra P-Code for joint concrete-symbolic path exploration and panic/invariant checking.

If this is right

  • It can locate runtime panics in Go infrastructure and blockchain code that unit tests and fuzzers miss.
  • The same run can enforce both built-in safety checks and user-supplied invariants.
  • Because P-Code is language-independent, the framework can be applied to C programs without rewriting the core engine.
  • Execution logs produced by the tool become a base for later automated classification of vulnerability patterns.

Where Pith is reading between the lines

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

  • If the P-Code mapping proves reliable, the method could be applied to large concurrent Go servers to reduce the cost of manual security reviews.
  • Pairing Zorya with existing Go fuzzers might give higher coverage on code that mixes goroutines and channels.
  • Testing the tool on programs that trigger subtle data-race panics would reveal whether the IR faithfully captures scheduling nondeterminism.

Load-bearing premise

Ghidra's P-Code can represent Go's runtime and concurrency model without losing critical details about panics and thread behavior.

What would settle it

Run Zorya on a collection of Go programs that contain documented runtime panics and observe whether it misses any of them or produces results that contradict the actual execution trace.

Figures

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

Figure 1
Figure 1. Figure 1: Overview of the contributions, including [PITH_FULL_IMAGE:figures/full_fig_p002_1.png] view at source ↗
read the original abstract

The widespread adoption of the Go programming language in infrastructure backends and blockchain projects has heightened the need for improved security measures. Established techniques such as unit testing, static analysis, and program fuzzing provide foundational protection mechanisms. Although symbolic execution tools have made significant contributions, opportunities remain to address the complexities of Go's runtime and concurrency model. In this work, we present Zorya, a novel methodology leveraging concrete and symbolic (concolic) execution to evaluate Go programs comprehensively. By systematically exploring execution paths to uncover vulnerabilities beyond conventional testing, symbolic execution offers distinct advantages, and coupling it with concrete execution mitigates the path explosion problem. Our solution employs Ghidra's P-Code as an intermediate representation (IR). This implementation detects runtime panics in the TinyGo compiler and supports both generic and custom invariants. Furthermore, P-Code's generic IR nature enables analysis of programs written in other languages such as C. Future enhancements may include intelligent classification of concolic execution logs to identify vulnerability patterns.

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 paper presents Zorya, a concolic execution framework for Go programs that uses Ghidra's P-Code as an intermediate representation. It combines concrete and symbolic execution to explore paths, detect runtime panics in TinyGo-compiled code, and check generic as well as custom invariants, while claiming that the generic IR enables analysis of other languages such as C.

Significance. If the approach can be shown to work reliably, it would offer a pragmatic way to surface concurrency-related bugs and invariant violations in Go that are difficult to reach with unit tests or fuzzers alone. Reusing an existing decompiler IR for multi-language support is a practical engineering choice. However, the complete absence of any quantitative results, case studies, or comparisons in the manuscript prevents any assessment of whether these potential benefits are realized.

major comments (2)
  1. [Abstract] Abstract: the claim that the implementation 'detects runtime panics in the TinyGo compiler' is presented without any reported detection counts, false-positive rates, example traces, or comparison to baselines, which is load-bearing for the central claim of comprehensive evaluation.
  2. [Methodology] Methodology description: no account is given of how Go-specific runtime features (goroutine scheduling, channel semantics, defer/panic/recover propagation, interface dispatch) are reconstructed or approximated inside the P-Code-based concolic engine; without such reconstruction the IR is unlikely to preserve the behaviors needed for reliable panic and invariant detection.
minor comments (1)
  1. [Future work] The final paragraph on future work mentions 'intelligent classification of concolic execution logs' but provides no concrete proposal or reference to existing log-analysis techniques.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the thorough review and constructive feedback. The comments highlight important aspects for improving the clarity and completeness of our presentation of Zorya. We address each major comment below.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the claim that the implementation 'detects runtime panics in the TinyGo compiler' is presented without any reported detection counts, false-positive rates, example traces, or comparison to baselines, which is load-bearing for the central claim of comprehensive evaluation.

    Authors: We agree with the referee that the abstract claim would benefit from supporting quantitative evidence. The manuscript currently emphasizes the framework design and methodology, with the detection capability demonstrated through the implementation but without aggregated metrics. In the revision, we will include quantitative results from our experiments, such as the number of panics detected across test programs, false positive rates, sample traces, and comparisons to other tools. revision: yes

  2. Referee: [Methodology] Methodology description: no account is given of how Go-specific runtime features (goroutine scheduling, channel semantics, defer/panic/recover propagation, interface dispatch) are reconstructed or approximated inside the P-Code-based concolic engine; without such reconstruction the IR is unlikely to preserve the behaviors needed for reliable panic and invariant detection.

    Authors: We appreciate this feedback. While the manuscript describes the use of P-Code as IR for concolic execution, we recognize that more explicit details on modeling Go runtime features are needed. We will revise the methodology to include explanations of how goroutine scheduling is approximated via multi-threaded symbolic execution, channel semantics through symbolic buffers and synchronization, defer/panic/recover via state tracking for control flow, and interface dispatch using symbolic type resolution. revision: yes

Circularity Check

0 steps flagged

No circularity: high-level tool description with independent implementation claims

full rationale

The paper presents Zorya as a concolic execution methodology using Ghidra P-Code IR to detect panics and invariants in Go programs compiled with TinyGo. No equations, fitted parameters, predictions, or derivation chains appear in the abstract or described content. Claims rest on the engineering of the framework and its application rather than any self-referential reduction, self-citation load-bearing step, or ansatz smuggled from prior work. The central premise about P-Code's suitability is an assumption open to external validation rather than a result forced by the paper's own inputs. This is a standard non-circular tool paper.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the assumption that P-Code accurately models Go semantics and that concolic execution can be applied without prohibitive path explosion. No free parameters or invented physical entities are introduced.

axioms (1)
  • domain assumption Ghidra's P-Code provides a faithful intermediate representation for Go's runtime and concurrency features.
    Invoked when stating that P-Code enables comprehensive evaluation of Go programs.
invented entities (1)
  • Zorya framework no independent evidence
    purpose: Concolic execution system for vulnerability detection in Go using P-Code IR.
    The paper introduces this as a novel methodology; no independent falsifiable evidence outside the description is provided.

pith-pipeline@v0.9.0 · 5708 in / 1303 out tokens · 29466 ms · 2026-05-19T12:48:25.495347+00:00 · methodology

discussion (0)

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

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

39 extracted references · 39 canonical work pages

  1. [1]

    The go programming language

    Go-Community. The go programming language. [Online]. Available: https://go.dev/

    work page

  2. [2]

    A formal semantics for p-code,

    N. Naus, F. Verbeek, D. Walker, and B. Ravindran, “A formal semantics for p-code,” in Verified Software. Theories, Tools and Experiments. , A. Lal and S. Tonetta, Eds. Springer International Publishing, pp. 111–128

    work page

  3. [3]

    Tinygo: Go compiler for small places

    TinyGo-Org. Tinygo: Go compiler for small places. [Online]. Available: https://github.com/tinygo-org/tinygo

    work page

  4. [4]

    Empirical analysis of vulnerabilities life cycle in golang ecosystem,

    J. Hu, L. Zhang, C. Liu, S. Yang, S. Huang, and Y . Liu, “Empirical analysis of vulnerabilities life cycle in golang ecosystem,” in Proceedings of the IEEE/ACM 46th International Conference on Software Engineering , ser. ICSE ’24. Association for Computing Machinery, pp. 1–13. [Online]. Available: https://dl.acm.org/doi/10. 1145/3597503.3639230

    work page arXiv

  5. [5]

    Available: https://ghidra-sre.org/

    NSA, “Ghidra.” [Online]. Available: https://ghidra-sre.org/

    work page

  6. [6]

    Eagle and K

    C. Eagle and K. Nance, The Ghidra Book: The Definitive Guide . No Starch Press, google-Books-ID: RVz6DwAAQBAJ

    work page

  7. [7]

    GoSec : Golang static analyzer,

    Securego, “GoSec : Golang static analyzer,” original-date: 2016-07- 18T18:01:08Z. [Online]. Available: https://github.com/securego/gosec

    work page 2016

  8. [8]

    GoVet : Golang static analyzer

    Google. GoVet : Golang static analyzer. [Online]. Available: https: //pkg.go.dev/cmd/vet

    work page

  9. [9]

    StaticCheck : Golang static analyzer

    ——. StaticCheck : Golang static analyzer. [Online]. Available: https://staticcheck.dev/docs/

    work page

  10. [10]

    kisielk/errcheck: checking for unchecked errors in go code

    K. Kisiel, “kisielk/errcheck: checking for unchecked errors in go code.” original-date: 2013-02-24T22:32:02Z. [Online]. Available: https://github.com/kisielk/errcheck

    work page 2013

  11. [11]

    snyk/cli,

    Snyk, “snyk/cli,” original-date: 2015-10-30T11:36:00Z. [Online]. Available: https://github.com/snyk/cli

    work page 2015

  12. [12]

    Available: https://codeql.github.com/

    CodeQL, “CodeQL.” [Online]. Available: https://codeql.github.com/

    work page

  13. [13]

    dvyukov/go-fuzz: randomized testing for go,

    D. Vyukov, “dvyukov/go-fuzz: randomized testing for go,” original- date: 2015-04-15T13:07:50Z. [Online]. Available: https://github.com/ dvyukov/go-fuzz

    work page 2015

  14. [14]

    google/gofuzz : a library for populating go objects with random values,

    Google, “google/gofuzz : a library for populating go objects with random values,” original-date: 2014-07-31T16:21:29Z. [Online]. Available: https://github.com/google/gofuzz

    work page 2014

  15. [15]

    leanovate/gopter: the GOlang property TestER,

    Leanovate, “leanovate/gopter: the GOlang property TestER,” original- date: 2016-02-11T07:20:49Z. [Online]. Available: https://github.com/ leanovate/gopter

    work page 2016

  16. [16]

    trailofbits/krf: a kernelspace randomized faulter

    T. of Bits, “trailofbits/krf: a kernelspace randomized faulter.” original- date: 2018-12-16T20:28:15Z. [Online]. Available: https://github.com/ trailofbits/krf

    work page 2018

  17. [17]

    trailofbits/on-edge: a library for detecting certain improper uses of the defer, panic, and recover pattern in go programs

    ——, “trailofbits/on-edge: a library for detecting certain improper uses of the defer, panic, and recover pattern in go programs.” original- date: 2019-03-15T10:12:00Z. [Online]. Available: https://github.com/ trailofbits/on-edge

    work page 2019

  18. [18]

    Stallman, R

    R. Stallman, R. Pesch, and S. Shebs, Debugging with GDB: the GNU source-level debugger, tenth edition, for GDB version 8.1.50.20180116- git ed. Free Software Foundation

    work page

  19. [19]

    Sleigh-rs,

    R. Brand ˜ao, “Sleigh-rs,” original-date: 2022-03-30T17:31:34Z. [Online]. Available: https://github.com/rbran/sleigh-rs

    work page 2022

  20. [20]

    Z3: An efficient SMT solver,

    L. de Moura and N. Bjørner, “Z3: An efficient SMT solver,” in Tools and Algorithms for the Construction and Analysis of Systems , C. R. Ramakrishnan and J. Rehof, Eds. Springer, pp. 337–340

    work page

  21. [21]

    Go-ethereum

    Ethereum-Foundation. Go-ethereum. [Online]. Available: https://geth. ethereum.org/

    work page

  22. [22]

    gollvm: an LLVM-based go compiler

    Go-Community. gollvm: an LLVM-based go compiler. [Online]. Available: https://go.googlesource.com/gollvm/

    work page

  23. [23]

    Valgrind: a framework for heavyweight dynamic binary instrumentation,

    N. Nethercote and J. Seward, “Valgrind: a framework for heavyweight dynamic binary instrumentation,” vol. 42, no. 6, pp. 89–100. [Online]. Available: https://dl.acm.org/doi/10.1145/1273442.1250746

    work page doi:10.1145/1273442.1250746

  24. [24]

    BAP: A binary analysis platform,

    D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz, “BAP: A binary analysis platform,” in Computer Aided Verification, G. Gopalakrishnan and S. Qadeer, Eds. Springer, pp. 463–469

    work page

  25. [25]

    Dynamic analysis and debugging of binary code for security applications,

    L. Li and C. Wang, “Dynamic analysis and debugging of binary code for security applications,” in Runtime Verification, A. Legay and S. Bensalem, Eds. Springer, pp. 403–423

    work page

  26. [26]

    Icicle: A re-designed emulator for grey-box firmware fuzzing,

    M. Chesser, S. Nepal, and D. C. Ranasinghe, “Icicle: A re-designed emulator for grey-box firmware fuzzing,” in Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis , ser. ISSTA 2023. New York, NY , USA: Association for Computing Machinery, 2023, p. 76–88. [Online]. Available: https://doi.org/10.1145/3597926.3598039

    work page doi:10.1145/3597926.3598039 2023

  27. [27]

    Ghidra’s support for go

    NSA. Ghidra’s support for go. [Online]. Avail- able: https://github.com/NationalSecurityAgency/ghidra/tree/master/ Ghidra/Features/Base/data/typeinfo/golang

    work page

  28. [28]

    GhidraScripts for golang,

    T. A. R. Center, “GhidraScripts for golang,” original- date: 2023-04-18T07:26:02Z. [Online]. Available: https://github.com/ advanced-threat-research/GhidraScripts

    work page 2023

  29. [29]

    TinyGo’s panics codebase

    TinyGo-Org. TinyGo’s panics codebase. [Online]. Available: https: //github.com/tinygo-org/tinygo/blob/release/src/runtime/panic.go

    work page

  30. [30]

    MAAT: Dynamic symbolic execution and binary analysis framework,

    T. of Bits, “MAAT: Dynamic symbolic execution and binary analysis framework,” original-date: 2021-10-19T09:23:10Z. [Online]. Available: https://github.com/trailofbits/maat

    work page 2021

  31. [31]

    Haybale: a general-purpose symbolic execution engine written in rust,

    PLSysSec, “Haybale: a general-purpose symbolic execution engine written in rust,” original-date: 2019-06-18T00:00:21Z. [Online]. Available: https://github.com/PLSysSec/haybale

    work page 2019

  32. [32]

    SymSan: Time and space efficient concolic execution via dynamic data-flow analysis,

    R-Fuzz, “SymSan: Time and space efficient concolic execution via dynamic data-flow analysis,” original-date: 2021-07-01T00:48:53Z. [Online]. Available: https://github.com/R-Fuzz/symsan

    work page 2021

  33. [33]

    Angr - the next generation of binary analysis,

    F. Wang and Y . Shoshitaishvili, “Angr - the next generation of binary analysis,” in 2017 IEEE Cybersecurity Development (SecDev) , pp. 8–9. [Online]. Available: https://ieeexplore.ieee.org/abstract/document/ 8077799

    work page 2017

  34. [34]

    MIASM: Reverse engineering framework

    MIASM. MIASM: Reverse engineering framework. [Online]. Available: https://miasm.re/blog/

    work page

  35. [35]

    Radius2: fast symbolic execution with r2,

    aemmitt ns, “Radius2: fast symbolic execution with r2,” original- date: 2021-04-25T03:45:10Z. [Online]. Available: https://github.com/ aemmitt-ns/radius2

    work page 2021

  36. [36]

    Radare2: Libre reversing framework,

    Radare2-org, “Radare2: Libre reversing framework,” original-date: 2012- 07-03T07:42:26Z. [Online]. Available: https://github.com/radareorg/ radare2

    work page 2012

  37. [37]

    C. C. Center. GhiHorn: Path analysis in ghidra using SMT solvers. [Online]. Available: https://insights.sei.cmu.edu/blog/ ghihorn-path-analysis-in-ghidra-using-smt-solvers/

    work page

  38. [38]

    CERT kaiju binary analysis framework for GHIDRA,

    ——, “CERT kaiju binary analysis framework for GHIDRA,” original- date: 2021-03-19T18:40:48Z. [Online]. Available: https://github.com/ CERTCC/kaiju

    work page 2021

  39. [39]

    DUCKEE GO: Dynamic and user-friendly ConcoliK execution engine in GO

    C. Shao, G. Yin, and J. Restivo, “DUCKEE GO: Dynamic and user-friendly ConcoliK execution engine in GO.” [Online]. Available: https://css.csail.mit.edu/6.858/2018/projects/cshao-graceyin-jrestivo.pdf 6

    work page 2018