Zorya: Automated Concolic Execution of Single-Threaded Go Binaries

Fuente: arXiv
Enregistré dans:
Détails bibliographiques
Auteurs principaux: Gorna, Karolina, Iooss, Nicolas, Seurin, Yannick, Khatoun, Rida
Format: Preprint
Publié: 2025
Sujets:
Accès en ligne:
Tags: Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
_version_ 1866914195440664576
author Gorna, Karolina
Iooss, Nicolas
Seurin, Yannick
Khatoun, Rida
author_facet Gorna, Karolina
Iooss, Nicolas
Seurin, Yannick
Khatoun, Rida
contents Go's adoption in critical infrastructure intensifies the need for systematic vulnerability detection, yet existing symbolic execution tools struggle with Go binaries due to runtime complexity and scalability challenges. In this work, we build upon Zorya, a concolic execution framework that translates Go binaries to Ghidra's P-Code intermediate representation to address these challenges. We added the detection of bugs in concretely not taken paths and a multi-layer filtering mechanism to concentrate symbolic reasoning on panic-relevant paths. Evaluation on five Go vulnerabilities demonstrates that panic-reachability gating achieves 1.8-3.9x speedups when filtering 33-70% of branches, and that Zorya detects all panics while existing tools detect at most two. Function-mode analysis proved essential for complex programs, running roughly two orders of magnitude faster than starting from main. This work establishes that specialized concolic execution can achieve practical vulnerability detection in language ecosystems with runtime safety checks.
format Preprint
id arxiv_https___arxiv_org_abs_2512_10799
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Zorya: Automated Concolic Execution of Single-Threaded Go Binaries
Gorna, Karolina
Iooss, Nicolas
Seurin, Yannick
Khatoun, Rida
Software Engineering
Programming Languages
Go's adoption in critical infrastructure intensifies the need for systematic vulnerability detection, yet existing symbolic execution tools struggle with Go binaries due to runtime complexity and scalability challenges. In this work, we build upon Zorya, a concolic execution framework that translates Go binaries to Ghidra's P-Code intermediate representation to address these challenges. We added the detection of bugs in concretely not taken paths and a multi-layer filtering mechanism to concentrate symbolic reasoning on panic-relevant paths. Evaluation on five Go vulnerabilities demonstrates that panic-reachability gating achieves 1.8-3.9x speedups when filtering 33-70% of branches, and that Zorya detects all panics while existing tools detect at most two. Function-mode analysis proved essential for complex programs, running roughly two orders of magnitude faster than starting from main. This work establishes that specialized concolic execution can achieve practical vulnerability detection in language ecosystems with runtime safety checks.
title Zorya: Automated Concolic Execution of Single-Threaded Go Binaries
topic Software Engineering
Programming Languages
url https://arxiv.org/abs/2512.10799