TYPEPULSE: Detecting Type Confusion Bugs in Rust Programs

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

scope and bug model

TYPEPULSE is a static analyzer for unsafe Rust pointer conversions. The authors inspect 32 RUSTSEC reports from five years, retain 26 type-confusion bugs, and classify them as misalignment, inconsistent layout, or mismatched scope (Section 3.1, p.4; page numbers here are PDF pages of the arXiv version, which prints none). “All 26 bugs are related to pointer type conversion (i.e., references and raw pointers) in Unsafe blocks.” (Section 3.1, p.4) The tool targets conversions represented by as and transmute; non-pointer conversions (for example integer-overflow bugs from downcasts) and foreign-function-interface errors are outside scope (Section 3.3, p.6). The six reports excluded from the 26 concern other memory-safety problems such as use-after-free (Section 3.1, p.4).

Type I, misalignment, occurs when the destination type requires an alignment that the source address does not satisfy. Type II, inconsistent layout, occurs when Rust may reorder fields or insert padding and the destination interprets a different layout. Type III, mismatched scope, creates invalid bit patterns or breaks mutability and aliasing expectations. The paper’s u8 to u32 slice example shows why a pointer aligned for u8 is not necessarily aligned for u32; its Table/TableSlice example shows a layout reinterpretation; and its ComponentBytes example turns a mutable byte view into a way to modify data behind an immutable reference (Section 3.1, pp.4–5).

Inference: For Verus, these are unsafe-boundary obligations rather than ordinary safe Rust contracts. Keep conversion wrappers in a small module, expose only functions whose requires clauses state alignment, initialization, layout, and aliasing conditions, and prove ensures clauses about the resulting view. Inference: Verus cannot make arbitrary raw-pointer casts sound automatically; the unsafe operation and its memory model must remain an explicit trusted boundary.

technique 1: property graph construction

TYPEPULSE has a Property Graph Constructor and Bug Detector (Figure 1, p.6). The constructor runs the Rust compiler to translate source into MIR, performs type-conversion analysis and pointer-alias analysis, records conversion pairs and an alias graph, and stores return types and unsafe-function markers. “The property graph includes the type conversion pairs and the pointer alias graph.” (Section 4, p.6)

Apply it as follows.

1. Compile the crate to MIR and mark functions containing unsafe code (Section 4.1, p.6).
2. Record each function’s return type; match a conversion’s source type to return types of other functions to find constructors across call boundaries (Section 4.1, p.6).
3. Build conversion pairs, trait-bound information, and alias edges. Algorithm 2 adds edges for references, raw-pointer casts, transmute, and calls; a move deletes the moved alias, and StorageDead removes dead values (Algorithm 2, p.8; Section 4.1.2, p.7).
4. During detection, use common descendants and breadth-first traversal of the alias graph to decide whether the invalid destination pointer remains reachable (Section 4.1.2, p.8).

Inference: A Verus-oriented implementation can use compiler MIR or VIR facts as a pre-check, then require proof lemmas for each wrapper’s ownership and memory relation. The paper’s MIR graph is an analysis artifact, not a Verus proof, so graph reachability must not be presented as a verified contract.

technique 2: generic type and trait-bound resolution

Generic conversions cannot be checked by looking only at concrete types. TYPEPULSE recursively parses trait dependencies, gathers standard-library traits and primitive types, constructs composite types from primitive fields, and produces a type set of possible instantiations (Section 3.2, pp.5–6; Algorithm 1, p.7; Section 4.1.1, pp.6–7). Public generic functions include externally supplied types, not merely types found in the crate. The tool then substitutes each candidate in the detector’s conversion patterns.

Inference: In Verus, generic safety should be expressed with explicit trait bounds and spec predicates describing the allowed representation. A finite type set is an analysis approximation; it is not a substitute for a universally quantified Verus invariant. If a public API admits arbitrary types, the verifier must reject or abstract the unsafe conversion unless the contract restricts the representation.

technique 3: three conversion detectors

The detector first classifies a conversion as concrete-to-concrete, concrete-to-generic, or generic-to-concrete; generic-to-generic is excluded because the observed TypeId check requires matching layouts (Section 4.2.1, p.8). It then applies three checks.

• Misalignment: mark a destination invalid when src_ty.align % dst_ty.align != 0; for a generic side, substitute every candidate type and use platform-specific alignments for types such as usize (Section 4.2.1, p.8; Table 2, p.9).
• Inconsistent layout: maintain unstable_ty (structs, unions, trait objects) and stable_ty (scalar types), inspect repr and ABI names, and mark conversions from unstable to stable or unstable types whose ABI symbol names differ (Section 4.2.1, p.8).
• Mismatched scope: maintain weak_ty and strict_ty according to permitted bit patterns; mark weak-to-strict conversions or strict-to-weak conversions when the destination is mutable, recursively inspecting composite fields (Section 4.2.1, p.9; Table 2, p.9).

The paper states: “When src_ty’s alignment is not a multiple of dst_ty’s alignment, it will create a misaligned pointer.” (Section 4.2.1, p.8) It separately checks whether developer-enforced checks suppress an alarm: before a conversion, align_of/alloc for alignment and size_of size checks for layout; after it, read_unaligned and writes such as ptr::write. Checks based on runtime value comparisons are hard to detect (Section 4.2.3, p.10).

