Symbolic Execution to Verify Vulnerabilities Detected by LLMs

Automating the verification of AI-detected security vulnerabilities using symbolic execution to eliminate false positives and prove exploitability.

Project Overview. An LLM identifies potential vulnerabilities in source code. The framework acts as a rigorous verification engine, using symbolic execution to validate these findings. Only mathematically proven vulnerabilities are reported; false positives are discarded.

Initial situation

Large Language Models (LLMs) are increasingly used for static code analysis and vulnerability detection. While they excel at identifying potential patterns, they suffer from a high rate of false positives, often flagging safe code as vulnerable because they lack a deep understanding of runtime behavior and data flow. Security teams are overwhelmed by manually verifying these alerts, leading to "alert fatigue" and reduced trust in automated tools. Current static analysis tools often lack the precision to distinguish between a theoretical bug and an actually exploitable vulnerability.

Problem statement / Project goal

The primary goal of this project is to bridge the gap between AI-driven detection and formal verification. The project aims to develop a Python-based framework that automatically takes vulnerability candidates identified by an LLM and verifies them using symbolic execution (powered by the angr framework). The system must prove whether a reported vulnerability is genuinely exploitable by generating a concrete proof of concept (symbolic state reaching an unsafe condition), thereby filtering out false positives and prioritizing critical risks.

Solution developed and its benefits

The developed framework provides a modular architecture for verifying memory-related vulnerabilities in C/C++ binaries. It supports multiple solver strategies for different vulnerability classes, including Stack Overflows, Heap Overflows, Use-After-Free, and Format String vulnerabilities. By leveraging symbolic execution, the tool mathematically proves whether an input exists that triggers the vulnerability, rather than relying on heuristics.

• Automated reduction of false positives from LLM-based code scans.
• Proof of exploitability via symbolic state analysis (e.g., unconstrained RIP, canary hits).
• Modular solver design allowing specific strategies for Stack, Heap, UAF, and Format String vulnerabilities.
• Integration of Model Context Protocol (MCP) for structured LLM-Agent communication.
• DWARF-aware analysis for accurate struct and variable resolution in binaries with debug symbols.
• Configurable simulation limits (max steps, loop bounds) to balance analysis depth and performance.
• Detailed evidence generation (concrete input values, crash states) for developer feedback.
• Custom heap simulation to model dynamic memory allocation and detection of logical errors.

The system significantly reduces the manual effort required for security audits. Instead of reviewing hundreds of potential issues, developers only need to address the verified, high-confidence vulnerabilities. The approach shifts the focus from "possible bugs" to "proven exploits".

Key terms

• Symbolic ExecutionProgram analysis technique treating inputs as symbols to explore all feasible execution paths.
• Large Language Models (LLM)AI models used for initial vulnerability detection and code pattern recognition.
• False Positive ReductionThe process of filtering out incorrectly flagged vulnerabilities to improve signal-to-noise ratio.
• Memory CorruptionClass of vulnerabilities including Overflows and Use-After-Free where memory integrity is violated.
• angrBinary analysis framework used for the symbolic execution engine.
• Model Context Protocol (MCP)Standard for connecting AI models to external tools and data sources.
• Unconstrained StateSymbolic execution state where the instruction pointer is fully symbolic, indicating potential control flow hijacking.
• DWARFDebugging format used to map binary addresses back to source code variables and structs.

Customer

Internal FHNW Project
Institute for Mobile and Distributed Systems (IMVS)
University of Applied Sciences Northwestern Switzerland
Bahnhofstrasse 6
5210 Windisch
IMVS Website

Team

Note: The illustrative diagrams on this page were generated using AI tools to visualize technical concepts and architecture.