Our ongoing R&D portfolio includes sophisticated programmatic solutions aimed at scaling deep security analysis. KMSEC has direct experience in the European market building automation-driven web assessment tooling and research tools exemplified by contributions from KMSEC to the concolic execution framework, Zorya—designed to automatically hunt for race conditions and logic state flaws in compiled binaries using symbolic execution engines.
Zorya leverages advanced symbolic execution engines to explore program paths, identify complex logic vulnerabilities, and detect concurrency issues that are often missed by traditional static and dynamic analysis tools. This framework is a testament to our commitment to research-led security solutions.
- COTS Tested: Rigorously validated against production-grade Commercial Off-The-Shelf software to ensure the discovery of critical bugs in real-world enterprise environments.
- Concolically Enhanced Analysis: Leverages a sophisticated hybrid of concrete and symbolic execution to resolve deep path dependencies and navigate complex logic states.
- Unique Go-Specific Race Insight: Provides specialized forensic-level analysis into concurrency primitives and memory safety patterns unique to the Go language and its runtime.
- Thread-Aware Hybrid Happens-Before + Lockset Analysis: Implements multi-layered formal methodologies for high-precision and automated data race discovery.
- Rust Developed: Engineered from the ground up in Rust to deliver the performance and safety required for scaling symbolic reasoning over complex binaries.
Key Technologies & Concepts:
Symbolic Execution
Concolic Testing
Binary Analysis
Race Conditions
Logic Flaws
Rust
Go
BLACK HAT ASIA ARSENAL ➔
ZORYA-VOLOS GITHUB REPO ➔
Zorya in Research: Academic Publications
Go's adoption in critical infrastructure intensifies the need for systematic vulnerability detection. Existing symbolic execution tools struggle with Go binaries due to runtime complexity and scalability. This work introduces Zorya, a concolically enhanced analysis framework, developed in Rust, for Go binaries. Zorya translates binaries to Ghidra's P-Code, offering unique depth of insight into Go-specific race conditions via thread-aware hybrid Happens-Before and Lockset analysis. It addresses scalability by detecting bugs in concretely not taken paths and employing multi-layer filtering. Zorya has been rigorously tested against COTS software.
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.
ADVANCE YOUR TOOLING 🔬