KLEECopilot, a Large Language Model-guided directed symbolic execution approach built on KLEE, exhibits only marginal sensitivity to model scale, supporting the efficacy of integrating security semantics and loop-exit prioritization.
Abstract
Symbolic execution effectively discovers security violations but suffers from path explosion. Engines like KLEE therefore use path prioritization heuristics to order state exploration, typically optimizing code coverage. However, path prioritization can become trapped in cyclic control-flow regions, where repeated branching consumes the exploration budget before exploration reaches vulnerable code beyond these cyclic regions. We propose KLEECopilot, a Large Language Model (LLM)-guided directed symbolic execution approach built on KLEE. KLEECopilot uses LLMs to mark potentially vulnerable code and guide path prioritization. It also integrates loop-exit prioritization to escape potentially non-vulnerable cycles and progress toward deeper vulnerabilities. Compared with baselines such as Empc, KLEECopilot improves basic block coverage by 42.24% and line coverage by 125.82%. It discovers 1,335 total violations and 87 unique violations, outperforming the second-best baseline by 32.2% in total violations and Empc by 24.3% in unique violations. Although KLEECopilot is sensitive to model family, it exhibits only marginal sensitivity to model scale, supporting the efficacy of integrating security semantics and loop-exit prioritization. Ablation studies further show that individual components contribute to effectiveness: alternative configurations involving searchers, internal components, marking sources, and prompt variants yield only 54--61 unique violations, while KLEECopilot maintains competitive code coverage.
The effectiveness of smart contract fuzzing depends strongly on whether generated transactions reach deep, state-dependent execution paths. Existing fuzzers often generate highly random call sequences, wasting executions on semantically invalid or low-value states and leaving vulnerabilities that require specific invocation orders unexplored. We present a lightweight method for generating fuzz test cases under bytecode-level static guidance. We construct an Ethereum virtual machine control-flow graph, extract paths containing vulnerability-relevant instructions, recover function selectors, and order externally callable functions according to storage read-write dependencies. A coverage-guided evolutionary strategy then generates, evaluates, recombines, and mutates executable seeds. Five dedicated runtime oracles target reentrancy, integer overflow or underflow, block-state dependence, unsafe delegate calls, and frozen Ether. The evaluation uses deployed Ethereum contracts, including labelled vulnerable contracts. SAEFUZZ detects most labelled vulnerable contracts, yielding 98.50% accuracy, 90.00% precision, and 81.82% recall. It also achieves 84.07% mean instruction coverage, with valid test cases accounting for 93.48% of generated cases. Ablation results indicate that static guidance, directed seed generation, and vulnerability-specific oracles each contribute to the final performance.
Large Language Models (LLMs) are increasingly used for software vulnerability detection, but their performance depends on how source code is represented in the input. Most prompting approaches use source code in its original form, while some works propose the use of structured representations. Abstract Syntax Trees (ASTs) are one of the most popular approaches, but AST verbosity increases input size relative to source code, making them hard to fit within some LLMs context windows. This paper investigates Behavior Trees (BTs) as an alternative intermediate representation for LLM-based vulnerability detection. BTs encode control flow, conditions, and executable actions more compactly than ASTs, making them a natural candidate when token count is a constraint. First, we propose a preprocessing stage that parses Java source code into ASTs and then converts them into BT representations. We then compare vulnerability detection performance across 460 Java samples from the Juliet Java test suite, using three input representations: raw source code, AST, and BT. All experiments use a single quantized local LLM, Mistral Small 3.2 24B (Q4_K_M). Our results show that using BT representations improves recall on short code samples, while raw source code achieves higher precision. On longer samples, BTs improve overall performance over the original representation and fit within the context window, whereas many ASTs exceed the context limit. These findings suggest that BTs can provide a compact and useful structured representation for vulnerability detection with quantized, locally deployable LLMs.
A hybrid pipeline combining static vulnerability candidate selection using Latent Semantic Analysis with dynamic verification through Large Language Model-assisted fuzzing is presented, which reduces manual effort while still requiring human validation.
Kevin Nguyen, Dominik Schoop· International Conference on...· 0 citations
Search-based regression-test generation effectively explores complex program structures, yielding high structural coverage, but its oracles are derived from the system under test: faults already present are recorded as expected behavior rather than exposed. Property-based testing offers independent semantic oracles, but depends on high-quality properties and gives little guidance for reaching deep states or satisfying selective preconditions. We present PROGRESS (PROperty-Guided REgression Search for Semantic Falsification), integrating intent-driven properties into coverage-guided, search-based evolutionary test generation to reach deep program states and detect violations of intended behavior. PROGRESS (1) extracts intent-bearing code context and uses a language-model pipeline to generate executable jqwik properties while limiting implementation leakage; (2) extends EvoSuite's DynaMOSA with a search objective and property-aware fitness function per property, rewarding progress through preconditions and prioritizing falsifying executions; and (3) binds property parameters and uses jqwik-provided generators to connect quantified inputs to evolving test sequences, steering generation toward coverage and bug-detection goals. We evaluate PROGRESS on 25 large-scale Java systems against regression-test generation, standalone property-based testing, and context ablations. PROGRESS detects 328/562 current-version bugs (58%) versus none for regression-test generation, and satisfies all preconditions for 70/150 hard-to-reach properties versus 18 for standalone jqwik. Ablations show documentation and caller/callee context are key to generating valid executable properties. PROGRESS preserves structural exploration while exposing faults missed by regression-derived assertions; we release a comprehensive artifact package.
D. Mo, Noshin Ulfat, Matthew B. Dwyer et al.· arXiv.org· 0 citations
ContainmentBench, a sandboxed benchmark comprising a 504-scenario specification dataset, a shared rollout-trace schema, and stage-scoped metrics for endpoint violations, logged propagation, and explicitly authorized taint-exposed proposals that commit, is introduced.
Wen-Hao Lan, Shan Li, Meiqi Wu et al.· 0 citations
This paper presents HarnessLLM, an automated workflow that leverages LLMs to generate verification harnesses for Rust code directly from existing test suites and is the first work to use LLMs for generating harnesses aimed at memory safety verification in real-world Rust projects.
Minghua Wang, Yuwei Liu, Lin Huang· Proceedings of the 2026 IEEE...· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
