PaperlayerView exact revision on arXiv

Source-linked AI summary

TyPatch: Transforming Patches into Typestate Rules for Kernel Bug Detection

Ruoyu Wang, Tuo Li, Jia Li

arXiv:2609.13728v1cs.SEcs.AIcs.CRcs.OS

TL;DR

Historical fixes contain defect relationships that can support kernel-wide detection, but complete-checker generation couples recovering those semantics with implementing analysis machinery. TyPatch generates structured typestate rules for a shared backend; on Linux v6.16 it found 559 distinct bugs, 121 confirmed, and used 88.3–90.1% fewer generation tokens than KNighter on matched patches.

  • Problem

    Static analyzers detect bug classes covered by expert-written rules, while many transferable defect relationships in historical fixes have not been converted into persistent detection capability.

    Source: §1 · p. 1

  • Method

    TyPatch has an LLM derive structured typestate rules from patches and executes accepted rules with a shared backend.

    Source: §1 · p. 2

  • Results

    559 distinct bugs were found in Linux v6.16, including 121 confirmed by kernel developers, and TyPatch used 88.3–90.1% fewer generation tokens than KNighter on matched patches.

    Source: §7 · p. 12

  • Takeaways & Limitations

    TyPatch’s rules preserve the seed patches’ core defect relation in 236 of 249 reviewed rules.

    Source: §7 · p. 12

    The rule approach is less suited to patches requiring reasoning beyond sequential object-state relations, such as size or bounds reasoning and non-temporal API changes.

    Source: §4.3 · p. 9

Abstract

from arXiv · show

Historical Linux kernel patches capture defect knowledge that applies beyond their original repair sites. Recent work has shown that large language models (LLMs) can generate static-analysis checkers from historical patches and use them to uncover new kernel bugs. However, complete-checker generation requires the model both to recover the defect semantics expressed by a patch and to implement sophisticated program-analysis machinery, including object tracking, alias analysis, path-state maintenance, and interprocedural propagation. Coupling these responsibilities in a single end-to-end code-generation task can turn a simple defect rule into an unstable and expensive analyzer-implementation problem. To address this problem, we present TyPatch, which decouples patch-specific defect semantics from analyzer implementation. An LLM translates each patch into a typestate rule specifying its tracked object, actions, guards, transitions, and violations. A shared backend then executes these rules, binding their actions to program events, tracking object identity across aliases, propagating typestate along program paths, and producing reports for all rules. On Linux v6.16, TyPatch finds 559 distinct bugs, 121 of which have been confirmed by kernel developers. In a matched 38-patch comparison with the state-of-the-art complete-checker construction workflow, TyPatch uses 88.3-90.1% fewer generation tokens, while its initial report pools achieve 3.42-14.95$\times$ the precision of those produced by that workflow.

1 Introduction

Historical kernel fixes encode defect relationships that can guide detection beyond the repaired lines, but turning them into checkers requires both semantic recovery and analyzer implementation. TyPatch separates those tasks by generating structured typestate rules for a shared backend.

Motivation

  • Static analyzers’ detectable bug classes depend on rules experts have implemented, leaving many patterns in historical fixes unconverted into persistent detection capability.New long-tail patterns require both kernel-semantic understanding and executable analysis rules.Source: §1 · p. 1
  • Historical fixes capture transferable relationships among objects, operations, and valid conditions, extending defect knowledge beyond the changed lines.Such relationships can guide automated detection of similar bugs across the kernel.Source: §1 · p. 1
  • Complete-checker generation couples patch understanding with implementation of framework-specific callbacks, alias-aware tracking, path-state updates, and reporting.The analysis mechanisms are largely common across patches, but generated checker implementations must reproduce them for each patch.Source: §1 · pp. 1–2

System

  • TyPatch has an LLM generate patch-specific typestate semantics while a shared backend supplies analysis mechanisms and executes accepted rules.The rule specifies tracked objects, actions, guards, transitions, violation state, and report evidence; deterministic validation and repair produce a valid rule or NoRule.Source: §1 · p. 2

Evaluation and impact

  • With GPT-5.5 and DeepSeek-v4-pro, TyPatch’s initial report precision was 4.67% and 9.11%, versus KNighter’s 0.31% and 2.66%, respectively.The matched comparison used KNighter’s 38-patch dataset and Linux v6.16.Source: §1 · p. 2
  • Across an evaluation of three LLMs on 100 Linux fixes, TyPatch-derived rules found 559 distinct bugs in Linux v6.16, including 121 confirmed by kernel developers.Source: §1 · p. 2

2 Motivation

Patch-to-checker generation requires recovering a defect relation and implementing it as an analyzer. A cgbc example shows that a correct plan can fail during checker implementation, motivating TyPatch’s division between patch-specific rules and shared analysis machinery.

