PaperlayerView exact revision on arXiv

Source-linked AI summary

Soundness Checking of Taint Flow Models

Samarth Kishor, Victor Nicolet, Joey Dodds

arXiv:2609.28750v1cs.SE

TL;DR

Precise taint flow models help static analyses scale, but manual modeling is tedious and potentially unsound, while inter-procedural modeling can be inefficient. The paper pairs LLM-generated models with a symbolic soundness checker that uses lightweight analyses and recursive callee models. Across the evaluated Go repositories, the approach proved properties that timed out without models and introduced no additional false positives.

  • Problem

    Precise taint models support scalable analyses, but manual modeling is tedious and potentially unsound, and inter-procedural analysis can be inefficient.

    Source: §1 · pp. 1–2

  • Method

    An LLM generates a precise candidate model, and a symbolic checker verifies soundness using static analyses and recursively checked callee models when needed.

    Source: §1 · p. 2

  • Results

    The approach proved 9 taint flow properties that timed out without models and added no false positives over baseline taint analysis.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The evaluated LLM-generated models enabled more efficient taint analysis without compromising soundness or precision in the studied setting.

    Source: §8 · p. 25

    Soundness checking is restricted to eligible methods, and dynamic dispatch makes proofs relative to the analyzed application.

    Source: §5.5 · p. 19

Abstract

from arXiv · show

Existing state-of-the-art static taint flow analyses for imperative programming languages can scale to large applications by using precise user-provided taint flow models of library methods. However, manually and precisely modeling a method's taint flows is tedious and potentially unsound. Furthermore, automatically modeling the method via an inter- procedural taint analysis can be inefficient. To solve this problem, we propose a guess-and-check approach: (1) an LLM agent that generates a precise taint flow model of a method and (2) a symbolic algorithm to check the soundness of the model. The algorithm deduces which taint flows must not occur in the method for the LLM's taint flow model to be sound, and uses lightweight static analyses (e.g., type system and pointer analysis) to prove these must-not-flows. When these analyses are insufficient, the algorithm deduces maximally-general callee models and recursively verifies their soundness, avoiding a full inter-procedural taint analysis in most cases. Since a more precise model requires fewer must-not-flows to be verified, the precision of the LLM's model directly determines the efficiency of our approach. We evaluate our approach on 97 LLM-generated taint flow models for methods in 6 large Go codebases and prove the models sound for 93% of the methods they cover. The proven-sound LLM-generated models are also precise, resulting in no new false-positives when proving taint flow properties.

1 INTRODUCTION

Precise method models let compositional taint analyses scale, but constructing them with inter-procedural analysis can be inefficient and existing models may not avoid false positives. The paper proposes using an LLM to generate precise candidate models, then checking their soundness with static analyses and recursive callee summaries.

1 INTRODUCTION

  • Precise whole-program taint analyses can require hours and tens of gigabytes on large applications, motivating reusable method models that summarize flows across calling contexts.Field-sensitive models can improve precision by tracking flows between individual object fields.Source: §1 · p. 1
  • The constructive approach uses inter-procedural compositional taint analysis to model methods, but its models may remain too imprecise to avoid false positives in real-world properties.Configuring an analysis to trade precision for performance is manual and may require knowledge users lack.Source: §1 · pp. 1–2
  • Instead, an LLM guesses a precise model that a soundness checker verifies, making verification effort depend on model precision rather than implementation details.The model-generation agent can use method documentation and source code to avoid worst-case models that send every input to every output.Source: §1 · p. 2
  • The checker derives must-not-flows from the difference between all possible input-output flows and the candidate model, then uses type-system and pointer analyses to prove them.If needed, it computes intra-procedural flows, deduces maximally-imprecise callee models, and recursively checks them rather than analyzing every transitively called function.Source: §1 · p. 2
  • The soundness proof assumes no unsafe memory operations or reflection and is relative to the analyzed application.The approach was instantiated for Go and evaluated across 6 repositories, 16 taint flow properties, and 97 automatically generated models.Source: §1 · pp. 2–3
  • The approach proved 9 taint flow properties that timed out without models, while LLM-generated models added no false positives over baseline taint analysis.The evaluation analyzed 6 Go repositories and automatically generated 97 models.Source: §1 · p. 3

2 RUNNING EXAMPLE

ProcessReq illustrates how the approach checks a precise LLM-generated taint model without analyzing every callee. Lightweight analyses and recursively checked callee models establish that the candidate flow from the request to the logger is sound.

