Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Exposing Go's Hidden Bugs: A Novel Concolic Framework

Karolina Gorna, Nicolas Iooss, Yannick Seurin, Rida Khatoun

TL;DR

This work presents Zorya, a concolic execution framework for Go binaries that uses Ghidra's P-Code as a granular intermediate representation. By building a custom P-Code generator/parser and a Rust-based engine with SMT support, Zorya enables concrete+symbolic analysis to reveal runtime panics and logic bugs beyond traditional testing. The approach demonstrates high accuracy outside Ghidra, detects all targeted TinyGo panics, and extends to C binaries, with plans to model multi-threaded Go programs and improve invariant-driven exploration. The work offers a practical pathway to deeper vulnerability discovery in Go ecosystems and cross-language binaries, potentially impacting security tooling for infrastructure and blockchain software.

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.

Exposing Go's Hidden Bugs: A Novel Concolic Framework

TL;DR

This work presents Zorya, a concolic execution framework for Go binaries that uses Ghidra's P-Code as a granular intermediate representation. By building a custom P-Code generator/parser and a Rust-based engine with SMT support, Zorya enables concrete+symbolic analysis to reveal runtime panics and logic bugs beyond traditional testing. The approach demonstrates high accuracy outside Ghidra, detects all targeted TinyGo panics, and extends to C binaries, with plans to model multi-threaded Go programs and improve invariant-driven exploration. The work offers a practical pathway to deeper vulnerability discovery in Go ecosystems and cross-language binaries, potentially impacting security tooling for infrastructure and blockchain software.

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.

Paper Structure

This paper contains 14 sections, 1 figure, 3 tables.

Table of Contents

  1. Introduction
  2. Background: Securing Go Code
  3. Overview of the contributions
  4. Core contributions
  5. Proof-of-Concept Functionalities
  6. Methodology
  7. Concolic execution and Go analysis
  8. P-Code as Intermediate Representation
  9. Bugs detection
  10. Running example
  11. Evaluation
  12. Discussion and Vision
  13. Related Work
  14. Conclusion

Figures (1)

  • Figure 1: Overview of the contributions, including Zorya, Pcode-generator and Pcode-parser.