EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming Kaustuv Mukherji1∗ , Jaikrishna Manojkumar Patil1 , Colton Payne1 , Paulo Shakarian1∗ , Dana Warmsley2 , Nigel Stepp2 , Evelyn Kim2 , 1
Syracuse University HRL Laboratories [email protected], [email protected], [email protected], [email protected], [email protected], [email protected], [email protected] 2
arXiv:2608.01763v1 [cs.CR] 3 Aug 2026
Abstract Large language models are increasingly used to reason about software vulnerabilities, but their outputs can silently violate domain knowledge, limiting their reliability in safety-critical settings such as medical devices. Prior work either treats that output as a prediction to be scored or constrains it to walks within a single knowledge graph; neither checks whether reasoning over a binary is consistent with an independent body of domain knowledge. We present EntailLLM, which validates each LLM-proposed analyst path by entailment: the path is a traversal of the binary’s function call graph, the domain knowledge is represented in a separate graph, and verification aligns the two under temporal annotated logic. Across three CWE classes, four LLMs, three prompting strategies, and seven binaries varying in size from 405 to 12,696 function call-graph nodes, domain knowledge raises pooled entailment from 78% to 98%, with entailment decreasing in only 3% of the experiments. EntailLLM is deployed end-toend on real medical-device binaries, reaching 98% pooled entailment without per-device tuning. Our system inherits the formal guarantees of generalized annotated logic, providing logical verification of LLM output that is both explainable and grounded in well-defined semantics.
1
Introduction
Large language models are increasingly applied to vulnerability discovery, from detection and triage to exploit reasoning and patch generation (Sheng et al. 2025). Yet they remain unreliable at identifying and reasoning about vulnerabilities unaided (Ullah et al. 2024), they produce confident inferences that probability-based checks cannot catch (Pan et al. 2023), and they mislead analysts when their suggestions go unchecked (Basque et al. 2026). These problems worsen for bespoke reverse-engineering tasks in domains such as medical devices, whose firmware is long-lived, hard to patch, and rarely shipped with source (Das 2022): analysis proceeds on decompiled binaries, where the semantic cues of source code are absent and intent must be reconstructed from low-level structure. In this paper we study the problem of identifying paths through a binary’s function call graph that lead toward a vulnerability and adhere to domain knowledge. We present EntailLLM, a system deployed at scale ∗
Preprint. Under review. Corresponding author.
Figure 1: An LLM mistake caught by domain knowledge. The green path (with bold arrows) through the codebase was selected; the orange nodes (with faded edges) denote other code blocks in the binary.
on real medical-device firmware, that improves an LLM’s ability to find such paths. Figure 1 is a screenshot of EntailLLM catching erroneous LLM output: the library function memset is correctly assigned to the memory-management class, but the LLM then assumes it can perform an integer size calculation—an inference that is structurally unremarkable yet supported by nothing memset does. EntailLLM does more than flag such violations. Pairing domain knowledge with self-refinement raises the fraction of paths entailed from 71% to 97% while increasing the number of entailed paths by 37%, from 1,054 to 1,445—more than any other configuration we evaluate. The distinction that makes this possible is between statistical clean-up, pruning candidate paths by structural signals such as the call graph, which an LLM or a graph-based method already does well, and semantic clean-up: rejecting a path that violates the meaning of the domain even when it is structurally plausible. Only a logic-based reasoner supplies the latter. EntailLLM treats each LLM-proposed path as a hypothesis and admits it only if a domain-knowledge graph (DKG) entails it. The trajectory is a traversal of the binary’s call graph while the constraints come from a separate DKG, so verification is an alignment between two graphs rather than a walk within one. The domain encoding instantiates hand-crafted templates over the knowledge graph’s triples,
yielding conjunctive, co-dependent-label rules grounded in CWE, MITRE, and device documentation. We assume the domain knowledge itself is accurate; our contribution lies in the machinery that enforces entailment by it. Our contributions are: (i) a reframing of LLM vulnerability analysis as cross-graph entailment checking of analyst traversals rather than final answers; (ii) a deployed, end-to-end system that localizes and explains non-entailments, reporting the first unsupported step with the rule firings behind it; and (iii) an evaluation across three CWE classes, four LLMs, three prompting strategies, and seven binaries, in which domain knowledge raises pooled entailment from 78% to 98%, decreasing in only 3 of 94 configurations. Section 2 formalizes the entailment-checking problem, Section 3 describes the system, Section 4 reports experiments, and Section 5 the deployment. Related Work. Work that reports gains from LLMs on security tasks pairs the model with structure rather than trusting it alone (Lekssays et al. 2025). Applying LLMs directly to stripped or decompiled binaries recovers source-like code, symbols, and readable decompiler output (Tan et al. 2024; Xie et al. 2024; Hu, Liang, and Chen 2024), improving the representation an analyst works from but not verifying that reasoning over it is consistent with what is known about the vulnerability class. Other work gates LLMs with structure to similar ends, translating a problem into symbolic form for a solver (Pan et al. 2023) or constraining generation to paths grounded in a knowledge graph (Luo et al. 2024a,b); these align reasoning to a walk within a single KG and are evaluated on natural-language QA. Our arrangement is closest to shielding in safe reinforcement learning (Alshiekh et al. 2018), where the LLM proposes freely and the logic decides what passes. But a shield strong enough to block unsafe behavior typically blocks useful behavior with it, and here we show that enriching the generator with the domain knowledge’s own derived vocabulary admits more logically correct analyst paths than shielding alone. Classical taint-based discovery and its recent LLM-driven variants (Redini et al. 2020; Liu et al. 2025) share our binary-level, source-free setting but aim to emit vulnerability alerts; where they use the LLM to produce the analysis, we use logic to check it. A detailed literature review appears in the Appendix.
2
Problem Description
Technical Preliminaries. We reason in generalized annotated logic (Kifer and Subrahmanian 1992), which supplies a single formal semantics generalizing fuzzy and other realvalued logics, and we work in a tractable fragment that admits exact polynomial-time deduction (Shakarian and Simari 2022) and represents time explicitly (Shakarian, Simari, and Subrahmanian 2012). We recall only what is needed here and refer the reader to that work for the full development. An annotated literal a:µ pairs a literal with an annotation µ = [ℓ, u] ⊆ [0, 1]. The lattice is ordered so that [0, 1]— total uncertainty—is the bottom element, while tight intervals such as [1, 1] and [0, 0] sit at the top. This makes the logic open-world: an unobserved literal is not false but merely uncertain, and inference narrows it, so the partial and noisy observations recovered from a binary need not be forced to
true or false. A temporal annotated fact (TAF) asserts such a literal at a time point, written a:(µ, t), and rules take the ∆t form ℓ0 :µ0 ←−− ℓ1 :µ1 ∧ · · · ∧ ℓm :µm , where a body satisfied at t makes the head hold at t + ∆t. A program Π is a set of TAFs and rules. An interpretation I maps each ground literal and time point to an annotation; it satisfies a:µ at t when µ ⊑ I(a, t), and is a model of Π when it satisfies every rule and TAF. Deduction iterates a fixpoint operator Γ to convergence, yielding the minimal model I ∗ . Γ is monotonic, converges in polynomial number of applications, and decides entailment. Entailment is therefore an exact, decidable consequence of the program’s semantics rather than a heuristic score, and because every interpretation is produced by an identifiable rule firing, each inference carries a trace of the facts and rules that led to it. Entailment Checking of Analyst Paths. Given a target binary and a weakness class (CWE), the LLM predicts exploration workflows an analyst might follow through the binary’s functions toward a vulnerability of that class. The input is the binary’s function call graph, functions as nodes and calls as edges, with each function labeled with a set of libc labels; the output is a sequence of connected callgraph nodes. Our prompts steer exploration toward the target weakness class and entailed traversals feed a fuzzer downstream in the deployed system, so the traversal is the input to discovery rather than a substitute for it. We evaluate CWE-121 (stack-based buffer overflow), CWE-415 (double free), and CWE-416 (use-after-free). We first fix a domainknowledge program Π = ΠT AF s ∪ ΠRules , assumed correct and fixed, whose facts encode the DKG and whose rules are described in Section 3. We denote a temporally ordered sequence of code blocks as: τ = ⟨CB0 , . . . , CBn ⟩. Then an LLM-proposed candidate analyst trajectory linked by a predicate called stepFrom is encoded by TAFs, and can be written as F (τ ) = { analystAt(CB0 ) : (µ0 , 0) } ∪ { stepFrom(CBi−1 , CBi ) : (⊤, i) }ni=1 asserting that each step is proposed at the corresponding time point, and we reason over Π ∪ F (τ ), whose minimal model we denote I ∗ . Note that τ and Π live in different graphs: τ is a chain in the binary’s call graph, whose connectivity is guaranteed by construction, while Π’s facts encode the DKG’s vulnerability concepts and typed semantic relations. Entailment is therefore an alignment between the two, not the existence of a path within either. A step CBi−1 → CBi is entailed when the domain knowledge verifies that the analyst can follow F (τ ) to reach CBi at time i: Π ∪ F (τ ) |=ent analystAt(CBi ) : (µ, i), µ ⪰ µmin where µmin is the minimum admissible bound. If no chain of rule firings can verify it, then the step is a non-entailment, meaning the LLM has proposed a move that contradicts with the domain knowledge. The entire trajectory is entailed Π |=ent τ when every step is entailed, i.e. ∀i ∈ {1, . . . , n} : I ∗ |=i analystAt(CBi ) : µi , µi ⪰ µmin The entailment-checking problem is to decide whether Π |=ent τ and, when it does not, to return the first failing step
Ghidra decompiler
libc labels & call graph LLM path generation analyst paths Reasoner (PyReason)
yielding for each function in the call graph the set of libc calls it references. +DK
entailed paths
Domain Knowledge
Fuzzer
Figure 2: The end-to-end EntailLLM pipeline. Solid boxes are EntailLLM stages, gray boxes its inputs, and dashed boxes place the system in the larger cybersecurity workflow. i∗ = min{ i : Π ∪ F (τ ) ̸|=ent analystAt(CBi ) : (µ, i) }. We retain exactly the entailed trajectories. Because I ∗ is computed exactly and in polynomial time under consistency (Theorems 3.2 and 3.4 of (Shakarian et al. 2011)), this decision and the localization of i∗ are exact rather than heuristic. We focused development on binary analysis because of our target deployment; the framework itself is agnostic to whether the call graph and its labels come from a decompiler or from source, and we leave source-code analysis to future work, studying a complete binary pipeline here. Several domainspecific reasons motivate the choice. Device firmware ships without source, and the compiled artifact is what runs, and optimization and field patching can leave it diverging from any source tree. We consume decompiler output rather than raw bytes because the decompiler recovers the call graph and, from symbol and relocation tables, the imported libc calls we use as labels—beacons that survive stripping, so no debug information is needed. We verify all traversals rather than only paths terminating in a vulnerability: reverse engineers proceed by beacon-driven exploration, recognizing API calls, strings, and constants to form and test hypotheses (Votipka et al. 2020; Sisco, Dudenhofer, and Bryant 2017; Bryant et al. 2011), so restricting attention to vulnerability terminating paths would discard the exploratory structure that makes the output useful and presuppose the analyst’s conclusion. Finally, admitting only domain-entailed paths reduces the volume of spurious paths a human must triage and yields explainable traces an auditor can inspect.
3
System description
Figure 2 shows the end-to-end EntailLLM pipeline. The input to the system is the analyzed binary’s call graph together with the libc labels of its code blocks. From these inputs, the pipeline proceeds through two core stages—LLM path generation and logical verification—before emitting the paths that survive verification. Labeled call graph. Ghidra’s static analysis recovers the binary’s structural representation. It disassembles the machine code, reconstructs functions and their boundaries, produces decompiled C-like output, and recovers the interprocedural call graph with cross-references. From symbol and relocation information it resolves the names of imported libc functions (e.g., strcpy, gets, realloc, system),
Domain Knowledge (DK). DK is a CWE-focused, codecentric ontology together with instantiated knowledge graphs for CWE-121, CWE-415, and CWE-416. We note that our approach is agnostic to the underlying knowledge graph, and it does not necessarily have to be associated with a CWE. We treat these as fixed and defer the study of knowledge graph extraction and correctness to other studies. The ontology used defines a layered class hierarchy—from concrete Beacons, CodeEntities, CodeOperations, and CodePatterns, through FaultConditions and OutcomeLevelFaults, to CWE-level VulnerabilityClasses—connected by typed relations such as is_a, can_cause, and mitigates. Each graph is populated by automated extraction from technical corpora (reverse-engineering manuals, security advisories, man pages), then refined by schema validation with targeted semantic review; together they span 105–188 entities and 232–403 relations over 14–16 relation types (per-graph counts in Appendix). A central modeling choice represents faults as unsafe variants of otherwise-neutral operations—an out_of_bounds_write as an unsafe_variant_of a generic memory_write. Safe and unsafe behavior coexist in one graph, and the reasoner can express how missing validation turns an ordinary operation into a memory-corruption event. DK also supplies the mapping rules that lift raw libc labels onto its own vocabulary during reasoning, so the labels attached to code blocks are expressed in the terms against which paths are later checked for entailment. For the +DK experimental setting, we pre-run the mapping rules and provide the LLM with additional labels. This supplies the generator with DK’s vocabulary but no entailment verdict: the injected labels come only from running the mapping rules over the labels already in the call graph, before any path is generated. Step 1: LLM Path Generation. The first stage proposes candidate analyst paths. Figure 3 shows the prompt structure. The model is given the target CWE and the binary’s label vocabulary, and asked for an ordered sequence of label subsets per path. The constraints ensure that the model cannot attribute behavior the binary does not exhibit, and that they are framed as analyst exploration rather than as vulnerability reports, so not every stage needs to be related to the CWE. What the model returns is not yet a path but a template. Beam search realizes each template against the actual call graph, instantiating every stage’s label subset as a concrete function and discarding any template whose sequence cannot be completed as a connected chain. The surviving realizations, deduplicated, are paths that are then input to the reasoner. Step 2: Entailment Checking. Verification is carried out with PyReason (Aditya et al. 2023), an open-source engine for generalized annotated logic that reasons directly over knowledge graphs. It executes the domain knowledge as a logic program and takes the realized paths as input. The logic program comprises of the DKG’s facts and mapping rules together with 42 non-ground rules obtained by instantiating a small set of hand-written templates over the graph’s entity–relation–entity triples. The rules fall into three fami-
System role You are a security analyst specializing in defensive binary code review. . . generate realistic code-review paths — ordered sequences of semantic function behaviors an analyst would examine when assessing a binary for a specific weakness type. Context CWE: CWE-121, Stack-based Buffer Overflow (id, name, MITRE description). Label vocabulary: groups of libc labels from Ghidra static analysis, each group co-occurring in one code region, e.g. Group 1: [gets, sprintf, strspn] .. . (N groups per binary) +DK. The only change under domain-knowledge enrichment: each group is augmented with reasonerderived DK labels, e.g. Group 1 becomes [gets, sprintf, strspn, missing_bounds_check, unchecked_memory_write, stack_pointer_overwrite, ...] Constraints Paths must be mutually diverse; framed as analyst exploration (not every stage need relate to the CWE); use only labels from the vocabulary; one label group per stage, no cross-group mixing; minimum 6 edges per path; at most 50 paths. Output format A single JSON object {"paths": [...]}; each path has path_id, an ordered cluster_sequence of label subsets, an exploration_score in [0, 1], and a short explanation. No text outside the JSON. Technique (varies for different methods) Zero-shot: “Generate the paths directly.” CoT: first emit a label_analysis triage of each group (immediately_suspicious / worth_investigating / likely_irrelevant), then generate paths with an added per-stage stage_reasoning field. Self-refinement: Three sequential calls sharing the blocks above. (1) Generate an initial path set (as zero-shot). (2) Critique: the paths are returned to the model, which reviews them for CWE relevance, diversity, ignored labels, and score calibration, replying with plain-text feedback. (3) Refine: regenerate an improved path set addressing that critique.
Figure 3: Structured prompt template for CWE-121. Full prompts appear in the appendix.
lies: label propagation, transitive closure, and analyst traversal with step control, of which Table 1 gives one traversal rule and one label-propagation rule. Verifying a single step may require more than one rule: a label-propagation rule may first combine the raw libc labels at one block into a semantic label, a DK mapping rule lift that label onto a DKG concept, and a transitive-closure rule chains relations across several hops, before a traversal rule can fire and validate the analyst’s move. Because PyReason computes the minimal model of the whole program, the reasoning is exact rather than a heuristic graph walk. If no combination of rules can validate a step, that step is non-entailed by the domain knowledge, and we
report the first such step (i∗ of Section 2) along with the full reasoning trace (Figure 6).
4
Experiments
Experimental Setup We evaluate across three weakness classes—CWE-121 (stack-based buffer overflow), CWE-415 (double free), and CWE-416 (use-after-free). Standard target binaries (std) are drawn from BinPool (Arasteh et al. 2025), a dataset of Debian binaries curated from historical CVEs; it spans 603 CVEs across 89 CWE classes, so the CWEs we target are represented by real compiled programs whose call graphs and libc usage resemble production firmware. Real-world targets (rw) are firmware extracted from deployed medical devices, confidentially provided, and are the targets EntailLLM is required to analyze in our production environment. Table 2 lists the seven binaries behind the results reported here. Note that ezurio is evaluated under both CWE-121 and CWE-416. Sizes span two orders of magnitude, from gpac (405 nodes, 571 edges) to unsafelib (12,696 nodes, 40,881 edges), exercising the pipeline on both small and large call graphs. Models. We report four models in the paper: Opus-4.8, GPT-5.5, Llama 4 Scout, and Kimi K2.5, spanning proprietary and open-weight families. Each model is run under all three prompting strategies and in two conditions—without and with domain knowledge supplied to the generator a priori (+DK)—giving 24 configurations per binary. Our initial selection also included Claude Fable 5, but its built-in safeguards, which redirect queries on certain sensitive topics including cybersecurity to a less specialized model, were triggered by our vulnerability-analysis prompts and prevented its use as a generator. Hyperparameters. Generation uses greedy decoding (t=0.0) throughout, since we evaluate each model’s most likely output rather than a sample. We request Npaths = 50 candidate path templates per call, lowered to 20 for Llama 4 Scout, whose 8,192-token output cap truncates a 50-path JSON. Paths must span at least six call-graph edges, lowered to four for gpac, whose 405-node graph is too shallow to admit many six-edge paths. Beam search relaxes to a maximum hop distance of h = 3. Of its parameters only Nsol , the number of realized chains kept per surviving template, was tuned—over {1, 2, 5, 10}: smaller values degraded results and larger ones raised runtime and LLM cost for no gain, so we use 5. Full settings and rationale are in Appendix. Metrics. For each configuration we report #Total, the number of unique trajectories that survive beam-search realization, and #Entail, how many of those the domain knowledge entails, with Entailment% = #Entail / #Total × 100 in parentheses. A trajectory that is realized but not entailed is spurious: a path the LLM found plausible that contradicts the domain knowledge. When aggregating over configurations we pool #Entail and #Total rather than averaging perconfiguration percentages, so that generations are weighted by the evidence they carry.
Rule
English Description
analystAt(CB2 ) : µpair ←−−− analystAt(CB1 ) : ∆t=1
[0.25, 1] ∧ hasLabel(CB1 , Lc ) : [0.1, 1] ∧ hasLabel(CB2 , Le ) : [0.1, 1] ∧ can_cause(Lc , Le ) : [0.1, 1] ∧ stepF rom(CB1 , CB2 ) : [1, 1] hasLabel(X, copy_operation) [0.9, 1] ←−−− hasLabel(X, sprintf ) ∆t=0
: :
[0.6, 1] ∧ hasLabel(X, strcpy) : [0.6, 1]
If the analyst is at code block CB1 , which is labeled with Lc , and code block CB2 is labeled with Le , and the domain knowledge asserts Lc can_cause Le , then the analyst may advance to CB2 . If code block X is observed to use both sprintf and strcpy, it is inferred with at least 90% confidence to perform a copy_operation.
Table 1: Two example rules from the logic program and their description in natural language. µpair is a pairwise-minimum bound function over annotations in the rule body, applied to the head atom if the rule is fired. Annotations in the body are bounds that must be contained by any possible grounding during the reasoning process. The full program appears in Appendix.
CWE
Binary
Type
Nodes
Edges
CWE-416
gpac mupdf-x11 mutool
std std std
405 3,341 3,569
571 11,883 14,051
CWE-121
htmldoc insulininject unsafelib
std rw rw
1,086 1,010 12,696
2,815 2,774 40,881
Both
ezurio
rw
1,155
3,322
Table 2: The binaries used across the target CWEs.
Compute. All experiments ran on a single server (AMD EPYC 9755, 128 cores, 754 GiB RAM, Ubuntu 24.04, Python 3.10), with every model accessed through a hosted API (Anthropic, OpenAI, AWS Bedrock). Peak resident memory was ∼21 MB for the generation stage and ∼931 MB for the reasoner, under 0.3% of available RAM, so the pipeline reproduces on commodity hardware.
Results and Discussion Tables 3 and 4 report results for the standard and real-world binaries, respectively. Results for binaries with CWE-415 are provided in the Appendix. Domain knowledge improves entailment for both binary types. Pooled entailment increases from 84.4% to 97.8% for standard BinPool binaries and from 71.4% to 98.0% for real-world medical device binaries, and the number of configurations at 100% entailment rises from 17 to 38 and from 16 to 39. Across the 94 configurations with output in both conditions, entailment improves in 59, is unchanged in 32, and only decreases in 3. A one-sided Wilcoxon signed-rank test over those 94 paired configurations confirms the shift (W + = 1905, W − = 48, p < 10−10 ; median +6.5 points); the 32 unchanged configurations were already at 100% entailment and are excluded as ties. The result holds for each binary type separately (std p = 2.3 × 10−9 ; rw p = 4.0 × 10−6 ). We note that configurations are not fully independent, since each model and each binary recurs across strategies.
Self-refinement with domain knowledge yields the most entailed paths. It produces more entailed paths than any other configuration: 806 on the standard binaries against 584 for zero-shot and 461 for chain-of-thought (CoT), and 639 on the device binaries against 403 and 413. It is also the only strategy for which domain knowledge raises the entailed count along with the rate, adding 182 paths on standard binaries and 209 on device binaries, and doing so in 26 of its 31 individual configurations against 16 of 32 for zeroshot and 12 of 31 for CoT. Self-refinement explores hardest and is correspondingly the least reliable unaided—60.9% entailment on device binaries—so while it has the most to gain, we see that the logical layer successfully utilizes that exploration into verified output. Results translate to real-world binaries. Unaided entailment on the device binaries is lower than the BinPool targets (71.4% vs 84.4%), yet under domain knowledge the two converge to 98.0% and 97.8%. The system is able to close the gap without per-device tuning of the logic. Stability across runs. To check that these gains are not an artifact of a single run, we repeated the full pipeline ten times and measured the spread in entailment across repetitions. As expected, LLM API responses varied, but domain knowledge both raised entailment and sharply narrowed its spread across runs under all three prompting strategies. Plots are included in the Appendix.
5
EntailLLM Deployment
EntailLLM is deployed end-to-end inside a vulnerabilitydiscovery pipeline, occupying the solid boxes of Figure 2. A decompiler upstream supplies the labeled call graph; EntailLLM proposes candidate analyst trajectories over it, checks each against the domain knowledge, and passes only the entailed ones to downstream tooling such as a fuzzer. Results on the three binaries extracted from deployed medical devices are reported in Table 4. EntailLLM runs as an interactive web application served from a REST API. The interface mirrors the system’s data flow. Figure 1 is a screenshot of the UI showing the graph of an analyzed binary with an LLMselected trajectory highlighted. Figure 4 shows a snippet of the analyst knowledge graph on the UI.
std:gpac (416) #Total #Entail(%)
std:mupdf-x11 (416) std:mutool (416) #Total #Entail(%) #Total #Entail(%)
std:htmldoc (121) #Total #Entail(%)
Model
Strategy
Opus-4.8
Zero-Shot + DK CoT + DK Self-Refinement + DK
3 8 17 16 8 15
3(100) 8(100) 16(94.12) 16(100) 8(100) 15(100)
69 101 47 58 63 71
40(57.97) 101(100) 38(80.85) 58(100) 50(79.37) 70(98.59)
52 62 5 13 65 84
38(73.08) 59(95.16) 5(100) 13(100) 64(98.46) 81(96.43)
70 98 87 55 62 86
69(98.57) 98(100) 87(100) 55(100) 60(96.77) 86(100)
GPT-5.5
Zero-Shot + DK CoT + DK Self-Refinement + DK
12 1 2 1 11 33
5(41.67) 1(100) 2(100) 1(100) 9(81.82) 33(100)
65 66 48 30 61 64
45(69.23) 61(92.42) 29(60.42) 30(100) 35(57.38) 64(100)
76 44 30 27 77 59
60(78.95) 42(95.45) 30(100) 27(100) 48(62.34) 57(96.61)
72 41 45 46 77 86
71(98.61) 41(100) 44(97.78) 46(100) 73(94.81) 86(100)
Llama-4 Scout
Zero-Shot + DK CoT + DK Self-Refinement + DK
6 1 29 7 5 13
6(100) 1(100) 19(65.52) 7(100) 5(100) 13(100)
14 30 73 18 15 33
9(64.29) 30(100) 54(73.97) 18(100) 10(66.67) 33(100)
5 4 10 19 4 4
1(20) 4(100) 8(80) 18(94.74) 0(0) 4(100)
78 36 65 22 28 31
73(93.59) 36(100) 65(100) 22(100) 26(92.86) 31(100)
Kimi K2.5
Zero-Shot + DK CoT + DK Self-Refinement + DK
13 29 6 5 11 2
13(100) 29(100) 6(100) 5(100) 11(100) 2(100)
14 30 79 44 90 72
14(100) 30(100) 79(100) 44(100) 51(56.67) 58(80.56)
33 23 102 72 142 82
33(100) 23(100) 83(81.37) 64(88.89) 114(80.28) 79(96.34)
167 20 32 37 60 94
159(95.21) 20(100) 32(100) 37(100) 60(100) 94(100)
Table 3: Unique paths realized (#Total) and entailed (#Entail) for the four standard BinPool binaries, each validated against the DK graph of the CWE shown in parentheses, without and with domain knowledge (+DK).
(a)
(b)
Figure 5: Plots showing how (a) reasoning time and (b) peak memory, of the reasoner scales for seven binaries.
Figure 4: An excerpt of the CWE_121 DK graph in the deployed system. Highlighted portions show how entities like function_pointer relate to the CWE_121 vulnerability class through KG relations like manifestation_of.
Scalability. Figure 5 shows the scaling capability of the reasoner. Memory remains mostly constant, while runtime scales linearly with steps of reasoning.
Trace. For every non-entailment, a reasoning trace, shown in Figure 6, is generated. This shows the exact step that was non-entailed by domain knowledge. On click on the UI, a more detailed trace showing the complete reasoning path leading to the non-entailment conclusion is available, and an example is provided in the Appendix. Compute. The system is deployed on an AWS EC2 r5ad.2xlarge instance (8 cores, AMD EPYC 7571, 64 GB RAM)—an order of magnitude smaller than the experiment server of Section 4.
Model
Strategy
rw:insulininject (121) rw:unsafelib (121) #Total #Entail(%) #Total #Entail(%)
rw:ezurio (121) #Total #Entail(%)
rw:ezurio (416) #Total #Entail(%)
Opus-4.8
Zero-Shot + DK CoT + DK Self-Refinement + DK
124 33 51 31 73 29
106(85.48) 33(100) 48(94.12) 26(83.87) 70(95.89) 29(100)
47 54 67 42 69 87
37(78.72) 54(100) 56(83.58) 41(97.62) 47(68.12) 81(93.1)
29 40 28 47 31 97
26(89.66) 40(100) 28(100) 47(100) 31(100) 97(100)
6 27 4 4 2 16
6(100) 27(100) 4(100) 4(100) 2(100) 16(100)
GPT-5.5
Zero-Shot + DK CoT + DK Self-Refinement + DK
69 37 45 26 73 87
60(86.96) 37(100) 34(75.56) 26(100) 40(54.79) 83(95.4)
53 35 35 42 66 63
41(77.36) 35(100) 24(68.57) 42(100) 42(63.64) 63(100)
24 61 15 28 16 16
21(87.5) 61(100) 14(93.33) 28(100) 14(87.5) 16(100)
23 7 9 6 11 5
14(60.9) 7(100) 9(100) 6(100) 8(72.7) 5(100)
Llama-4 Scout
Zero-Shot + DK CoT + DK Self-Refinement + DK
12 15 70 9 22 30
7(58.33) 15(100) 58(82.86) 6(66.67) 22(100) 30(100)
4 7 30 42 15 13
4(100) 7(100) 24(80) 42(100) 9(60) 13(100)
17 12 17 16 18 9
17(100) 12(100) 17(100) 16(100) 18(100) 9(100)
3 5 5 0 12 16
3(100) 5(100) 5(100) NA 12(100) 16(100)
Kimi K2.5
Zero-Shot + DK CoT + DK Self-Refinement + DK
158 11 134 41 140 41
57(36.08) 11(100) 108(80.6) 41(100) 8(5.71) 41(100)
136 31 69 33 108 83
88(64.71) 25(80.65) 48(69.57) 33(100) 60(55.56) 78(93.98)
62 23 18 41 50 62
61(98.38) 23(100) 17(94.44) 41(100) 47(94) 62(100)
14 11 4 14 0 0
14(100) 11(100) 4(100) 14(100) NA NA
Table 4: Unique paths realized (#Total) and entailed (#Entail) for the three real-world medical-device binaries, each validated against the DK graph of the CWE shown in parentheses, without and with domain knowledge (+DK). binaries—domain knowledge raises pooled entailment from 78.0% to 97.9%, decreasing for only 3 of 94 configurations. The strongest configuration is self-refinement with domain knowledge, which raises entailment from 71.0% to 97.4% while increasing the number of entailed paths by 37%, from 1,054 to 1,445. The effect transfers to deployed firmware: unaided entailment on the medical-device binaries is lower than the BinPool targets (71.4% against 84.4%), yet under domain knowledge both converge to 98.0% and 97.8%. The system is able to close the gap without per-device tuning of the logic. Figure 6: The explainable trace showing entailment (first two, in green) and non-entailment (rest, in red) for the analyst path selected by the LLM in Figure 1.
6
Conclusion and Future Work
We presented EntailLLM, a deployed system that pairs LLM generation of analyst traversal paths through a software codebase with logic-programming verification against domain knowledge. A surviving path is therefore not merely a plausible traversal of the function call graph to a language model, but provably entailed by the encoded domain knowledge. Aggregated over the weakness classes we examine—four LLMs, three prompting strategies, and seven
We plan to extend this work in three directions. Currently, we exclusively measure logical entailment. While this is an important problem, it would add value to the system if we could also measure exploitability. We have found validated vulnerability labels for real device firmware to be scarce, and we are working to obtain them through coordinated disclosure, vendor collaboration, and expert red-teaming so that EntailLLM can be evaluated against confirmed vulnerabilities. Second, we are looking to extend the study to include a measure of coverage of the different strategies. Third, we are extending the pipeline to include a corrector module which takes a non-entailed path as an input, and attempts to produce a logically entailed alternative with minimal edits.
Acknowledgments This research was, in part, funded by the Advanced Research Projects Agency for Health (ARPA-H). The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of the U.S. Government. Research in this paper is related to the invention described in U.S. provisional patent application 64/077,998: Automatic Vulnerability Analysis of Software Consistent with Domain Knowledge.
References Aditya, D.; Mukherji, K.; Balasubramanian, S.; Chaudhary, A.; and Shakarian, P. 2023. PyReason: Software for Open World Temporal Logic. In AAAI Spring Symposium: MAKE. Alshiekh, M.; Bloem, R.; Ehlers, R.; Könighofer, B.; Niekum, S.; and Topcu, U. 2018. Safe reinforcement learning via shielding. In Proceedings of the AAAI conference on artificial intelligence, volume 32. Arasteh, S.; Nikitopoulos, G.; Wu, W.-C.; Weideman, N.; Portnoy, A.; Raghothaman, M.; and Hauser, C. 2025. BinPool: A Dataset of Vulnerabilities for Binary Security Analysis. In Proceedings of the 33rd ACM International Conference on the Foundations of Software Engineering (FSE Companion). Basque, Z. L.; Doria, S.; Soneji, A.; Gibbs, W.; Doupé, A.; Shoshitaishvili, Y.; Losiouk, E.; Wang, R.; Aonzo, S.; et al. 2026. Decompiling the Synergy: An Empirical Study of Human-LLM Teaming in Software Reverse Engineering. In NDSS. Bryant, A.; Mills, R.; Peterson, G.; and Grimaila, M. 2011. Software reverse engineering as a sensemaking task. Journal of Information Assurance and Security, 6(6): 483–494. Das, A. 2022. Know Your Infusion Pump Vulnerabilities and Secure Your Healthcare Organization. Technical report, Palo Alto Networks Unit 42. Analysis of over 200,000 infusion pumps; https://unit42.paloaltonetworks.com/infusionpump-vulnerabilities/. Hu, P.; Liang, R.; and Chen, K. 2024. DeGPT: Optimizing Decompiler Output with LLM. In NDSS. Kifer, M.; and Subrahmanian, V. 1992. Theory of Generalized Annotated Logic Programming and its Applications. J. Log. Program., 12(3&4): 335–367. Lekssays, A.; Mouhcine, H.; Tran, K.; Yu, T.; and Khalil, I. 2025. {LLMxCPG}:{Context-Aware} vulnerability detection through code property {Graph-Guided} large language models. In 34th USENIX Security Symposium (USENIX Security 25), 489–507. Liu, P.; Sun, C.; Zheng, Y.; Feng, X.; Qin, C.; Wang, Y.; Xu, Z.; Li, Z.; Di, P.; Jiang, Y.; et al. 2025. Llm-powered static binary taint analysis. ACM Transactions on Software Engineering and Methodology, 34(3): 1–36. Luo, L.; Li, Y.-F.; Haffari, R.; and Pan, S. 2024a. Reasoning on graphs: Faithful and interpretable large language model reasoning. In International Conference on Learning Representations, volume 2024, 14400–14423.
Luo, L.; Zhao, Z.; Haffari, G.; Li, Y.-F.; Gong, C.; and Pan, S. 2024b. Graph-constrained reasoning: Faithful reasoning on knowledge graphs with large language models. arXiv preprint arXiv:2410.13080. Pan, L.; Albalak, A.; Wang, X.; and Wang, W. 2023. LogicLM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning. In Bouamor, H.; Pino, J.; and Bali, K., eds., Findings of the Association for Computational Linguistics: EMNLP 2023, 3806–3824. Singapore: Association for Computational Linguistics. Redini, N.; Machiry, A.; Wang, R.; Spensky, C.; Continella, A.; Shoshitaishvili, Y.; Kruegel, C.; and Vigna, G. 2020. Karonte: Detecting Insecure Multi-binary Interactions in Embedded Firmware. In 2020 IEEE Symposium on Security and Privacy (SP), 1544–1561. Shakarian, P.; Parker, A.; Simari, G. I.; and Subrahmanian, V. V. S. 2011. Annotated probabilistic temporal logic. ACM Trans. Comput. Logic, 12(2). Shakarian, P.; and Simari, G. I. 2022. Extensions to Generalized Annotated Logic and an Equivalent Neural Architecture. In 2022 Fourth International Conference on Transdisciplinary AI (TransAI), 63–70. IEEE. Shakarian, P.; Simari, G. I.; and Subrahmanian, V. 2012. Annotated probabilistic temporal logic: Approximate fixpoint implementation. ACM Transactions on Computational Logic (TOCL), 13(2): 1–33. Sheng, Z.; Chen, Z.; Gu, S.; Huang, H.; Gu, G.; and Huang, J. 2025. LLMs in Software Security: A Survey of Vulnerability Detection Techniques and Insights. ACM Comput. Surv., 58(5). Sisco, Z. D.; Dudenhofer, P. P.; and Bryant, A. R. 2017. Modeling information flow for an autonomous agent to support reverse engineering work. The Journal of Defense Modeling and Simulation, 14(3): 245–256. Tan, H.; Luo, Q.; Li, J.; and Zhang, Y. 2024. Llm4decompile: Decompiling binary code with large language models. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, 3473–3487. Ullah, S.; Han, M.; Pujar, S.; Pearce, H.; Coskun, A.; and Stringhini, G. 2024. Llms cannot reliably identify and reason about security vulnerabilities (yet?): A comprehensive evaluation, framework, and benchmarks. In 2024 IEEE symposium on security and privacy (SP), 862–880. IEEE. Votipka, D.; Rabin, S.; Micinski, K.; Foster, J. S.; and Mazurek, M. L. 2020. An observational investigation of reverse {Engineers’} processes. In 29th USENIX Security Symposium (USENIX Security 20), 1875–1892. Xie, D.; Zhang, Z.; Jiang, N.; Xu, X.; Tan, L.; and Zhang, X. 2024. Resym: Harnessing llms to recover variable and data structure symbols from stripped binaries. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 4554–4568.
Supplementary Material EntailLLM: Verifying LLM-Generated Vulnerability Discovery Paths with Domain Knowledge via Logic Programming
Contents
G Pipeline Configuration
10
A Stability and the Random Baseline
1 H The Complete Logic Program
B Aggregate Analysis
5
C Results for CWE-415
7
D Scalability of the Reasoner
8
E Evaluation Binaries
8 K Domain Knowledge: Ontology and Graphs
21
F Language Models
10 L Extended Related Work
22
A
15
I
Deployment: Reasoning Trace Example
17
J
Prompt Templates
17
Stability and the Random Baseline
To check that the reported experimental results are not an artifact of a single run, and to establish what entailment rate an uninformed generator would achieve, we repeated the full pipeline ten times for each of the four models, three prompting strategies, and two conditions on two cases: insulininject under CWE-121 and mupdf-x11 under CWE-416. Alongside these we ran ten independent rounds of random sampling, in which 25 analyst paths are drawn directly from the binary’s call graph, matched to the LLM conditions on path length and on the label-group constraint, so that the only difference is which labels a path visits. Figures 1–6 show the resulting distributions; all settings are otherwise those of the experimental setup in the main paper. Random sampling attains 18.0 ± 8.5% entailment on insulininject and 46.4 ± 9.1% on mupdf-x11. Every model–strategy–combination runs on these two targets exceeds random sampling under a one-sided Mann–Whitney test against the ten random rounds (p < 0.05; most at p < 10−3 ). Pooled over models, unaided generation sits 57– 64 points above random on insulininject and 32–38 points above on mupdf-x11; with domain knowledge the margins widen to 79–81 and 47–51 points. We make two observations. First, in general our use of LLMs generates better paths across strategies, when compared to a completely random selection of paths. Second, Entailment is further improved by the addition of domain knowledge across several runs. Averaged over the twelve model–strategy cells per target, the standard deviation of entailment across runs falls from 10.7 to 4.2 on insulininject and from 9.7 to 5.8 on mupdf-x11. The effect is largest where unaided behaviour is least reliable: Kimi K2.5 under self-refinement moves from 54.1 ± 11.3% to 98.3 ± 2.8% on insulininject, and GPT-5.5 under zero-shot from 66.3 ± 9.9% to 99.6 ± 0.8% on mupdf-x11. Several conditions become degenerate under +DK, entailing every realized path in all ten runs. Although generation uses greedy decoding, hosted inference APIs are not bit-reproducible; variable request batching perturbs logits enough to flip near-tied argmax decisions, which is the source of the spread reported here. A run contributes no measurement when the model returns no usable path set. This occurs once in 240 runs on insulininject but in 10.4% of runs on mupdf-x11, and is concentrated in Llama-4 Scout, whose 8,192-token output cap truncates longer responses. Aggregated over all conditions, generation failure accounts for 0% of GPT-5.5 runs, 3.9% of Kimi K2.5, 6.7% of Opus-4.8, and 24.4% of Llama-4 Scout. 1
Figure 1: Zero-shot on insulininject (CWE-121). Each box is ten independent runs: grey is random sampling, blue unaided generation, orange the same model with domain knowledge (+DK). Random sampling attains 18.0 ± 8.5% entailment. A box collapsed to a single line indicates zero variance across runs.
Figure 2: Chain-of-thought on insulininject (CWE-121). Conventions as in Figure 1.
2
Figure 3: Self-refinement on insulininject (CWE-121).
Figure 4: Zero-shot on mupdf-x11 (CWE-416). Conventions as in Figure 1; random sampling attains 46.4 ± 9.1%, so the margin over random is smaller on this target than on insulininject.
3
Figure 5: Chain-of-thought on mupdf-x11 (CWE-416). Conventions as in Figure 1.
Figure 6: Self-refinement on mupdf-x11 (CWE-416). Conventions as in Figure 1.
4
Entail%
#Entailed
Binary
Type CWE Random base
dropbear mupdf-x11 mutool htmldoc htmldoc
std std std std std
415 416 416 415 121
18.4 46.4 54.8 88.8 85.6
40.2 91.3 71.2 96.8 80.5 95.5 92.3 100.0 97.2 100.0
132 454 484 455 819
189 597 471 473 652
insulininject unsafelib ezurio ezurio ezurio
rw rw rw rw rw
121 121 415 416 121
18.0 40.0 68.4 63.2 84.8
63.6 96.9 68.7 96.6 80.7 100.0 87.1 100.0 95.7 100.0
618 480 46 81 311
378 514 62 111 452
+DK base +DK
Table 1: Pooled entailment and entailed-path counts per binary–CWE pair, over all model×strategy configurations, ordered by unaided LLM entailment within each type. Random is the random-sampling mean. Unaided LLM entailment spans 40.2–97.2% with no consistent std/rw pattern, and tracks the random rate closely; under domain knowledge every pair reaches 91.3–100%.
B
Aggregate Analysis
This section aggregates the per-configuration results of the main paper and of Section C along three axes: by binary, by absolute entailed-path count, and by statistical significance. Unless stated otherwise, figures pool #Entail and #Total over configurations rather than averaging per-configuration percentages, so that each configuration is weighted by the evidence it carries.
B.1
Per-Binary Results
Table 1 pools every model and strategy for each binary–CWE pair. Two things are visible. Entailment for unaided LLM is ordered almost exactly as random sampling is—dropbear is lowest on both, htmldoc highest—so how well a model appears to do without domain knowledge might be correlated to how permissive the domain knowledge is for that binary. An LLM generator raises the floor over random sampling, but under +DK that ordering disappears: all pairs get to similarly high entailment percentage.
B.2
Entailed-Path Counts
The main paper reports entailment rates. Table 2 gives the underlying counts. We notice that while the entailment rate always increases for all cases, number of entailed paths fluctuates slightly. Self-refinement shows the best improvements both in rate and number of entailments.
B.3
Statistical Significance
Across all 118 paired configurations, entailment improves in 77, is unchanged in 38, and decreases in 3; over the 94 configurations of the main paper the counts are 59, 32 and 3. Every subset is significant at p < 10−5 . On CWE-415 no configuration decreases at all, giving W − = 0 and a maximal effect size. Note that, configurations are not fully independent—each model appears in 30 and each binary–CWE pair in 12—so we treat the per-subset tests as descriptive rather than as independent confirmatory comparisons, and apply no multiplicity correction.
5
Entail%
#Entailed
Type
Strategy
base
+DK
base
+DK
count up
std std std
Zero-Shot CoT Self-Refinement
82.7 82.9 77.4
98.1 98.5 96.8
828 772 847
866 604 1043
14/23 10/23 17/22
rw rw rw
Zero-Shot CoT Self-Refinement
72.0 82.9 61.8
98.6 97.9 97.8
586 500 450
430 415 672
8/17 6/16 13/17
Table 2: Entailment rate and absolute entailed-path count by binary type and strategy, pooled over all three weakness classes. Count up is the number of configurations in which domain knowledge raised the entailed count, out of those producing output in both conditions. Self-refinement is the only strategy for which the count rises on both target types; chain-of-thought reduces it in both.
Subset
n
n′
W+ W−
p median 3.7 × 10−14
All three CWEs 118 80 3180 CWE-121 & 416 94 62 1905
60 48 3.8 × 10−11
r
+8.83 0.963 +6.54 0.951
std rw
68 46 1078 50 34 572
3 7.1 × 10−14 +8.14 0.994 23 1.3 × 10−6 +10.73 0.923
CWE-416 CWE-121 CWE-415
46 25 48 37 24 18
1 36 0
324 667 171
6.0 × 10−8 +6.70 0.994 9.7 × 10−7 +6.54 0.898 3.8 × 10−6 +11.88 1.000
Table 3: One-sided Wilcoxon signed-rank tests on paired (baseline, +DK) entailment percentages. n is the number of configurations with output in both conditions, n′ the number after excluding ties; every tie is a configuration already at 100% entailment without domain knowledge. Median is the change in percentage points; r is the matched-pairs rank-biserial effect size. The second row is the subset reported in the main paper.
6
std:htmldoc std:dropbear rw:ezurio #Total #Entail(%) #Total #Entail(%) #Total #Entail(%)
Model
Strategy
Opus-4.8
Zero-Shot + DK CoT + DK Self-Refinement + DK
80 58 45 42 57 84
70(87.5) 58(100) 41(91.11) 42(100) 52(91.23) 84(100)
33 19 3 6 21 17
19(57.58) 19(100) 1(33.33) 6(100) 11(52.38) 17(100)
26 27 2 2 13 29
20(76.92) 27(100) 2(100) 2(100) 12(92.31) 29(100)
GPT-5.5
Zero-Shot + DK CoT + DK Self-Refinement + DK
57 66 49 48 80 71
54(94.74) 66(100) 42(85.71) 48(100) 71(88.75) 71(100)
52 39 26 23 39 37
16(30.77) 32(82.05) 14(53.85) 23(100) 11(28.21) 31(83.78)
7 0 0 0 9 4
4(57.14) NA NA NA 8(88.89) 4(100)
Llama-4 Scout
Zero-Shot + DK CoT + DK Self-Refinement + DK
19 36 0 0 0 0
19(100) 36(100) NA NA NA NA
5 24 44 7 0 0
5(100) 24(100) 11(25) 7(100) NA NA
0 0 0 0 0 0
NA NA NA NA NA NA
Zero-Shot + DK CoT Kimi K2.5 + DK Self-Refinement + DK
6 47 56 10 44 11
6(100) 47(100) 56(100) 10(100) 44(100) 11(100)
0 0 31 7 74 28
NA NA 10(32.26) 7(100) 34(45.95) 23(82.14)
0 0 0 0 0 0
NA NA NA NA NA NA
Table 4: CWE-415 (double free): unique paths realized (#Total) and entailed (#Entail), without and with domain knowledge (+DK). NA marks a configuration that produced no realized paths.
C
Results for CWE-415
The CWE-415 evaluation uses ezurio, dropbear and htmldoc, introduced in Table 5. dropbear is the secondsmallest in the study after gpac. Results follow the pattern of the two classes reported in the main paper. Pooled entailment rises from 72.1% to 97.6%, entailment improves in 18 of the 24 configurations that produced output in both conditions, is unchanged in 6, and decreases in none. The gain is concentrated where unaided LLM entailment is weakest: dropbear moves from 40.2% to 91.3%, while htmldoc and ezurio start at 92.3% and 80.7% and both reach 100%. Unlike CWE-121 and CWE-416, the entailed count also rises in aggregate here, from 633 to 724 paths. We note that ezurio yields output in only 9 of its 24 configurations—all of Opus-4.8 and three cells of GPT5.5. Llama-4 Scout produces nothing at all under self-refinement on any binary, and nothing on htmldoc under chain-of-thought; Kimi K2.5 produces nothing on dropbear under zero-shot. These are the generation failures characterised in Section A, and they are the reason CWE-415 is reported here rather than in the main paper. These results go to show how LLM results can vary significantly between models, and how larger state-of-the-art models often outperform other models.
7
Figure 7: Reasoning runtime versus number of reasoning time steps for all CWE-121 (solid) and CWE-416 (dashed) binaries.
D
Scalability of the Reasoner
Figures 7 and 8 report reasoner runtime and peak memory as the number of reasoning time steps grows, for all CWE-121 (solid) and CWE-416 (dashed) binaries, including rw:ezurio under CWE-416. The horizontal axis is PyReason’s time setting, which we fix to the number of steps in an analyst path: verifying a trajectory of n steps requires the reasoner to run for n time points, so this axis is the length of the trajectory being checked. Each point is an independent run in a fresh reasoner process with time fixed to the value shown. Runtime grows linearly with the number of time steps for every binary, so the slope of each line is the cost of one additional reasoning step. This per-step cost is found to be proportional to how many groundings the reasoner produces at each step. The slopes actually order the binaries by grounding volume: rw:unsafelib produces the most groundings per step (∼1,760) and has the steepest slope (∼1.4 s per step), while std:gpac produces the fewest and has the shallowest. Peak memory is flat at roughly 880 MB for every binary because the footprint is dominated by fixed startup costs—the Python interpreter, the JIT-compiled reasoner, and the loaded rules and knowledge graph—all done before any reasoning occurs. The additional memory per time step of reasoning is small by comparison: running six steps instead of one raises peak RSS by at most ∼16 MB, about 2% of the baseline. The small spread across binaries (878–931 MB) is also found to be proportional to the grounding volume. For deployment, we note that verification cost scales with trajectory length and with the grounding volume of the binary–DKG pairing, not with the number of trajectories checked, since each is verified independently and the program is restarted after every run. As the memory footprint is dominated by startup, a reasoner process sized for the largest binary is then sized for all of them. The deployment instance of 64 GB (Section 5 of the main paper) has roughly 70× the peak requirement of any single run.
E
Evaluation Binaries
Table 5 lists function call graphs for every binary used in the study. Graphs are recovered by Ghidra and restricted to the libc subset: functions that reference at least one imported libc routine, together with the calls among them, since these are the nodes over which entailment is defined. Seven of the eight appear in the main results; dropbear is used only for CWE-415 (Section C).
8
Figure 8: Peak resident set size (RSS) after reasoning versus number of reasoning time steps for all CWE-121 (solid) and CWE-416 (dashed) binaries. The footprint is dominated by fixed startup cost.
Binary
Type
CWE
Nodes
Edges
Standard (BinPool) gpac std dropbear std htmldoc std mupdf-x11 std mutool std
416 415 121, 415 416 416
405 816 1,086 3,341 3,569
571 2,416 2,815 11,883 14,051
1,010 1,155 12,696
2,774 3,322 40,881
Real-world (medical device) insulininject rw 121 ezurio rw 121, 415, 416 unsafelib rw 121
Table 5: All binary call graphs, grouped by target type and ordered by size. Sizes span two orders of magnitude, from 405 to 12,696 nodes.
9
Model limits Model
Route
Opus-4.8 GPT-5.5 Kimi K2.5 Llama-4 Scout
Anthropic 1,000,000 OpenAI 1,050,000 AWS Bedrock 256,000 AWS Bedrock (US) 128,000
Our settings
Context Max out max-tok n-paths 128,000 128,000 16,384 8,192
85,536 85,536 16,384 8,192
$/1M
50 5.00 / 25.00 50 5.00 / 30.00 50 0.60 / 3.00 20 0.17 / 0.66
Table 6: Language models used in our experiments. Context and Max out are the model’s own limits; max-tok and n-paths are the values we request. For Kimi K2.5 and Llama-4 Scout the requested budget equals the model’s output cap, so the cap binds. Prices are per million input / output tokens at the time of the experiments. Temperature is 0.0 throughout.
F
Language Models
Table 6 lists the four models used, together with the routing and generation settings under which each was called. All calls go through litellm, which selects the API key by model-id prefix, and all use greedy decoding (t=0.0).
G
Pipeline Configuration
This section gives the full parameter settings, then reports the two measurements that justify the one parameter we tuned: how many templates a model returns and how many of those the beam search can realize (Section G.2), and what changes when the realization budget is doubled (Section G.3).
G.1
Hyperparameters
The full hyperparameter values and rationale are shown in Table 7.
G.2
Template Generation and Realization
A model does not return paths directly: it returns templates, ordered sequences of label subsets, which beam search must instantiate against the actual call graph. Tables 8 and 9 report this funnel per configuration for CWE-121 and CWE-416. Of 8,160 templates requested across the two classes, models returned 4,291 (52.6%), of which 2,683 (62.4%) realized as at least one connected chain, ultimately yielding 7,671 unique paths—a mean of 2.86 per surviving template, below the cap of Nsol = 5 because deduplication removes repeats. Roughly a third of what a model produces therefore reaches the reasoner. The rest is discarded by the structural filter before any semantic check is applied. Domain knowledge is provided before generation rather than on realization. The return rate rises from 45.6% to 57.2% under +DK. So, enrichment makes models propose more.
G.3
Sensitivity to the Beam-Search Budget
Nsol , the number of realized chains kept per surviving template, was the only beam-search parameter tuned. Table 10 repeats the entire CWE-121 evaluation at Nsol = 10, with every other setting unchanged. Doubling the budget realizes roughly 1.7× as many paths—4,884 against 2,838 without domain knowledge, and 3,413 against 2,026 with it. But, pooled entailment under +DK is 97.2% at Nsol = 10 against 98.5% at Nsol = 5. The effect of domain knowledge is therefore not dependent on how many realizations the beam search retains, and the smaller budget is preferred on runtime and API cost.
10
Parameter
Value
Rationale
0.0
Greedy decoding, to evaluate each model’s most likely output rather than a sample. Candidate path templates requested per call. Llama4 Scout is reduced to 20 because its 8,192-token output cap truncates a 50-path JSON, most often under chain-ofthought. Opus-4.8 and GPT-5.5 Kimi K2.5 (equals the model’s output cap) Llama-4 Scout (equals the model’s output cap)
Generation (LLM) temperature n-paths
max-tokens
50 (Llama-4: 20)
85,536 16,384 8,192
Beam-search realization h (max hop distance) beam-width max-back-hops hop-weight bh-weight extra-label-weight
3 100 3 0.1 0.2 1.0
Nsol
5
Default, not tuned. Default, not tuned. Default, not tuned. Default, not tuned; score penalty per hop beyond the first. Default, not tuned; score penalty per back-hop. Default, not tuned; penalty per extra label on a matched node, favouring tight matches. Realized trajectories emitted per surviving template. Varied over {1, 2, 5, 10}; Smaller values do not generate enough results. N = 10 raised runtime, enrichment context size, and API cost without providing comparable entailment improvements (Section G.3).
Path constraint MIN PATH EDGES
6 (gpac: 4)
Minimum path length in edges. Lowered to 4 for gpac, whose 405-node call graph is too shallow to admit many six-edge paths.
Table 7: Hyperparameter values and rationale.
11
Model
Strategy
rw:insulininject rw:unsafelib rw:ezurio std:htmldoc #Req #Ret #Sol #Req #Ret #Sol #Req #Ret #Sol #Req #Ret #Sol
Opus-4.8
Zero-Shot + DK CoT + DK Self-Refinement + DK
50 50 50 50 50 50
25 30 12 20 18 32
25 17 12 12 18 17
50 50 50 50 50 50
20 40 15 20 18 50
15 36 15 20 17 46
50 50 50 50 50 50
15 30 12 20 15 50
9 25 9 16 9 43
50 50 50 50 50 50
15 50 20 25 17 40
15 44 19 23 16 40
GPT-5.5
Zero-Shot + DK CoT + DK Self-Refinement + DK
50 50 50 50 50 50
15 15 10 12 16 20
15 12 9 9 16 20
50 50 50 50 50 50
15 20 12 12 20 20
13 17 9 12 19 20
50 50 50 50 50 50
15 18 12 10 15 20
10 16 5 8 8 4
50 50 50 50 50 50
18 15 10 12 20 20
15 15 10 12 19 20
Llama-4 Scout
Zero-Shot + DK CoT + DK Self-Refinement + DK
20 20 20 20 20 20
20 20 20 3 20 20
5 9 16 3 6 17
20 20 20 20 20 20
20 20 20 20 20 20
4 2 15 18 4 9
20 20 20 20 20 20
20 20 20 20 20 20
7 4 4 10 5 3
20 20 20 20 20 20
20 20 15 15 20 20
18 18 15 15 9 11
Zero-Shot + DK CoT Kimi K2.5 + DK Self-Refinement + DK
50 50 50 50 50 50
50 50 30 15 40 50
49 5 30 11 39 19
50 50 50 50 50 50
40 30 20 50 30 40
35 15 14 9 30 39
50 50 50 50 50 50
20 50 15 25 50 50
18 5 7 14 28 18
50 50 50 50 50 50
50 50 30 20 25 50
39 5 8 10 14 28
Table 8: Template generation and realization counts for CWE-121. #Req is the number of path templates requested, #Ret the number the model returned, and #Sol the number of returned templates that beam search realized as at least one connected call-graph chain. The unique paths that result from #Sol appear as #Total in the main results tables.
12
Model
Strategy
std:gpac std:mupdf-x11 std:mutool rw:ezurio #Req #Ret #Sol #Req #Ret #Sol #Req #Ret #Sol #Req #Ret #Sol
Opus-4.8
Zero-Shot + DK CoT + DK Self-Refinement + DK
50 50 50 50 50 50
10 30 10 20 14 21
2 19 5 16 5 12
50 50 50 50 50 50
15 40 10 20 15 25
15 38 10 20 15 25
50 50 50 50 50 50
12 30 12 20 15 50
11 30 1 16 15 50
50 50 50 50 50 50
15 50 12 20 12 50
4 23 3 14 2 30
GPT-5.5
Zero-Shot + DK CoT + DK Self-Refinement + DK
50 50 50 50 50 50
15 20 12 15 16 26
4 1 1 1 3 15
50 50 50 50 50 50
15 20 12 12 20 20
13 19 11 11 20 20
50 50 50 50 50 50
18 12 10 12 20 22
17 12 8 12 19 22
50 50 50 50 50 50
16 15 12 12 20 20
6 2 3 2 5 1
Llama-4 Scout
Zero-Shot + DK CoT + DK Self-Refinement + DK
20 20 20 20 20 20
20 20 20 3 20 20
2 5 10 3 5 12
20 20 20 20 20 20
15 10 20 20 20 20
4 10 19 20 5 18
20 20 20 20 20 20
15 10 4 20 20 20
2 6 2 18 1 2
20 20 20 20 20 20
10 10 5 3 20 20
2 2 1 0 5 20
Zero-Shot + DK CoT Kimi K2.5 + DK Self-Refinement + DK
50 50 50 50 50 50
50 45 15 15 12 25
5 29 3 6 5 6
50 50 50 50 50 50
50 30 20 20 40 30
4 11 19 17 38 28
50 50 50 50 50 50
50 20 30 20 50 30
7 10 30 20 50 27
50 50 50 50 50 50
20 15 15 50 20 20
8 6 1 23 0 0
Table 9: Template generation and realization counts for CWE-416. Columns as in Table 8.
13
Model
Strategy
rw:insulininject rw:unsafelib rw:ezurio std:htmldoc #Total #Entail(%) #Total #Entail(%) #Total #Entail(%) #Total #Entail(%)
Opus-4.8
Zero-Shot + DK CoT + DK Self-Refinement + DK
233 56 100 43 127 92
214(91.85) 56(100) 93(93) 43(100) 124(97.64) 91(98.91)
78 107 123 97 118 126
63(80.77) 99(92.52) 107(86.99) 95(97.94) 79(66.95) 117(92.86)
38 131 34 84 38 102
35(92.11) 131(100) 34(100) 84(100) 38(100) 102(100)
138 68 169 111 117 167
136(98.55) 68(100) 169(100) 111(100) 114(97.44) 167(100)
GPT-5.5
Zero-Shot + DK CoT + DK Self-Refinement + DK
129 35 85 26 135 47
114(88.37) 35(100) 65(76.47) 26(100) 97(71.85) 47(100)
82 68 58 62 97 95
68(82.93) 68(100) 43(74.14) 62(100) 58(59.79) 92(96.84)
29 25 18 42 16 27
25(86.21) 25(100) 17(94.44) 42(100) 14(87.5) 27(100)
138 86 75 66 142 134
137(99.28) 86(100) 74(98.67) 66(100) 136(95.77) 134(100)
Llama-4 Scout
Zero-Shot + DK CoT + DK Self-Refinement + DK
22 15 136 59 33 37
12(54.55) 15(100) 123(90.44) 56(94.92) 33(100) 37(100)
4 55 62 40 20 73
4(100) 54(98.18) 48(77.42) 40(100) 13(65) 35(47.94)
29 99 17 15 18 9
29(100) 90(90.9) 17(100) 15(100) 18(100) 9(100)
144 47 130 51 54 73
136(94.44) 47(100) 130(100) 51(100) 51(94.44) 73(100)
Zero-Shot + DK CoT Kimi K2.5 + DK Self-Refinement + DK
296 6 239 52 277 62
184(62.16) 6(100) 194(81.17) 50(96.15) 93(33.57) 60(96.77)
247 51 134 54 171 225
175(70.85) 44(86.27) 89(66.42) 54(100) 105(61.4) 215(95.56)
14 56 23 97 63 126
14(100) 56(100) 22(95.65) 97(100) 56(88.89) 126(100)
288 49 50 61 96 104
272(94.44) 49(100) 50(100) 61(100) 96(100) 104(100)
Table 10: CWE-121 with Nsol = 10: unique paths realized (#Total) and entailed (#Entail), without and with domain knowledge (+DK). Pooled entailment rises from 82.3% to 97.2%, against 78.5% to 98.5% at Nsol = 5.
14
H
The Complete Logic Program
The program Π consists of the 42 non-ground rules listed below, reproduced verbatim in PyReason syntax. The head annotation paired minimum bounds ann fn is the annotation function µpair of the main paper: it assigns the head the componentwise minimum of the bounds satisfied by the body clauses, so a step is never given a confidence higher than its weakest supporting evidence. The same program is shared across all three CWEs; only the knowledge graph the reasoner reasons with changes. Throughout the experiments, we take the minimum admissible bound µmin of the main paper’s problem formulation to be [0.25, 1], matching the guard on analystAt(CB1) in the traversal rules: an analyst is considered present at a block if its bound is at least [0.25, 1].
H.1
Analyst-Traversal and Step-Control Rules (8)
analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lcause):[0.1,1], hasLabel(CB2, Leffect):[0.1,1], can_cause(Lcause, Leffect):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lcontrib):[0.1,1], hasLabel(CB2, Lfault):[0.1,1], contributes_to(Lcontrib, Lfault):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lop):[0.1,1], hasLabel(CB2, Lderived):[0.1,1], derives(Lop, Lderived):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lunsafe):[0.1,1], hasLabel(CB2, Lsafe_concept):[0.1,1], unsafe_variant_of(Lunsafe, Lsafe_concept):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lfault):[0.1,1], hasLabel(CB2, Lcwe):[0.1,1], manifestation_of(Lfault, Lcwe):[0.1,1], stepFrom(CB1, CB2) analystAt(CB2):paired_minimum_bounds_ann_fn <-1 analystAt(CB1):[0.25,1], hasLabel(CB1, Lfunc):[0.1,1], hasLabel(CB2, Lop):[0.1,1], implements(Lfunc, Lop):[0.1,1], stepFrom(CB1, CB2) future(Y) <-1 stepFrom(X,Y), analystAt(X):[0.01,1] ~stepFrom(X,Y) <- future(Y), ~analystAt(Y):[0.25,1], ~analystAt(X)
The six traversal rules advance the analyst one step per time point (<-1): if the analyst occupies CB1 with lower bound at least 0.25 and the trajectory contains the edge stepFrom(CB1, CB2), the step is entailed whenever some knowledge-graph relation (can cause, contributes to, derives, unsafe variant of, manifestation of, implements) links a label observed on CB1 to a label observed on CB2. The clause thresholds ([0.1, 1] on hasLabel and on the relation, [0.25, 1] on analystAt) act only as gates; the bound assigned to the head is computed by paired minimum bounds ann fn, which recovers the (cause, effect) label pairing imposed by the relation clause. For each grounded relation edge it takes the elementwise minimum of the relation’s bound and the hasLabel bounds of the matching labels on the two code blocks, so inference is never mixed across unrelated label pairs, and annotates analystAt(CB2) with the pair attaining the highest lower bound. If no pair meets the threshold, the head retains its default [0, 1], complete uncertainty, and the step is not entailed. The final two rules make that failure explicit for reporting. future(Y) marks the block one step ahead on the analyst trajectory; if the analyst never reaches there, the negation rule drives stepFrom(X,Y) toward [0, 0], contradicting the trajectory edge asserted at [1, 1]. The two formulations converge. The head failing to reach µmin and the resulting bound conflict on stepFrom identify the same step, and is shown in the reasoning trace of Figure 9.
15
H.2
Propagation Rules (28)
H.2.1
Label-Propagation Rules (13)
These map raw libc labels to higher-level semantic labels through conjunctive clauses. A single libc call is often ambiguous, but the combination is not. Head annotations encode confidence in how strongly a combination implies the semantic label. hasLabel(X, memory_write):[1.0,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, memmove):[0.6,1] hasLabel(X, memory_write):[1.0,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, memory_write):[1.0,1] <- hasLabel(X, sprintf):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, memory_write):[0.778,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, memset):[0.6,1] hasLabel(X, memory_write):[0.714,1] <- hasLabel(X, memmove):[0.6,1], hasLabel(X, memset):[0.6,1] hasLabel(X, memory_write):[0.5,1] <- hasLabel(X, memset):[0.6,1], hasLabel(X, snprintf):[0.6,1] hasLabel(X, memory_write):[0.429,1] <- hasLabel(X, memset):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, memory_write):[0.2,1] <- hasLabel(X, fgets):[0.6,1], hasLabel(X, memset):[0.6,1] hasLabel(X, copy_operation):[1.0,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, memmove):[0.6,1] hasLabel(X, copy_operation):[1.0,1] <- hasLabel(X, memcpy):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, copy_operation):[0.9,1] <- hasLabel(X, sprintf):[0.6,1], hasLabel(X, strcpy):[0.6,1] hasLabel(X, input_operation):[1.0,1] <- hasLabel(X, fgets):[0.6,1], hasLabel(X, sscanf):[0.6,1] hasLabel(X, size):[1.0,1] <- hasLabel(X, destination_size_validation):[0.6,1], hasLabel(X, length_calculation):[0.6,1]
H.2.2
Relation-Propagation Rules (15)
These connect a code block’s observed labels to the domain concepts of the DKG through the graph’s typed relations. Most relations are instantiated in both directions with different bounds, so that strong and weak evidence propagate asymmetrically. hasLabel(CB, Lsemantic):[0.84,1] <-0 hasLabel(CB, Lbinary_feature):[0.7,1], evidence_of(Lbinary_feature, Lsemantic) hasLabel(CB, Lbinary_feature):[0.36,1] <-0 hasLabel(CB, Lsemantic):[0.95,1], evidence_of(Lbinary_feature, Lsemantic) hasLabel(CB, Lparent):[1,1] <-0 hasLabel(CB, Lchild):[0.7,1], is_a(Lchild, Lparent) hasLabel(CB, Lchild):[0.1,1] <-0 hasLabel(CB, Lparent):[0.95,1], is_a(Lchild, Lparent) hasLabel(CB, Lop):[0.87,1] <-0 hasLabel(CB, Lpart):[0.7,1], required_component_of(Lpart, Lop) hasLabel(CB, Lop):[0.25,1] <-0 hasLabel(CB, Lpart):[0.95,1], required_component_of(Lpart, Lop) hasLabel(CB, Lop):[0.32,1] <-0 hasLabel(CB, Lpart):[0.95,1], informative_component_of(Lpart, Lop) hasLabel(CB, Lpart):[0.29,1] <-0 hasLabel(CB, Lop):[0.95,1], informative_component_of(Lpart, Lop) hasLabel(CB, Lop):[0.15,1] <-0 hasLabel(CB, Lpart):[0.95,1], incidental_component_of(Lpart, Lop) hasLabel(CB, Lpart):[0.2,1] <-0 hasLabel(CB, Lop):[0.95,1], incidental_component_of(Lpart, Lop) hasLabel(CB, Lrealization):[0.9,1] <-0 hasLabel(CB, Lop):[0.7,1], possible_realization(Lrealization, Lop) hasLabel(CB, Lop):[0.4,1] <-0 hasLabel(CB, Lrealization):[0.9,1], possible_realization(Lrealization, Lop) hasLabel(CB, Lconcept):[0.41,1] <-0 hasLabel(CB, Lop):[0.9,1], involves(Lop, Lconcept)
16
hasLabel(CB, Lused):[0.3,1] <-0 hasLabel(CB, Lop):[0.95,1], may_use(Lop, Lused) hasLabel(CB, Lop):[0.18,1] <-0 hasLabel(CB, Lused):[0.95,1], may_use(Lop, Lused)
H.3
Transitive-Closure Rules (6)
These make a DKG relation transitive where its semantics warrant it, letting the reasoner chain multi-hop causal and compositional relationships that no single edge states explicitly. can_cause(E1, E3) <- can_cause(E1, E2), can_cause(E2, E3) contributes_to(E1, E3) <- contributes_to(E1, E2), contributes_to(E2, E3) derives(E1, E3) <- derives(E1, E2), derives(E2, E3) involves(E1, E3) <- involves(E1, E2), involves(E2, E3) is_a(E1, E3) <- is_a(E1, E2), is_a(E2, E3) required_component_of(E1, E3) <- required_component_of(E1, E2), required_component_of(E2, E3)
I
Deployment: Reasoning Trace Example
A reasoning trace accompanies every non-entailment inference. A tree recording which observations and which rule firings produced each bound, rooted at the first step the domain knowledge does not entail. Figure 9 shows the trace for the running example of the main paper, in which an LLM assigns memset to the memory-management class and then assumes it can perform an integer size calculation. The leaves are facts of two kinds: libc hasLabel observations on the code blocks along the path (here userInput and scanf), and the stepFrom edges of the proposed trajectory itself, annotated [1, 1]. Interior nodes are rule firings. A relation-propagation rule fires on the conjunction of observed labels to derive the higher-level stack based buffer overflow label, which is what bridges code-level evidence to the CWE 121 domain-knowledge graph; traversal and step-control rules then advance the analyst along the prefix that the domain knowledge does entail. At the root, no relation in the domain-knowledge graph connects the labels at the two blocks, so no traversal rule fires and analystAt at that block never reaches µmin . The step-control rule of Section H then makes the corresponding stepFrom bound [0, 0], contradicting the [1, 1] set from the trajectory, and the program reports the conflict as a non-entailment at that step. Because every node records both its bound update and the fact or rule that caused it, an analyst can audit exactly which observations and which rule firings reject the step, rather than receiving an unexplained conclusion.
J
Prompt Templates
All three prompting techniques share an identical base prompt: the system role, the CWE information, the Ghidra label vocabulary, and the constraint and output-format blocks. The techniques differ only in a final technique-specific block and, for self-refinement, in a multi-call structure. We therefore give the base prompt once (Section J.1) and then the per-technique additions (Sections J.2–J.4). The transcript below is the CWE-416 prompt for gpac; the main paper shows the abridged CWE-121 form. Three fields are substituted per target: the CWE information, the label vocabulary, and MIN PATH EDGES, which is 4 here because gpac’s call graph is too shallow for six-edge paths and 6 for every other binary (Section G.1). Under domain-knowledge enrichment (+DK) the only change is that each label group in the vocabulary is augmented with reasoner-derived DK labels (Section J.5); every other block is byte-identical. Prompts are reproduced verbatim.
J.1
Shared Base Prompt
Sent in full on every call, including each of the three self-refinement calls. Label groups beyond the three shown are omitted for space; a binary typically yields tens of groups.
17
Figure 9: The reasoning trace behind a non-entailment inference, for the analyst path of the running example in the main paper. Green leaves are facts (libc label observations and the trajectory’s own stepFrom edges); orange nodes are rule derivations, each annotated with the bound it assigns; the red root is the first step no domain-knowledge relation entails. Each node records the fact or rule responsible for its bound update. === SYSTEM PROMPT === You are a security analyst specializing in defensive binary code review. You reason about which sequences of function behaviors in a binary are relevant to a given software weakness class (CWE), so that code regions worth reviewing can be prioritized for detection and remediation. Your task is to generate realistic code-review paths - ordered sequences of semantic function behaviors an analyst would examine when assessing a binary for a specific weakness type. These paths describe which code a reviewer would inspect during analysis, not necessarily what they would find. === USER PROMPT === CWE Information: CWE ID: CWE-416 CWE Name: Use After Free CWE Description: Use After Free - a program continues to use a pointer after the memory it references has been freed, allowing an attacker to control the freed region and influence program behavior or execution. Binary Static Analysis Labels: The following are groups of function labels detected via Ghidra static analysis of the target binary. Each group represents functions that co-occur in the same code region. Use these as your label vocabulary when constructing path stages: Group 1: [’__stack_chk_fail’, ’abort’, ’clock’, ’exit’, ’exp’, ’fwrite’, ’gmtime’, ’log’, ’realloc’, ’remove’, ’scanf’, ’sin’, ’sprintf’, ’strcat’, ’strcpy’, ’strtol’, ’vsnprintf’, ’vsprintf’] Group 2: [’abort’, ’fseek’, ’ftell’, ’fwrite’, ’vfprintf’] Group 3: [’__stack_chk_fail’, ’clock’, ’exit’, ’fputs’, ’fread’, ’fseek’, ’ftell’, ’fwrite’, ’log’, ’sprintf’, ’strcat’, ’strcpy’, ’strrchr’, ’strtol’] Path Diversity: The generated exploration paths should be meaningfully different from each other. Each path should represent a different way an analyst might examine the code
18
while assessing it for the mentioned weakness. Exploration Path Framing: Each path represents the exploration journey of a human expert or security researcher navigating through the binary, looking for potential vulnerabilities. Not every stage in the path needs to directly relate to CWE-416 - a human expert would follow interesting code paths, investigate suspicious functions, explore memory management patterns, and sometimes backtrack from dead ends. The path reflects how someone would realistically explore the code, not just the shortest route to a vulnerability. Label Vocabulary Constraint: Every label used in every stage subset must come from the provided label vocabularies. Do not use any label that does not appear in the provided vocabularies. Label Group Selection Constraint: At each stage of the path, select one label group from the provided groups and use only those labels from that group that makes sense for that stage. All labels within a single stage must come from the same group. Minimum Path Length: Each generated path must contain at least 4 edges (transitions between stages). Paths with fewer than 4 edges are invalid. Per Path Reasoning: For each exploration path, provide a brief explanation under the key ’explanation’ describing the analyst’s reasoning - how this sequence of labels represents a plausible region of code to examine when assessing the target weakness. Exploration Likelihood Score: For each path, provide a score between 0.0 and 1.0 under the key ’exploration_score’ reflecting how likely an analyst would examine this trajectory when reviewing the binary. A score of 1.0 means an analyst would very likely follow this path, 0.0 means unlikely. Number of Paths: Generate maximum 50 exploration paths. Each path must be unique and independently valid. You can also decide to generate fewer than 50 paths if you determine that there are not that many high-quality, distinct paths to generate. Do not generate more than 50 paths. Free Label Subset Path Output: Return your response as a valid JSON object with the following structure: { "paths": [ { "path_id": <integer>, "cluster_sequence": [ ["label1", "label2", ...], ["label1", ...], ... ], "vulnerability_score": <float between 0.0 and 1.0>, "exploration_score": <float between 0.0 and 1.0>, "explanation": "<2 sentence explanation of why an analyst would examine this path when assessing the target weakness>" } ] } Each entry in cluster_sequence is a subset of one or more labels chosen freely from any of the provided label sets. Labels can be mixed from different sets
19
within the same stage. Do not include any text outside the JSON object. Do not use markdown formatting or code blocks.
J.2
Zero-Shot
Appended to the base prompt; a single call. Zero-Shot: Using the information provided above, generate exploration paths for the given CWE. Do not ask for clarification. Generate the paths directly.
J.3
Chain-of-Thought
Appended to the base prompt; a single call returning one JSON object in which a triage phase precedes generation. Chain-of-Thought (CoT): Reason step by step before answering, and return everything as a single JSON object that extends the output structure specified above. Phase 1 - Label analysis. Before generating any paths, examine the label groups provided above. Produce a top-level "label_analysis" object that, for each group you consider relevant, classifies its labels into one of three categories for the target CWE: "immediately_suspicious", "worth_investigating", or "likely_irrelevant", each with a one-line justification. Use this triage to decide which labels to choose for path stages. Phase 2 - Path generation. Then generate the exploration paths. Keep every field required above unchanged (path_id, cluster_sequence, vulnerability_score, exploration_score, explanation). Additionally, for each path include a "stage_reasoning" field: an array with one entry per stage in cluster_sequence, where entry i explains, stage by stage, what the analyst infers from the combination of labels present at stage i - what seeing those labels together in the same code region suggests, and why that leads to the next stage. The final JSON object must have this shape: { "label_analysis": { ... }, "paths": [ { <all fields required above>, "stage_reasoning": ["stage 0 inference", ...] } ] } Do not ask for clarification. Do not include any text outside the JSON object. Do not use markdown formatting or code blocks. Generate the analysis and paths directly.
J.4
Self-Refinement
A three-call loop. Every call re-sends the full base prompt; only the additions are shown. Call 1 is identical to zero-shot, so the loop’s cost is three generations per configuration. --- Call 1: Generate (identical to zero-shot) --Iterative Self-Refinement: Using the information provided above, generate exploration paths for the given CWE. Do not ask for clarification. Generate the paths directly. --- Call 2: Critique --[base prompt + Call-1 instruction], then: --Here are the exploration paths you generated: [ <JSON path set from Call 1> ]
20
Critically review these paths for the target CWE. What is wrong with them? Are they diverse enough? Are important labels being ignored? Are the vulnerability and exploration scores well calibrated? Respond with concise verbal feedback in plain text only - do not output JSON, code blocks, or paths. --- Call 3: Refine --[base prompt + Call-1 instruction], then: --Here are your original exploration paths: [ <JSON path set from Call 1> ] Here is feedback on them: [ <plain-text critique from Call 2> ] Now generate improved exploration paths that address this feedback. Return the refined paths using exactly the same JSON output format specified above. Do not include any text outside the JSON object. Do not use markdown formatting or code blocks.
J.5
Domain-Knowledge Enrichment
Under +DK the label vocabulary is the only block that changes. Before generation we run the domain knowledge’s mapping rules over the libc labels already present on each code block and append the derived labels to that block’s group. The generator therefore receives DK’s vocabulary but no entailment verdict, and the reasoner has not yet seen any trajectory at this point. A group that reads Group 1: [’gets’, ’sprintf’, ’strspn’]
in the baseline condition becomes Group 1: [’gets’, ’sprintf’, ’strspn’, ’missing_bounds_check’, ’unchecked_memory_write’, ’stack_pointer_overwrite’, ...]
under +DK. The added terms are DKG concepts rather than libc symbols, so the model can express a stage in the vocabulary the reasoner will later check against, instead of only in terms of the raw calls Ghidra recovered.
K
Domain Knowledge: Ontology and Graphs
The domain knowledge is a CWE-focused, code-centric ontology together with a set of instantiated knowledge graphs, one per weakness class. The ontology defines a layered class hierarchy—from concrete Beacons, CodeEntities, CodeOperations and CodePatterns, through FaultConditions and OutcomeLevelFaults, to CWE-level VulnerabilityClasses, connected by a fixed set of typed relations (e.g. is a, unsafe variant of, can cause, mitigates). A central modelling choice is to represent faults as unsafe variants of otherwise-neutral operations: an out of bounds write is an unsafe variant of a generic memory write. Safe and unsafe behaviour therefore coexist in a single graph, and the reasoner can express how missing or incorrect validation turns an ordinary operation into a memory-corruption event. The layering supports reasoning in both directions: forward, from observable beacons up through the class hierarchy to a CWE-level determination, and backward, from a hypothesised classification down to the code-level evidence that would confirm or refute it. The relation-propagation rules of Section H implement exactly this, which is why most relations are instantiated in both directions with asymmetric bounds. Each graph is populated initially by automated extraction from technical corpora (reverse-engineering manuals, security advisories, man pages), then refined by automated schema validation with targeted semantic review. We treat the resulting graphs as fixed and assumed correct throughout; the extraction and validation of domain-knowledge graphs is a separate problem that this work does not address.
21
Entities DK graph
Relations
Classes
Total
Types
Total
Rel./ent.
9 8 8
188 105 111
16 14 14
403 318 232
2.14 3.03 2.09
CWE-121 (stack buffer overflow) CWE-415 (double free) CWE-416 (use-after-free)
Table 11: The three per-CWE knowledge graphs. All graphs are directed. Classes counts ontology classes instantiated in the graph, Types the distinct relation types used, and Rel./ent. the mean number of relations per entity.
K.1
Graph Statistics
The 16 relation types, taken as the union across graphs, are contributes to, can cause, manifestation of, unsafe variant of, involves, implements, validates, may use, derives, possible realization, is a, evidence of, mitigates, required component of, informative component of and incidental component of. CWE-121 uses all 16; CWE-415 and CWE-416 use 14 each, CWE-415 omitting derives and involves and CWE-416 omitting derives and unsafe variant of. Six of the 16 are made transitive by the closure rules of Section H, and six adjudicate analyst steps in the traversal rules.
L
Extended Related Work
L.1
LLMs for Vulnerability Detection
LLMs are increasingly applied to software vulnerability detection across source code, repair, and binaries; recent surveys chart the rapid growth of this area since 2023 and catalogue the models, datasets, and evaluation setups now in use Sheng et al. (2025). A recurring finding, however, is that current models are not yet dependable on their own: a comprehensive benchmarking study by Ullah et al. Ullah et al. (2024) concludes that LLMs cannot yet reliably identify or reason about security vulnerabilities. Work that does report gains typically pairs the LLM with structure rather than trusting it in isolation—LLMxCPG, for example, uses code-property-graph slices to focus an LLM on vulnerability-relevant context Lekssays et al. (2025). This unreliability is the gap our work targets: rather than treating LLM output as an answer, we treat each proposed analyst path as a hypothesis to be checked against domain knowledge, and we operate on decompiled binaries because source is unavailable for the medical-device firmware we analyse.
L.2
LLMs for Binary Reverse Engineering
A fast-growing line of work applies LLMs directly to stripped or decompiled binaries: LLM4Decompile trains models to recover source-like code from assembly Tan et al. (2024); ReSym recovers variable and data-structure symbols from stripped binaries Xie et al. (2024); and DeGPT uses an LLM to refine and explain decompiler output Hu, Liang, and Chen (2024). Most relevant to our setting, an empirical study of human–LLM teaming in reverse engineering shows that LLMs can accelerate analyst comprehension but also mislead when their suggestions go unchecked Basque et al. (2026). These efforts improve the readability or recovered structure of a binary; they do not verify that an analyst’s reasoning over that binary is consistent with what is known about the vulnerability class. Our contribution is complementary and sits downstream: we take the recovered call-graph structure and libc labels as input and add a logical verification layer over the analyst paths reasoned on top of them.
L.3
Logic and Program Analysis for Binary Vulnerability Discovery
Classical binary vulnerability discovery relies on static analysis and taint tracking. Karonte propagates taint across the multiple binaries of a firmware image to surface insecure interactions, and its authors note that whole-firmware analysis without such cross-binary reasoning produces overwhelming alert volumes Redini et al. (2020). More 22
recently, LATTE couples an LLM with binary taint analysis, automating the taint-propagation and inspection rules that previously required manual expert customisation and reporting new CVEs in real firmware Liu et al. (2025). These systems share our binary-level, source-free setting and our use of domain rules, but their goal is to emit vulnerability alerts via taint propagation. Ours is a different problem: we verify whether an analyst’s exploration path is logically entailed by a domain-knowledge graph under a temporal annotated logic, retaining the exploratory structure that alert-only pipelines discard while still steering it toward vulnerabilities. Where LATTE uses the LLM to produce the analysis, we use logic to check the LLM output.
L.4
Constraining and Verifying LLM Reasoning with Structure
Because LLM hallucinations are often confident and cannot be caught by probability-based checks, a growing body of work pairs LLMs with symbolic or structured components. Logic-LM translates a problem into symbolic form, solves it with a deterministic solver, and self-refines from solver errors Pan et al. (2023); knowledge-graph-guided methods such as Reasoning-on-Graphs Luo et al. (2024a) and Graph-Constrained Reasoning Luo et al. (2024b) constrain LLM reasoning to paths grounded in a KG to reduce hallucination on question-answering benchmarks. We share the premise that an independent structured layer must gate LLM output, but differ in kind rather than degree. These methods align reasoning to a walk within a single knowledge graph and are evaluated on naturallanguage QA. In our setting the object being verified is a trajectory through the binary’s call graph, while the constraints it must satisfy live in a separate domain-knowledge graph, so verification is an alignment between two graphs rather than a walk within one. The temporal, open-world semantics also admit constraints those methods do not model: analyst position is time-indexed, so a step is licensed only at the time point it is proposed, and negation over derived state lets the program assert what the domain knowledge fails to establish rather than only what it establishes (Section H). The target is likewise different—provable, explainable accept/reject inferences in a safety-critical binary domain, rather than answer faithfulness on general benchmarks.
L.5
Vulnerabilities in Medical-Device Software
The application domain motivates the entire effort. Connected medical devices —infusion pumps, insulin pumps, pacemakers—run long-lived embedded software that is hard to patch and frequently analysable only as deployed binaries. Large-scale analyses underscore the scale of the problem: a study of over 200,000 infusion pumps found that roughly three-quarters carried known security weaknesses, many tied to years-old, unpatched CVEs Das (2022), and reviews of FDA safety communications document repeated device vulnerabilities with direct patient-safety consequences Menon (2026). This is precisely the regime our system is built for: source-free analysis of the deployed artifact, with a logical guarantee that surviving analyst paths are consistent with encoded domain knowledge.
L.6
Summary
Unlike prior LLM-for-security work, which treats the model’s output as a prediction to be trusted or scored, we treat each LLM-proposed analyst trajectory as a hypothesis and pose its validation as a formal entailment-checking problem against domain-knowledge. To our knowledge, this is the first framework to verify LLM-generated exploration paths—as opposed to final answers or natural-language reasoning—using temporal annotated logic.
References Basque, Z. L.; Doria, S.; Soneji, A.; Gibbs, W.; Doupé, A.; Shoshitaishvili, Y.; Losiouk, E.; Wang, R.; Aonzo, S.; et al. 2026. Decompiling the Synergy: An Empirical Study of Human-LLM Teaming in Software Reverse Engineering. In NDSS. Das, A. 2022. Know Your Infusion Pump Vulnerabilities and Secure Your Healthcare Organization. Technical report, Palo Alto Networks Unit 42. Analysis of over 200,000 infusion pumps; https://unit42.paloaltonetworks. com/infusion-pump-vulnerabilities/. 23
Hu, P.; Liang, R.; and Chen, K. 2024. DeGPT: Optimizing Decompiler Output with LLM. In NDSS. Lekssays, A.; Mouhcine, H.; Tran, K.; Yu, T.; and Khalil, I. 2025. {LLMxCPG}:{Context-Aware} vulnerability detection through code property {Graph-Guided} large language models. In 34th USENIX Security Symposium (USENIX Security 25), 489–507. Liu, P.; Sun, C.; Zheng, Y.; Feng, X.; Qin, C.; Wang, Y.; Xu, Z.; Li, Z.; Di, P.; Jiang, Y.; et al. 2025. Llm-powered static binary taint analysis. ACM Transactions on Software Engineering and Methodology, 34(3): 1–36. Luo, L.; Li, Y.-F.; Haffari, R.; and Pan, S. 2024a. Reasoning on graphs: Faithful and interpretable large language model reasoning. In International Conference on Learning Representations, volume 2024, 14400–14423. Luo, L.; Zhao, Z.; Haffari, G.; Li, Y.-F.; Gong, C.; and Pan, S. 2024b. Graph-constrained reasoning: Faithful reasoning on knowledge graphs with large language models. arXiv preprint arXiv:2410.13080. Menon, V. 2026. Cybersecurity Breaches in Medical Devices: Analyzing FDA Safety Communications in Response to Patient Security Concerns. Frontiers in Digital Health, 8: 1701551. Pan, L.; Albalak, A.; Wang, X.; and Wang, W. 2023. Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning. In Bouamor, H.; Pino, J.; and Bali, K., eds., Findings of the Association for Computational Linguistics: EMNLP 2023, 3806–3824. Singapore: Association for Computational Linguistics. Redini, N.; Machiry, A.; Wang, R.; Spensky, C.; Continella, A.; Shoshitaishvili, Y.; Kruegel, C.; and Vigna, G. 2020. Karonte: Detecting Insecure Multi-binary Interactions in Embedded Firmware. In 2020 IEEE Symposium on Security and Privacy (SP), 1544–1561. Sheng, Z.; Chen, Z.; Gu, S.; Huang, H.; Gu, G.; and Huang, J. 2025. LLMs in Software Security: A Survey of Vulnerability Detection Techniques and Insights. ACM Comput. Surv., 58(5). Tan, H.; Luo, Q.; Li, J.; and Zhang, Y. 2024. Llm4decompile: Decompiling binary code with large language models. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing, 3473–3487. Ullah, S.; Han, M.; Pujar, S.; Pearce, H.; Coskun, A.; and Stringhini, G. 2024. Llms cannot reliably identify and reason about security vulnerabilities (yet?): A comprehensive evaluation, framework, and benchmarks. In 2024 IEEE symposium on security and privacy (SP), 862–880. IEEE. Xie, D.; Zhang, Z.; Jiang, N.; Xu, X.; Tan, L.; and Zhang, X. 2024. Resym: Harnessing llms to recover variable and data structure symbols from stripped binaries. In Proceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, 4554–4568.
24