2 RUNNING EXAMPLE

  • ProcessReq parses and asynchronously logs an HTTP request, while parseReq is complex and logReq raises concurrency challenges for flow-sensitive analysis.The example motivates checking a precise candidate rather than constructing it through an inter-procedural analysis.Source: §2 · p. 3
  • The LLM proposes {req⇝log}, and the algorithm checks whether that candidate over-approximates all possible taint flows through the method and its callees.The candidate is generated instead of being constructed by a potentially inefficient flow-sensitive inter-procedural taint analysis.Source: §2 · pp. 3–4
  • Comparing the candidate with the most-general summary yields three must-not-flows: req̸⇝ret, log̸⇝req, and log̸⇝ret.These flows must be absent in ProcessReq and its transitive callees for the candidate to be sound.Source: §2 · p. 4
  • Type analysis cannot prove the remaining flows to pointer-like req, while immutability analysis proves ret is constant and removes log̸⇝ret.The type analysis can rule out flows to non-pointer-like outputs; the return value is nil or an error-string constant.Source: §2 · p. 4
  • The soundness conclusion excludes implicit taint flows, so the return value's dependence on len(body)==0 does not count as a taint flow.The approach therefore concludes that no tainted data flows to the return value.Source: §2 · p. 4
  • When static checks are insufficient, the algorithm analyzes ProcessReq intraprocedurally and deduces callee models constrained by its known flows and must-not-flows.The computed flows leave call nodes unresolved; callee models must not introduce flows that would violate the candidate model.Source: §2 · pp. 5–6
  • The deduced models are parseReq: {req⇝ret} and logReq: {body⇝log, req⇝log, log⇝body}, allowing parseReq to use its sound most-general summary.The approach avoids expensive taint-flow computation for parseReq without losing precision in the example.Source: §2 · p. 6
  • The algorithm proves the ProcessReq model {req⇝log} sound without an inefficient taint analysis of its callees.For logReq, type and immutability analyses establish the remaining must-not-flows; the check assumes the program is data-race-free.Source: §2 · p. 6

3 TAINT SEMANTICS

The paper formalizes taint propagation and method summaries in a simple imperative language. Its semantics track flows between access paths, including aliasing and caller-visible effects across method calls.

3 TAINT SEMANTICS

  • The taint semantics instrument a simple imperative language to track flows and formalize when a taint flow model is sound.The language supports heap-allocated objects and method calls.Source: §3 · p. 6

3.1 Programming Language

  • Program states pair an environment mapping variables to object values with a heap mapping memory locations and fields to object values.Statements evaluate a state to a new state through the evaluation function.Source: §3.1 · pp. 6–7

3.1.1 Method calls.

  • Method calls create a fresh callee environment from parameters and arguments while sharing the caller's heap, so heap modifications can be observed after return.The section also defines program traces as ordered statement sequences.Source: §3.1.1 · p. 7

3.2 Taint Flows

  • Taint flows are tracked between bounded access paths, with pointer analysis resolving may-aliasing and method-call semantics propagating flows between parameters, arguments, and returns.Access paths represent heap locations and are bounded to support sound analysis of recursive objects.Source: §3.2 · pp. 7–8

3.3 Taint Flow Model

  • A method model summarizes caller-visible input-to-output flows across calls, and soundness requires it to over-approximate the summarized flows of every call.The formalization defines summaries per call and aggregates them across program traces.Source: §3.3 · pp. 8–9

4 SYNTHESIZING AND CHECKING TAINT FLOW MODELS

The section pairs LLM-generated candidate taint models with an algorithm that checks their soundness, aiming to avoid the cost of computing precise models through full inter-procedural analysis. The checker first proves absent flows with lightweight analyses, then reasons about remaining flows through callee summaries.

4 SYNTHESIZING AND CHECKING TAINT FLOW MODELS

  • The checker combines LLM model synthesis with lightweight soundness checks, while the soundness-checking step can still become as expensive as full taint analysis.The authors report that in most cases the overall approach, including LLM generation time, is more efficient than the constructive approach.Source: §4 · p. 9

4.1 LLM-based Model Synthesis

  • The LLM agent uses code and analysis tools to generate a candidate model, but the system automatically checks it afterward because the agent may skip or ignore its own checks.The tools include source, SSA, type, and alias information.Source: §4.1 · pp. 9–10

4.2.1 Algorithm overview.

  • The checker identifies flows absent from the candidate relative to the most-general summary and attempts to prove each absent flow cannot occur.It uses lightweight analyses first and recursively checks deduced callee models when those analyses leave flows unproven.Source: §4.2.1 · p. 10, §4.2 · p. 10

