EXPERIMENTAL — This tool is research-grade software. Do not use in production environments without understanding its limitations.
Find 0days in production binaries using only the binary as input.
No source code. No debug symbols. No prior knowledge of the target. Drop in a stripped ELF binary, get back memory corruption vulnerabilities with concrete exploitation witnesses — automatically. PE and Mach-O support is planned for a future release.
$ ./wsolve /usr/bin/ls
Pre-filter: 71 function(s) with sink calls
BOUNDED : 31 → skipped (argument provably safe)
UNKNOWN : 40 → targeted (symbolic execution)
[klee x retdec] UNSAFE 30 violation(s) across 27/60 target(s)
Verdict : UNKNOWN Confidence : LOW
Under the hood: the binary is lifted to LLVM IR, a taint pre-filter eliminates provably safe functions, then KLEE explores all reachable paths symbolically across the remaining targets. IKOS, SeaHorn, and SMACK run in parallel for independent corroboration. The whole thing runs in Docker — one command, no environment setup.
- Docker
- Python 3.6+
- Ubuntu 22.04+ / Debian 12+
- Ghidra 12+ — optional, post-verification of KLEE hits
- LLM — optional, interprocedural triage of KLEE hits: local via Ollama, or a DeepSeek/Mistral/OpenAI API key
git clone https://github.com/endrazine/wsolver
cd wsolver
make # builds wbin2llvm + wsolver
make docker # builds the solver image (~2 min first time, cached after)New here? See QUICKSTART.md to go from clone to a real
finding in a few commands. For the full setup — lifters, Ghidra, LLM triage,
and the /etc/wsolver/wsolver.conf configuration file — see
INSTALL.md.
Optional: LLM triage
Install Ollama and pull a model:
curl -fsSL https://ollama.com/install.sh | sh
ollama pull deepseek-coder:6.7b-instruct-q4_K_M # fast (~4GB)
ollama pull deepseek-coder:33b-instruct-q4_K_M # better quality (~20GB)./wsolve /usr/bin/ls
./wsolve /usr/sbin/nginx ./nginx-resultsOutput lands in wsolve_out/<binary>_<timestamp>/results/. Violations come
with KLEE witness inputs you can replay directly.
Ghidra is auto-detected if installed under ~/wsolver/, ~/ghidra_*_PUBLIC/,
or /opt/ghidra_*_PUBLIC/.
KLEE proves a memory-corruption crash within a function, but on lifted,
per-function IR it does not soundly establish whether attacker-controlled input
actually reaches that function across the call graph. wllm fills that gap: it
performs the interprocedural step. For each KLEE hit it builds a backward
slice — the sink function plus the callers that reach it — and asks an LLM to
trace the vulnerable argument to its origin and judge whether that origin is
attacker-controllable.
The LLM decides what counts as untrusted from its own knowledge (argv, env, files, sockets, IPC, deserialized data, …) — there is no hardcoded source list, so it generalizes beyond toy inputs to real APIs.
Two backends: a local model via Ollama (default, no key), or any OpenAI-compatible API — DeepSeek, Mistral, xAI/Grok, OpenAI. DeepSeek V4-Pro is recommended for real triage; weaker models mis-handle the lifted IR.
RUNDIR=$(ls -td wsolve_out/vuln_stackbof_*/ | head -1)
python3 wllm.py "$RUNDIR/results/wsolver_report.json" \
--ir "$RUNDIR/ir/vuln_stackbof_retdec.ll" \
--backend openai --api-key-file ./key.txt --verbose[wllm] [1/1] vuln (strcpy)
[wllm] slice: vuln, main
════════════════════════════════════════
LLM Triage Summary
Model : deepseek-v4-pro
════════════════════════════════════════
REAL [HIGH ] vuln (strcpy)
Stack buffer overflow in vuln, potentially leading to
arbitrary code execution
════════════════════════════════════════
Results: 1 REAL 0 FALSE_POSITIVE 0 UNCERTAIN
Given the main → vuln slice, the model traces argv[1] into vuln's
strcpy and confirms the overflow is attacker-reachable — REAL. With only
vuln's isolated body it cannot see where input comes from and (correctly,
for that limited view) cannot confirm reachability. The interprocedural slice is
what makes the verdict sound.
The slice depth (levels of callers) is set with --slice-depth or
LLM_SLICE_DEPTH in wsolver.conf (default 2). Results are written to
llm_triage.json and merged back into wsolver_report.json.
The API key is never stored in config — pass it with --api-key-file (a file
containing the key) or --api-key-env (the name of an environment variable).
# Vulnerable binary — strcpy with no bounds check
./wsolve samples/vuln_stackbof
# → UNSAFE, 1 violation, concrete witness
# Safe binary — strcpy guarded by strlen check
./wsolve samples/safe2
# → SAFE, HIGH confidenceThe sample binaries ship precompiled so everyone analyses identical bytes, and
are rebuildable from source with make -C samples (see samples/Makefile).
-
wunstrip recovers function names from
.eh_frameunwind data — present in almost every production binary for C++ exception handling, even when the symbol table is stripped. -
RetDec / Rev.ng / Anvill lift the binary to LLVM IR — the same intermediate representation used by Clang, giving formal verification tools a precise semantic model of every memory operation.
-
wir_filter traces dangerous arguments (sizes, format strings, pointers) backward through SSA definitions. Functions where the argument is provably bounded are eliminated before symbolic execution starts.
-
KLEE explores all paths through the remaining functions symbolically, finding inputs that trigger memory corruption. IKOS, SeaHorn, and SMACK run independently for corroboration.
-
(Optional) Ghidra decompiles each KLEE hit to confirm violations are genuine and not harness artifacts.
-
(Optional) wllm performs the interprocedural step KLEE cannot: for each hit it slices backward from the sink through its callers and asks an LLM (local via Ollama, or DeepSeek/Mistral/OpenAI via an OpenAI-compatible API) to trace the vulnerable argument to its origin and decide whether that origin is attacker-controllable — returning REAL, FALSE_POSITIVE, or UNCERTAIN with a structured rationale. KLEE owns soundness of the crash; the LLM owns reachability across function boundaries.
| Code | Meaning |
|---|---|
| 0 | SAFE |
| 1 | UNSAFE |
| 2 | UNKNOWN |
| 3 | Usage error |
See DOCUMENTATION.md for pipeline internals, Docker image details, sink configuration, and architecture notes.
MIT License — Copyright (c) 2026 Jonathan Brossard. See LICENSE.