2 Motivation

  • Patch-to-checker generation combines recovering a patch’s defect relation with implementing that relation through framework-specific analyzer machinery.Implementation requires callbacks, object identity, alias handling, and path-state updates.Source: §2 · pp. 2–3

2.1 Correct Plan, Incorrect Checker

  • For the cgbc patch, all 20 generated plans identified the missing null check, and all 20 checkers compiled, but only 2 of 10 GPT-5.5 checkers and none of 10 Opus 4.8 checkers distinguished the buggy seed from its fix.Thus, 18 of 20 candidates failed after recovering the missing-check relationship.Source: §2.1 · p. 3
  • The plan traces the allocator return through a structure field and local alias to an unsafe use, but the checker’s Loc-derived store key and Val-derived lookup key differ, skipping the alias update.The failure arises in checker implementation rather than recovery of the patch semantics.Source: §2.1 · p. 3, Figure 2 · p. 3

2.2 Generate the Rule, Reuse the Analyzer

  • TyPatch asks the model to emit a structured typestate rule and implements common object propagation, alias handling, and path-state maintenance once in a shared backend.The tracked object, actions, guards, and transitions vary across patches, while these analysis mechanisms are common.Source: §2.2 · p. 3
  • For the same cgbc patch, the rule binds devm_kzalloc() as the source, its non-null successor as the guard, and the later dereference as the violation.The backend carries the object through the structure field and local alias, applying the non-null transition only on the continuing branch; GPT-5.5 and Opus 4.8 each generated the rule in one attempt.Source: §2.2 · p. 4, Figure 3 · p. 4

3 Method

TyPatch separates patch-specific defect semantics from analyzer implementation: an LLM creates validated typestate rules, and a shared backend executes them over kernel code. The method defines the rule representation, its construction and validation, and the backend’s shared analysis mechanisms.

3.1 Typestate Rule Representation

  • Each typestate rule specifies a tracked object, actions and guards, transitions, a violation state, and the evidence required for a report.Object and action bindings connect the machine to program values and events; the shared analyzer handles unbound operations that transport objects between state-changing actions.Source: §3 · p. 4, §3.1 · p. 5

3 Method

  • TyPatch connects patch-derived defect knowledge to a shared backend by expressing it as a rule representation the backend can execute.For each patch, the system returns a validated rule or NoRule; the backend loads accepted rules to analyze the kernel’s LLVM IR and control-flow graph.Source: §3 · p. 4

3.2 Constructing Rules from Patches

  • For each patch, TyPatch combines commit, diff, and source evidence to generate a structured rule or NoRule, then validates, normalizes, and serializes executable rules.Validation checks grounding and internal consistency, can request up to two revisions, and returns NoRule if construction does not succeed.Source: §3.2 · pp. 5–6

3.3 Shared Typestate Analysis

  • TyPatch executes accepted rules over LLVM IR and the control-flow graph using shared action matching, alias-aware tracking, path-sensitive propagation, evidence screening, and grouped execution.The backend binds rule actions to events, keeps independent rule states, and rejects a candidate only when it proves the required evidence constraints impossible.Source: §3.3 · pp. 6–7

4 Evaluation

The evaluation tests whether TyPatch finds Linux kernel bugs, how rule construction compares with complete-checker construction, and whether generated rules preserve seed semantics. Across Linux v6.16 scans and a matched 38-patch comparison, it reports bug findings, construction and report-quality results, and rule-fidelity analyses.

4.1 Experimental Setup

  • The evaluation scans Linux v6.16 using rules from 100 historical fixes across eight bug families, and compares both systems on 38 shared-benchmark commits.The three research questions cover bug finding, construction and initial report quality, and rule fidelity.Source: §4.1 · p. 7, §4 · p. 7

4.2 RQ1: Linux Bug Finding

  • GPT-5.5, DeepSeek-v4-pro, and Opus 4.8 generate rules for 91, 74, and 84 of the 100 seeds, with coverage differences largest for three bug families.Table 1 breaks rule coverage down by family; refcount imbalances are the largest TP group for GPT and DeepSeek, while Opus contributes substantially more missing-release findings.Source: §4.2 · pp. 7–8, Table 1 · p. 8
  • TyPatch finds 559 distinct bugs in Linux v6.16, including 121 confirmed by kernel developers; 377 (67.4%) are surfaced by rules from at least two models.The findings span all eight evaluated typestate families and multiple kernel subsystems.Source: §4.2 · p. 8

4.3 RQ2: Rule vs. Checker Construction

  • Across both models, TyPatch completes construction for more patches with fewer model calls; one reported comparison shows 25 patches with 90 calls versus KNighter’s 23 valid checkers from 198 candidates with 826 calls.Source: §4.3 · pp. 8–9

