Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery

• URL: http://arxiv.org/abs/2604.06506v1
• Date: Tue, 07 Apr 2026 22:35:52 GMT
• Title: Guiding Symbolic Execution with Static Analysis and LLMs for Vulnerability Discovery
• Abstract summary: Symbolic execution detects vulnerabilities with precision, but applying it to larges requires harnesses that set up symbolic state, model dependencies, and specify assertions.<n>We present Static Analysis Informed and LLM-Orchestrated Symbolic Execution (SAILOR), which automates symbolic execution harness construction by combining static analysis with LLM-based synthesis.<n>SAILOR operates in three phases: (1) static analysis identifies candidate vulnerable locations and generates vulnerability specifications; (2) an LLM uses vulnerability specifications and orchestrates harness synthesis by iteratively refining drivers, stubs, and assertions against compiler and symbolic execution feedback; symbolic execution then detects vulnerabilities using the generated harness, and (3) concrete replay
• Score: 3.462916206368371
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Symbolic execution detects vulnerabilities with precision, but applying it to large codebases requires harnesses that set up symbolic state, model dependencies, and specify assertions. Writing these harnesses has traditionally been a manual process requiring expert knowledge, which significantly limits the scalability of the technique. We present Static Analysis Informed and LLM-Orchestrated Symbolic Execution (SAILOR), which automates symbolic execution harness construction by combining static analysis with LLM-based synthesis. SAILOR operates in three phases: (1) static analysis identifies candidate vulnerable locations and generates vulnerability specifications; (2) an LLM uses vulnerability specifications and orchestrates harness synthesis by iteratively refining drivers, stubs, and assertions against compiler and symbolic execution feedback; symbolic execution then detects vulnerabilities using the generated harness, and (3) concrete replay validates the symbolic execution results against the unmodified project source. This design combines the scalability of static analysis, the code reasoning of LLMs, the path precision of symbolic execution, and the ground truth produced by concrete execution. We evaluate SAILOR on 10 open-source C/C++ projects totaling 6.8 M lines of code. SAILOR discovers 379 distinct, previously unknown memory-safety vulnerabilities (421 confirmed crashes). The strongest of five baselines we compare SAILOR to (agentic vulnerability detection using Claude Code with full codebase access and unlimited interaction), finds only 12 vulnerabilities. Each phase of SAILOR is critical: Without static analysis targeting confirmed vulnerabilities drop 12.2X; without iterative LLM synthesis zero vulnerabilities are confirmed; and without symbolic execution no approach can detect more than 12 vulnerabilities.

Related papers