4.2 Incremental Soundness Checking Algorithm

  • The algorithm’s key efficiency features are lightweight analyses that are at most linear in program size and deduced callee summaries based on intra-procedural flows.The authors identify these as the key aspects of their approach.Source: §4.2.1 · p. 11

4.2.2 Most-general Summary.

  • The most-general summary includes every input-to-output access-path flow up to a constant path-length bound, and is sound by construction.The candidate is sound if the concrete summary is contained in it; proving all flows excluded by the candidate cannot occur establishes that containment.Source: §4.2.2 · p. 11

4.3 Lightweight Analyses

Lightweight analyses prove must-not-flows using type, write, and read information. They rule out flows to immutable outputs and from unread inputs, avoiding more costly checks for those cases.

4.3 Lightweight Analyses

  • The lightweight analyses test whether inputs are unread and outputs are immutable, which can establish must-not-flows without tracing taint through every path.The analysis set includes types, immutability, and read checks.Source: §4.3 · p. 11

4.3.1 Types analysis.

  • A non-pointer-like parameter is unchanged after a method returns, so an access path rooted at it cannot receive a caller-visible taint flow.The type analysis uses this fact to prove must-not-flows to such parameter paths.Source: §4.3.1 · pp. 11–12

4.3.2 Immutability analysis.

  • An output pointer is immutable when it and its aliases are never written in the method or its transitive callees and it is not returned.The analysis uses this condition to prove that no input can flow to that output.Source: §4.3.2 · p. 12

4.3.3 Read analysis.

  • The read analysis proves no flow from an input access path when it and all its aliases are never read in the method or its transitive callees.It checks memory loads and is described as the inverse of the immutability analysis.Source: §4.3.3 · p. 12

4.4 Deducing Callee Summaries

For must-not-flows that lightweight checks cannot prove, the algorithm builds an inter-procedural graph from intra-procedural analysis and deduces callee summaries with Max-SAT. It recursively checks those summaries; if all deduced callee summaries are sound, the enclosing model is sound.

4.4 Deducing Callee Summaries

  • The algorithm avoids full inter-procedural taint analysis by combining intra-procedural flows with deduced callee edges to complete a graph that represents possible flows.It uses a sound field-sensitive intra-procedural analysis and assumes the most-general callee summary when computing flows across calls.Source: §4.4 · pp. 12–13
  • The graph distinguishes known intra-procedural and call-site edges from unknown callee input-to-output edges, which are the summaries to deduce.Vertices represent access paths in calling contexts; repeated calls to a callee have distinct call-site contexts, while the deduced summary is shared across call sites.Source: §4.4 · p. 13
  • The graph computation terminates for recursive methods because access paths are bounded and vertices use only the immediate call site as context.An unsatisfiable Max-SAT model means no valid callee summaries satisfy the requirements; co-optimal solutions may exist, and the algorithm recursively checks a selected solution’s summaries.Source: §4.4 · pp. 13–14
  • Max-SAT enforces known edges and forbids paths violating must-not-flows, while maximizing unknown callee edges to obtain least-precise summaries.Maximizing these edges reduces restrictions and therefore the static-analysis burden for proving must-not-flows in callees.Source: §4.4 · p. 14
  • If all deduced callee summaries are sound, the enclosing method model is sound.The soundness argument uses the graph’s paths and the Max-SAT constraints that block paths for must-not-flows.Source: §4.4 · p. 15

4.5 Efficiency

The efficiency analysis separates lightweight checks, intra-procedural analysis, graph construction, and Max-SAT costs. The best-case advantage is that the algorithm need not analyze every transitive callee.

4.5 Efficiency

  • The lightweight checks and graph construction scale with method and callee statements or graph vertices and edges, while Max-SAT clause count is dominated by reachability constraints.Reachability contributes O(|I_m| · |E_m|) clauses; known-edge and soft constraints contribute O(|E_m|).Source: §4.5 · pp. 15–16
  • The worst-case recursive algorithm runs at most 1 + |C*| times, where C* is the set of transitive callees reachable from the call graph.The constructive approach is classical inter-procedural taint analysis.Source: §4.5 · pp. 15–16
  • In the best case, the algorithm recurses only into callees whose deduced summaries still have unproven must-not-flows, rather than analyzing every transitive callee.The authors argue this comparison is more useful for efficiency because their approach adds Max-SAT cost only for callees reaching summary deduction.Source: §4.5 · p. 16

5 INSTANTIATION FOR GO

The Go instantiation adapts the model format and soundness checks to Go features, using type and pointer analyses to prove must-not-flows and a taint analysis when needed. Its guarantees are bounded by model restrictions and assumptions about the program and Go semantics.

