From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2026
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866910238505959424 |
|---|---|
| author | Gorna, Karolina Iooss, Nicolas Seurin, Yannick Khatoun, Rida Makan, Keith |
| author_facet | Gorna, Karolina Iooss, Nicolas Seurin, Yannick Khatoun, Rida Makan, Keith |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2605_03492 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries Gorna, Karolina Iooss, Nicolas Seurin, Yannick Khatoun, Rida Makan, Keith Cryptography and Security Symbolic Computation Software Engineering 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. |
| title | From TinyGo to gc Compiler: Extending Zorya's Concolic Framework to Real-World Go Binaries |
| topic | Cryptography and Security Symbolic Computation Software Engineering |
| url | https://arxiv.org/abs/2605.03492 |