Zorya is a concolic execution engine built in Rust. It translates binaries to Ghidra's P-Code, drives symbolic exploration with Z3, and finds vulnerabilities in compiled Go programs: from memory-safety panics to concurrency bugs surfaced by an event-driven plugin layer. This is a deterministic tool that records coverage and explored paths in real time.
Multi-layer filtering concentrates symbolic reasoning on panic-relevant paths, achieving 1.8–3.9× speedups by pruning 33–70% of irrelevant branches.
Zorya analyzes executables with symbols to help developers find bugs in the binaries they build before production deployment.
Zorya discovers bugs in two complementary ways: runtime panic-function checks, and de facto bug discovery through overlay concolic execution on alternative paths.
Ghidra's intermediate representation abstracts ISA specifics. Analyze x86_64, ARM, or any Ghidra-supported architecture through one engine.
Tested against go-ethereum (Geth), Kubernetes, Gin framework, Omni Network, and known CVEs including CVE-2022-30631.
Interactive guided mode for exploration, plus a fuzzer module for automated batch campaigns with JSON configs and timeout management.
The executor fires typed events: memory accesses, branches, calls, syscalls, thread events, panics, onto an event bus. Detectors subscribe only to what they need, hold private state, and return a verdict, so they extend analysis without touching the core.
Multi-threaded Go binaries are restored thread-by-thread from GDB, and plugin detectors reason over goroutine interleavings: data races, TOCTOU check-use windows, and send-on-closed-channel panics, each reported with the input that triggers it.
Fetching latest documentation from the repository...
Observes cross-thread memory accesses and lock-primitive calls, classifies each cell with vector-clock happens-before plus lockset analysis, and couples every race witness to the symbolic inputs, reporting whether it races for every input or only for a specific input class, with the triggering value.
Pairs a security-sensitive check (SO_PEERCRED, stat, access) with its later use and flags the exploitable window. Overlay concolic execution reaches checks gated behind attacker-influenced input and Z3-solves the triggering byte.
Tracks channel create, close and send, then flags a send on an already-closed channel: a deterministic panic when the close precedes the send in one goroutine, or a schedule-dependent race across goroutines, verified feasible with Z3.
The scheduler, a WaitGroup invariant checker, and a weak-memory-model detector are planned subscribers on the same bus. Volos originates from the zorya-volos work by Keith Makan / KMSEC and is ported onto the plugin layer.