4.2 RQ1: Linux Bug Finding

  • Two developer-confirmed transfers carry nullable-object and all-path initialization rules across subsystems to expose unchecked allocation and short-transfer bugs.The examples transfer from RDMA receive to WWAN transmit, and from ALSA control logic to a media-driver I2C helper.Source: §4.2 · p. 8, Figure 7 · p. 9

4.3 RQ2: Rule vs. Checker Construction

  • 88.3–90.1% fewer generation tokens and 3.42–14.95× the precision of KNighter are reported for TyPatch in the matched comparison, before report-level post-processing.The comparison also reports 2.72–14.27× as many true-positive report instances.Source: Table 3 · p. 9, §4.3 · p. 10
  • Under GPT-5.5, initial precision is 4.67% versus 0.31%; under DeepSeek-v4-pro, it is 9.11% versus 2.66%, for TyPatch and KNighter, respectively.Under GPT-5.5, three broad rules account for 2,729 of the 2,849 additional reports relative to DeepSeek-v4-pro.Source: Table 3 · p. 9, §4.3 · p. 9

4.4 RQ3: Rule Fidelity and Misalignment

  • 236 of 249 generated rules (94.8%) preserve seed relations, and aligned rules account for 1,131 of 1,132 model-specific true positives.Of the aligned rules, 159 reproduce audited fields exactly and 77 broaden a predicate or API binding without changing the core relation; 10 of 13 mismatches concern object or action selection.Source: Table 4 · p. 10, §4.4 · p. 10

5 Discussion

TyPatch presents its rules as a growing ecosystem of executable defect knowledge that can evolve with the kernel. The discussion also describes downstream report verification and provides artifacts for reproducibility.

A growing rule ecosystem

  • Rules from different patches or models share an interface and backend, so improvements to wrappers, alias transfer, or path predicates can benefit the rule pool.Developer-confirmed findings and fixes can become new seeds; future work could extend rules to cross-interface protocols, numerical constraints, and concurrent histories.Source: §5 · p. 10

Orthogonal report verification

  • A downstream agent could inspect each report’s seed, bound actions, object history, and source context to reject infeasible or unrelated candidates.The RQ2 comparison evaluates initial report pools before report-level post-processing.Source: §5 · p. 10

Artifact Availability

  • The artifact provides the synthesizer, backend, repair commits, frozen rule pools, deduplication code, and a Docker image for reproducing Linux v6.16 scans.The image includes the source tree, LLVM IR, and compilation database.Source: §5 · p. 10

6 Related Work

Prior work provides scalable analysis infrastructure and methods for recovering rules, but often depends on expert-authored rules, many examples, predefined patterns, or candidate-level LLM review. TyPatch instead generates explicit typestate rules from patch evidence and executes them with a shared backend, avoiding repeated complete-checker implementation.

6.1 Traditional Static Analysis

  • Existing static-analysis tools apply rules at scale, but new defect knowledge still must be encoded as corresponding rules.The tools include Coccinelle, Smatch, and the Clang Static Analyzer.Source: §6.1 · p. 11
  • Typestate analysis tracks object states across actions, while PATA and SPATA address alias, path, and interprocedural propagation.These systems illustrate the specialized analysis needed to execute state rules accurately.Source: §6.1 · p. 11
  • Automated rule-recovery approaches draw on behaviors, traces, revisions, and API usage, but often need many examples or restrict rules to predefined patterns.Spinfer infers semantic patches from multiple code-change examples.Source: §6.1 · p. 11
  • APHP extracts post-handling specifications from patch code and commit descriptions, while SEAL derives interface specifications from program-dependence changes.TyPatch uses commit messages, diffs, and source context to represent tracked objects, actions, guards, states, and transitions, including constraints not visible in changed value-flow paths.Source: §6.1 · p. 11

6.2 LLM-Assisted Static Analysis

  • LLM-assisted systems either supply semantic information to existing analyzers or use patch-derived rules to select candidates for LLM review [26] [37] [41].In the latter approach, an LLM still reasons over individual candidates.Source: §6.2 · p. 11
  • KNighter generates complete checkers from patch-derived plans, combining patch-specific semantics with checker implementation.TyPatch instead has the model describe object-state rules and relies on a shared backend to bind and propagate them through aliases and control flow.Source: §6.2 · pp. 11–12

7 Conclusion

TyPatch generates structured typestate rules from Linux kernel patches and executes them with a shared alias-aware, path-sensitive backend. Across its evaluation, it finds bugs in Linux v6.16 and uses fewer generation tokens than KNighter on matched patches.