5 INSTANTIATION FOR GO

  • Go’s instantiation uses Argot and extends method inputs to include package globals and closure free variables, with outputs also including those inputs and return values.The checkable model format supports function, method, and interface model types, but interface models are field-insensitive and checked against concrete implementations in the application.Source: §5 · p. 16, §5.1 · pp. 16–17

5.1 Taint Flow Model

  • The checkable model format excludes higher-order functions and flows to or from global or bound/free variables, so some methods cannot be proven sound even though Argot can analyze those features.For closures, callee summaries are checkable when their inputs and outputs are fully resolved; reads or writes to globals are conservatively treated as unsound.Source: §5.1 · pp. 16–17

5.2 Most-General Summary

  • The most-general summary is sound under data-race-free execution and no unsafe memory manipulation; unsafe pointer arithmetic can expose access paths outside the summary’s inputs.The authors identify reflection and concurrency operations as further considerations in their proof sketch.Source: §5.2 · pp. 17–18

5.3.1 Types analysis.

  • The types analysis proves that a non-pointer-like output cannot be tainted by any input, assuming data-race-free execution and no unsafe memory manipulation.The proof relies on Go’s type system to show that the output is not heap-allocated.Source: §5.3.1 · p. 18

5.3.2 Immutability and read analyses.

  • The immutability and read analyses use Go’s pointer analysis to prove must-not-flows, but their soundness depends on excluding reflection and unsafe memory manipulation.The analyses use constant return values as immutable; flow-insensitive pointer analysis remains sound with concurrency, whereas a flow-sensitive version would not.Source: §5.3.2 · pp. 18–19

5.4.1 Taint analysis.

  • Argot’s flow-, context-, and field-sensitive taint analysis does not yet soundly handle some panic/recover and unbounded defer flows, and inherits pointer-analysis limitations.The approach could use a flow-insensitive analysis for those control-flow cases at a cost in precision.Source: §5.4.1 · p. 19

5.4.2 Callee models.

  • When checking methods that call closures, the approach can derive callee summaries with free variables bound to values in enclosing scopes.For nestedClosures, the deduced outer and inner summaries connect their free variables to the corresponding enclosing values.Source: §5.4.2 · p. 19

5.5 Limitations

  • Soundness proofs are application-relative under dynamic dispatch and depend on the authors’ interpretation of Go semantics, data-race-free execution, a sound call graph, and no free variables in modeled methods.Proving implicit taint-flow properties is outside the approach’s scope.Source: §5.5 · pp. 19–20

6 EVALUATION

The evaluation tests soundness, precision, and efficiency on Go programs, comparing the LLM-based approach with a baseline taint analysis and constructive model generation. The checked models avoid additional false positives and make several otherwise intractable analyses feasible, while recursive checking and Max-SAT deduction contribute to model verification.

Experimental Setup

  • The evaluation covered Go repositories and taint-flow properties, manually checking scenarios to distinguish false positives from real flows and selecting cases with deep call-graph exploration.The study collected 97 interesting methods; interface-method checks could cover implementations, yielding 2,535 total methods checked.Source: §6 · pp. 20–21
  • The agent generated models for interesting methods, then the evaluation separately ran soundness checking, constructive generation, and taint analyses with and without generated models.The checker and baseline used the same pointer and taint analyses, instantiated with Argot; standard-library models were assumed sound despite incomplete coverage.Source: §6 · pp. 21–22

Soundness of Generated Models

  • 118 methods (5%) had unsound generated models, while 2% of outcomes were soundy; two repositories’ soundy models were manually checked as sound.A soundy result means the checker proved the must-not-flows but encountered a feature threatening the soundness result.Source: Table 2 · p. 22, §6 · p. 22

Usefulness of Soundness-Checking Sub-Analyses

  • Recursive deduction and checking of callee summaries was crucial for checking models in amazon-ssm-agent, where the agent generated most-general summaries for over 2,000 methods across the applications.This does not mean most-general summaries can replace the approach: using them too often was expected to cause additional false positives, which were not observed in the RQ4 evaluation.Source: §6 · pp. 22–23

Efficiency

  • With LLM-generated sound models, the slowest taint-analysis run plus soundness checking took less than 3 minutes, while the baseline timed out on 3 of 6 applications.The combined approach was slower only on the sample repository, where both runs took less than 1 minute; soundness checking alone took slightly over 2.5 minutes at most.Source: Table 4 · p. 23, §6 · pp. 23–24

Precision of Model Generation

  • Across all benchmarks, LLM-generated models yielded no additional false positives compared with taint analysis without generated models.For examples where the baseline timed out, hand-written models supplied a false-positive baseline.Source: §6 · p. 23