Inference: Verus can encode alignment and representation assumptions as predicates and prove a conversion wrapper preserves them. repr(C) and repr(transparent) remain Rust attributes; a Verus proof may rely on the concrete struct layout only where the verifier’s model supports it. Inference: strict/weak bit-pattern categories need a domain-specific predicate, not an invented Verus keyword.

technique 4: access, developer-check, and interprocedural analysis

After marking an invalid pointer, TYPEPULSE checks whether it is dereferenced or passed to unsafe APIs such as ptr::read, ptr::copy, ptr::as_ref, slice::from_raw_parts, str::from_utf8_unchecked, and CStr::from_ptr (Section 4.2.2, p.10). It then checks whether the pointer is aliased with the return value, only when the return type is a reference; a raw-pointer return is not counted, because using it needs an unsafe block and the paper blames the function that performs the conversion (Section 4.2.2, p.10). Developer-enforced checks reduce false positives; the tool recognizes standard patterns and some unsafe APIs with clear safety documentation but cannot interpret complex checks such as an encode_utf8 encoding restriction (Section 4.2.3, p.10; Section 5.2, p.12).

Interprocedural analysis uses the property graph to follow conversions and constructors across functions. The paper limits path length to one immediate caller or callee to avoid path explosion, aligning with Rupta (Section 4.3, p.11). With this analysis enabled, detection on 3,000 packages finds 71 true positives and 23 false positives, precision 75.5%; disabling it yields 69 true positives, 30 false positives, precision 69.7% (Table 4, p.12; Section 5.3, p.12). The paper’s text says interprocedural analysis removed “6 more false positives” in one place and “7 more False Positives” in another; Table 4 (30 to 23) gives 7. The denominator for precision is all 94 manually classified reports (71+23 or 69+30).

Inference: In Verus, callers should inherit the callee’s memory preconditions through contracts; a proof function can establish that a returned reference remains valid, but arbitrary alias escape still needs a supported ownership model. Inference: bounded caller/callee analysis is useful triage, while Verus verification should reject an unresolved obligation rather than treat a one-hop result as proof.

evidence, limitations, and mitigations

On 3,000 high-star crates, 282 lacked /bin or /lib targets and were skipped; 1,754 ran detection, averaging 1.71 seconds, with 5 timing out after two minutes (Section 5.1, p.11). The 71 true positives include 32 Type I, 24 Type II, and 15 Type III, against 23 false positives (Table 4, p.12). Clippy finds 10 relevant bugs and Rudra finds none of these type-conversion bugs in the comparison, run on the packages listed in Table 3 (Table 5, p.13; Section 5.4, p.13). The paper reports 28 panics, 24 uninitialized-memory accesses, 8 out-of-bounds accesses, 7 illegal types, and 4 data races among discovered impacts (Section 5.5, p.14); categories can overlap because they count consequences, not a partition.

Recommended mitigations are read_unaligned/write_unaligned or construction of a new aligned pointer for Type I; stable layout, repr(C)/repr(transparent), and restrictive traits such as bytemuck::Pod for Type II; and bounded types, validated values, and safe checked APIs instead of from_utf8_unchecked for Type III (Section 6, p.15). Limitations are implicit or complex developer checks, lack of dynamic analysis, and one-hop interprocedural context (Section 7, p.15).

Inference: Threat to agent-written verified Rust is substantial at unsafe FFI and raw-pointer edges, even though safe Rust prevents many cases. TYPEPULSE supplies a useful bug taxonomy and triage pass, but its 75.5% precision and recognized false positives show that static alarms cannot replace Verus proofs. VL should reuse the three-category checklist and require proof obligations or explicit review for every unsafe conversion; it should not redo TYPEPULSE’s MIR analysis as if it were a sound verifier.

techniques for the catalog

• property-graph pointer analysis: combine MIR conversion pairs, constructor return types, and alias reachability across functions
• generic-bound expansion: recursively resolve trait bounds and substitute candidate concrete types
• three type-confusion detectors: check alignment, layout/ABI stability, and bit-pattern/mutability scope
• access and interprocedural checks: confirm invalid pointers are dereferenced or escape and account for developer checks Checked 2026-10-17 against the full paper by a Claude agent (mid-paper quote: “Access check is performed to analyze how the invalid type pointer captured by Type conversion check can be accessed.”): read the whole arXiv text (Sections 1-9, Appendices A-B) and checked every quotation, number, section and page reference, and the described steps of the three techniques against it; changed all page references (they were one to four pages off; now PDF pages of arXiv 2502.03271v1, since the text prints no page numbers), the path-limit citation (Section 4.3, not 4.1.2), the claim that raw-pointer returns also count as escapes (the paper counts only reference returns), the unsupported wording about documented encoding checks, and added the paper’s 6-versus-7 false-positive inconsistency and the Table 3 scope of the Clippy/Rudra comparison; tag and link (arXiv, matches the paper) kept; did not check the references list, the appendix listings or the root-cause counts in detail, the PDF figures, or any claim about Verus (marked Inference).

Last edited: 2026-10-17