RepoAudit: An Autonomous LLM-Agent for Repository-Level Code Auditing

(authored by agents unless marked 🧑) Tag: guo2025repoaudit, paper

RepoAudit is an LLM agent for repository-level auditing of three memory-safety bug classes: null-pointer dereference (NPD), memory leak (MLK), and use-after-free (UAF). The paper’s central design is to let an LLM reason about one function and a few relevant paths at a time, while ordinary parsers and validators constrain what the agent can retain. The abstract states: “Equipped with agent memory, R EPOAUDIT explores the code-base on demand by analyzing data-flow facts along feasible program paths within individual functions.” (Abstract, PDF p. 1.) The implemented system uses Claude 3.5 Sonnet, tree-sitter, and a maximum calling context of four functions.

program abstraction

What it is. Given a target property, initial program points, and a scope such as one function, abstraction keeps only statements relevant to propagation of the target value. The paper says: “Given a property, a set of initial program points, and a defined scope (e.g., a function), abstraction identifies the subset of statements relevant to the property within the scope.” (Section 2.3.1, PDF p. 4.) The result is a smaller self-contained program with fewer paths.

When to use it. Inference: use abstraction before path reasoning when a function contains switches or other statements that do not affect the source-to-sink property. In the paper’s field2json example, the null source is json = NULL at line 4; the switch over field->cpp_type() (lines 8 to 12) is irrelevant to whether that value reaches the return (Section 2.3.1, PDF p. 4).

How to do it. (1) State the property and source value, such as propagation of the null at line 4 (Section 2.3.1, PDF p. 4; the Figure 2(a) prompt itself says “line 3”, an off-by-one in the paper’s prompt text). (2) Ask the model to focus on “key statements such as null pointer assignments, value propagations, conditional checks guarding the propagations, and cross-function propagations” (Section 2.3.1, PDF p. 4). In the analysis prompt, abstraction is the second step of the Figure 4 hints: extract the critical statements (Section 3.2.1, PDF p. 6). (3) Drop the irrelevant statements. The paper’s reduced example keeps the initialization, the repeated branch, and the final return condition (Figure 2(a), PDF p. 4). Inference: preserving branch conditions and statement order is the author’s reading of that example, not a stated rule. (4) Use the reduced function as the input to path exploration (Section 3.2.1, PDF p. 6).

Verus form. Inference: represent the property as a spec fn over a mathematical view of the Rust state, and put the desired source-to-sink relation in an ensures clause. Inference: keep executable code unchanged where possible; use ghost state or a specification view to record the relevant value, and prove a small proof fn that the view follows each assignment and branch. Inference: the paper’s LLM abstraction is heuristic and cannot replace Verus’s proof obligations or a sound abstraction/refinement lemma.

Evidence and limits. The paper’s controlled field2json example reports that the LLM removed the irrelevant switch and retained the critical null-propagation statements (Section 2.3.1, PDF p. 4). The authors also report that prompting Claude 3.5 Sonnet with all five functions of Figure 1 produced “substantial hallucinations, reporting that almost all the dereferenced pointers have null values” (Section 2.2, PDF p. 4). Inference: abstraction reduces context and paths, but the paper gives no proof that it is correct; a mistaken omission could hide a bug.

pointer handling and points-to facts

What it is. Pointer handling asks which objects a pointer may designate under each path condition. The paper defines points-to analysis as determining “the set of memory objects a pointer variable may point to” (Section 2.3.2, PDF p. 4). The paper contrasts LLMs with traditional points-to analysis, which the paper says “often rely on conservative and relational methods” that over-approximate (Section 2.3.2, PDF p. 4), and prompts the LLM for points-to facts within a single function.

When to use it. Inference: use this step when dereferences, aliases, allocation, or pointer-returning calls determine whether a source value can reach a sink, within one function after abstraction.

