arXiv:2605.03492v1 [cs.CR] 5 May 2026
From TinyGo to gc Compiler: Extending Zorya’s Concolic Framework to Real-World Go Binaries Karolina Gorna
Nicolas Iooss
Yannick Seurin
Telecom Paris and Ledger Donjon Paris, France [email protected]
Ledger Donjon Zurich, Switzerland [email protected]
Ledger Donjon Paris, France [email protected]
Rida Khatoun
Keith Makan
Telecom Paris Palaiseau, France [email protected]
University of the Western Cape Cape Town, South Africa [email protected]
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.
CCS Concepts • Software and its engineering → Software verification and validation; • Security and privacy → Software security engineering.
Keywords Concolic execution, Go, Binary analysis, SMT solver, Overlay execution, Vulnerability detection, P-Code ACM Reference Format: Karolina Gorna, Nicolas Iooss, Yannick Seurin, Rida Khatoun, and Keith Makan. 2026. From TinyGo to gc Compiler: Extending Zorya’s Concolic Framework to Real-World Go Binaries. In Proceedings of The 30th International Conference on Evaluation and Assessment in Software Engineering (EASE 2026). ACM, New York, NY, USA, 6 pages. https://doi.org/xx.xxxx/ xxxxxxx.xxxxxx
1
Introduction
The Go programming language is widely adopted in cloud infrastructure, container orchestration (e.g., Kubernetes [4]), and
This work is licensed under a Creative Commons Attribution 4.0 International License. EASE 2026, Glasgow, United Kingdom © 2026 Copyright held by the owner/author(s). ACM ISBN xxx-x-xxxx-xxxx-x/2026/xx https://doi.org/xx.xxxx/xxxxxxx.xxxxxx
blockchain systems [28]. Security analysis of Go binaries remains difficult because the standard gc compiler produces executables with a complex runtime. This runtime manages goroutines, garbage collection, and preemptive scheduling through multiple OS threads. Existing symbolic execution tools such as KLEE [37], angr [34], and Radius2 [1] were designed for C/C++ and do not model Gospecific mechanisms. Furthermore, most of them use LLVM as an intermediate representation (IR), to which Go doesn’t compile fully. Zorya was introduced by Gorna et al. [18, 19] as a concolic execution framework, that combines concrete and symbolic execution for code exploration and vulnerability detection. It lifts binaries to Ghidra’s P-Code intermediate representation [21] and targets Go binaries compiled with TinyGo [30], a compiler that produces single-threaded executables with a minimal runtime. The second version added a panic-reachability gating filter to focus symbolic reasoning on panic-reachable paths. However, TinyGo is rarely used in production. Real-world Go projects are compiled with gc [9], the standard Go toolchain. A gc binary differs from a TinyGo binary in several fundamental ways. First, the gc runtime spawns multiple OS threads at startup to host goroutine scheduling. Second, the runtime uses cooperative and asynchronous preemption: a sentinel value in the goroutine descriptor forces function prologues to yield control. Third, the binary invokes Linux VDSO functions for time queries, which are memory-mapped at runtime and absent from the ELF file. These differences prevented the previous versions of Zorya from analyzing gc binaries. This paper presents the extensions required to bridge this gap. Specifically, our contributions are as follows: • Concolic analysis of gc-compiled binaries: This work extends Zorya to analyze multi-threaded binaries produced by the standard Go compiler.1 • Real-world Go vulnerability dataset: A corpus of 11 realworld Go vulnerabilities from production projects, with reproduction workflows and triggering inputs.2 • Comparative evaluation: Zorya is evaluated against seven state-of-the-art tools (three static analyzers, two fuzzers, two binary-level symbolic executors) and detects 7/11 bugs, including a silent integer overflow no other tool finds without an oracle.3 1 https://github.com/Ledger-Donjon/zorya 2 https://github.com/Ledger-Donjon/logic_bombs_go 3 https://github.com/Ledger-Donjon/zorya-evaluation
Preprint. Accepted in the 30th ACM International Conference on Evaluation and Assessment in Software Engineering (EASE 2026)
Gorna et al.
EASE 2026, Tue 9 - Fri 12 June 2026, Glasgow, United Kingdom
Assumptions. Zorya assumes correct Ghidra disassembly; execution halts if jumps target unidentified code. We mitigate this via preprocessing and compiler predictable layouts. Currently, Zorya analyzes non-interactive binaries requiring inputs at initialization.
2 Background 2.1 Symbolic Execution and its Limits in Go Given a program 𝑃 with input variables 𝑋 = {𝑥 1, . . . , 𝑥𝑛 }, symbolic execution replaces each 𝑥𝑖 with a symbolic value 𝑠𝑖 and treats operations symbolically. At each branch on a predicate 𝜑 (𝑠 1, . . . , 𝑠𝑛 ), the engine forks: one path adds 𝜑 to the path condition Π, while the other adds ¬𝜑. An SMT solver [6] then checks if Π is solvable to see if a path is possible. To reduce path explosion—where the number of paths grows too fast for the solver—concolic execution performs both concrete and symbolic execution. It uses real values to drive the program’s flow while keeping symbolic expressions to check other paths. The Go runtime contains roughly 300,000 lines of code [12] and creates major hurdles for symbolic tools. Its complex, versionspecific structures for goroutines, garbage collection, and stack management often trigger path explosion before the tool even reaches the user’s code. Additionally, many engines do not model the low-level OS calls (like futex or clone) that Go needs. As a result, while tools like BINSEC [8] and SymQEMU [23] offer some binary-level support, other frameworks like KLEE, angr and Radius2 often fail to run gc-compiled binaries at all [19].
2.2
Go Analysis Tools
The Go ecosystem provides several analysis tools. We briefly describe the most used ones and those used in our evaluation. Static analyzers. go vet [17] is the standard static checker shipped with the Go toolchain; it detects common mistakes such as unreachable code and incorrect format strings. staticcheck [16] extends go vet with additional style and correctness checks. Then, gosec [26] focuses on security patterns; its G115 rule flags typeconversion overflows (e.g., uint64 to int) but does not check sametype arithmetic overflows. govulncheck [13] queries the Go advisory database and reports known CVEs affecting the binary’s dependencies. nilaway [20] performs inter-procedural nil-flow inference to detect potential nil-pointer dereferences. Fuzzers. go test -fuzz [11] is the built-in coverage-guided fuzzer introduced in Go 1.18. It replaced the earlier go-fuzz tool [33], which is now deprecated. GoLibAFL [27] is a coverage-guided fuzzer based on LibAFL; it instruments Go binaries at the source level and achieves higher throughput than the built-in fuzzer. Both fuzzers require a manually written harness for each tested function. Support tools. Go also ships with debugging and inspection utilities. Delve [10] is the standard Go debugger, aware of goroutines and Go types. go tool nm [14] lists the symbols in a compiled binary, which is useful for locating functions and understanding binary layout. These tools are used alongside the analyzers above.
2.3
The Zorya Concolic Framework
Zorya is a concolic execution engine for analyzing compiled binaries. It lifts x86-64 binaries to Ghidra’s P-Code, a register-transfer intermediate representation with approximately 70 opcodes. Each
P-Code instruction is executed with both a concrete value (from a gdb memory dump) and a symbolic expression (maintained by the Z3 SMT solver). The concrete value drives control flow; the symbolic expression accumulates constraints. In its initial version, Zorya supported only TinyGo-compiled Go binaries. TinyGo produces single-threaded executables with a cooperative scheduler and no preemption. The runtime is small, and most system interactions are direct syscalls. This simplified environment allowed Zorya to execute binaries end-to-end without modeling thread management or complex runtime internals. The second version introduced a panic-reachability gating filter that uses a precomputed reverse call graph to skip branches that cannot reach a panic site, yielding 1.8–3.9× speedups. In this paper, we further introduce overlay path analysis, a copyon-write mechanism [31] that executes the untaken branch of a conditional to detect vulnerabilities such as null-pointer dereferences and integer overflows, as illustrated in Figure 1.
3
Related Work
Selective path exploration. Classical symbolic execution forks the full state at every branch [2]. SAGE [15] negates collected constraints offline without forking; S2E [5] uses copy-on-write snapshots to reduce fork cost; Driller [29] invokes concolic execution only when a fuzzer stalls. Zorya’s overlay shares S2E’s copy-onwrite principle but at a finer granularity: it explores the untaken branch for a bounded number of instructions, then discards the overlay. Our evaluation uses BINSEC and SymQEMU instead, as they operate directly on Linux ELF binaries—SAGE targets Windows PE, S2E requires a full VM image, and Driller depends on AFL instrumentation. Multi-threaded symbolic execution. Cloud9 [3] extends KLEE to model pthread primitives and explore thread interleavings for concurrency-bug detection. Zorya addresses a different problem: the Go runtime spawns OS threads before user code runs, and the analysis must manage them—restoring state from dumps and scheduling execution—so that the concolic engine can reach userlevel functions. Integer overflow detection. IntScope [35] detects overflows in x86 binaries via symbolic execution; IOC [7] instruments C/C++ source to catch undefined integer behavior at runtime. Both target C/C++, where overflows are undefined. In Go, unsigned arithmetic wraps silently by specification. The closest contemporary effort, go-panikint [32], modifies the Go compiler to turn silent overflows into explicit panics for fuzzers. Positioning. Prior work addresses each of these aspects in isolation; Zorya combines fine-grained overlay exploration, multi-thread initial-state recovery, and silent-overflow detection for Go binaries.
4 Overlay Concolic Execution 4.1 Copy-on-Write State A key challenge in concolic execution is reasoning about paths not taken by the concrete trace. Classical approaches fork the entire state at each branch, leading to exponential growth [2]. Zorya instead uses an overlay mechanism inspired by copy-on-write semantics: when a conditional branch involves tracked symbolic variables, Zorya creates a lightweight overlay for the untaken path. Reads
Preprint. Accepted in the 30th ACM International Conference on Evaluation and Assessment in Software Engineering (EASE 2026)
From TinyGo to gc Compiler: Extending Zorya’s Concolic Framework to Real-World Go Binaries
EASE 2026, Tue 9 - Fri 12 June 2026, Glasgow, United Kingdom
Figure 1: Overview of Zorya workflow, including AST exploration and Overlay Concolic Execution. Note: At each conditional branch (CBranch), the path not taken concretely is analyzed. For Go binaries, the AST is first explored from the corresponding node to locate panic, fatal, or abort call sites. If one is found, the SMT solver checks whether satisfying variable assignments exist (function or binary arguments, depending on the mode), indicating a potential vulnerability. Then, for all binary types, an overlay concolic execution is performed over the next 15 instructions to detect vulnerabilities that may occur without triggering a runtime panic. This Analyzer Routine is applied to both the taken and not-taken paths; if the check succeeds, the solver reports the feasibility of the faulty path. The state is then restored and concolic execution resumes.
4.3
first consult the overlay and fall through to the base state on a miss; writes go exclusively to the overlay. This avoids cloning the full execution state, which can exceed 1 GiB for gc binaries with large heaps, so only registers and memory bytes actually modified during overlay execution incur a copy.
4.2
We illustrate Zorya’s integer overflow detector on Go-Ethereum’s memoryGasCost function (geth v1.6.0), shown in Listing 1. The guard on line 3 prevents toWordSize from overflowing, but does not prevent the squaring on line 7 from wrapping: for large inputs the true product exceeds 64 bits and Go silently truncates it, letting an attacker allocate massive EVM memory while paying near-zero gas. Zorya runs this function with concrete arguments that follow a valid, non-overflowing path. The overflow is detected entirely through the symbolic expressions attached to each variable. Ghidra lifts the multiplication to a P-Code INT_MULT instruction.
Overlay Execution Protocol
The overlay execution proceeds as follows: (1) Save the executor’s mutable state: unique temporary variables, current address, call stack depth, freed stack frames, and the null-check cache. (2) Set the overlay’s instruction pointer (RIP) to the untaken branch target. (3) Execute up to 𝑁 P-Code instruction blocks (default 𝑁 =15) using the standard executor, which transparently reads from and writes to the overlay. (4) At each instruction, check for vulnerability patterns before execution: null-pointer dereferences (loads and stores) and integer overflows; and, not yet evaluated, division by zero and accesses to freed stack frames. (5) On finding a vulnerability, record it and return. On reaching a RETURN, a loop, or the depth limit, stop. (6) Discard the overlay. Restore all saved state so the main execution path is unaffected. The null-check cache deserves special attention. During overlay execution, SAT results (confirmed nullable pointers) are retained because the vulnerability is real regardless of the path. UNSAT results (proven non-null under the real path’s constraints) are cleared because the negated branch may make previously-safe pointers nullable.
Illustrative Example: Overlay Detection of an Integer Overflow
func memoryGasCost ( mem * Memory , newMemSize uint64 ) ( uint64 , error ) { 3 if newMemSize > MaxUint64 -32 { 4 return 0 , errGasUintOverflow 5 } 6 newMemSizeWords := toWordSize ( newMemSize ) 7 square := newMemSizeWords * newMemSizeWords 8 linCoef := newMemSizeWords * MemoryGas 9 quadCoef := square / QuadCoeffDiv 10 fee := linCoef + quadCoef - mem . lastGasCost 11 return fee , nil 12 } 1 2
Listing 1: Vulnerable memoryGasCost in Go-Ethereum v1.6.0 . At that point, the overflow checker widens both 64-bit symbolic operands to 128 bits and queries Z3: if the upper half of the product can be non-zero, the multiplication can silently wrap. Z3 confirms the overflow in 0.39 s and returns a concrete witness. No other tool in our evaluation can detect this bug without relying on a manually written oracle (Table 1).
Preprint. Accepted in the 30th ACM International Conference on Evaluation and Assessment in Software Engineering (EASE 2026)
Gorna et al.
EASE 2026, Tue 9 - Fri 12 June 2026, Glasgow, United Kingdom
Table 1: Evaluation of Go toolchain tools, symbolic execution tools and Zorya against a real-world Go bugs dataset. ✓ indicates caught vulnerability; empty cells indicate the vulnerability was not caught. Size (MB)
staticcheck
gosec
nilaway
Technique used
Static Analysis
Static Analysis
Static Analysis
Fuzzing
Needs Additional Files or Automated Execution (Auto.) ?
Auto.
Auto.
Auto.
Outputs the execution trace of each instruction ?
No
No
No
Nil Pointer Dereference
Integer Overflow
Index Out of Bounds
go-fuzz
GoLibAFL
Zorya
BINSEC
SymQEMU
KLEE
Fuzzing
Concolic Execution
Symbolic Execution
Symbolic Execution
Symbolic Execution
Harness
Harness
Auto.
Init Files
Auto.
LLVM bitcode
No
No
Yes
Yes
No
Yes
.
.
.
.
.
.
.
.
.
kubectl-2025
106
.
.
.
✓
✓
✓
kubelet-2025
121
.
.
.
✓
✓
✓
geth-graphql-2025
71
.
.
✓
✓
✓
✓
geth-tracers-2024
66
.
.
✓
✓
✓
✓
p224-elliptic-2021 fasthttp-2020 tendermint-2018
3.3 6.5 34
. . .
. . .
. . .
. . .
. . .
. . .
evm-gascost-2017
19
.
.
.
.
.
✓
kube-sm-2025
87
.
.
.
✓
✓
.
coredns-2025
110
.
.
.
✓
✓
✓
goprotobuf-2013
3.8
.
.
.
✓
✓
✓
Table 2: Overlay activity across the 11 binaries. (a) side bug caught during overlay execution at the indicated depth; (b) depth 15 reached, then an AST scan + Z3 confirmed a panic site on the same path; (c) no side bug. Binary
Side bug
(a) Caught during overlay execution kubelet-2025 Concrete nil deref geth-graphql-2025 Concrete nil write
Opcode
Depth
LOAD STORE
3 2
(b) Depth limit reached, confirmed on same path kubelet-2025 Reachable panic CBRANCH geth-tracers-2024 Reachable panicIndex CBRANCH kube-sm-2025 Reachable panic CBRANCH goprotobuf-2013 OOB slice access LOAD tendermint-2018 Nil pointer deref LOAD tendermint-2018 Reachable panic ( × 3) CBRANCH
15 15 15 15 15 15
(c) No side bug: kubectl-2025, coredns-2025, evm-gascost-2017, fasthttp-2020, p224-elliptic-2021
Table 3: Average detection time per tool, based on the 8 Go vulnerability cases found. Tool nilaway go test -fuzz GoLibAFL Zorya
Avg. Detection Time ≈2 s 0.18 s ≈7 s 16.5 min
5 Implementation 5.1 Compiler-Aware Exploration Zorya adapts its vulnerability detection strategy based on the compiler. TinyGo inserts explicit calls to runtime.nilpanic() at nil
Analyzer routine (LOAD check) Analyzer routine (LOAD check) Panic-reach. (nilPanic) Analyzer routine (LOAD check)
.
.
.
. . . Analyzer routine (INT_MULT check)
. . .
. . .
. . .
.
.
.
. Panic-reach. (panicIndex) Panic-reach. (panicIndex)
.
.
.
.
.
.
.
.
.
checks, so AST exploration detects these panics. Overlay analysis is also enabled for TinyGo binaries because they can contain undefined behavior that do not trigger explicit panic calls. The gc compiler uses CPU traps for implicit nil dereferences (signalbased panics) and explicit panic calls; both detection methods are therefore required [24]. Since Zorya operates on Ghidra’s P-Code, a language-agnostic intermediate representation, it can also analyze C and C++ binaries. These binaries lack Go’s panic infrastructure and rely solely on overlay execution for vulnerability detection.
5.2
Multi-Thread State Management
Zorya manages all OS threads present in the target binary. At initialization, a gdb script dumps the register state, thread-local storage bases, and backtrace of every thread. Each thread is classified by its backtrace: the thread executing main.main is marked as the main thread, the runtime.sysmon thread is marked as the system monitor, and all others are marked as waiting. The scheduler supports two policies. In main-only mode, only the main thread executes. In round-robin mode [25], threads switch cooperatively at function call boundaries after a configurable number of P-Code instructions. Thread switches occur only at function calls, mirroring Go’s cooperative preemption model.
5.3
Correctness, Soundness and Completeness
Zorya is sound for the concrete path: every instruction is executed with its real concrete value, and symbolic expressions mirror the concrete operations. On overlay paths, Zorya is best-effort and may miss vulnerabilities beyond the depth limit or produce false positives when under-constrained symbolic variables yield satisfying but practically unreachable assignments. The tool is incomplete by design: it follows a single concrete trace and explores untaken branches to a bounded depth, since complete path exploration is
Preprint. Accepted in the 30th ACM International Conference on Evaluation and Assessment in Software Engineering (EASE 2026)
From TinyGo to gc Compiler: Extending Zorya’s Concolic Framework to Real-World Go Binaries
infeasible for gc binaries whose runtime alone contains hundreds of thousands of basic blocks.
6
Evaluation
We evaluate Zorya on real-world Go binaries compiled with gc, measuring detection accuracy, detection scope, and comparison with existing tools, under the following research questions: • RQ1: Can Zorya detect vulnerabilities in real-world multithreaded binaries compiled with the Go compiler? • RQ2: Can Zorya detect vulnerabilities not related to runtime panics? • RQ3: How does Zorya compare to other Go tools and symbolic execution tools regarding vulnerability detection?
6.1
Experimental Setup
Experiments ran on 64-bit Linux with an Intel Core i9-12900K (24 threads, 3.2 GHz) and 125 GiB of RAM, using Zorya v0.0.5 and Ghidra v12. To ensure an accurate reproduction of the bugs, each target was compiled using the specific Go toolchain version that was current at the time its respective fix commit was reported. We evaluated Zorya against staticcheck, gosec, nilaway, go test -fuzz, GoLibAFL, BINSEC v0.10.1, and SymQEMU. All tools were used with default configurations; where no versioned release was available, we used the latest code from the respective repositories as of January 2026.
6.2
Benchmark
Our benchmark includes 11 real-world vulnerabilities from production Go projects, inspired by the Logic Bomb [36] approach of focused programs isolating specific runtime failures. Each vulnerability was derived from an actual bug fix: we identified the root cause from the commit message and patch, then compiled the vulnerable version of the project. For standalone applications we used the full production binary; for libraries, we compiled an example program from the project’s official repository that exercises the faulty code path. All binaries are multi-threaded gc compilations. The vulnerabilities span three classes: (i) Nil pointer dereferences, 4 cases: uninitialized struct fields or unchecked pointers dereferenced before validation, from Kubernetes and Go-Ethereum. (ii) Integer overflows, 4 cases: silent arithmetic wrapping in unsigned or signed multiplication and accumulation, from GoEthereum, Tendermint, fasthttp, and Go’s standard library. (iii) Index out-of-bounds, 3 cases: empty slices accessed without length checks or overflow-induced negative indices, from kubestate-metrics, CoreDNS, and golang/protobuf.
6.3
Results and Analysis
Table 1 summarizes the detection results across all 11 vulnerabilities and eight tools. RQ1: Multi-threaded gc binary analysis. Zorya correctly dumps the register state, TLS bases, and backtraces of all OS threads spawned by the gc runtime. It retrieves the runtime’s internal offsets (goroutine descriptor, stack guard, processor struct) and neutralizes preemption before entering the target function. All 11 runs used the main-only scheduling policy, which restricts concolic execution to the main thread. This strategy is well suited to function-mode
EASE 2026, Tue 9 - Fri 12 June 2026, Glasgow, United Kingdom
analysis: it enables continuous exploration of the function body without interruption from the garbage collector, the system monitor, or other runtime activities. Under this configuration, Zorya detects 7 of 11 vulnerabilities: four nil-pointer dereferences, one integer overflow, and two index out-of-bounds panics. Finding 1: Zorya successfully analyzes gc-compiled multithreaded Go binaries and detects 7 out of 11 real-world vulnerabilities using function-mode analysis with main-only scheduling. RQ2: Detection beyond runtime panics. Of the 7 primary detections, 4 are caught by the Analyzer Routine on the taken path, including the silent INT_MULT overflow that no other tool finds, and 3 by AST panic-reachability on the not-taken branch. Overlay execution further surfaces 10 side findings across 6 binaries (Table 2): 2 caught directly within the 15-instruction depth exploration (kubelet at depth 3; geth-graphql at depth 2), and 8 via an AST fallback once the exploration depth is reached, suggesting it should be increased. All correspond to functions that accept nil pointers or nil-valued interfaces, a pattern permitted by Go but confirmed satisfiable and reachable by Z3. The 5 remaining binaries yield no side finding: p224-elliptic and fasthttp halt on heavy runtime helpers; the others reach depth 15 without exposing a new pattern. Finding 2: The 7 primary bugs are caught by the Analyzer Routine on the taken path (including the silent overflow unique to Zorya) or by the AST panic-reachability. Overlay execution additionally surfaces side issues in 2 binaries. RQ3: Comparison with other tools. Table 1 shows that static analyzers (staticcheck, gosec) detect none of the 11 bugs. gosec’s G115 rule flags type-conversion overflows (e.g., uint64 to int) but misses same-type arithmetic overflows. nilaway finds two nilpointer dereferences in Go-Ethereum but cannot analyze Kubernetes packages due to dependency resolution failures. BINSEC and SymQEMU detect none of the 11 bugs; both lack support for Go’s runtime primitives. Fuzzers (go test -fuzz and GoLibAFL) are strong at detecting crash-producing bugs but require a harness for each tested function. They also detect kube-sm-2025, which Zorya misses: the vulnerable path traverses runtime.memmove, whose symbolic execution exhausts resources before reaching the fault site. For found bugs, fuzzers average a few seconds (Table 3), whereas Zorya averages 16.5 minutes because it executes every instruction symbolically rather than only exploring the AST for known bug patterns, but in return produces an exact instruction-level execution trace that fuzzers do not provide. Finding 3: Function-mode analysis is essential for complex realworld binaries: Zorya is slower than fuzzers but yields a full instruction-level trace and detects silent vulnerabilities without oracles or harnesses.
7
Discussion, Limits and Improvements
Symbolic analysis. Reaching a deep bug requires executing every preceding instruction. Symbolic summaries for heavy runtime helpers and lightweight checkpointing are the two natural mitigations. Extending symbolization to local variables would also broaden the detectable surface.
Preprint. Accepted in the 30th ACM International Conference on Evaluation and Assessment in Software Engineering (EASE 2026)
Gorna et al.
EASE 2026, Tue 9 - Fri 12 June 2026, Glasgow, United Kingdom
Overlay Concolic Execution. The exploration depth, fixed to 15 instructions, warrants a more principled calibration. This approach is particularly suited to paths gated by nested conditionals. Evaluation dataset and concurrency. The evaluation binaries belong to the cloud and blockchain ecosystems and have over 5,000 GitHub stars. Issues were selected to cover vulnerability classes within Zorya’s known detection scope. The round-robin scheduler has not yet been evaluated against concurrency-bug classes. Additional vulnerability patterns (e.g., division by zero, use-after-free) can be supported by extending the set of inspected P-Code operations. A more extensive evaluation on C corpora is planned [19]. Other tools. BINSEC requires symbolic support for additional syscalls and CPU instructions to handle the Go runtime. SymQEMU would benefit from support for Go’s cooperative preemption and multi-threaded initialization. Tools such as KLEE or SymCC [22] require a functional Go-to-LLVM-IR compiler front-end. This study is limited to deterministic tools. It would be relevant to evaluate the corpus with machine-learning models for bug detection, but the approach would be fundamentally different.
8
Conclusion
This paper extends Zorya to binaries compiled with the gc compiler. Of the 7 primary detections, 4 are caught by the Analyzer Routine on the taken paths and 3 by AST panic-reachability; overlay execution additionally surfaces 2 side findings on the not taken paths. The evaluation highlights a gap in the Go security landscape: static analyzers miss bugs requiring program-specific arithmetic or aliasing reasoning, fuzzers require per-function harnesses, and binary-level symbolic executors cannot yet handle the Go runtime. Zorya is slower than fuzzers but fully automatic and able to detect silent vulnerabilities that produce no crash signal. Future work targets broader symbolic coverage and concurrency-bug detection. Acknowledgment. The authors thank the anonymous reviewers for their valuable feedback and the Ledger Donjon, Telecom Paris, and University of the Western Cape teams for their support.
References [1] aemmitt ns. 2025. aemmitt-ns/radius2. https://github.com/aemmitt-ns/radius2 original-date: 2021-04-25T03:45:10Z. [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 [3] Stefan Bucur, Vlad Ureche, Cristian Zamfir, and George Candea. 2011. Parallel symbolic execution for automated real-world software testing. In Proceedings of the sixth conference on Computer systems (EuroSys ’11). Association for Computing Machinery, New York, NY, USA, 183–198. doi:10.1145/1966445.1966463 [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 [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 [6] Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools 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 [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 [8] Adel Djoudi and Sébastien Bardin. 2015. BINSEC: Binary Code Analysis with Low-Level Regions. In Tools 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
[9] Go-Community. [n. d.]. Introduction to the Go compiler. https://go.dev/src/cmd/ compile/README [10] Go-Community. 2026. go-delve/delve. https://github.com/go-delve/delve original-date: 2014-05-20T19:24:43Z. [11] Go-Community. 2026. Go Fuzzing - The Go Programming Language. https: //go.dev/doc/security/fuzz/ [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. govulncheck command [13] Go-Community. golang.org/x/vuln/cmd/govulncheck - Go Packages. https://pkg.go.dev/ golang.org/x/vuln/cmd/govulncheck [14] Go-Community. 2026. nm command - cmd/nm - Go Packages. https://pkg.go. dev/cmd/nm [15] Patrice Godefroid, Michael Y. Levin, and David Molnar. 2012. SAGE: Whitebox Fuzzing for Security Testing: SAGE has had a remarkable impact at Microsoft. Queue 10, 1 (Jan. 2012), 20–27. doi:10.1145/2090147.2094081 [16] Google. 2018. StaticCheck : Golang static analyzer. https://staticcheck.dev/docs/ [17] Google. 2024. GoVet : Golang static analyzer. https://pkg.go.dev/cmd/vet [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]. [19] Karolina Gorna, Nicolas Iooss, Yannick Seurin, and Rida Khatoun. 2026. Concolic Execution Optimized for Go Binaries using Ghidra’s P-Code. In Software Engineering and Management: Theory and Applications: Volume 18. Springer Nature, 161–176. Google-Books-ID: Q7LCEQAAQBAJ. [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/ [21] NSA. 2017. Ghidra. https://ghidra-sre.org/ [22] Sebastian Poeplau and Aurélien Francillon. 2020. Symbolic execution with { SymCC } : Don’t interpret, compile!. In 29th USENIX Security Symposium (USENIX Security 20). 181–198. [23] Sebastian Poeplau and Aurélien Francillon. 2021. SymQEMU: Compilation-based symbolic execution for binaries. In NDSS 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 [24] Ralf’s Ramblings. 2025. There is no memory safety without thread safety. https: //www.ralfj.de/blog/2025/07/24/memory-safety.html [25] Rasmus V. Rasmussen and Michael A. Trick. 2008. Round robin scheduling – a survey. European Journal of Operational Research 188, 3 (Aug. 2008), 617–636. doi:10.1016/j.ejor.2007.05.046 [26] Securego. 2024. GoSec : Golang static analyzer. https://github.com/securego/ gosec original-date: 2016-07-18T18:01:08Z. [27] Security-Research-Labs. 2026. srlabs/golibafl. https://github.com/srlabs/golibafl original-date: 2025-04-01T15:13:33Z. [28] GitHub Staff. 2024. Octoverse: AI leads Python to top language as the number of global developers surges. https://github.blog/news-insights/octoverse/octoverse2024/ [29] Nick Stephens, John Grosen, Christopher Salls, Andrew Dutcher, Ruoyu Wang, Jacopo Corbetta, Yan Shoshitaishvili, Christopher Kruegel, and Giovanni Vigna. 2016. 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 [30] TinyGo-Org. 2019. Tinygo: Go compiler for small places. https://github.com/ tinygo-org/tinygo [31] 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: 21621241. [32] Kevin Valerio. 2025. Detect Go’s silent arithmetic bugs with gopanikint. https://blog.trailofbits.com/2025/12/31/detect-gos-silent-arithmeticbugs-with-go-panikint/ [33] Dmitry Vyukov. 2024. dvyukov/go-fuzz: randomized testing for Go. https: //github.com/dvyukov/go-fuzz original-date: 2015-04-15T13:07:50Z. [34] Fish Wang and Yan Shoshitaishvili. 2017. Angr - The Next Generation of Binary Analysis. In 2017 IEEE Cybersecurity Development (SecDev). IEEE, 8–9. doi:10. 1109/SecDev.2017.14 [35] Tielei Wang, Tao Wei, Zhiqiang Lin, and Wei Zou. [n. d.]. IntScope: Automatically Detecting Integer Overflow Vulnerability in X86 Binary Using Symbolic Execution. ([n. d.]). [36] Hui Xu, Yangfan Zhou, Yu Kang, and Michael R. Lyu. 2017. Concolic Execution on Small-Size Binaries: Challenges and Empirical Study. In 2017 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE/IFIP, 181–188. doi:10.1109/DSN.2017.11 [37] Tao Zhang, Pan Wang, and Xi Guo. 2020. A Survey of Symbolic Execution and Its Tool KLEE. Procedia Computer Science 166 (Jan. 2020), 330–334. doi:10.1016/j. procs.2020.02.090
Preprint. Accepted in the 30th ACM International Conference on Evaluation and Assessment in Software Engineering (EASE 2026)