Witchcraft Solver - Automated 0day Discovery in Stripped Binaries

The talk presents Witchcraft Solver, a pipeline that takes a stripped ELF binary with no source, symbols or harness and searches it for bugs. The speaker opens with a long digression on the limits of formal reasoning and AI claims, then argues that the practical problem is getting from a binary to a candidate vulnerability and then to a working exploit input.

The pipeline lifts binaries to LLVM bytecode using several open-source lifters. Function boundaries are recovered from exception-handling frame sections instead of relying on IDA. Sink functions come from sanitizer backtraces produced by OSS-Fuzz and ARVO. The bytecode then goes to several symbolic and abstract-interpretation analyzers, and an LLM triages the reports. On FFmpeg, about 26 candidates were flagged, and the triage separated false positives from a few real memory corruptions. A comparison on a libjpeg-turbo bug with no public exploit contrasts coverage-based fuzzing, directed fuzzing and concolic execution on a stripped binary.

The closing section looks at future work toward machine-checked proofs and at the preservation of vulnerability records, including the revival of the BugTraq mailing list. A demonstration of a type-confusion flaw in the Lean prover makes the point that proof tools also have bugs. The takeaway is that binary-only pipelines can reach real programs, but their output still needs human or formal verification.