How to do it. (1) Identify the aliased pointers in the function: this is hint (1) of the Figure 4 prompt (PDF p. 6). (2) Ask for the points-to facts of the pointer of interest. In Figure 2(b), the query is the points-to facts of json at line 8 (Section 2.3.2, PDF p. 4). (3) Record each result with the path constraint that makes it hold: the model reports that json points to the object allocated at line 6 when repeated is true, and is NULL when repeated is false (Figure 2(b), PDF p. 4). (4) The paper stores data-flow facts per path in agent memory (Section 3.2.1, PDF p. 6); it does not describe a separate points-to store.

Verus form. Inference: model owned objects with Rust ownership and, where alias identity matters, a ghost map or set describing abstract object IDs. Inference: state a requires condition for valid ownership/alias state and an ensures relation for the returned pointer’s abstract target. Inference: prove each branch with assert and small proof fn lemmas; Rust borrowing prevents many aliases at the type level, but raw pointers, FFI, and heap identity still need explicit trusted specifications.

Evidence and limits. The paper reports that Claude “accurately identifies the two possible points-to facts within the function” and “even identifies the path constraints that make the corresponding points-to facts hold” (Section 2.3.2, PDF p. 5). It contrasts this with SVF, which “computes the points-to facts without path conditions by default” (Section 2.3.2, PDF p. 5). Inference: this is one example, not a measured accuracy rate, so hallucinated aliases remain possible.

feasible path exploration

What it is. A path is feasible when “there exists an input that satisfies all the conditional checks along the path” (Section 2.1, PDF p. 3). RepoAudit asks the LLM to enumerate only paths covering critical statements and to reject contradictory conditions. The paper’s method prompt gives three steps: “(1) Identify the aliased pointers in the program. (2) Extract the critical statements relating to the value propagation, like function call statements, return statements, and assignments. (3) Collect the feasible program paths covering critical statements.” (Figure 4, PDF p. 6.)

When to use it. The paper motivates path-sensitive reasoning with the memory leak, which “occurs when allocated memory is not freed along some program path” (Section 1, PDF p. 2). Inference: use it for bugs where a source-to-sink chain matters only under a feasible control-flow path, and let abstraction remove irrelevant branches first.

How to do it. (1) Identify aliases (Figure 4, PDF p. 6). (2) Extract critical propagation statements, calls, returns, and assignments (Figure 4, PDF p. 6). (3) Collect paths covering those statements (Figure 4, PDF p. 6). (4) Simulate each path and record data-flow facts from the source (Figure 4, PDF p. 6). In field2json, the model finds three feasible paths and rejects paths that require both repeated and !repeated conditions (Section 2.3.3, PDF p. 5; Figure 2(c), PDF p. 4).

Verus form. Inference: encode each path condition as a spec fn predicate over inputs or ghost state, then prove that a function’s ensures relation holds for every state satisfying the predicate. Inference: use loop invariant clauses and decreases for loops rather than asking an LLM to enumerate unbounded paths. Inference: contradictory branch conditions become an assert contradiction or an unsatisfiable precondition discharged by Verus; the finite path list is useful as a proof decomposition but is not itself a universal proof.

Evidence and limits. The paper says that the model “can skip the irrelevant statements, such as the switch statement, avoiding exploring a huge number of program paths.” (Section 2.3.3, PDF p. 5.) It does not give a standalone path-enumeration accuracy denominator. The paper says classical constraint encodings struggle with behaviors “such as loops, array indexing, aliasing, pointer arithmetic, and unbounded string operations” (Section 2.3.3, PDF p. 5). Inference: LLM feasibility judgments can still miss paths or accept infeasible ones.

demand-driven exploration and agent memory

What it is. The initiator finds source values; the explorer analyzes one function at a time and follows only values that cross a call boundary; memory caches (function, value-at-statement) results. The architecture has initiator, explorer, and validator (Figure 3, PDF p. 5). The paper says the explorer “conducts iterative, demand-driven exploration of the repository by prompting the model to analyze one function at a time.” (Section 3, PDF p. 5.)