• GoAT-X: A Graph of Auditing Thoughts for Securing Token Transactions in Cross-Chain Contracts [52.51342355102833]
  Cross-chain bridges, the critical infrastructure of the multi-chain ecosystem, have become a primary target for attackers.<n>Existing defenses, such as bytecode-level static analysis, are ill-equipped to handle the semantic complexity of cross-chain interactions.<n>We propose GoAT-X, a framework that shifts automated cross-chain smart contracts auditing from pattern matching toward systematic first-principles verification.
  arXiv  Detail & Related papers  (2026-04-27T11:34:21Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• A Prompt-Based Framework for Loop Vulnerability Detection Using Local LLMs [0.0]
  This study proposes a prompt-based framework for the detection of loop vulnerabilities within Python 3.7+ code.<n>The framework targets three categories of loop-related issues, such as control and logic errors, security risks inside loops, and resource management inefficiencies.<n>The designed prompt-based framework included key safeguarding features such as language-specific awareness, code-aware grounding, version sensitivity, and hallucination prevention.
  arXiv  Detail & Related papers  (2026-01-21T04:53:38Z)
• Multi-Agent Taint Specification Extraction for Vulnerability Detection [49.27772068704498]
  Static Application Security Testing (SAST) tools using taint analysis are widely viewed as providing higher-quality vulnerability detection results.<n>We present SemTaint, a multi-agent system that strategically combines the semantic understanding of Large Language Models (LLMs) with traditional static program analysis.<n>We integrate SemTaint with CodeQL, a state-of-the-art SAST tool, and demonstrate its effectiveness by detecting 106 of 162 vulnerabilities previously undetectable by CodeQL.
  arXiv  Detail & Related papers  (2026-01-15T21:31:51Z)
• The Trojan Knowledge: Bypassing Commercial LLM Guardrails via Harmless Prompt Weaving and Adaptive Tree Search [58.8834056209347]
  Large language models (LLMs) remain vulnerable to jailbreak attacks that bypass safety guardrails to elicit harmful outputs.<n>We introduce the Correlated Knowledge Attack Agent (CKA-Agent), a dynamic framework that reframes jailbreaking as an adaptive, tree-structured exploration of the target model's knowledge base.
  arXiv  Detail & Related papers  (2025-12-01T07:05:23Z)
• QLCoder: A Query Synthesizer For Static Analysis of Security Vulnerabilities [18.588864089739598]
  QLCoder is an agentic framework that automatically synthesizes queries in CodeQL, a powerful static analysis engine.<n>QLCode embeds an LLM in a synthesis loop with execution feedback, while constraining its reasoning using a custom MCP interface.<n>We evaluate QLCode on 176 existing CVEs across 111 Java projects.
  arXiv  Detail & Related papers  (2025-11-11T17:06:04Z)
• LLM-Driven Adaptive Source-Sink Identification and False Positive Mitigation for Static Analysis [0.0]
  textscAdaTaint adaptively infers source/sink specifications and filters spurious alerts through neuro-symbolic reasoning.<n>textscAdaTaint grounds model suggestions in program facts and constraint validation, ensuring both adaptability and determinism.<n>Results show that textscAdaTaint reduces false positives by textbf43.7% on average and improves recall by textbf11.2% compared to state-of-the-art baselines.
  arXiv  Detail & Related papers  (2025-11-06T03:44:10Z)
• CASTLE: Benchmarking Dataset for Static Code Analyzers and LLMs towards CWE Detection [2.5228276786940182]
  This paper introduces CASTLE, a benchmarking framework for evaluating the vulnerability detection capabilities of different methods.<n>We assess 13 static analysis tools, 10 LLMs, and 2 formal verification tools using a hand-crafted dataset of 250 micro-benchmark programs covering 25 common CWEs.
  arXiv  Detail & Related papers  (2025-03-12T14:30:05Z)
• SeCodePLT: A Unified Platform for Evaluating the Security of Code GenAI [58.29510889419971]
  Existing benchmarks for evaluating the security risks and capabilities of code-generating large language models (LLMs) face several key limitations.<n>We introduce a general and scalable benchmark construction framework that begins with manually validated, high-quality seed examples and expands them via targeted mutations.<n>Applying this framework to Python, C/C++, and Java, we build SeCodePLT, a dataset of more than 5.9k samples spanning 44 CWE-based risk categories and three security capabilities.
  arXiv  Detail & Related papers  (2024-10-14T21:17:22Z)
• SORRY-Bench: Systematically Evaluating Large Language Model Safety Refusal [64.9938658716425]
  SORRY-Bench is a proposed benchmark for evaluating large language models' (LLMs) ability to recognize and reject unsafe user requests.<n>First, existing methods often use coarse-grained taxonomy of unsafe topics, and are over-representing some fine-grained topics.<n>Second, linguistic characteristics and formatting of prompts are often overlooked, like different languages, dialects, and more -- which are only implicitly considered in many evaluations.
  arXiv  Detail & Related papers  (2024-06-20T17:56:07Z)
• IRIS: LLM-Assisted Static Analysis for Detecting Security Vulnerabilities [14.188864624736938]
  Large language models (or LLMs) have shown impressive code generation capabilities but they cannot do complex reasoning over code to detect such vulnerabilities.<n>We propose IRIS, a neuro-symbolic approach that systematically combines LLMs with static analysis to perform whole-repository reasoning for security vulnerability detection.
  arXiv  Detail & Related papers  (2024-05-27T14:53:35Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.