Efficiency

  • Constructive model generation timed out on sample and amazon-ssm-agent, and produced sound summaries for fewer than 10% of methods in the remaining programs.The timeouts arose from complex intra-procedural taint flows causing state-space explosion; the other programs’ modeled methods had simpler flows.Source: §6 · p. 24
  • The checker solved 956 Max-SAT constraints in 165 microseconds for amazon-ssm-agent’s client.NewRequest, deducing a callee model with 297 field-sensitive flows.Although worst-case complexity is NP-complete, the evaluation observed no checker scalability issues; methods with hundreds of inputs and outputs may pose a concern.Source: §6 · p. 24

7 RELATED WORK

Prior work provides compositional taint analysis, user-defined or synthesized models, and methods for inferring data flows. This work combines LLM-based model synthesis with soundness checking, while differing in its use of source code and its restriction to explicit flows.

Compositional Analysis

  • Compositional analyses summarize method effects to support context-sensitive inter-procedural dataflow analysis, including IFDS, IDE, and WPDS.The foundational functional approach is attributed to Sharir and Pnueli.Source: §7 · p. 24

User-Defined Taint Flow Models

  • Tools including TAJ, Andromeda, FlowDroid, CompTaint, and Argot accept user-defined models but do not verify their soundness.This work addresses that limitation by checking soundness of provided models.Source: §7 · p. 24

Synthesizing Taint Flow Models

  • Taser, Zhai et al., and STaint synthesize models without soundness guarantees; this work equips an LLM agent with tools and checks its synthesized models.Their approaches use dynamic tainting, documentation-based syntax-guided synthesis, and LLM inference for PHP database operations, respectively.Source: §7 · p. 24
  • StubDroid and ModAlyzer compute complete reusable models through inter-procedural taint analysis but inherit its scalability limitations.Source: §7 · p. 24
  • Abduction and context-free-language reachability synthesize sound summaries from known flows but assume implementations are unavailable and rely on a human soundness oracle.Unlike those approaches, this work checks the soundness of deduced callee summaries; unlike Flowistry, it supports arbitrary models using type and may-alias information but only explicit flows.Source: §7 · pp. 24–25

Light-Weight Static Analyses

  • Lightweight-analysis work uses mutability and type information to improve data-flow precision, while this work’s immutability analysis resembles Milanova et al.’s side-effect analysis.FlowDroid handles immutable Java parameter types; Flowistry uses Rust’s ownership and mutability types, and FlowCFL combines CFL reachability with reference immutability.Source: §7 · p. 25

8 CONCLUSION

The paper presents an LLM-assisted approach to taint analysis and identifies extensions to other techniques and languages as future work. Its implementation is limited to Go, and the authors hope to encourage further research on specification synthesis for scalable static analysis.

Conclusion

  • The approach aims to improve taint-analysis efficiency with LLM-synthesized precise models without compromising soundness or precision.Source: §8 · p. 25
  • Future work could investigate more efficient symbolic or machine-learning synthesis and apply the checker to existing approaches.Source: §8 · p. 25
  • The approach is instantiated only for Go; applying it to languages such as Java is future work.Source: §8 · p. 25

A.1 Prompt

The appendix prompt instructs an LLM to generate Go dataflow summaries for Argot, covering input-to-output effects, complex data paths, and soundness-oriented analysis guidance. It also supplies request examples and asks for YAML-only output unless complex flows need explanation.

A.1 Prompt

  • The prompt targets Go-function dataflow summaries for Argot, describing which inputs affect which outputs.Source: §A.1 · p. 28

A.1.1 Complex Data Flows

  • Complex flows use suffix notation for struct fields, array, slice, or map elements, and nested field-element paths.For maps, [*] denotes both keys and values because the format cannot distinguish them.Source: §A.1.1 · p. 28

A.1.2 Task Instructions

  • The task instructions ask the agent to understand the function, identify input-output flows, and include flows across all execution paths.Source: §A.1.2 · p. 28

A.1.3 Important Notes

  • The prompt emphasizes conservative summaries, checking with argot_dataflow_check, error returns, mutations, and branches, loops, and error conditions.Source: §A.1.3 · p. 28

A.1.4 Example Request

  • A single-function example request names a function, source-file path, and package.Source: §A.1.4 · p. 28
  • The examples also show requests for summaries of all functions suggested by a taint-tool configuration and for YAML-only output.The YAML-only instruction allows explanations when a flow is complex and needs clarification.Source: §A.1.4 · p. 28
Loading 2609.28750v1…