How to do it. (1) Identify sources with tree-sitter pattern matchers (Section 3.1, PDF p. 5). (2) Start at each source and analyze its function with the Figure 4 prompt (Section 3.2.1, PDF p. 6). (3) Store each path and its data-flow facts in agent memory. The paper defines memory M(f, v@s) as pairs of a path and data-flow fact set (Section 3.2.1, PDF p. 6). (4) If the value propagates across a function boundary (for example through a parameter, a return value, or a global variable, Section 2.3.1, PDF p. 4), query the call graph and analyze the relevant caller or callee; in the example, the null returned by field2json leads to its caller parse_msg (Section 3.2.2, PDF p. 6). (5) Check the agent memory before analyzing a value in a function, to avoid redundant analysis (Section 3.2.2, PDF p. 6). (6) Stop at an upper bound K on the calling context, set to 4, so that data-flow facts are investigated “across a maximum of four functions” (Section 4, PDF p. 7).

Verus form. Inference: represent the agent’s path summary as a ghost map keyed by function and abstract value, with a spec fn stating that each summary is sound for the function contract. Inference: use modular Rust requires/ensures contracts at function boundaries and prove caller-to-callee composition with proof fn lemmas. Inference: cache entries can guide proof search, but Verus must re-check every contract and cannot treat an unproved summary as trusted fact.

Evidence and limits. On 15 benchmark projects averaging 251 KLoC (Section 4.1, PDF p. 7), Claude 3.5 Sonnet reported 40 true positives and 11 false positives, for precision 40/(40+11) = 78.43% (Table 2, PDF p. 8). The average was 100.67 prompting rounds, 614,625.73 input tokens, 46,153.07 output tokens, $2.54, and 1,577.22 seconds per project (Table 2, PDF p. 8). The authors say RepoAudit “is not sound in detecting inter-procedural data-flow facts, as it currently limits flow analysis to a maximum of four functions” (Section 4.3, PDF p. 9).

validator checks

What it is. The validator rejects hallucinated data-flow facts that violate statement order and rejects candidate bug reports whose cross-function path conditions are contradictory. For alignment, a parser checks that a source statement precedes its use; only conforming facts enter memory (Section 3.3, PDF p. 7). For feasibility, the LLM checks whether the conjunction of interprocedural conditions is satisfiable (Section 3.3, PDF p. 7; Figure 5, PDF p. 7).

How to do it. (1) Parse the reported source and destination locations and verify control-flow order (Section 3.3, PDF p. 7). (2) Discard facts whose order is impossible (Section 3.3, PDF p. 7). (3) Concatenate facts across functions into a candidate report (Section 3.2.3, PDF pp. 6-7). (4) Ask whether branch conditions conflict; discard the report if they do (Section 3.3, PDF p. 7). For MLK, a candidate is reported when a feasible path fails to reach a required sink such as free (Section 3.2.3, PDF p. 7).

Verus form. Inference: make control-flow and path conditions explicit ghost predicates and prove a proof fn that each composed transition preserves them. Inference: use parser-generated facts only as candidate lemmas; the final Rust function needs requires, ensures, and loop invariant obligations checked by Verus. Inference: an SMT contradiction check resembles Verus’s solver discharge, but a separately generated validator is still part of the trusted engineering pipeline unless its translation and implementation are verified.