7 Conclusion

  • TyPatch uses structured typestate rules and a shared alias-aware, path-sensitive backend to analyze Linux kernel patches.The rule pool found 559 distinct bugs in Linux v6.16, including 121 confirmed by kernel developers; 236 of 249 rules preserved their seed’s core defect relation.Source: §7 · p. 12
  • 88.3–90.1% fewer generation tokens than KNighter, with more artifacts and more precise initial reports under both models, on 38 matched patches.The conclusion describes structured rule generation as stable, low-cost, scalable analysis that grows with repair history.Source: §7 · p. 12

A.1 Patch-to-Rule Algorithm

The algorithm constructs evidence, generates a structured rule, and applies staged validation and repair. It returns NoRule when indicated or when the candidate does not pass validation.

A.1 Patch-to-Rule Algorithm

  • Construction builds context from the patch message, diff, and kernel source, then generates a structured rule candidate.The algorithm may return NoRule instead of proceeding with a candidate.Source: §A.1 · p. 14
  • Schema validation and binding grounding precede normalization and state-machine validation.The algorithm records schema, grounding, and state-machine failures before proceeding to backend validation.Source: §A.1 · p. 14
  • A candidate that passes backend validation is serialized and returned as a rule.The algorithm checks for accumulated failures before serialization.Source: §A.1 · p. 14

A.2 Implementation Details

TyPatch implements patch-to-rule construction in Python and its shared backend in C++ over LLVM IR. Context expansion, rule serialization, and scan settings constrain how evidence and executable bindings reach the backend.

A.2 Implementation Details

  • Patch-to-rule construction is implemented in Python, while the shared backend is implemented in C++ over LLVM IR.Source: §A.2 · p. 14
  • Construction context is limited to three changed function bodies, 200 lines each, and 500 lines total, with specified source expansion and at most two selected few-shot examples.Source expansion includes ordinary functions, multiline macros, one-level wrappers, cleanup declarations, and one level of callees; excerpts retain file:line provenance.Source: §A.2 · p. 14
  • The serializer completes rule components, maps report constraints to fail-open path screening, emits the .ts format, and attaches scan settings.The model-facing schema contains R; normalized rules record executable bindings selected by the model.Source: §A.2 · p. 14

A.3 Evaluation Protocol

The evaluation assigns each rule a scan scope, configures report collection and review, and applies distinct reporting procedures across RQ1 and RQ2. The protocol also specifies the matched comparison set, true-positive criterion, and model-usage accounting.

A.3 Evaluation Protocol

  • Rules receive kernel or module scope; generic or unresolved bindings default to kernel scope, and the LLM may retain or widen—but not narrow—local scope.Rules with identical target sets are grouped to reduce rule–target combinations; both RQ1 and RQ2 enable this step for TyPatch.Source: §A.3 · p. 14
  • RQ1 excludes reports from rules producing more than 2,000 raw whole-kernel reports, while RQ2 applies no report-count gate.The gate removes 2 of 91 GPT rules, 1 of 74 DeepSeek rules, and 3 of 84 Opus rules.Source: §A.3 · p. 14
  • Reports are merged by source site and connected downstream sinks, while seed-site and kernel-test reports are excluded from production-bug totals.The protocol uses a two-hour limit per translation unit; reports from different rules or object keys are joined transitively when they share a sink.Source: §A.3 · p. 14
  • The matched set contains 38 commits from six sequential object-state families, and reports from different generated artifacts remain distinct after deduplication.Each rule or checker is deduplicated by sink file, function, and line; report refinement and triage are outside both artifact-generation arms.Source: §A.3 · pp. 14–15
  • A report counts as a true positive only when its ordered actions concern the same abstract object along a feasible path.All reported populations were manually reviewed against the same Linux v6.16 source.Source: §A.3 · p. 15
  • TyPatch’s generation-token totals include initial rule generation, repairs, and LLM-based scope planning, but exclude backend execution and manual review.Token totals use provider-reported input, cached-input, and output counts; model-call counts include scope-planning calls.Source: §A.3 · p. 15

A.4 Additional Results

Within TyPatch, DeepSeek-v4-pro has higher precision than GPT-5.5, with the difference concentrated in three broad GPT-5.5 rules. The accompanying tables describe rule-construction costs and the family-level composition of RQ2 report instances.

A.4 Additional Results

  • Table 5 reports RQ1 rule-construction cost in thousands of model tokens, including initial generation, repair attempts, and scope planning.Source: Table 5 · p. 15
  • Table 6 presents RQ2 true-positive report instances by family, not distinct bugs.Reports from different artifacts remain distinct.Source: Table 6 · p. 15, §A.4 · p. 15
  • 9.11% vs. 4.67%: DeepSeek-v4-pro achieves higher precision than GPT-5.5 within TyPatch.Three overly broad GPT-5.5 rules produce 2,729 of the 2,849 additional reports relative to DeepSeek-v4-pro; false positives primarily involve different-object propagation, infeasible paths, or guards or initialization preceding the reported use.Source: §A.4 · p. 15
Loading 2609.13728v1…