Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code

Researchers Dimitrios Bouras and Sergey Mechtaev have developed Gordian, a breakthrough hybrid symbolic execution framework that solves a fundamental limitation in program analysis. Traditional symbolic execution—a technique for automatically exploring program paths—gets stuck on 'solver-hostile' code fragments involving complex math, unbounded data structures, or deep execution paths. While recent attempts to replace constraint solvers with LLMs failed at global reasoning, Gordian takes a smarter hybrid approach: it uses LLMs selectively to generate lightweight 'ghost code' that guides traditional SMT solvers through difficult sections.

Gordian implements three types of ghost code: inverting difficult fragments with bidirectional constraint propagation, creating solver-friendly surrogate models, and semantically partitioning unbounded heap spaces. Built on the KLEE symbolic execution engine, Gordian was tested on synthetic 'logic bombs,' the mathematical library FDLibM, and real-world programs like libexpat, jq, and bc. The results are striking: 52-84% better coverage than traditional symbolic execution and 86-419% better than pure LLM-based approaches, while using 90-96% fewer LLM tokens. This makes sophisticated program analysis practical for security auditing, bug finding, and verification of complex software systems.