Pass the SALT 2026

Automated Vulnerability Detection in Go: Concolic Execution for Multi-Threaded Binaries
2026-06-30 , Amphitheater 122

Go powers critical infrastructure, but analyzing compiled Go binaries for security issues remains difficult in practice.

In this talk, we present Zorya, an open-source concolic analysis framework designed to detect vulnerabilities directly at the binary level, including bugs that do not immediately crash the program.

We will show how Zorya combines runtime state recovery, symbolic reasoning, and constraint solving with the Z3 SMT solver to analyze real-world Go targets. Attendees will learn where traditional approaches fall short, how Zorya helps uncover exploit-relevant paths, and how this can improve real security audit workflows.


This session presents Zorya end-to-end as a security analysis capability, with recent advances included as part of a broader system view.

What attendees will get:

  • How Zorya works in practice: concrete+symbolic execution over binary code, via Ghidra P-Code and Z3.
  • What makes it usable on real Go binaries: compiler/runtime-aware strategies for TinyGo and gc targets, including multi-threaded/runtime constraints.
  • Coverage beyond obvious crashes: overlay path analysis to inspect untaken paths and detect silent bugs without custom oracles.
  • Operational usage model: interactive mode, function-focused exploration, and campaign/fuzzer-driven workflows.
  • Evidence on real cases: vulnerability findings across real-world Go projects, with reproducible artifacts and lessons learned.

The talk is intended for offensive security practitioners, reverse engineers, and defenders who need practical methods to audit compiled Go software when source-level tooling is insufficient.

Website: https://zorya.karolinagorna.net
Project: https://github.com/Ledger-Donjon/zorya
Evaluation: https://github.com/Ledger-Donjon/zorya-evaluation

Karolina Gorna is a PhD candidate at Télécom Paris, conducting her research with the Ledger Donjon on vulnerability detection and formal methods. She holds an ANSSI ESSI certification and previously led KRYPTOSPHERE, a tech student association of over 500 members across France. When she is not chasing silent integer overflows, she organizes and competes in hackathons including NASA Space Apps Challenge and ETH Global. She has also delivered technical training for AFORP and MIT Professional Education, and enjoys bridging academic research with hands-on security practice.