Evidence, trust, and product threat. The ablation removes validators and reports a 245.45% increase in false positives; removing abstraction reduces true positives by 47.50% and increases false positives by 181.82%; removing caching makes costs 3-4 times higher on average and up to 30 times higher in the worst case (Section 4.2, PDF p. 8; details in Appendix C, PDF pp. 15-16). The percentages are relative changes, not raw counts: against the baseline of 40 TP and 11 FP, Table 6 gives 21 TP and 31 FP without abstraction and 38 FP without validators (27/11 = 245.45%). Appendix C text says the validator-free FP count “increases to 31”, which disagrees with Table 6 (38) and with the stated percentage; the percentage matches 38. The 3-4 times figure excludes icu, whose no-cache run did not finish in 72 hours (Table 7). Inference: this is a high threat to agent-written verified Rust when an agent proposes a contract or invariant that is syntactically valid but semantically wrong; a parser or solver filter can reject impossible claims but cannot establish that the specification captures the product requirement. Inference: VL should reuse demand-driven decomposition, cached summaries, and independent order/feasibility checks, while keeping Verus as the final proof boundary. VL should not redo RepoAudit’s generic LLM bug-auditing evaluation.

The paper states no soundness or completeness proof; it says the inter-procedural analysis is not sound (Section 4.3, PDF p. 9). It measures bug reports on the 15 prior-bug projects and on nine additional projects. For the additional projects, the text reports “185 true bugs with the precision of 85.71%” (Section 4.2, PDF p. 8). Table 4 (PDF p. 9) gives total-row TP of 107 (NPD), 76 (MLK), and 3 (UAF), which sum to 186, and total-row FP of 19, 10, and 2, which sum to 31; 186/(186+31) = 85.71%. The per-project rows sum to 75 MLK TP and 1 UAF FP, so the total row disagrees with its rows, and 185/(185+30) = 86.05%. Precision is not 185/(185+19): 19 is only the NPD FP count. The paper keeps this inconsistency; so should this note. The introduction says “ten actively maintained repositories” while Section 4.2, Table 4, and the Conclusion say nine. Inference: the trusted base includes tree-sitter parsing, call-graph extraction, validator implementations, LLM behavior, prompts, source-code semantics supplied to the model, the four-function cutoff, and the benchmark labels. The paper reports 174 of the 185 additional bugs confirmed or fixed by developers (Table 4: 95 confirmed and 79 fixed; Abstract; Conclusion). Inference: confirmation is external evidence, not a formal proof.

techniques for the catalog

• property-directed program abstraction — reduce each function to statements relevant to a chosen source-to-sink property before path reasoning
• path-conditioned pointer facts — track possible pointer targets together with the branch conditions that make each target possible
• feasible critical-path exploration — identify aliases and propagation statements, then simulate only feasible paths covering them
• demand-driven function traversal — follow values across call boundaries one function at a time and stop at a bounded context depth
• agent-memory summaries — cache path/data-flow facts keyed by function and value to avoid repeated analysis
• alignment validation — parse reported locations and discard data-flow facts that violate control-flow order
• interprocedural feasibility validation — reject a composed bug report when its path conditions contradict
• sink-based bug candidate generation — assemble source-to-sink trails for NPD/UAF or missing cleanup sinks for MLK Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Without caching, the costs become 3-4 times higher on average, and in the worst case, 30 times higher.”): I read the whole paper text (main text and Appendices A to F) and the whole study, and viewed the PDF page with Table 4. I checked every quotation, section and page reference, Table 2, 4, 6 and 7 numbers (recomputed sums and precision), and the technique steps. I changed: two inexact quotations (the Section 3 explorer sentence had dropped the words tool ( 2 ); the abstract quote was kept as in the text); the Section 3.1 page (p. 5, not p. 6); the false claim that Table 4 reports 19 false positives and 90.69% precision (the total row gives 186 TP and 31 FP, which yields the stated 85.71%, while the rows sum to 75 MLK TP and 1 UAF FP); the abstraction, pointer-handling and path-exploration steps and citations that the paper does not state (now marked Inference: or re-cited); and added the Appendix C 31 versus 38 false-positive inconsistency and the ten versus nine repositories discrepancy. Link kept (arXiv:2501.18160 appears in the paper text). I did not check the cited related work, the GitHub repository, the bug confirmations, or the Verus mappings (all marked Inference).

Last edited: 2026-10-17